harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Abelian/FunctorCategory.lean
theorem coimageImageComparison_app' :
    (coimageImageComparison α).app X =
      (coimageObjIso α X).hom ≫ coimageImageComparison (α.app X) ≫ (imageObjIso α X).inv

Proof state:
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ (coimageImageComparison α).app X = (coimageObjIso α X).hom ≫ coimageImageComparison (α.app X) ≫ (imageObjIso α X).inv

Tactic:
simp only [coimageImageComparison_app, Iso.hom_inv_id_assoc, Iso.hom_inv_id, Category.assoc,
  Category.comp_id]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Content.lean
theorem isPrimitive_primPart (p : R[X]) : p.primPart.IsPrimitive

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p.content = 0
⊢ p.content * p.primPart.content = p.content * 1

Tactic:
conv_rhs => rw [p.eq_C_content_mul_primPart, mul_one, content_C_mul, normalize_content]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p.content = 0
⊢ p.primPart.IsPrimitive

Tactic:
rw [isPrimitive_iff_content_eq_one]

Result:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p.content = 0
⊢ p.primPart.content = 1

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ p.primPart.IsPrimitive

Tactic:
by_cases h : p = 0

Result:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
⊢ p.primPart.IsPrimitive

case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p = 0
⊢ p.primPart.IsPrimitive

Proof state:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
⊢ p.primPart.IsPrimitive

Tactic:
simp [h]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p.content = 0
⊢ p.primPart.content = 1

Tactic:
apply mul_left_cancel₀ h

Result:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p.content = 0
⊢ p.content * p.primPart.content = p.content * 1

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p = 0
⊢ p.primPart.IsPrimitive

Tactic:
rw [← content_eq_zero_iff] at h

Result:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p.content = 0
⊢ p.primPart.IsPrimitive
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma HomologyData.exact_iff (h : S.HomologyData) :
    S.Exact ↔ IsZero h.left.H

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
this : S.HasHomology
⊢ S.Exact ↔ IsZero h.left.H

Tactic:
exact LeftHomologyData.exact_iff h.left

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
⊢ S.Exact ↔ IsZero h.left.H

Tactic:
haveI := HasHomology.mk' h

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
this : S.HasHomology
⊢ S.Exact ↔ IsZero h.left.H
-- Mathlib/Probability/Kernel/Composition/Lemmas.lean
lemma compProd_eq_parallelComp_comp_copy_comp [SFinite μ] [IsSFiniteKernel κ] :
    μ ⊗ₘ κ = (Kernel.id ∥ₖ κ) ∘ₘ Kernel.copy α ∘ₘ μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
⊢ μ ⊗ₘ κ = ⇑(Kernel.id ∥ₖ κ) ∘ₘ ⇑(Kernel.copy α) ∘ₘ μ

Tactic:
rw [compProd_eq_comp_prod, ← Kernel.parallelComp_comp_copy, Measure.comp_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem Decidable.or_congr_right' [Decidable a] (h : ¬a → (b ↔ c)) : a ∨ b ↔ a ∨ c

Proof state:
a b c : Prop
inst✝ : Decidable a
h : ¬a → (b ↔ c)
⊢ a ∨ b ↔ a ∨ c

Tactic:
rw [or_iff_not_imp_left, or_iff_not_imp_left]

Result:
a b c : Prop
inst✝ : Decidable a
h : ¬a → (b ↔ c)
⊢ ¬a → b ↔ ¬a → c

Proof state:
a b c : Prop
inst✝ : Decidable a
h : ¬a → (b ↔ c)
⊢ ¬a → b ↔ ¬a → c

Tactic:
exact imp_congr_right h

Result:
no goals
-- Mathlib/CategoryTheory/Limits/IndYoneda.lean
@[reassoc (attr := simp)]
lemma colimitHomIsoLimitYoneda'_inv_comp_π [HasLimitsOfShape I (Type u₂)] (A : C) (i : I) :
    (colimitHomIsoLimitYoneda' F A).inv ≫ (coyoneda.map (colimit.ι F ⟨i⟩).op).app A =
      limit.π (F.rightOp ⋙ yoneda.obj A) i

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : Iᵒᵖ ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape I (Type u₂)
A : C
i : I
⊢ (colimitHomIsoLimitYoneda' F A).inv ≫ (coyoneda.map (colimit.ι F (op i)).op).app A =
    limit.π (F.rightOp ⋙ yoneda.obj A) i

Tactic:
rw [← colimitHomIsoLimitYoneda'_hom_comp_π, ← Category.assoc,
  Iso.inv_hom_id, Category.id_comp]

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem multiplicity_eq_zero_of_coprime {p a b : ℕ} (hp : p ≠ 1)
    (hle : multiplicity p a ≤ multiplicity p b) (hab : Nat.Coprime a b) : multiplicity p a = 0

Proof state:
case h
p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
nh : 0 < multiplicity p a
da : p ∣ a
db : p ∣ b
⊢ False

Tactic:
have := Nat.dvd_gcd da db

Result:
case h
p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
nh : 0 < multiplicity p a
da : p ∣ a
db : p ∣ b
this : p ∣ a.gcd b
⊢ False

Proof state:
p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
nh : 0 < multiplicity p a
⊢ p ∣ a

Tactic:
simpa [multiplicity_eq_zero] using nh.ne.symm

Result:
no goals

Proof state:
case h
p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
⊢ ¬0 < multiplicity p a

Tactic:
intro nh

Result:
case h
p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
nh : 0 < multiplicity p a
⊢ False

Proof state:
case h
p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
nh : 0 < multiplicity p a
da : p ∣ a
db : p ∣ b
this : p ∣ a.gcd b
⊢ False

Tactic:
rw [Coprime.gcd_eq_one hab, Nat.dvd_one] at this

Result:
case h
p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
nh : 0 < multiplicity p a
da : p ∣ a
db : p ∣ b
this : p = 1
⊢ False

Proof state:
p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
nh : 0 < multiplicity p a
da : p ∣ a
⊢ p ∣ b

Tactic:
simpa [multiplicity_eq_zero] using (nh.trans_le hle).ne.symm

Result:
no goals

Proof state:
case h
p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
nh : 0 < multiplicity p a
⊢ False

Tactic:
have da : p ∣ a := by simpa [multiplicity_eq_zero] using nh.ne.symm

Result:
case h
p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
nh : 0 < multiplicity p a
da : p ∣ a
⊢ False

Proof state:
p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
⊢ multiplicity p a = 0

Tactic:
apply Nat.eq_zero_of_not_pos

Result:
case h
p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
⊢ ¬0 < multiplicity p a

Proof state:
case h
p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
nh : 0 < multiplicity p a
da : p ∣ a
db : p ∣ b
this : p = 1
⊢ False

Tactic:
exact hp this

Result:
no goals

Proof state:
case h
p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
nh : 0 < multiplicity p a
da : p ∣ a
⊢ False

Tactic:
have db : p ∣ b := by simpa [multiplicity_eq_zero] using (nh.trans_le hle).ne.symm

Result:
case h
p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
nh : 0 < multiplicity p a
da : p ∣ a
db : p ∣ b
⊢ False
-- Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean
theorem incMatrix_apply' [Zero R] [One R] [DecidableEq α] [DecidableRel G.Adj] {a : α}
    {e : Sym2 α} : G.incMatrix R a e = if e ∈ G.incidenceSet a then 1 else 0

Proof state:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : Zero R
inst✝² : One R
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a : α
e : Sym2 α
⊢ (if e ∈ G.incidenceSet a then 1 e else 0) = if e ∈ G.incidenceSet a then 1 else 0

Tactic:
convert rfl

Result:
no goals

Proof state:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : Zero R
inst✝² : One R
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a : α
e : Sym2 α
⊢ incMatrix R G a e = if e ∈ G.incidenceSet a then 1 else 0

Tactic:
unfold incMatrix Set.indicator

Result:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : Zero R
inst✝² : One R
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a : α
e : Sym2 α
⊢ (if e ∈ G.incidenceSet a then 1 e else 0) = if e ∈ G.incidenceSet a then 1 else 0
-- Mathlib/Algebra/MonoidAlgebra/ToDirectSum.lean
theorem toAddMonoidAlgebra_mul [AddMonoid ι] [Semiring M]
    [∀ m : M, Decidable (m ≠ 0)] (f g : ⨁ _ : ι, M) :
    (f * g).toAddMonoidAlgebra = toAddMonoidAlgebra f * toAddMonoidAlgebra g

Proof state:
case inj
ι : Type u_1
M : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ Function.Injective AddMonoidAlgebra.toDirectSum

Tactic:
apply Function.LeftInverse.injective

Result:
case inj.a
ι : Type u_1
M : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ Function.LeftInverse ?inj.g AddMonoidAlgebra.toDirectSum

case inj.g
ι : Type u_1
M : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ (⨁ (x : ι), M) → AddMonoidAlgebra M ι

Proof state:
ι : Type u_1
M : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ (f * g).toAddMonoidAlgebra.toDirectSum = (f.toAddMonoidAlgebra * g.toAddMonoidAlgebra).toDirectSum

Tactic:
simp

Result:
no goals

Proof state:
case inj.a
ι : Type u_1
M : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ Function.LeftInverse ?inj.g AddMonoidAlgebra.toDirectSum

case inj.g
ι : Type u_1
M : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ (⨁ (x : ι), M) → AddMonoidAlgebra M ι

Tactic:
apply AddMonoidAlgebra.toDirectSum_toAddMonoidAlgebra

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ (f * g).toAddMonoidAlgebra = f.toAddMonoidAlgebra * g.toAddMonoidAlgebra

Tactic:
apply_fun AddMonoidAlgebra.toDirectSum

Result:
ι : Type u_1
M : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ (f * g).toAddMonoidAlgebra.toDirectSum = (f.toAddMonoidAlgebra * g.toAddMonoidAlgebra).toDirectSum

case inj
ι : Type u_1
M : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ Function.Injective AddMonoidAlgebra.toDirectSum
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem coeff_eq_zero_of_lt {f : MvPolynomial σ R} {d : σ →₀ ℕ} (hd : m.degree f ≺[m] d) :
    f.coeff d = 0

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : m.toSyn (m.degree f) < m.toSyn d
⊢ coeff d f = 0

Tactic:
rw [← not_le] at hd

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : ¬m.toSyn d ≤ m.toSyn (m.degree f)
⊢ coeff d f = 0

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : ¬m.toSyn d ≤ m.toSyn (m.degree f)
⊢ coeff d f = 0

Tactic:
by_contra hf

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : ¬m.toSyn d ≤ m.toSyn (m.degree f)
hf : ¬coeff d f = 0
⊢ False

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : ¬m.toSyn d ≤ m.toSyn (m.degree f)
hf : ¬coeff d f = 0
⊢ False

Tactic:
apply hd (m.le_degree (mem_support_iff.mpr hf))

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem monomial_def [DecidableEq σ] (n : σ →₀ ℕ) :
    (monomial R n) = LinearMap.single R (fun _ ↦ R) n

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : DecidableEq σ
n : σ →₀ ℕ
⊢ LinearMap.single R (fun x => R) n = LinearMap.single R (fun x => R) n

Tactic:
convert rfl

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : DecidableEq σ
n : σ →₀ ℕ
⊢ monomial R n = LinearMap.single R (fun x => R) n

Tactic:
rw [monomial]

Result:
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : DecidableEq σ
n : σ →₀ ℕ
⊢ LinearMap.single R (fun x => R) n = LinearMap.single R (fun x => R) n
-- Mathlib/Order/JordanHolder.lean
theorem ext {s₁ s₂ : CompositionSeries X} (h : ∀ x, x ∈ s₁ ↔ x ∈ s₂) : s₁ = s₂ :=
  toList_injective <|
    List.eq_of_perm_of_sorted
      (by
        classical
        exact List.perm_of_nodup_nodup_toFinset_eq s₁.toList_nodup s₂.toList_nodup
          (Finset.ext <| by simpa only [List.mem_toFinset, RelSeries.mem_toList]))
      s₁.toList_sorted s₂.toList_sorted

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : ∀ (x : X), x ∈ s₁ ↔ x ∈ s₂
⊢ ∀ (a : X), a ∈ (toList s₁).toFinset ↔ a ∈ (toList s₂).toFinset

Tactic:
simpa only [List.mem_toFinset, RelSeries.mem_toList]

Result:
no goals

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : ∀ (x : X), x ∈ s₁ ↔ x ∈ s₂
⊢ (toList s₁).Perm (toList s₂)

Tactic:
classical
exact List.perm_of_nodup_nodup_toFinset_eq s₁.toList_nodup s₂.toList_nodup
  (Finset.ext <| by simpa only [List.mem_toFinset, RelSeries.mem_toList])

Result:
no goals

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : ∀ (x : X), x ∈ s₁ ↔ x ∈ s₂
⊢ (toList s₁).Perm (toList s₂)

Tactic:
exact List.perm_of_nodup_nodup_toFinset_eq s₁.toList_nodup s₂.toList_nodup
  (Finset.ext <| by simpa only [List.mem_toFinset, RelSeries.mem_toList])

Result:
no goals
-- Mathlib/Combinatorics/Quiver/Path.lean
theorem eq_of_length_zero (p : Path a b) (hzero : p.length = 0) : a = b

Proof state:
case cons
V : Type u
inst✝ : Quiver V
a b b✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ b
hzero : (a✝¹.cons a✝).length = 0
⊢ a = b

Tactic:
cases Nat.succ_ne_zero _ hzero

Result:
no goals

Proof state:
V : Type u
inst✝ : Quiver V
a b : V
p : Path a b
hzero : p.length = 0
⊢ a = b

Tactic:
cases p

Result:
case nil
V : Type u
inst✝ : Quiver V
a : V
hzero : nil.length = 0
⊢ a = a

case cons
V : Type u
inst✝ : Quiver V
a b b✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ b
hzero : (a✝¹.cons a✝).length = 0
⊢ a = b

Proof state:
case nil
V : Type u
inst✝ : Quiver V
a : V
hzero : nil.length = 0
⊢ a = a

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Ideal.lean
theorem IsProper.not_mem_of_compl_mem (hI : IsProper I) (hxc : xᶜ ∈ I) : x ∉ I

Proof state:
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsProper
hxc : xᶜ ∈ I
hx : x ∈ I
⊢ False

Tactic:
apply hI.top_not_mem

Result:
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsProper
hxc : xᶜ ∈ I
hx : x ∈ I
⊢ ⊤ ∈ I

Proof state:
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsProper
hxc : xᶜ ∈ I
hx : x ∈ I
ht : x ⊔ xᶜ ∈ I
⊢ ⊤ ∈ I

Tactic:
rwa [sup_compl_eq_top] at ht

Result:
no goals

Proof state:
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsProper
hxc : xᶜ ∈ I
hx : x ∈ I
⊢ ⊤ ∈ I

Tactic:
have ht : x ⊔ xᶜ ∈ I := sup_mem ‹_› ‹_›

Result:
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsProper
hxc : xᶜ ∈ I
hx : x ∈ I
ht : x ⊔ xᶜ ∈ I
⊢ ⊤ ∈ I

Proof state:
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsProper
hxc : xᶜ ∈ I
⊢ x ∉ I

Tactic:
intro hx

Result:
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsProper
hxc : xᶜ ∈ I
hx : x ∈ I
⊢ False
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem nodal_eq_mul_nodal_erase [DecidableEq ι] {i : ι} (hi : i ∈ s) :
    nodal s v = (X - C (v i)) * nodal (s.erase i) v

Proof state:
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : DecidableEq ι
i : ι
hi : i ∈ s
⊢ nodal s v = (X - C (v i)) * nodal (s.erase i) v

Tactic:
simp_rw [nodal, Finset.mul_prod_erase _ (fun x => X - C (v x)) hi]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem eq_of_add_eq_of_aleph0_le {a b c : Cardinal} (h : a + b = c) (ha : a < c) (hc : ℵ₀ ≤ c) :
    b = c

Proof state:
case a
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
hb : b < c
this : a + b < c
⊢ False

Tactic:
simp [h, lt_irrefl] at this

Result:
no goals

Proof state:
case a
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ ¬b < c

Tactic:
intro hb

Result:
case a
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
hb : b < c
⊢ False

Proof state:
case a
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ b ≤ c

Tactic:
rw [← h]

Result:
case a
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ b ≤ a + b

Proof state:
case a
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ b ≤ a + b

Tactic:
apply self_le_add_left

Result:
no goals

Proof state:
case a
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
hb : b < c
⊢ False

Tactic:
have : a + b < c := add_lt_of_lt hc ha hb

Result:
case a
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
hb : b < c
this : a + b < c
⊢ False

Proof state:
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ b = c

Tactic:
apply le_antisymm

Result:
case a
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ b ≤ c

case a
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ c ≤ b

Proof state:
case a
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ c ≤ b

Tactic:
rw [← not_lt]

Result:
case a
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ ¬b < c
-- Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
lemma KernelFork.IsLimit.isIso_ι {X Y : C} {f : X ⟶ Y} (c : KernelFork f)
    (hc : IsLimit c) (hf : f = 0) : IsIso c.ι

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : KernelFork f
hc : IsLimit c
hf : f = 0
⊢ IsIso (Fork.ι c)

Tactic:
let e : c.pt ≅ X := IsLimit.conePointUniqueUpToIso hc
  (KernelFork.IsLimit.ofId (f : X ⟶ Y) hf)

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : KernelFork f
hc : IsLimit c
hf : f = 0
e : c.pt ≅ X := hc.conePointUniqueUpToIso (ofId f hf)
⊢ IsIso (Fork.ι c)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : KernelFork f
hc : IsLimit c
hf : f = 0
e : c.pt ≅ X := hc.conePointUniqueUpToIso (ofId f hf)
eq : e.inv ≫ Fork.ι c = 𝟙 X
this : IsIso (e.inv ≫ Fork.ι c)
⊢ IsIso (Fork.ι c)

Tactic:
exact IsIso.of_isIso_comp_left e.inv c.ι

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : KernelFork f
hc : IsLimit c
hf : f = 0
e : c.pt ≅ X := hc.conePointUniqueUpToIso (ofId f hf)
⊢ IsIso (Fork.ι c)

Tactic:
have eq : e.inv ≫ c.ι = 𝟙 X := Fork.IsLimit.lift_ι hc

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : KernelFork f
hc : IsLimit c
hf : f = 0
e : c.pt ≅ X := hc.conePointUniqueUpToIso (ofId f hf)
eq : e.inv ≫ Fork.ι c = 𝟙 X
⊢ IsIso (Fork.ι c)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : KernelFork f
hc : IsLimit c
hf : f = 0
e : c.pt ≅ X := hc.conePointUniqueUpToIso (ofId f hf)
eq : e.inv ≫ Fork.ι c = 𝟙 X
⊢ IsIso (𝟙 X)

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : KernelFork f
hc : IsLimit c
hf : f = 0
e : c.pt ≅ X := hc.conePointUniqueUpToIso (ofId f hf)
eq : e.inv ≫ Fork.ι c = 𝟙 X
⊢ IsIso (e.inv ≫ Fork.ι c)

Tactic:
rw [eq]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : KernelFork f
hc : IsLimit c
hf : f = 0
e : c.pt ≅ X := hc.conePointUniqueUpToIso (ofId f hf)
eq : e.inv ≫ Fork.ι c = 𝟙 X
⊢ IsIso (𝟙 X)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : KernelFork f
hc : IsLimit c
hf : f = 0
e : c.pt ≅ X := hc.conePointUniqueUpToIso (ofId f hf)
eq : e.inv ≫ Fork.ι c = 𝟙 X
⊢ IsIso (Fork.ι c)

Tactic:
haveI : IsIso (e.inv ≫ c.ι) := by
  rw [eq]
  infer_instance

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : KernelFork f
hc : IsLimit c
hf : f = 0
e : c.pt ≅ X := hc.conePointUniqueUpToIso (ofId f hf)
eq : e.inv ≫ Fork.ι c = 𝟙 X
this : IsIso (e.inv ≫ Fork.ι c)
⊢ IsIso (Fork.ι c)
-- Mathlib/Topology/LocallyConstant/Basic.lean
theorem exists_eq_const [PreconnectedSpace X] [Nonempty Y] {f : X → Y} (hf : IsLocallyConstant f) :
    ∃ y, f = Function.const X y

Proof state:
case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : X → Y
hf : IsLocallyConstant f
h : Nonempty X
⊢ ∃ y, f = Function.const X y

Tactic:
exact ⟨f (Classical.arbitrary X), hf.eq_const _⟩

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : X → Y
hf : IsLocallyConstant f
⊢ ∃ y, f = Function.const X y

Tactic:
rcases isEmpty_or_nonempty X with h | h

Result:
case inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : X → Y
hf : IsLocallyConstant f
h : IsEmpty X
⊢ ∃ y, f = Function.const X y

case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : X → Y
hf : IsLocallyConstant f
h : Nonempty X
⊢ ∃ y, f = Function.const X y

Proof state:
case inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : X → Y
hf : IsLocallyConstant f
h : IsEmpty X
⊢ ∃ y, f = Function.const X y

Tactic:
exact ⟨Classical.arbitrary Y, funext <| h.elim⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filterMap_map (f : α → β) (g : β → Option γ) (l : List α) :
    filterMap g (map f l) = filterMap (g ∘ f) l

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → Option γ
l : List α
⊢ filterMap g (map f l) = filterMap (g ∘ f) l

Tactic:
rw [← filterMap_eq_map, filterMap_filterMap]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → Option γ
l : List α
⊢ filterMap (fun x => ((some ∘ f) x).bind g) l = filterMap (g ∘ f) l

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → Option γ
l : List α
⊢ filterMap (fun x => ((some ∘ f) x).bind g) l = filterMap (g ∘ f) l

Tactic:
rfl

Result:
no goals