harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Filtered/Final.lean
theorem Functor.final_iff_isFiltered_structuredArrow [IsFilteredOrEmpty C] :
    Final F ↔ ∀ d, IsFiltered (StructuredArrow d F)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
⊢ F.Final → ∀ (d : D), IsFiltered (StructuredArrow d F)

Tactic:
rw [final_iff_of_isFiltered]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
⊢ ((∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)) ∧
      ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t) →
    ∀ (d : D), IsFiltered (StructuredArrow d F)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
⊢ ((∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)) ∧
      ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t) →
    ∀ (d : D), IsFiltered (StructuredArrow d F)

Tactic:
exact fun h => isFiltered_structuredArrow_of_isFiltered_of_exists F h.1 h.2

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
⊢ F.Final ↔ ∀ (d : D), IsFiltered (StructuredArrow d F)

Tactic:
refine ⟨?_, fun h => final_of_isFiltered_structuredArrow F⟩

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
⊢ F.Final → ∀ (d : D), IsFiltered (StructuredArrow d F)
-- Mathlib/Algebra/MvPolynomial/Variables.lean
theorem vars_C : (C r : MvPolynomial σ R).vars = ∅

Proof state:
R : Type u
σ : Type u_1
r : R
inst✝ : CommSemiring R
⊢ (C r).vars = ∅

Tactic:
classical rw [vars_def, degrees_C, Multiset.toFinset_zero]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
r : R
inst✝ : CommSemiring R
⊢ (C r).vars = ∅

Tactic:
rw [vars_def, degrees_C, Multiset.toFinset_zero]

Result:
no goals
-- Mathlib/MeasureTheory/SetSemiring.lean
lemma diff_sUnion_eq_sUnion_disjointOfDiffUnion (hC : IsSetSemiring C) (hs : s ∈ C)
    (hI : ↑I ⊆ C) : s \ ⋃₀ I = ⋃₀ hC.disjointOfDiffUnion hs hI

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
⊢ s \ ⋃₀ ↑I = ⋃₀ ↑(hC.disjointOfDiffUnion hs hI)

Tactic:
classical
rw [(hC.exists_disjoint_finset_diff_eq hs hI).choose_spec.2.2]
simp only [disjointOfDiffUnion, coe_sdiff, coe_singleton, diff_singleton_subset_iff]
rw [sUnion_diff_singleton_empty]

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
⊢ s \ ⋃₀ ↑I = ⋃₀ ↑(hC.disjointOfDiffUnion hs hI)

Tactic:
rw [(hC.exists_disjoint_finset_diff_eq hs hI).choose_spec.2.2]

Result:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
⊢ ⋃₀ ↑⋯.choose = ⋃₀ ↑(hC.disjointOfDiffUnion hs hI)

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
⊢ ⋃₀ ↑⋯.choose = ⋃₀ (↑⋯.choose \ {∅})

Tactic:
rw [sUnion_diff_singleton_empty]

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
⊢ ⋃₀ ↑⋯.choose = ⋃₀ ↑(hC.disjointOfDiffUnion hs hI)

Tactic:
simp only [disjointOfDiffUnion, coe_sdiff, coe_singleton, diff_singleton_subset_iff]

Result:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
⊢ ⋃₀ ↑⋯.choose = ⋃₀ (↑⋯.choose \ {∅})
-- Mathlib/Computability/Partrec.lean
theorem nat_rec {f : α → ℕ} {g : α → σ} {h : α → ℕ × σ → σ} (hf : Computable f) (hg : Computable g)
    (hh : Computable₂ h) :
    Computable fun a => Nat.rec (motive := fun _ => σ) (g a) (fun y IH => h a (y, IH)) (f a) :=
  (Partrec.nat_rec hf hg hh.partrec₂).of_eq fun a => by simp; induction f a <;> simp [*]

Proof state:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ × σ → σ
hf : Computable f
hg : Computable g
hh : Computable₂ h
a : α
⊢ Nat.rec (Part.some (g a)) (fun y IH => IH.bind fun i => Part.some (h a (y, i))) (f a) =
    Part.some (Nat.rec (g a) (fun y IH => h a (y, IH)) (f a))

Tactic:
induction f a <;> simp [*]

Result:
no goals

Proof state:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ × σ → σ
hf : Computable f
hg : Computable g
hh : Computable₂ h
a : α
⊢ Nat.rec (↑g a) (fun y IH => IH.bind fun i => ↑(h a) (y, i)) (f a) =
    (↑fun a => Nat.rec (g a) (fun y IH => h a (y, IH)) (f a)) a

Tactic:
simp

Result:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ × σ → σ
hf : Computable f
hg : Computable g
hh : Computable₂ h
a : α
⊢ Nat.rec (Part.some (g a)) (fun y IH => IH.bind fun i => Part.some (h a (y, i))) (f a) =
    Part.some (Nat.rec (g a) (fun y IH => h a (y, IH)) (f a))
-- Mathlib/Data/Real/Irrational.lean
theorem add_cases : Irrational (x + y) → Irrational x ∨ Irrational y

Proof state:
x y : ℝ
⊢ x ∈ Set.range Rat.cast ∧ y ∈ Set.range Rat.cast → x + y ∈ Set.range Rat.cast

Tactic:
rintro ⟨⟨rx, rfl⟩, ⟨ry, rfl⟩⟩

Result:
case intro.intro.intro
rx ry : ℚ
⊢ ↑rx + ↑ry ∈ Set.range Rat.cast

Proof state:
x y : ℝ
⊢ x + y ∉ Set.range Rat.cast → x ∉ Set.range Rat.cast ∨ y ∉ Set.range Rat.cast

Tactic:
contrapose!

Result:
x y : ℝ
⊢ x ∈ Set.range Rat.cast ∧ y ∈ Set.range Rat.cast → x + y ∈ Set.range Rat.cast

Proof state:
case intro.intro.intro
rx ry : ℚ
⊢ ↑rx + ↑ry ∈ Set.range Rat.cast

Tactic:
exact ⟨rx + ry, cast_add rx ry⟩

Result:
no goals

Proof state:
x y : ℝ
⊢ Irrational (x + y) → Irrational x ∨ Irrational y

Tactic:
delta Irrational

Result:
x y : ℝ
⊢ x + y ∉ Set.range Rat.cast → x ∉ Set.range Rat.cast ∨ y ∉ Set.range Rat.cast
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
lemma ofHom_injective {f₁ f₂ : F ⟶ G} (h : ofHom f₁ = ofHom f₂) : f₁ = f₂ :=
  (Cocycle.equivHom F G).injective (by ext1; exact h)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
f₁ f₂ : F ⟶ G
h : ofHom f₁ = ofHom f₂
⊢ (Cocycle.equivHom F G) f₁ = (Cocycle.equivHom F G) f₂

Tactic:
ext1

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
f₁ f₂ : F ⟶ G
h : ofHom f₁ = ofHom f₂
⊢ ↑((Cocycle.equivHom F G) f₁) = ↑((Cocycle.equivHom F G) f₂)

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
f₁ f₂ : F ⟶ G
h : ofHom f₁ = ofHom f₂
⊢ ↑((Cocycle.equivHom F G) f₁) = ↑((Cocycle.equivHom F G) f₂)

Tactic:
exact h

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
/-- Binary, squared, and division-free **arithmetic mean-geometric mean inequality**
(aka AM-GM inequality) for linearly ordered commutative semirings. -/
lemma two_mul_le_add_sq [ExistsAddOfLE α] [MulPosStrictMono α]
    [AddLeftReflectLE α] [AddLeftMono α]
    (a b : α) : 2 * a * b ≤ a ^ 2 + b ^ 2

Proof state:
α : Type u
inst✝⁵ : CommSemiring α
inst✝⁴ : LinearOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftReflectLE α
inst✝ : AddLeftMono α
a b : α
⊢ 2 * a * b ≤ a ^ 2 + b ^ 2

Tactic:
simpa [fn_min_add_fn_max (fun x ↦ x * x), sq, two_mul, add_mul]
  using mul_add_mul_le_mul_add_mul (@min_le_max _ _ a b) (@min_le_max _ _ a b)

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
theorem linearIndependent_iff :
    LinearIndependent R v ↔ ∀ l, Finsupp.linearCombination R v l = 0 → l = 0

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ LinearIndependent R v ↔ ∀ (l : ι →₀ R), (Finsupp.linearCombination R v) l = 0 → l = 0

Tactic:
simp [linearIndependent_iff_ker, LinearMap.ker_eq_bot']

Result:
no goals
-- Mathlib/Order/Filter/CardinalInter.lean
theorem cardinal_iInter_mem {s : ι → Set α} (hic : #ι < c) :
    (⋂ i, s i) ∈ l ↔ ∀ i, s i ∈ l

Proof state:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
s : ι → Set α
hic : #ι < c
⊢ ⋂₀ range s ∈ l ↔ ∀ (i : ι), s i ∈ l

Tactic:
apply (cardinal_sInter_mem (lt_of_le_of_lt Cardinal.mk_range_le hic)).trans

Result:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
s : ι → Set α
hic : #ι < c
⊢ (∀ s_1 ∈ range s, s_1 ∈ l) ↔ ∀ (i : ι), s i ∈ l

Proof state:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
s : ι → Set α
hic : #ι < c
⊢ ⋂ i, s i ∈ l ↔ ∀ (i : ι), s i ∈ l

Tactic:
rw [← sInter_range _]

Result:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
s : ι → Set α
hic : #ι < c
⊢ ⋂₀ range s ∈ l ↔ ∀ (i : ι), s i ∈ l

Proof state:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
s : ι → Set α
hic : #ι < c
⊢ (∀ s_1 ∈ range s, s_1 ∈ l) ↔ ∀ (i : ι), s i ∈ l

Tactic:
exact forall_mem_range

Result:
no goals
-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem mem_range_toPermHom_iff' {τ} : τ ∈ (toPermHom g).range ↔
    (fun (c : g.cycleFactorsFinset) ↦ c.val.support.card) ∘ τ =
      fun (c : g.cycleFactorsFinset) ↦ c.val.support.card

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
τ : Perm { x // x ∈ g.cycleFactorsFinset }
⊢ τ ∈ (toPermHom g).range ↔ (fun c => (↑c).support.card) ∘ ⇑τ = fun c => (↑c).support.card

Tactic:
rw [mem_range_toPermHom_iff, funext_iff]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
τ : Perm { x // x ∈ g.cycleFactorsFinset }
⊢ (∀ (c : { x // x ∈ g.cycleFactorsFinset }), (↑(τ c)).support.card = (↑c).support.card) ↔
    ∀ (x : { x // x ∈ g.cycleFactorsFinset }), ((fun c => (↑c).support.card) ∘ ⇑τ) x = (↑x).support.card

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
τ : Perm { x // x ∈ g.cycleFactorsFinset }
⊢ (∀ (c : { x // x ∈ g.cycleFactorsFinset }), (↑(τ c)).support.card = (↑c).support.card) ↔
    ∀ (x : { x // x ∈ g.cycleFactorsFinset }), ((fun c => (↑c).support.card) ∘ ⇑τ) x = (↑x).support.card

Tactic:
simp only [Finset.coe_sort_coe, Subtype.forall, Function.comp_apply]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
/-- See `Real.log_le_sub_one_of_pos` for the stronger version when `x ≠ 0`. -/
lemma log_le_self (hx : 0 ≤ x) : log x ≤ x

Proof state:
x : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ x - 1 ≤ x

Tactic:
linarith

Result:
no goals

Proof state:
x : ℝ
hx : 0 ≤ x
⊢ log x ≤ x

Tactic:
obtain rfl | hx := hx.eq_or_lt

Result:
case inl
hx : 0 ≤ 0
⊢ log 0 ≤ 0

case inr
x : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ log x ≤ x

Proof state:
case inl
hx : 0 ≤ 0
⊢ log 0 ≤ 0

Tactic:
simp

Result:
no goals

Proof state:
case inr
x : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ log x ≤ x

Tactic:
exact (log_le_sub_one_of_pos hx).trans (by linarith)

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem comap_ne_top [RingHomClass F R S] (hK : K ≠ ⊤) : comap f K ≠ ⊤ :=
  (ne_top_iff_one _).2 <| by rw [mem_comap, map_one]; exact (ne_top_iff_one _).1 hK

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
K : Ideal S
inst✝ : RingHomClass F R S
hK : K ≠ ⊤
⊢ 1 ∉ comap f K

Tactic:
rw [mem_comap, map_one]

Result:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
K : Ideal S
inst✝ : RingHomClass F R S
hK : K ≠ ⊤
⊢ 1 ∉ K

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
K : Ideal S
inst✝ : RingHomClass F R S
hK : K ≠ ⊤
⊢ 1 ∉ K

Tactic:
exact (ne_top_iff_one _).1 hK

Result:
no goals
-- Mathlib/Topology/MetricSpace/DilationEquiv.lean
theorem ratio_symm (e : X ≃ᵈ Y) : ratio e.symm = (ratio e)⁻¹ :=
  eq_inv_of_mul_eq_one_left <| by rw [← ratio_trans, symm_trans_self, ratio_refl]

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
e : X ≃ᵈ Y
⊢ ratio e.symm * ratio e = 1

Tactic:
rw [← ratio_trans, symm_trans_self, ratio_refl]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem le_log_of_opow_le {b x c : Ordinal} (hb : 1 < b) (h : b ^ c ≤ x) : c ≤ log b x

Proof state:
b x c : Ordinal.{u_1}
hb : 1 < b
h : b ^ c ≤ x
⊢ c ≤ log b x

Tactic:
obtain rfl | hx := eq_or_ne x 0

Result:
case inl
b c : Ordinal.{u_1}
hb : 1 < b
h : b ^ c ≤ 0
⊢ c ≤ log b 0

case inr
b x c : Ordinal.{u_1}
hb : 1 < b
h : b ^ c ≤ x
hx : x ≠ 0
⊢ c ≤ log b x

Proof state:
case inr
b x c : Ordinal.{u_1}
hb : 1 < b
h : b ^ c ≤ x
hx : x ≠ 0
⊢ c ≤ log b x

Tactic:
exact (opow_le_iff_le_log hb hx).1 h

Result:
no goals

Proof state:
case inl
b c : Ordinal.{u_1}
hb : 1 < b
h : b ^ c ≤ 0
⊢ c ≤ log b 0

Tactic:
rw [Ordinal.le_zero, opow_eq_zero] at h

Result:
case inl
b c : Ordinal.{u_1}
hb : 1 < b
h : b = 0 ∧ c ≠ 0
⊢ c ≤ log b 0

Proof state:
case inl
b c : Ordinal.{u_1}
hb : 1 < b
h : b = 0 ∧ c ≠ 0
⊢ c ≤ log b 0

Tactic:
exact (zero_lt_one.asymm <| h.1 ▸ hb).elim

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem attach_append (xs ys : List α) :
    (xs ++ ys).attach = xs.attach.map (fun ⟨x, h⟩ => ⟨x, mem_append_left ys h⟩) ++
      ys.attach.map fun ⟨x, h⟩ => ⟨x, mem_append_right xs h⟩

Proof state:
α : Type u_1
xs ys : List α
⊢ pmap Subtype.mk xs ⋯ ++ pmap Subtype.mk ys ⋯ = pmap (fun a h => ⟨a, ⋯⟩) xs ⋯ ++ pmap (fun a h => ⟨a, ⋯⟩) ys ⋯

Tactic:
congr 1 <;>
exact pmap_congr_left _ fun _ _ _ _ => rfl

Result:
no goals

Proof state:
α : Type u_1
xs ys : List α
⊢ (xs ++ ys).attach =
    map
        (fun x =>
          match x with
          | ⟨x, h⟩ => ⟨x, ⋯⟩)
        xs.attach ++
      map
        (fun x =>
          match x with
          | ⟨x, h⟩ => ⟨x, ⋯⟩)
        ys.attach

Tactic:
simp only [attach, attachWith, pmap, map_pmap, pmap_append]

Result:
α : Type u_1
xs ys : List α
⊢ pmap Subtype.mk xs ⋯ ++ pmap Subtype.mk ys ⋯ = pmap (fun a h => ⟨a, ⋯⟩) xs ⋯ ++ pmap (fun a h => ⟨a, ⋯⟩) ys ⋯
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem mul_div_self_cancel_iff {I : FractionalIdeal R₁⁰ K} : I * (1 / I) = 1 ↔ ∃ J, I * J = 1 :=
  ⟨fun h => ⟨1 / I, h⟩, fun ⟨J, hJ⟩ => by rwa [← eq_one_div_of_mul_eq_one_right I J hJ]⟩

Proof state:
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
x✝ : ∃ J, I * J = 1
J : FractionalIdeal R₁⁰ K
hJ : I * J = 1
⊢ I * (1 / I) = 1

Tactic:
rwa [← eq_one_div_of_mul_eq_one_right I J hJ]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_smul (A : Matrix n n R) (c : R) : det (c • A) = c ^ Fintype.card n * det A :=
  calc
    det (c • A) = det ((diagonal fun _ => c) * A)

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
c : R
⊢ (c • A).det = ((diagonal fun x => c) * A).det

Tactic:
rw [smul_eq_diagonal_mul]

Result:
no goals

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
c : R
⊢ (diagonal fun x => c).det * A.det = c ^ Fintype.card n * A.det

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Endofunctor/Algebra.lean
theorem iso_of_iso (f : A₀ ⟶ A₁) [IsIso f.1] : IsIso f :=
  ⟨⟨{ f := inv f.1
      h

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
A₀ A₁ : Algebra F
f : A₀ ⟶ A₁
inst✝ : IsIso f.f
⊢ f ≫ { f := inv f.f, h := ⋯ } = 𝟙 A₀

Tactic:
aesop_cat

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
A₀ A₁ : Algebra F
f : A₀ ⟶ A₁
inst✝ : IsIso f.f
⊢ F.map (inv f.f) ≫ A₀.str = A₁.str ≫ inv f.f

Tactic:
rw [IsIso.eq_comp_inv f.1, Category.assoc, ← f.h]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
A₀ A₁ : Algebra F
f : A₀ ⟶ A₁
inst✝ : IsIso f.f
⊢ F.map (inv f.f) ≫ F.map f.f ≫ A₁.str = A₁.str

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
A₀ A₁ : Algebra F
f : A₀ ⟶ A₁
inst✝ : IsIso f.f
⊢ F.map (inv f.f) ≫ F.map f.f ≫ A₁.str = A₁.str

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
A₀ A₁ : Algebra F
f : A₀ ⟶ A₁
inst✝ : IsIso f.f
⊢ { f := inv f.f, h := ⋯ } ≫ f = 𝟙 A₁

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Topology/Sober.lean
lemma genericPoints_eq_singleton [QuasiSober α] [IrreducibleSpace α] [T0Space α] :
    genericPoints α = {genericPoint α}

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : QuasiSober α
inst✝¹ : IrreducibleSpace α
inst✝ : T0Space α
⊢ genericPoints α = {genericPoint α}

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : QuasiSober α
inst✝¹ : IrreducibleSpace α
inst✝ : T0Space α
x : α
⊢ x ∈ genericPoints α ↔ x ∈ {genericPoint α}

Proof state:
case h
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : QuasiSober α
inst✝¹ : IrreducibleSpace α
inst✝ : T0Space α
x : α
⊢ x ∈ genericPoints α ↔ x ∈ {genericPoint α}

Tactic:
rw [genericPoints, irreducibleComponents_eq_singleton]

Result:
case h
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : QuasiSober α
inst✝¹ : IrreducibleSpace α
inst✝ : T0Space α
x : α
⊢ x ∈ {x | closure {x} ∈ {univ}} ↔ x ∈ {genericPoint α}
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma eventually_one_sub_smoothingFn_nonneg : ∀ᶠ (n : ℕ) in atTop, 0 ≤ 1 - ε n

Proof state:
⊢ ∀ᶠ (n : ℕ) in atTop, 0 ≤ 1 - ε ↑n

Tactic:
filter_upwards [eventually_one_sub_smoothingFn_pos] with n hn

Result:
case h
n : ℕ
hn : 0 < 1 - ε ↑n
⊢ 0 ≤ 1 - ε ↑n

Proof state:
case h
n : ℕ
hn : 0 < 1 - ε ↑n
⊢ 0 ≤ 1 - ε ↑n

Tactic:
exact le_of_lt hn

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
theorem geom_sum_mul_neg [Ring α] (x : α) (n : ℕ) :
    (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n

Proof state:
α : Type u
inst✝ : Ring α
x : α
n : ℕ
⊢ (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n

Tactic:
have := congr_arg Neg.neg (geom_sum_mul x n)

Result:
α : Type u
inst✝ : Ring α
x : α
n : ℕ
this : -((∑ i ∈ range n, x ^ i) * (x - 1)) = -(x ^ n - 1)
⊢ (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n

Proof state:
α : Type u
inst✝ : Ring α
x : α
n : ℕ
this : -((∑ i ∈ range n, x ^ i) * (x - 1)) = -(x ^ n - 1)
⊢ (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n

Tactic:
rw [neg_sub, ← mul_neg, neg_sub] at this

Result:
α : Type u
inst✝ : Ring α
x : α
n : ℕ
this : (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n
⊢ (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n

Proof state:
α : Type u
inst✝ : Ring α
x : α
n : ℕ
this : (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n
⊢ (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n

Tactic:
exact this

Result:
no goals
-- Mathlib/Computability/Tape.lean
theorem Tape.move_right_n_head {Γ} [Inhabited Γ] (T : Tape Γ) (i : ℕ) :
    ((Tape.move Dir.right)^[i] T).head = T.nth i

Proof state:
Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
i : ℕ
⊢ ((move Dir.right)^[i] T).head = T.nth ↑i

Tactic:
induction i generalizing T

Result:
case zero
Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
⊢ ((move Dir.right)^[0] T).head = T.nth ↑0

case succ
Γ : Type u_1
inst✝ : Inhabited Γ
n✝ : ℕ
a✝ : ∀ (T : Tape Γ), ((move Dir.right)^[n✝] T).head = T.nth ↑n✝
T : Tape Γ
⊢ ((move Dir.right)^[n✝ + 1] T).head = T.nth ↑(n✝ + 1)

Proof state:
case zero
Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
⊢ ((move Dir.right)^[0] T).head = T.nth ↑0

Tactic:
rfl

Result:
no goals

Proof state:
case succ
Γ : Type u_1
inst✝ : Inhabited Γ
n✝ : ℕ
a✝ : ∀ (T : Tape Γ), ((move Dir.right)^[n✝] T).head = T.nth ↑n✝
T : Tape Γ
⊢ ((move Dir.right)^[n✝ + 1] T).head = T.nth ↑(n✝ + 1)

Tactic:
simp only [*, Tape.move_right_nth, Int.ofNat_succ, iterate_succ, Function.comp_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem toArray_mapFinIdx (f : (i : Nat) → α → (h : i < n) → β) (v : Vector α n) :
    (v.mapFinIdx f).toArray =
      v.toArray.mapFinIdx (fun i a h => f i a (by simpa [v.size_toArray] using h)) :=
  rfl

Proof state:
α : Type ?u.22995
n : Nat
β : Type ?u.22999
f : (i : Nat) → α → i < n → β
v : Vector α n
i : Nat
a : α
h : i < v.size
⊢ i < n

Tactic:
simpa [v.size_toArray] using h

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
lemma exists_isNClique_cliqueNum [Fintype α] : ∃ s, G.IsNClique G.cliqueNum s :=
  Nat.sSup_mem ⟨0, by simp [isNClique_empty.mpr rfl]⟩ G.fintype_cliqueNum_bddAbove

Proof state:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
⊢ 0 ∈ {n | ∃ s, G.IsNClique n s}

Tactic:
simp [isNClique_empty.mpr rfl]

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts/FunctorCategory.lean
@[simp]
lemma associator_inv_app (F₁ F₂ F₃ : J ⥤ C) (j : J) :
    (α_ F₁ F₂ F₃).inv.app j = (α_ _ _ _).inv

Proof state:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ (α_ F₁ F₂ F₃).inv.app j = (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).inv

Tactic:
rw [← cancel_mono ((α_ _ _ _).hom), Iso.inv_hom_id, ← associator_hom_app, Iso.inv_hom_id_app]

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem relfinrank_comap (f : L →+* E) (B : Subfield L) :
    relfinrank (A.comap f) B = relfinrank A (B.map f)

Proof state:
E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A : Subfield E
f : L →+* E
B : Subfield L
⊢ (comap f A).relfinrank B = A.relfinrank (map f B)

Tactic:
simpa using congr(toNat $(lift_relrank_comap A f B))

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem two_pow_sub_two_pow_pred (h : 0 < w) :
    2 ^ w - 2 ^ (w - 1) = 2 ^ (w - 1)

Proof state:
w : Nat
h : 0 < w
⊢ 2 ^ w - 2 ^ (w - 1) = 2 ^ (w - 1)

Tactic:
simp [← Nat.two_pow_pred_add_two_pow_pred h]

Result:
no goals
-- Mathlib/GroupTheory/Complement.lean
@[to_additive] lemma IsComplement.pairwiseDisjoint_smul (hst : IsComplement S T) :
    S.PairwiseDisjoint (· • T) := fun a ha b hb hab ↦ disjoint_iff_forall_ne.2 <| by
  rintro _ ⟨c, hc, rfl⟩ _ ⟨d, hd, rfl⟩
  exact hst.1.ne (a₁ := (⟨a, ha⟩, ⟨c, hc⟩)) (a₂:= (⟨b, hb⟩, ⟨d, hd⟩)) (by simp [hab])

Proof state:
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
S T : Set G
hst : IsComplement S T
a : G
ha : a ∈ S
b : G
hb : b ∈ S
hab : a ≠ b
c : G
hc : c ∈ T
d : G
hd : d ∈ T
⊢ (fun x => a • x) c ≠ (fun x => b • x) d

Tactic:
exact hst.1.ne (a₁ := (⟨a, ha⟩, ⟨c, hc⟩)) (a₂:= (⟨b, hb⟩, ⟨d, hd⟩)) (by simp [hab])

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
hst : IsComplement S T
a : G
ha : a ∈ S
b : G
hb : b ∈ S
hab : a ≠ b
c : G
hc : c ∈ T
d : G
hd : d ∈ T
⊢ (⟨a, ha⟩, ⟨c, hc⟩) ≠ (⟨b, hb⟩, ⟨d, hd⟩)

Tactic:
simp [hab]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
hst : IsComplement S T
a : G
ha : a ∈ S
b : G
hb : b ∈ S
hab : a ≠ b
⊢ ∀ ⦃a_1 : G⦄, a_1 ∈ (fun x => x • T) a → ∀ ⦃b_1 : G⦄, b_1 ∈ (fun x => x • T) b → a_1 ≠ b_1

Tactic:
rintro _ ⟨c, hc, rfl⟩ _ ⟨d, hd, rfl⟩

Result:
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
S T : Set G
hst : IsComplement S T
a : G
ha : a ∈ S
b : G
hb : b ∈ S
hab : a ≠ b
c : G
hc : c ∈ T
d : G
hd : d ∈ T
⊢ (fun x => a • x) c ≠ (fun x => b • x) d
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Offset.lean
theorem Nat.lo_eq_false_of_ro (u v k₁ k₂ : Nat) : isLt k₁ k₂ = true → u ≤ v + k₁ → (v + k₂ ≤ u) = False

Proof state:
u v k₁ k₂ : Nat
⊢ isLt k₁ k₂ = true → u ≤ v + k₁ → (v + k₂ ≤ u) = False

Tactic:
simp [isLt]

Result:
u v k₁ k₂ : Nat
⊢ k₁ < k₂ → u ≤ v + k₁ → u < v + k₂

Proof state:
u v k₁ k₂ : Nat
⊢ k₁ < k₂ → u ≤ v + k₁ → u < v + k₂

Tactic:
omega

Result:
no goals