out.lean

/home/rwbarton/.elan/toolchains/3.4.1/lib/lean/library/init/algebra/classes.lean:⟨124, 17⟩:
  structure/class is_strict_total_order has only Prop fields, but non-Prop type:
    Π (α : Type u), (α → α → Prop) → Type

/home/rwbarton/.elan/toolchains/3.4.1/lib/lean/library/init/classical.lean:⟨15, 22⟩:
  lemma classical.indefinite_description has non-Prop type:
    Π {α : Sort u} (p : α → Prop), (∃ (x : α), p x) → {x // p x}

/home/rwbarton/.elan/toolchains/3.4.1/lib/lean/library/init/classical.lean:⟨38, 14⟩:
  lemma _private.1877771293.u has non-Prop type:
    Prop → Prop

/home/rwbarton/.elan/toolchains/3.4.1/lib/lean/library/init/classical.lean:⟨39, 14⟩:
  lemma _private.4103271433.v has non-Prop type:
    Prop → Prop

/home/rwbarton/.elan/toolchains/3.4.1/lib/lean/library/init/classical.lean:⟨105, 22⟩:
  lemma classical.strong_indefinite_description has non-Prop type:
    Π {α : Sort u} (p : α → Prop), nonempty α → {x // (∃ (y : α), p y) → p x}

/home/rwbarton/.elan/toolchains/3.4.1/lib/lean/library/init/core.lean:⟨217, 6⟩:
  lemma prod.mk.inj_arrow has non-Prop type:
    Π {α : Type u} {β : Type v} {x₁ : α} {y₁ : β} {x₂ : α} {y₂ : β},
      (x₁, y₁) = (x₂, y₂) → Π ⦃P : Sort w⦄, (x₁ = x₂ → y₁ = y₂ → P) → P

/home/rwbarton/.elan/toolchains/3.4.1/lib/lean/library/init/core.lean:⟨225, 6⟩:
  lemma pprod.mk.inj_arrow has non-Prop type:
    Π {α : Type u} {β : Type v} {x₁ : α} {y₁ : β} {x₂ : α} {y₂ : β},
      (x₁, y₁) = (x₂, y₂) → Π ⦃P : Sort w⦄, (x₁ = x₂ → y₁ = y₂ → P) → P

/home/rwbarton/.elan/toolchains/3.4.1/lib/lean/library/init/data/nat/lemmas.lean:⟨853, 8⟩:
  lemma nat.discriminate has non-Prop type:
    Π {B : Sort u} {n : ℕ}, (n = 0 → B) → (Π (m : ℕ), n = nat.succ m → B) → B

/home/rwbarton/.elan/toolchains/3.4.1/lib/lean/library/init/data/nat/lemmas.lean:⟨858, 8⟩:
  lemma nat.two_step_induction has non-Prop type:
    Π {P : ℕ → Sort u},
      P 0 → P 1 → (Π (n : ℕ), P n → P (nat.succ n) → P (nat.succ (nat.succ n))) → Π (a : ℕ), P a

/home/rwbarton/.elan/toolchains/3.4.1/lib/lean/library/init/data/nat/lemmas.lean:⟨864, 8⟩:
  lemma nat.sub_induction has non-Prop type:
    Π {P : ℕ → ℕ → Sort u},
      (Π (m : ℕ), P 0 m) →
      (Π (n : ℕ), P (nat.succ n) 0) →
      (Π (n m : ℕ), P n m → P (nat.succ n) (nat.succ m)) → Π (n m : ℕ), P n m

/home/rwbarton/.elan/toolchains/3.4.1/lib/lean/library/init/logic.lean:⟨136, 6⟩:
  lemma heq.elim has non-Prop type:
    Π {α : Sort u} {a : α} {p : α → Sort v} {b : α}, a == b → p a → p b

/home/rwbarton/.elan/toolchains/3.4.1/lib/lean/library/init/wf.lean:⟨38, 6⟩:
  lemma well_founded.recursion has non-Prop type:
    Π {α : Sort u} {r : α → α → Prop},
      well_founded r → Π {C : α → Sort v} (a : α), (Π (x : α), (Π (y : α), r y x → C y) → C x) → C a

/home/rwbarton/math/lean/mathlib/lint/analysis/topology/continuity.lean:⟨716, 6⟩:
  structure/class locally_compact_space has only Prop fields, but non-Prop type:
    Π (α : Type u_5) [_inst_1 : topological_space α], Type

/home/rwbarton/math/lean/mathlib/lint/analysis/topology/continuity.lean:⟨719, 6⟩:
  lemma locally_compact_of_compact_nhds has non-Prop type:
    Π {α : Type u_1} [_inst_1 : topological_space α] [_inst_2 : t2_space α],
      (∀ (x : α), ∃ (s : set α), s ∈ (nhds x).sets ∧ compact s) → locally_compact_space α

/home/rwbarton/math/lean/mathlib/lint/analysis/topology/continuity.lean:⟨740, 6⟩:
  lemma locally_compact_of_compact has non-Prop type:
    Π {α : Type u_1} [_inst_1 : topological_space α] [_inst_2 : t2_space α],
      compact set.univ → locally_compact_space α

/home/rwbarton/math/lean/mathlib/lint/analysis/topology/topological_space.lean:⟨637, 6⟩:
  structure/class t1_space has only Prop fields, but non-Prop type:
    Π (α : Type u) [_inst_2 : topological_space α], Type

/home/rwbarton/math/lean/mathlib/lint/analysis/topology/topological_space.lean:⟨653, 6⟩:
  structure/class t2_space has only Prop fields, but non-Prop type:
    Π (α : Type u) [_inst_2 : topological_space α], Type

/home/rwbarton/math/lean/mathlib/lint/analysis/topology/topological_space.lean:⟨962, 6⟩:
  lemma t2_space_top has non-Prop type:
    Π {α : Type u}, t2_space α

/home/rwbarton/math/lean/mathlib/lint/category/traversable/basic.lean:⟨76, 6⟩:
  structure/class is_lawful_traversable has only Prop fields, but non-Prop type:
    Π (t : Type u → Type u) [_inst_1 : traversable t], Type (u+1)

/home/rwbarton/math/lean/mathlib/lint/data/finset.lean:⟨956, 28⟩:
  lemma finset.strong_induction_on has non-Prop type:
    Π {α : Type u_1} {p : finset α → Sort u_2} (s : finset α),
      (Π (s : finset α), (Π (t : finset α), t ⊂ s → p t) → p s) → p s

/home/rwbarton/math/lean/mathlib/lint/logic/basic.lean:⟨84, 8⟩:
  lemma imp_intro has non-Prop type:
    Π {α : Sort u_1} {β : Sort u_2}, α → β → α

/home/rwbarton/math/lean/mathlib/lint/logic/basic.lean:⟨109, 8⟩:
  lemma not.elim has non-Prop type:
    Π {a : Prop} {α : Sort u_1}, ¬a → a → α

/home/rwbarton/math/lean/mathlib/lint/logic/basic.lean:⟨516, 22⟩:
  lemma classical.dec has non-Prop type:
    Π (p : Prop), decidable p

/home/rwbarton/math/lean/mathlib/lint/logic/basic.lean:⟨517, 22⟩:
  lemma classical.dec_pred has non-Prop type:
    Π {α : Sort u_1} (p : α → Prop), decidable_pred p

/home/rwbarton/math/lean/mathlib/lint/logic/basic.lean:⟨518, 22⟩:
  lemma classical.dec_rel has non-Prop type:
    Π {α : Sort u_1} (p : α → α → Prop), decidable_rel p

/home/rwbarton/math/lean/mathlib/lint/logic/basic.lean:⟨519, 22⟩:
  lemma classical.dec_eq has non-Prop type:
    Π (α : Sort u_1), decidable_eq α

/home/rwbarton/math/lean/mathlib/lint/order/order_iso.lean:⟨141, 8⟩:
  lemma order_embedding.nat_lt has non-Prop type:
    Π {α : Type u_1} {r : α → α → Prop} [_inst_1 : is_strict_order α r] (f : ℕ → α),
      (∀ (n : ℕ), r (f n) (f (n + 1))) → has_lt.lt ≼o r

/home/rwbarton/math/lean/mathlib/lint/order/order_iso.lean:⟨150, 8⟩:
  lemma order_embedding.nat_gt has non-Prop type:
    Π {α : Type u_1} {r : α → α → Prop} [_inst_1 : is_strict_order α r] (f : ℕ → α),
      (∀ (n : ℕ), r (f (n + 1)) (f n)) → gt ≼o r

/home/rwbarton/math/lean/mathlib/lint/order/order_iso.lean:⟨243, 8⟩:
  lemma order_iso.sum_lex_congr has non-Prop type:
    Π {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {r₁ : α₁ → α₁ → Prop}
    {r₂ : α₂ → α₂ → Prop} {s₁ : β₁ → β₁ → Prop} {s₂ : β₂ → β₂ → Prop},
      r₁ ≃o r₂ → s₁ ≃o s₂ → sum.lex r₁ s₁ ≃o sum.lex r₂ s₂

/home/rwbarton/math/lean/mathlib/lint/order/order_iso.lean:⟨250, 8⟩:
  lemma order_iso.prod_lex_congr has non-Prop type:
    Π {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {r₁ : α₁ → α₁ → Prop}
    {r₂ : α₂ → α₂ → Prop} {s₁ : β₁ → β₁ → Prop} {s₂ : β₂ → β₂ → Prop},
      r₁ ≃o r₂ → s₁ ≃o s₂ → prod.lex r₁ s₁ ≃o prod.lex r₂ s₂

/home/rwbarton/math/lean/mathlib/lint/tactic/interactive.lean:⟨285, 6⟩:
  lemma tactic.interactive.generalize_a_aux has non-Prop type:
    Π {α : Sort u}, (Π (x : Sort u), (α → x) → x) → α

/home/rwbarton/.elan/toolchains/3.4.1/lib/lean/library/init/algebra/classes.lean:⟨124, 17⟩:
  structure/class is_strict_total_order has only Prop fields, but non-Prop type:
    Π (α : Type u), (α → α → Prop) → Type

/home/rwbarton/.elan/toolchains/3.4.1/lib/lean/library/init/classical.lean:⟨15, 22⟩:
  lemma classical.indefinite_description has non-Prop type:
    Π {α : Sort u} (p : α → Prop), (∃ (x : α), p x) → {x // p x}

/home/rwbarton/.elan/toolchains/3.4.1/lib/lean/library/init/classical.lean:⟨38, 14⟩:
  lemma _private.1877771293.u has non-Prop type:
    Prop → Prop

/home/rwbarton/.elan/toolchains/3.4.1/lib/lean/library/init/classical.lean:⟨39, 14⟩:
  lemma _private.4103271433.v has non-Prop type:
    Prop → Prop

/home/rwbarton/.elan/toolchains/3.4.1/lib/lean/library/init/classical.lean:⟨105, 22⟩:
  lemma classical.strong_indefinite_description has non-Prop type:
    Π {α : Sort u} (p : α → Prop), nonempty α → {x // (∃ (y : α), p y) → p x}

/home/rwbarton/.elan/toolchains/3.4.1/lib/lean/library/init/core.lean:⟨217, 6⟩:
  lemma prod.mk.inj_arrow has non-Prop type:
    Π {α : Type u} {β : Type v} {x₁ : α} {y₁ : β} {x₂ : α} {y₂ : β},
      (x₁, y₁) = (x₂, y₂) → Π ⦃P : Sort w⦄, (x₁ = x₂ → y₁ = y₂ → P) → P

/home/rwbarton/.elan/toolchains/3.4.1/lib/lean/library/init/core.lean:⟨225, 6⟩:
  lemma pprod.mk.inj_arrow has non-Prop type:
    Π {α : Type u} {β : Type v} {x₁ : α} {y₁ : β} {x₂ : α} {y₂ : β},
      (x₁, y₁) = (x₂, y₂) → Π ⦃P : Sort w⦄, (x₁ = x₂ → y₁ = y₂ → P) → P

/home/rwbarton/.elan/toolchains/3.4.1/lib/lean/library/init/data/nat/lemmas.lean:⟨853, 8⟩:
  lemma nat.discriminate has non-Prop type:
    Π {B : Sort u} {n : ℕ}, (n = 0 → B) → (Π (m : ℕ), n = nat.succ m → B) → B

/home/rwbarton/.elan/toolchains/3.4.1/lib/lean/library/init/data/nat/lemmas.lean:⟨858, 8⟩:
  lemma nat.two_step_induction has non-Prop type:
    Π {P : ℕ → Sort u},
      P 0 → P 1 → (Π (n : ℕ), P n → P (nat.succ n) → P (nat.succ (nat.succ n))) → Π (a : ℕ), P a

/home/rwbarton/.elan/toolchains/3.4.1/lib/lean/library/init/data/nat/lemmas.lean:⟨864, 8⟩:
  lemma nat.sub_induction has non-Prop type:
    Π {P : ℕ → ℕ → Sort u},
      (Π (m : ℕ), P 0 m) →
      (Π (n : ℕ), P (nat.succ n) 0) →
      (Π (n m : ℕ), P n m → P (nat.succ n) (nat.succ m)) → Π (n m : ℕ), P n m

/home/rwbarton/.elan/toolchains/3.4.1/lib/lean/library/init/logic.lean:⟨136, 6⟩:
  lemma heq.elim has non-Prop type:
    Π {α : Sort u} {a : α} {p : α → Sort v} {b : α}, a == b → p a → p b

/home/rwbarton/.elan/toolchains/3.4.1/lib/lean/library/init/wf.lean:⟨38, 6⟩:
  lemma well_founded.recursion has non-Prop type:
    Π {α : Sort u} {r : α → α → Prop},
      well_founded r → Π {C : α → Sort v} (a : α), (Π (x : α), (Π (y : α), r y x → C y) → C x) → C a

/home/rwbarton/math/lean/mathlib/lint/analysis/topology/continuity.lean:⟨716, 6⟩:
  structure/class locally_compact_space has only Prop fields, but non-Prop type:
    Π (α : Type u_5) [_inst_1 : topological_space α], Type

/home/rwbarton/math/lean/mathlib/lint/analysis/topology/continuity.lean:⟨719, 6⟩:
  lemma locally_compact_of_compact_nhds has non-Prop type:
    Π {α : Type u_1} [_inst_1 : topological_space α] [_inst_2 : t2_space α],
      (∀ (x : α), ∃ (s : set α), s ∈ (nhds x).sets ∧ compact s) → locally_compact_space α

/home/rwbarton/math/lean/mathlib/lint/analysis/topology/continuity.lean:⟨740, 6⟩:
  lemma locally_compact_of_compact has non-Prop type:
    Π {α : Type u_1} [_inst_1 : topological_space α] [_inst_2 : t2_space α],
      compact set.univ → locally_compact_space α

/home/rwbarton/math/lean/mathlib/lint/analysis/topology/topological_space.lean:⟨637, 6⟩:
  structure/class t1_space has only Prop fields, but non-Prop type:
    Π (α : Type u) [_inst_2 : topological_space α], Type

/home/rwbarton/math/lean/mathlib/lint/analysis/topology/topological_space.lean:⟨653, 6⟩:
  structure/class t2_space has only Prop fields, but non-Prop type:
    Π (α : Type u) [_inst_2 : topological_space α], Type

/home/rwbarton/math/lean/mathlib/lint/analysis/topology/topological_space.lean:⟨962, 6⟩:
  lemma t2_space_top has non-Prop type:
    Π {α : Type u}, t2_space α

/home/rwbarton/math/lean/mathlib/lint/category/traversable/basic.lean:⟨76, 6⟩:
  structure/class is_lawful_traversable has only Prop fields, but non-Prop type:
    Π (t : Type u → Type u) [_inst_1 : traversable t], Type (u+1)

/home/rwbarton/math/lean/mathlib/lint/category_theory/category.lean:⟨82, 10⟩:
  structure/class category_theory.concrete_category has only Prop fields, but non-Prop type:
    Π {c : Type u → Type v}, out_param (Π {α β : Type u}, c α → c β → (α → β) → Prop) → Type

/home/rwbarton/math/lean/mathlib/lint/computability/turing_machine.lean:⟨1362, 30⟩:
  lemma turing.TM2to1.stmt_st_rec has non-Prop type:
    Π {K : Type u_1} [_inst_1 : decidable_eq K] {Γ : K → Type u_2} {Λ : Type u_3} [_inst_2 : inhabited Λ]
    {σ : Type u_4} [_inst_3 : inhabited σ] {C : turing.TM2.stmt Γ Λ σ → Sort l},
      (Π (k : K) (s : turing.TM2to1.st_act k) (q : turing.TM2.stmt Γ Λ σ), C q → C (turing.TM2to1.st_run s q)) →
      (Π (a : σ → σ) (q : turing.TM2.stmt Γ Λ σ), C q → C (turing.TM2.stmt.load a q)) →
      (Π (p : σ → bool) (q₁ q₂ : turing.TM2.stmt Γ Λ σ),
         C q₁ → C q₂ → C (turing.TM2.stmt.branch p q₁ q₂)) →
      (Π (l : σ → Λ), C (turing.TM2.stmt.goto l)) →
      C turing.TM2.stmt.halt → Π (n : turing.TM2.stmt Γ Λ σ), C n

/home/rwbarton/math/lean/mathlib/lint/data/finset.lean:⟨956, 28⟩:
  lemma finset.strong_induction_on has non-Prop type:
    Π {α : Type u_1} {p : finset α → Sort u_2} (s : finset α),
      (Π (s : finset α), (Π (t : finset α), t ⊂ s → p t) → p s) → p s

/home/rwbarton/math/lean/mathlib/lint/data/pfun.lean:⟨387, 30⟩:
  lemma pfun.fix_induction has non-Prop type:
    Π {α : Type u_1} {β : Type u_2} {f : α →. β ⊕ α} {b : β} {C : α → Sort u_3} {a : α},
      b ∈ pfun.fix f a →
      (Π (a : α),
         b ∈ pfun.fix f a → (Π (a' : α), b ∈ pfun.fix f a' → sum.inr a' ∈ f a → C a') → C a) →
      C a

/home/rwbarton/math/lean/mathlib/lint/data/rat.lean:⟨196, 30⟩:
  lemma rat.num_denom_cases_on has non-Prop type:
    Π {C : ℚ → Sort u} (a : ℚ),
      (Π (n : ℤ) (d : ℕ), d > 0 → nat.coprime (int.nat_abs n) d → C (rat.mk n ↑d)) → C a

/home/rwbarton/math/lean/mathlib/lint/data/rat.lean:⟨200, 30⟩:
  lemma rat.num_denom_cases_on' has non-Prop type:
    Π {C : ℚ → Sort u} (a : ℚ), (Π (n : ℤ) (d : ℕ), d ≠ 0 → C (rat.mk n ↑d)) → C a

/home/rwbarton/math/lean/mathlib/lint/data/real/cau_seq_completion.lean:⟨156, 6⟩:
  structure/class cau_seq.is_complete has only Prop fields, but non-Prop type:
    Π {α : Type u_1} [_inst_1 : discrete_linear_ordered_field α] (β : Type u_2) [_inst_2 : ring β]
    (abv : β → α) [_inst_3 : is_absolute_value abv], Type

/home/rwbarton/math/lean/mathlib/lint/field_theory/subfield.lean:⟨11, 6⟩:
  structure/class is_subfield has only Prop fields, but non-Prop type:
    Π {F : Type u_1} [_inst_1 : field F], set F → Type

/home/rwbarton/math/lean/mathlib/lint/group_theory/group_action.lean:⟨55, 6⟩:
  structure/class is_group_action has only Prop fields, but non-Prop type:
    Π {α : Type u} {β : Type v} [_inst_1 : group α], (α → β → β) → Type

/home/rwbarton/math/lean/mathlib/lint/logic/basic.lean:⟨84, 8⟩:
  lemma imp_intro has non-Prop type:
    Π {α : Sort u_1} {β : Sort u_2}, α → β → α

/home/rwbarton/math/lean/mathlib/lint/logic/basic.lean:⟨109, 8⟩:
  lemma not.elim has non-Prop type:
    Π {a : Prop} {α : Sort u_1}, ¬a → a → α

/home/rwbarton/math/lean/mathlib/lint/logic/basic.lean:⟨516, 22⟩:
  lemma classical.dec has non-Prop type:
    Π (p : Prop), decidable p

/home/rwbarton/math/lean/mathlib/lint/logic/basic.lean:⟨517, 22⟩:
  lemma classical.dec_pred has non-Prop type:
    Π {α : Sort u_1} (p : α → Prop), decidable_pred p

/home/rwbarton/math/lean/mathlib/lint/logic/basic.lean:⟨518, 22⟩:
  lemma classical.dec_rel has non-Prop type:
    Π {α : Sort u_1} (p : α → α → Prop), decidable_rel p

/home/rwbarton/math/lean/mathlib/lint/logic/basic.lean:⟨519, 22⟩:
  lemma classical.dec_eq has non-Prop type:
    Π (α : Sort u_1), decidable_eq α

/home/rwbarton/math/lean/mathlib/lint/number_theory/dioph.lean:⟨82, 6⟩:
  structure/class fin2.is_lt has only Prop fields, but non-Prop type:
    ℕ → ℕ → Type

/home/rwbarton/math/lean/mathlib/lint/order/order_iso.lean:⟨141, 8⟩:
  lemma order_embedding.nat_lt has non-Prop type:
    Π {α : Type u_1} {r : α → α → Prop} [_inst_1 : is_strict_order α r] (f : ℕ → α),
      (∀ (n : ℕ), r (f n) (f (n + 1))) → has_lt.lt ≼o r

/home/rwbarton/math/lean/mathlib/lint/order/order_iso.lean:⟨150, 8⟩:
  lemma order_embedding.nat_gt has non-Prop type:
    Π {α : Type u_1} {r : α → α → Prop} [_inst_1 : is_strict_order α r] (f : ℕ → α),
      (∀ (n : ℕ), r (f (n + 1)) (f n)) → gt ≼o r

/home/rwbarton/math/lean/mathlib/lint/order/order_iso.lean:⟨243, 8⟩:
  lemma order_iso.sum_lex_congr has non-Prop type:
    Π {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {r₁ : α₁ → α₁ → Prop}
    {r₂ : α₂ → α₂ → Prop} {s₁ : β₁ → β₁ → Prop} {s₂ : β₂ → β₂ → Prop},
      r₁ ≃o r₂ → s₁ ≃o s₂ → sum.lex r₁ s₁ ≃o sum.lex r₂ s₂

/home/rwbarton/math/lean/mathlib/lint/order/order_iso.lean:⟨250, 8⟩:
  lemma order_iso.prod_lex_congr has non-Prop type:
    Π {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {r₁ : α₁ → α₁ → Prop}
    {r₂ : α₂ → α₂ → Prop} {s₁ : β₁ → β₁ → Prop} {s₂ : β₂ → β₂ → Prop},
      r₁ ≃o r₂ → s₁ ≃o s₂ → prod.lex r₁ s₁ ≃o prod.lex r₂ s₂

/home/rwbarton/math/lean/mathlib/lint/set_theory/zfc.lean:⟨254, 22⟩:
  lemma classical.all_definable has non-Prop type:
    Π {n : ℕ} (F : arity Set n), pSet.definable n F

/home/rwbarton/math/lean/mathlib/lint/tactic/interactive.lean:⟨285, 6⟩:
  lemma tactic.interactive.generalize_a_aux has non-Prop type:
    Π {α : Sort u}, (Π (x : Sort u), (α → x) → x) → α