harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Lemmas.lean
theorem monotone_filterRevM
    {m : Type → Type v} [Monad m] [∀ α, PartialOrder (m α)] [MonoBind m] {α : Type}
    (f : γ → α → m Bool) (xs : List α) (hmono : monotone f) :
    monotone (fun x => xs.filterRevM (f x))

Proof state:
γ : Type w
inst✝³ : PartialOrder γ
m : Type → Type v
inst✝² : Monad m
inst✝¹ : (α : Type) → PartialOrder (m α)
inst✝ : MonoBind m
α : Type
f : γ → α → m Bool
xs : List α
hmono : monotone f
⊢ monotone fun x => List.filterRevM (f x) xs

Tactic:
exact monotone_filterAuxM f xs.reverse [] hmono

Result:
no goals
-- Mathlib/Data/Finset/Option.lean
theorem eraseNone_eq_biUnion [DecidableEq α] (s : Finset (Option α)) :
    eraseNone s = s.biUnion Option.toFinset

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset (Option α)
a✝ : α
⊢ a✝ ∈ eraseNone s ↔ a✝ ∈ s.biUnion Option.toFinset

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset (Option α)
⊢ eraseNone s = s.biUnion Option.toFinset

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset (Option α)
a✝ : α
⊢ a✝ ∈ eraseNone s ↔ a✝ ∈ s.biUnion Option.toFinset
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Int.lean
theorem add_le_iff_le_sub {a b c : Int} : a + b ≤ c ↔ a ≤ c - b

Proof state:
a b c : Int
⊢ a ≤ c + -b ↔ a ≤ c - b

Tactic:
rfl

Result:
no goals

Proof state:
a b c : Int
⊢ a + b ≤ c ↔ a ≤ c - b

Tactic:
conv =>
  lhs
  rw [← Int.add_zero c, ← Int.sub_self (-b), Int.sub_eq_add_neg, ← Int.add_assoc, Int.neg_neg,
    Int.add_le_add_iff_right]

Result:
a b c : Int
⊢ a ≤ c + -b ↔ a ≤ c - b
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem num_denom_add (x y : RatFunc K) :
    (x + y).num * (x.denom * y.denom) = (x.num * y.denom + x.denom * y.num) * (x + y).denom :=
  (num_mul_eq_mul_denom_iff (mul_ne_zero (denom_ne_zero x) (denom_ne_zero y))).mpr <| by
    conv_lhs => rw [← num_div_denom x, ← num_div_denom y]
    rw [div_add_div, RingHom.map_mul, RingHom.map_add, RingHom.map_mul, RingHom.map_mul]
    · exact algebraMap_ne_zero (denom_ne_zero x)
    · exact algebraMap_ne_zero (denom_ne_zero y)

Proof state:
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ x + y =
    (algebraMap K[X] (RatFunc K)) (x.num * y.denom + x.denom * y.num) /
      (algebraMap K[X] (RatFunc K)) (x.denom * y.denom)

Tactic:
conv_lhs => rw [← num_div_denom x, ← num_div_denom y]

Result:
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ (algebraMap K[X] (RatFunc K)) x.num / (algebraMap K[X] (RatFunc K)) x.denom +
      (algebraMap K[X] (RatFunc K)) y.num / (algebraMap K[X] (RatFunc K)) y.denom =
    (algebraMap K[X] (RatFunc K)) (x.num * y.denom + x.denom * y.num) /
      (algebraMap K[X] (RatFunc K)) (x.denom * y.denom)

Proof state:
case hb
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ (algebraMap K[X] (RatFunc K)) x.denom ≠ 0

Tactic:
exact algebraMap_ne_zero (denom_ne_zero x)

Result:
no goals

Proof state:
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ (algebraMap K[X] (RatFunc K)) x.num / (algebraMap K[X] (RatFunc K)) x.denom +
      (algebraMap K[X] (RatFunc K)) y.num / (algebraMap K[X] (RatFunc K)) y.denom =
    (algebraMap K[X] (RatFunc K)) (x.num * y.denom + x.denom * y.num) /
      (algebraMap K[X] (RatFunc K)) (x.denom * y.denom)

Tactic:
rw [div_add_div, RingHom.map_mul, RingHom.map_add, RingHom.map_mul, RingHom.map_mul]

Result:
case hb
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ (algebraMap K[X] (RatFunc K)) x.denom ≠ 0

case hd
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ (algebraMap K[X] (RatFunc K)) y.denom ≠ 0

Proof state:
case hd
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ (algebraMap K[X] (RatFunc K)) y.denom ≠ 0

Tactic:
exact algebraMap_ne_zero (denom_ne_zero y)

Result:
no goals
-- Mathlib/MeasureTheory/Integral/DominatedConvergence.lean
theorem continuousOn_primitive_Icc (h_int : IntegrableOn f (Icc a b) μ) :
    ContinuousOn (fun x => ∫ t in Icc a x, f t ∂μ) (Icc a b)

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
aux : (fun x => ∫ (t : ℝ) in Icc a x, f t ∂μ) = fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ) (Icc a b)

Tactic:
exact continuousOn_primitive h_int

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
⊢ (fun x => ∫ (t : ℝ) in Icc a x, f t ∂μ) = fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ

Tactic:
ext x

Result:
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
x : ℝ
⊢ ∫ (t : ℝ) in Icc a x, f t ∂μ = ∫ (t : ℝ) in Ioc a x, f t ∂μ

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
aux : (fun x => ∫ (t : ℝ) in Icc a x, f t ∂μ) = fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in Icc a x, f t ∂μ) (Icc a b)

Tactic:
rw [aux]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
aux : (fun x => ∫ (t : ℝ) in Icc a x, f t ∂μ) = fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ) (Icc a b)

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in Icc a x, f t ∂μ) (Icc a b)

Tactic:
have aux : (fun x => ∫ t in Icc a x, f t ∂μ) = fun x => ∫ t in Ioc a x, f t ∂μ := by
  ext x
  exact integral_Icc_eq_integral_Ioc

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
aux : (fun x => ∫ (t : ℝ) in Icc a x, f t ∂μ) = fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in Icc a x, f t ∂μ) (Icc a b)

Proof state:
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
x : ℝ
⊢ ∫ (t : ℝ) in Icc a x, f t ∂μ = ∫ (t : ℝ) in Ioc a x, f t ∂μ

Tactic:
exact integral_Icc_eq_integral_Ioc

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
theorem card_eq_two : #s = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y}

Proof state:
case mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
a b : α
hab : a ∉ {b}
⊢ ∃ x y, x ≠ y ∧ {a, b} = {x, y}

Tactic:
exact ⟨a, b, not_mem_singleton.1 hab, rfl⟩

Result:
no goals

Proof state:
case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ a t, a ∉ t ∧ insert a t = s ∧ ∃ a, t = {a}) → ∃ x y, x ≠ y ∧ s = {x, y}

Tactic:
rintro ⟨a, _, hab, rfl, b, rfl⟩

Result:
case mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
a b : α
hab : a ∉ {b}
⊢ ∃ x y, x ≠ y ∧ {a, b} = {x, y}

Proof state:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ #s = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y}

Tactic:
constructor

Result:
case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ #s = 2 → ∃ x y, x ≠ y ∧ s = {x, y}

case mpr
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ x y, x ≠ y ∧ s = {x, y}) → #s = 2

Proof state:
case mpr
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ x y, x ≠ y ∧ s = {x, y}) → #s = 2

Tactic:
rintro ⟨x, y, h, rfl⟩

Result:
case mpr.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
x y : α
h : x ≠ y
⊢ #{x, y} = 2

Proof state:
case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ a t, a ∉ t ∧ insert a t = s ∧ #t = 1) → ∃ x y, x ≠ y ∧ s = {x, y}

Tactic:
simp_rw [card_eq_one]

Result:
case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ a t, a ∉ t ∧ insert a t = s ∧ ∃ a, t = {a}) → ∃ x y, x ≠ y ∧ s = {x, y}

Proof state:
case mpr.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
x y : α
h : x ≠ y
⊢ #{x, y} = 2

Tactic:
exact card_pair h

Result:
no goals

Proof state:
case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ #s = 2 → ∃ x y, x ≠ y ∧ s = {x, y}

Tactic:
rw [card_eq_succ]

Result:
case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ a t, a ∉ t ∧ insert a t = s ∧ #t = 1) → ∃ x y, x ≠ y ∧ s = {x, y}
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem natSepDegree_dvd_natDegree (h : Irreducible f) :
    f.natSepDegree ∣ f.natDegree

Proof state:
case intro
F : Type u
inst✝ : Field F
f : F[X]
h : Irreducible f
q : ℕ
h✝ : ExpChar F q
hf : HasSeparableContraction q f
⊢ hf.degree ∣ f.natDegree

Tactic:
exact hf.dvd_degree

Result:
no goals

Proof state:
case intro
F : Type u
inst✝ : Field F
f : F[X]
h : Irreducible f
q : ℕ
h✝ : ExpChar F q
⊢ f.natSepDegree ∣ f.natDegree

Tactic:
have hf := h.hasSeparableContraction q

Result:
case intro
F : Type u
inst✝ : Field F
f : F[X]
h : Irreducible f
q : ℕ
h✝ : ExpChar F q
hf : HasSeparableContraction q f
⊢ f.natSepDegree ∣ f.natDegree

Proof state:
F : Type u
inst✝ : Field F
f : F[X]
h : Irreducible f
⊢ f.natSepDegree ∣ f.natDegree

Tactic:
obtain ⟨q, _⟩ := ExpChar.exists F

Result:
case intro
F : Type u
inst✝ : Field F
f : F[X]
h : Irreducible f
q : ℕ
h✝ : ExpChar F q
⊢ f.natSepDegree ∣ f.natDegree

Proof state:
case intro
F : Type u
inst✝ : Field F
f : F[X]
h : Irreducible f
q : ℕ
h✝ : ExpChar F q
hf : HasSeparableContraction q f
⊢ f.natSepDegree ∣ f.natDegree

Tactic:
rw [hf.natSepDegree_eq]

Result:
case intro
F : Type u
inst✝ : Field F
f : F[X]
h : Irreducible f
q : ℕ
h✝ : ExpChar F q
hf : HasSeparableContraction q f
⊢ hf.degree ∣ f.natDegree
-- Mathlib/Order/Filter/CardinalInter.lean
theorem EventuallyLE.cardinal_bUnion {S : Set ι} (hS : #S < c)
    {s t : ∀ i ∈ S, Set α} (h : ∀ i hi, s i hi ≤ᶠ[l] t i hi) :
    ⋃ i ∈ S, s i ‹_› ≤ᶠ[l] ⋃ i ∈ S, t i ‹_›

Proof state:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
S : Set ι
hS : #↑S < c
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋃ x, s ↑x ⋯ ≤ᶠ[l] ⋃ x, t ↑x ⋯

Tactic:
exact EventuallyLE.cardinal_iUnion hS fun i => h i i.2

Result:
no goals

Proof state:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
S : Set ι
hS : #↑S < c
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋃ i, ⋃ (h : i ∈ S), s i h ≤ᶠ[l] ⋃ i, ⋃ (h : i ∈ S), t i h

Tactic:
simp only [biUnion_eq_iUnion]

Result:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
S : Set ι
hS : #↑S < c
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋃ x, s ↑x ⋯ ≤ᶠ[l] ⋃ x, t ↑x ⋯
-- Mathlib/Data/Finset/BooleanAlgebra.lean
theorem compl_insert : (insert a s)ᶜ = sᶜ.erase a

Proof state:
case h
α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ∈ (insert a s)ᶜ ↔ a✝ ∈ sᶜ.erase a

Tactic:
simp only [not_or, mem_insert, mem_compl, mem_erase]

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ (insert a s)ᶜ = sᶜ.erase a

Tactic:
ext

Result:
case h
α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ∈ (insert a s)ᶜ ↔ a✝ ∈ sᶜ.erase a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem get!_eq_getElem! [Inhabited α] (l : List α) (i) : l.get! i = l[i]!

Proof state:
α : Type u_1
inst✝ : Inhabited α
l : List α
i : Nat
⊢ l[i]?.getD default = l[i]!

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Inhabited α
l : List α
i : Nat
⊢ l.get! i = l[i]!

Tactic:
simp [get!_eq_getD]

Result:
α : Type u_1
inst✝ : Inhabited α
l : List α
i : Nat
⊢ l[i]?.getD default = l[i]!
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_le_rpow_of_exponent_le (hx : 1 ≤ x) (hyz : y ≤ z) : x ^ y ≤ x ^ z

Proof state:
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ rexp (log x * y) ≤ rexp (log x * z)

Tactic:
rw [exp_le_exp]

Result:
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ log x * y ≤ log x * z

Proof state:
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ log x * y ≤ log x * z

Tactic:
exact mul_le_mul_of_nonneg_left hyz (log_nonneg hx)

Result:
no goals

Proof state:
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ rexp (log x * y) ≤ x ^ z

Tactic:
rw [rpow_def_of_pos (lt_of_lt_of_le zero_lt_one hx)]

Result:
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ rexp (log x * y) ≤ rexp (log x * z)

Proof state:
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ x ^ y ≤ x ^ z

Tactic:
repeat' rw [rpow_def_of_pos (lt_of_lt_of_le zero_lt_one hx)]

Result:
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ rexp (log x * y) ≤ rexp (log x * z)
-- Mathlib/MeasureTheory/Constructions/Cylinders.lean
theorem empty_mem_measurableCylinders (α : ι → Type*) [∀ i, MeasurableSpace (α i)] :
    ∅ ∈ measurableCylinders α

Proof state:
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ ∅ ∈ measurableCylinders α

Tactic:
simp_rw [measurableCylinders, mem_iUnion, mem_singleton_iff]

Result:
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ ∃ i i_1, ∃ (_ : MeasurableSet i_1), ∅ = cylinder i i_1

Proof state:
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ ∃ i i_1, ∃ (_ : MeasurableSet i_1), ∅ = cylinder i i_1

Tactic:
exact ⟨∅, ∅, MeasurableSet.empty, (cylinder_empty _).symm⟩

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma exact_and_mono_f_iff_f_is_kernel [S.HasHomology] :
    S.Exact ∧ Mono S.f ↔ Nonempty (IsLimit (KernelFork.ofι S.f S.zero))

Proof state:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
inst✝ : S.HasHomology
hS : S.Exact
right✝ : Mono S.f
⊢ Nonempty (IsLimit (KernelFork.ofι S.f ⋯))

Tactic:
exact ⟨hS.fIsKernel⟩

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
inst✝ : S.HasHomology
⊢ S.Exact ∧ Mono S.f ↔ Nonempty (IsLimit (KernelFork.ofι S.f ⋯))

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
inst✝ : S.HasHomology
⊢ S.Exact ∧ Mono S.f → Nonempty (IsLimit (KernelFork.ofι S.f ⋯))

case mpr
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
inst✝ : S.HasHomology
⊢ Nonempty (IsLimit (KernelFork.ofι S.f ⋯)) → S.Exact ∧ Mono S.f

Proof state:
case mpr
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
inst✝ : S.HasHomology
⊢ Nonempty (IsLimit (KernelFork.ofι S.f ⋯)) → S.Exact ∧ Mono S.f

Tactic:
intro ⟨hS⟩

Result:
case mpr
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
inst✝ : S.HasHomology
hS : IsLimit (KernelFork.ofι S.f ⋯)
⊢ S.Exact ∧ Mono S.f

Proof state:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
inst✝ : S.HasHomology
⊢ S.Exact ∧ Mono S.f → Nonempty (IsLimit (KernelFork.ofι S.f ⋯))

Tactic:
intro ⟨hS, _⟩

Result:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
inst✝ : S.HasHomology
hS : S.Exact
right✝ : Mono S.f
⊢ Nonempty (IsLimit (KernelFork.ofι S.f ⋯))

Proof state:
case mpr
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
inst✝ : S.HasHomology
hS : IsLimit (KernelFork.ofι S.f ⋯)
⊢ S.Exact ∧ Mono S.f

Tactic:
exact ⟨S.exact_of_f_is_kernel hS, mono_of_isLimit_fork hS⟩

Result:
no goals
-- Mathlib/Topology/Algebra/Monoid.lean
theorem exists_open_nhds_one_split {s : Set M} (hs : s ∈ 𝓝 (1 : M)) :
    ∃ V : Set M, IsOpen V ∧ (1 : M) ∈ V ∧ ∀ v ∈ V, ∀ w ∈ V, v * w ∈ s

Proof state:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulOneClass M
inst✝ : ContinuousMul M
s : Set M
hs : s ∈ 𝓝 1
this : (fun a => a.1 * a.2) ⁻¹' s ∈ 𝓝 (1, 1)
⊢ ∃ V, IsOpen V ∧ 1 ∈ V ∧ ∀ v ∈ V, ∀ w ∈ V, v * w ∈ s

Tactic:
simpa only [prod_subset_iff] using exists_nhds_square this

Result:
no goals

Proof state:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulOneClass M
inst✝ : ContinuousMul M
s : Set M
hs : s ∈ 𝓝 1
⊢ s ∈ 𝓝 (1 * 1)

Tactic:
simpa only [one_mul] using hs

Result:
no goals

Proof state:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulOneClass M
inst✝ : ContinuousMul M
s : Set M
hs : s ∈ 𝓝 1
⊢ ∃ V, IsOpen V ∧ 1 ∈ V ∧ ∀ v ∈ V, ∀ w ∈ V, v * w ∈ s

Tactic:
have : (fun a : M × M => a.1 * a.2) ⁻¹' s ∈ 𝓝 ((1, 1) : M × M) :=
  tendsto_mul (by simpa only [one_mul] using hs)

Result:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulOneClass M
inst✝ : ContinuousMul M
s : Set M
hs : s ∈ 𝓝 1
this : (fun a => a.1 * a.2) ⁻¹' s ∈ 𝓝 (1, 1)
⊢ ∃ V, IsOpen V ∧ 1 ∈ V ∧ ∀ v ∈ V, ∀ w ∈ V, v * w ∈ s
-- Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean
lemma map_self_succ :
    map hj F τ j (Order.succ j) (Order.le_succ j) (by rfl) =
      (objIso F X ⟨j, by simp⟩).hom ≫ τ ≫ (objSuccIso hj F X).inv

Proof state:
C : Type u_1
inst✝² : Category.{?u.26613, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
⊢ Order.succ j ≤ Order.succ j

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
⊢ j ≤ j

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
⊢ ¬Order.succ j ≤ j

Tactic:
simpa only [Order.succ_le_iff_isMax] using hj

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
⊢ (if h₁ : Order.succ j ≤ j then (objIso F X ⟨j, ⋯⟩).hom ≫ F.map (homOfLE ⋯) ≫ (objIso F X ⟨Order.succ j, h₁⟩).inv
    else
      if h₂ : j ≤ j then
        (objIso F X ⟨j, h₂⟩).hom ≫ F.map (𝟙 ⟨j, h₂⟩) ≫ τ ≫ (objSuccIso hj F X).inv ≫ 𝟙 (obj F X ⟨Order.succ j, ⋯⟩)
      else eqToHom ⋯) =
    (objIso F X ⟨j, ⋯⟩).hom ≫ τ ≫ (objSuccIso hj F X).inv

Tactic:
rw [dif_neg (by simpa only [Order.succ_le_iff_isMax] using hj),
  dif_pos (by rfl), Functor.map_id, comp_id, id_comp]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{?u.26613, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
⊢ j ∈ Set.Iic j

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
⊢ map hj F τ j (Order.succ j) ⋯ ⋯ = (objIso F X ⟨j, ⋯⟩).hom ≫ τ ≫ (objSuccIso hj F X).inv

Tactic:
dsimp [map]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
⊢ (if h₁ : Order.succ j ≤ j then (objIso F X ⟨j, ⋯⟩).hom ≫ F.map (homOfLE ⋯) ≫ (objIso F X ⟨Order.succ j, h₁⟩).inv
    else
      if h₂ : j ≤ j then
        (objIso F X ⟨j, h₂⟩).hom ≫ F.map (𝟙 ⟨j, h₂⟩) ≫ τ ≫ (objSuccIso hj F X).inv ≫ 𝟙 (obj F X ⟨Order.succ j, ⋯⟩)
      else eqToHom ⋯) =
    (objIso F X ⟨j, ⋯⟩).hom ≫ τ ≫ (objSuccIso hj F X).inv
-- Mathlib/Data/Complex/Basic.lean
theorem normSq_add (z w : ℂ) : normSq (z + w) = normSq z + normSq w + 2 * (z * conj w).re

Proof state:
z w : ℂ
⊢ (z.re + w.re) * (z.re + w.re) + (z.im + w.im) * (z.im + w.im) =
    z.re * z.re + z.im * z.im + (w.re * w.re + w.im * w.im) + 2 * (z.re * w.re - z.im * -w.im)

Tactic:
ring

Result:
no goals

Proof state:
z w : ℂ
⊢ normSq (z + w) = normSq z + normSq w + 2 * (z * (starRingEnd ℂ) w).re

Tactic:
dsimp [normSq]

Result:
z w : ℂ
⊢ (z.re + w.re) * (z.re + w.re) + (z.im + w.im) * (z.im + w.im) =
    z.re * z.re + z.im * z.im + (w.re * w.re + w.im * w.im) + 2 * (z.re * w.re - z.im * -w.im)
-- Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean
lemma Nonempty.div_zero (hs : s.Nonempty) : s / 0 = 0 :=
  s.div_zero_subset.antisymm <| by simpa [mem_div] using hs

Proof state:
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
⊢ 0 ⊆ s / 0

Tactic:
simpa [mem_div] using hs

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Monadic.lean
theorem forIn_yield_eq_foldlM [Monad m] [LawfulMonad m]
    (l : Array α) (f : α → β → m γ) (g : α → β → γ → β) (init : β) :
    forIn l init (fun a b => (fun c => .yield (g a b c)) <$> f a b) =
      l.foldlM (fun b a => g a b <$> f a b) init

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m γ
g : α → β → γ → β
init : β
toList✝ : List α
⊢ (forIn { toList := toList✝ } init fun a b => (fun c => ForInStep.yield (g a b c)) <$> f a b) =
    foldlM (fun b a => g a b <$> f a b) init { toList := toList✝ }

Tactic:
simp [List.foldlM_map]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : Array α
f : α → β → m γ
g : α → β → γ → β
init : β
⊢ (forIn l init fun a b => (fun c => ForInStep.yield (g a b c)) <$> f a b) = foldlM (fun b a => g a b <$> f a b) init l

Tactic:
cases l

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m γ
g : α → β → γ → β
init : β
toList✝ : List α
⊢ (forIn { toList := toList✝ } init fun a b => (fun c => ForInStep.yield (g a b c)) <$> f a b) =
    foldlM (fun b a => g a b <$> f a b) init { toList := toList✝ }
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem choose_succ_left (n k : ℕ) (hk : 0 < k) :
    choose (n + 1) k = choose n (k - 1) + choose n k

Proof state:
case intro
n l : ℕ
hk : 0 < l + 1
⊢ (n + 1).choose (l + 1) = n.choose (l + 1 - 1) + n.choose (l + 1)

Tactic:
rfl

Result:
no goals

Proof state:
n k : ℕ
hk : 0 < k
⊢ (n + 1).choose k = n.choose (k - 1) + n.choose k

Tactic:
obtain ⟨l, rfl⟩ : ∃ l, k = l + 1 := Nat.exists_eq_add_of_le' hk

Result:
case intro
n l : ℕ
hk : 0 < l + 1
⊢ (n + 1).choose (l + 1) = n.choose (l + 1 - 1) + n.choose (l + 1)
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
lemma fromSpec_top [IsAffine X] : (isAffineOpen_top X).fromSpec = X.isoSpec.inv

Proof state:
X : Scheme
inst✝ : IsAffine X
⊢ ⋯.fromSpec = X.isoSpec.inv

Tactic:
rw [fromSpec, isoSpec_inv, Category.assoc, ← @Scheme.isoSpec_inv_naturality,
  ← Spec.map_comp_assoc, Scheme.Opens.ι_appTop, ← X.presheaf.map_comp, ← op_comp,
  eqToHom_comp_homOfLE, ← eqToHom_eq_homOfLE rfl, eqToHom_refl, op_id, X.presheaf.map_id,
  Spec.map_id, Category.id_comp]

Result:
no goals
-- Mathlib/Data/List/MinMax.lean
theorem maximum_of_length_pos_mem (h : 0 < l.length) :
    maximum_of_length_pos h ∈ l

Proof state:
α : Type u_1
inst✝ : LinearOrder α
l : List α
h : 0 < l.length
⊢ maximum_of_length_pos h ∈ l

Tactic:
apply maximum_mem

Result:
case a
α : Type u_1
inst✝ : LinearOrder α
l : List α
h : 0 < l.length
⊢ l.maximum = ↑(maximum_of_length_pos h)

Proof state:
case a
α : Type u_1
inst✝ : LinearOrder α
l : List α
h : 0 < l.length
⊢ l.maximum = ↑(maximum_of_length_pos h)

Tactic:
simp only [coe_maximum_of_length_pos]

Result:
no goals