harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
@[simp]
lemma insidePart_add : (p + q).insidePart = p.insidePart

Proof state:
case e_self.e_p.e_toList
p q : DyckWord
h : p ≠ 0
⊢ List.take (p.firstReturn + 1) ↑(p + q) = List.take (p.firstReturn + 1) ↑p

Tactic:
exact take_append_of_le_length (firstReturn_lt_length h)

Result:
no goals

Proof state:
p q : DyckWord
h : p ≠ 0
⊢ ↑({ toList := List.take (p.firstReturn + 1) ↑(p + q), count_U_eq_count_D := ⋯, count_D_le_count_U := ⋯ }.denest ⋯) =
    ↑({ toList := List.take (p.firstReturn + 1) ↑p, count_U_eq_count_D := ⋯, count_D_le_count_U := ⋯ }.denest ⋯)

Tactic:
congr 3

Result:
case e_self.e_p.e_toList
p q : DyckWord
h : p ≠ 0
⊢ List.take (p.firstReturn + 1) ↑(p + q) = List.take (p.firstReturn + 1) ↑p

Proof state:
p q : DyckWord
h : p ≠ 0
⊢ (p + q).insidePart = p.insidePart

Tactic:
simp_rw [insidePart, firstReturn_add, add_eq_zero', h, false_and, dite_false, ite_false,
  DyckWord.ext_iff, take]

Result:
p q : DyckWord
h : p ≠ 0
⊢ ↑({ toList := List.take (p.firstReturn + 1) ↑(p + q), count_U_eq_count_D := ⋯, count_D_le_count_U := ⋯ }.denest ⋯) =
    ↑({ toList := List.take (p.firstReturn + 1) ↑p, count_U_eq_count_D := ⋯, count_D_le_count_U := ⋯ }.denest ⋯)
-- Mathlib/Algebra/Order/Ring/Basic.lean
lemma sq_pos_of_neg (ha : a < 0) : 0 < a ^ 2

Proof state:
R : Type u_3
inst✝ : StrictOrderedRing R
a : R
ha : a < 0
⊢ 0 < a * a

Tactic:
exact mul_pos_of_neg_of_neg ha ha

Result:
no goals

Proof state:
R : Type u_3
inst✝ : StrictOrderedRing R
a : R
ha : a < 0
⊢ 0 < a ^ 2

Tactic:
rw [sq]

Result:
R : Type u_3
inst✝ : StrictOrderedRing R
a : R
ha : a < 0
⊢ 0 < a * a
-- Mathlib/Analysis/Complex/Periodic.lean
theorem tendsto_at_I_inf (hh : 0 < h) (hf : Periodic f h)
    (h_hol : ∀ᶠ z in I∞, DifferentiableAt ℂ f z) (h_bd : BoundedAtFilter I∞ f) :
    Tendsto f I∞ (𝓝 <| cuspFunction h f 0)

Proof state:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f ↑h
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
⊢ Tendsto (cuspFunction h f) (𝓝[≠] 0) (𝓝 (cuspFunction h f 0))

Tactic:
exact tendsto_nhdsWithin_of_tendsto_nhds
  (differentiableAt_cuspFunction_zero hh hf h_hol h_bd).continuousAt.tendsto

Result:
no goals

Proof state:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f ↑h
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
this : Tendsto (cuspFunction h f) (𝓝[≠] 0) (𝓝 (cuspFunction h f 0))
⊢ Tendsto f I∞ (𝓝 (cuspFunction h f 0))

Tactic:
simpa only [Function.comp_def, eq_cuspFunction hh.ne' hf] using this.comp (qParam_tendsto hh)

Result:
no goals

Proof state:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f ↑h
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
⊢ Tendsto f I∞ (𝓝 (cuspFunction h f 0))

Tactic:
suffices Tendsto (cuspFunction h f) (𝓝[≠] 0) (𝓝 <| cuspFunction h f 0) by
  simpa only [Function.comp_def, eq_cuspFunction hh.ne' hf] using this.comp (qParam_tendsto hh)

Result:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f ↑h
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
⊢ Tendsto (cuspFunction h f) (𝓝[≠] 0) (𝓝 (cuspFunction h f 0))
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma inv_le_one₀ (ha : 0 < a) : a⁻¹ ≤ 1 ↔ 1 ≤ a

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulMono G₀
ha : 0 < a
⊢ a⁻¹ ≤ 1 ↔ 1 ≤ a

Tactic:
simpa using inv_mul_le_one₀ ha (b := 1)

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Construction.lean
theorem natTrans_hcomp_injective {F G : W.Localization ⥤ D} {τ₁ τ₂ : F ⟶ G}
    (h : 𝟙 W.Q ◫ τ₁ = 𝟙 W.Q ◫ τ₂) : τ₁ = τ₂

Proof state:
case w.h
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
F G : W.Localization ⥤ D
τ₁ τ₂ : F ⟶ G
h : 𝟙 W.Q ◫ τ₁ = 𝟙 W.Q ◫ τ₂
X : W.Localization
⊢ τ₁.app X = τ₂.app X

Tactic:
have eq := (objEquiv W).right_inv X

Result:
case w.h
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
F G : W.Localization ⥤ D
τ₁ τ₂ : F ⟶ G
h : 𝟙 W.Q ◫ τ₁ = 𝟙 W.Q ◫ τ₂
X : W.Localization
eq : (objEquiv W).toFun ((objEquiv W).invFun X) = X
⊢ τ₁.app X = τ₂.app X

Proof state:
case w.h
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
F G : W.Localization ⥤ D
τ₁ τ₂ : F ⟶ G
h : 𝟙 W.Q ◫ τ₁ = 𝟙 W.Q ◫ τ₂
X : W.Localization
eq : (objEquiv W).toFun ((objEquiv W).invFun X) = X
⊢ τ₁.app X = τ₂.app X

Tactic:
simp only [objEquiv] at eq

Result:
case w.h
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
F G : W.Localization ⥤ D
τ₁ τ₂ : F ⟶ G
h : 𝟙 W.Q ◫ τ₁ = 𝟙 W.Q ◫ τ₂
X : W.Localization
eq : W.Q.obj X.as.obj = X
⊢ τ₁.app X = τ₂.app X

Proof state:
case w.h
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
F G : W.Localization ⥤ D
τ₁ τ₂ : F ⟶ G
h : 𝟙 W.Q ◫ τ₁ = 𝟙 W.Q ◫ τ₂
X : W.Localization
eq : W.Q.obj X.as.obj = X
⊢ τ₁.app X = τ₂.app X

Tactic:
rw [← eq, ← NatTrans.id_hcomp_app, ← NatTrans.id_hcomp_app, h]

Result:
no goals

Proof state:
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
F G : W.Localization ⥤ D
τ₁ τ₂ : F ⟶ G
h : 𝟙 W.Q ◫ τ₁ = 𝟙 W.Q ◫ τ₂
⊢ τ₁ = τ₂

Tactic:
ext X

Result:
case w.h
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
F G : W.Localization ⥤ D
τ₁ τ₂ : F ⟶ G
h : 𝟙 W.Q ◫ τ₁ = 𝟙 W.Q ◫ τ₂
X : W.Localization
⊢ τ₁.app X = τ₂.app X
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem cof_eq_zero {o} : cof o = 0 ↔ o = 0 :=
  ⟨inductionOn o fun _ r _ z =>
      let ⟨_, hl, e⟩ := cof_eq r
      type_eq_zero_iff_isEmpty.2 <|
        ⟨fun a =>
          let ⟨_, h, _⟩ := hl a
          (mk_eq_zero_iff.1 (e.trans z)).elim' ⟨_, h⟩⟩,
    fun e => by simp [e]⟩

Proof state:
o : Ordinal.{u_1}
e : o = 0
⊢ o.cof = 0

Tactic:
simp [e]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem coeff_mul_X_pow' (p : R[X]) (n d : ℕ) :
    (p * X ^ n).coeff d = ite (n ≤ d) (p.coeff (d - n)) 0

Proof state:
case neg.hnc
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
⊢ ¬x.2 = n

Tactic:
exact ((le_of_add_le_right (mem_antidiagonal.mp hx).le).trans_lt <| not_le.mp h).ne

Result:
no goals

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
h : n ≤ d
⊢ (p * X ^ n).coeff d = p.coeff (d - n)

Tactic:
rw [← tsub_add_cancel_of_le h, coeff_mul_X_pow, add_tsub_cancel_right]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ (p * X ^ n).coeff d = if n ≤ d then p.coeff (d - n) else 0

Tactic:
split_ifs with h

Result:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
h : n ≤ d
⊢ (p * X ^ n).coeff d = p.coeff (d - n)

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
h : ¬n ≤ d
⊢ (p * X ^ n).coeff d = 0

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
h : ¬n ≤ d
⊢ (p * X ^ n).coeff d = 0

Tactic:
refine (coeff_mul _ _ _).trans (Finset.sum_eq_zero fun x hx => ?_)

Result:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
⊢ p.coeff x.1 * (X ^ n).coeff x.2 = 0

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
⊢ p.coeff x.1 * (X ^ n).coeff x.2 = 0

Tactic:
rw [coeff_X_pow, if_neg, mul_zero]

Result:
case neg.hnc
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
⊢ ¬x.2 = n
-- Mathlib/Order/Birkhoff.lean
@[simp] lemma infIrredUpperSet_symm_apply (s : {s : UpperSet α // InfIrred s}) [Fintype s] :
    infIrredUpperSet.symm s = (s.1 : Set α).toFinset.inf id

Proof state:
α : Type u_1
inst✝³ : SemilatticeInf α
inst✝² : OrderTop α
inst✝¹ : Finite α
s : { s // InfIrred s }
inst✝ : Fintype ↥↑s
⊢ infIrredUpperSet.symm s = (↑↑s).toFinset.inf id

Tactic:
classical
obtain ⟨s, hs⟩ := s
obtain ⟨a, rfl⟩ := infIrred_iff_of_finite.1 hs
cases nonempty_fintype α
have : LocallyFiniteOrder α := Fintype.toLocallyFiniteOrder
simp [symm_apply_eq]

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : SemilatticeInf α
inst✝² : OrderTop α
inst✝¹ : Finite α
s : { s // InfIrred s }
inst✝ : Fintype ↥↑s
⊢ infIrredUpperSet.symm s = (↑↑s).toFinset.inf id

Tactic:
obtain ⟨s, hs⟩ := s

Result:
case mk
α : Type u_1
inst✝³ : SemilatticeInf α
inst✝² : OrderTop α
inst✝¹ : Finite α
s : UpperSet α
hs : InfIrred s
inst✝ : Fintype ↥↑⟨s, hs⟩
⊢ infIrredUpperSet.symm ⟨s, hs⟩ = (↑↑⟨s, hs⟩).toFinset.inf id

Proof state:
case mk
α : Type u_1
inst✝³ : SemilatticeInf α
inst✝² : OrderTop α
inst✝¹ : Finite α
s : UpperSet α
hs : InfIrred s
inst✝ : Fintype ↥↑⟨s, hs⟩
⊢ infIrredUpperSet.symm ⟨s, hs⟩ = (↑↑⟨s, hs⟩).toFinset.inf id

Tactic:
obtain ⟨a, rfl⟩ := infIrred_iff_of_finite.1 hs

Result:
case mk.intro
α : Type u_1
inst✝³ : SemilatticeInf α
inst✝² : OrderTop α
inst✝¹ : Finite α
a : α
hs : InfIrred (UpperSet.Ici a)
inst✝ : Fintype ↥↑⟨UpperSet.Ici a, hs⟩
⊢ infIrredUpperSet.symm ⟨UpperSet.Ici a, hs⟩ = (↑↑⟨UpperSet.Ici a, hs⟩).toFinset.inf id

Proof state:
case mk.intro.intro
α : Type u_1
inst✝³ : SemilatticeInf α
inst✝² : OrderTop α
inst✝¹ : Finite α
a : α
hs : InfIrred (UpperSet.Ici a)
inst✝ : Fintype ↥↑⟨UpperSet.Ici a, hs⟩
val✝ : Fintype α
⊢ infIrredUpperSet.symm ⟨UpperSet.Ici a, hs⟩ = (↑↑⟨UpperSet.Ici a, hs⟩).toFinset.inf id

Tactic:
have : LocallyFiniteOrder α := Fintype.toLocallyFiniteOrder

Result:
case mk.intro.intro
α : Type u_1
inst✝³ : SemilatticeInf α
inst✝² : OrderTop α
inst✝¹ : Finite α
a : α
hs : InfIrred (UpperSet.Ici a)
inst✝ : Fintype ↥↑⟨UpperSet.Ici a, hs⟩
val✝ : Fintype α
this : LocallyFiniteOrder α
⊢ infIrredUpperSet.symm ⟨UpperSet.Ici a, hs⟩ = (↑↑⟨UpperSet.Ici a, hs⟩).toFinset.inf id

Proof state:
case mk.intro.intro
α : Type u_1
inst✝³ : SemilatticeInf α
inst✝² : OrderTop α
inst✝¹ : Finite α
a : α
hs : InfIrred (UpperSet.Ici a)
inst✝ : Fintype ↥↑⟨UpperSet.Ici a, hs⟩
val✝ : Fintype α
this : LocallyFiniteOrder α
⊢ infIrredUpperSet.symm ⟨UpperSet.Ici a, hs⟩ = (↑↑⟨UpperSet.Ici a, hs⟩).toFinset.inf id

Tactic:
simp [symm_apply_eq]

Result:
no goals

Proof state:
case mk.intro
α : Type u_1
inst✝³ : SemilatticeInf α
inst✝² : OrderTop α
inst✝¹ : Finite α
a : α
hs : InfIrred (UpperSet.Ici a)
inst✝ : Fintype ↥↑⟨UpperSet.Ici a, hs⟩
⊢ infIrredUpperSet.symm ⟨UpperSet.Ici a, hs⟩ = (↑↑⟨UpperSet.Ici a, hs⟩).toFinset.inf id

Tactic:
cases nonempty_fintype α

Result:
case mk.intro.intro
α : Type u_1
inst✝³ : SemilatticeInf α
inst✝² : OrderTop α
inst✝¹ : Finite α
a : α
hs : InfIrred (UpperSet.Ici a)
inst✝ : Fintype ↥↑⟨UpperSet.Ici a, hs⟩
val✝ : Fintype α
⊢ infIrredUpperSet.symm ⟨UpperSet.Ici a, hs⟩ = (↑↑⟨UpperSet.Ici a, hs⟩).toFinset.inf id
-- Mathlib/Algebra/Azumaya/Basic.lean
lemma coe_tensorEquivEnd : tensorEquivEnd R = AlgHom.mulLeftRight R R

Proof state:
R : Type u_1
inst✝ : CommSemiring R
⊢ ↑(tensorEquivEnd R) = AlgHom.mulLeftRight R R

Tactic:
ext

Result:
case hb.H.h
R : Type u_1
inst✝ : CommSemiring R
x✝ : Rᵐᵒᵖ
⊢ (((AlgHom.restrictScalars R ↑(tensorEquivEnd R)).comp Algebra.TensorProduct.includeRight) x✝) 1 =
    (((AlgHom.restrictScalars R (AlgHom.mulLeftRight R R)).comp Algebra.TensorProduct.includeRight) x✝) 1

Proof state:
case hb.H.h
R : Type u_1
inst✝ : CommSemiring R
x✝ : Rᵐᵒᵖ
⊢ (((AlgHom.restrictScalars R ↑(tensorEquivEnd R)).comp Algebra.TensorProduct.includeRight) x✝) 1 =
    (((AlgHom.restrictScalars R (AlgHom.mulLeftRight R R)).comp Algebra.TensorProduct.includeRight) x✝) 1

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem ext_iff {p q : R[X]} : p = q ↔ ∀ n, coeff p n = coeff q n

Proof state:
case ofFinsupp
R : Type u
inst✝ : Semiring R
q : R[X]
f : ℕ →₀ R
⊢ { toFinsupp := f } = q ↔ ∀ (n : ℕ), { toFinsupp := f }.coeff n = q.coeff n

Tactic:
rcases q with ⟨g : ℕ →₀ R⟩

Result:
case ofFinsupp.ofFinsupp
R : Type u
inst✝ : Semiring R
f g : ℕ →₀ R
⊢ { toFinsupp := f } = { toFinsupp := g } ↔ ∀ (n : ℕ), { toFinsupp := f }.coeff n = { toFinsupp := g }.coeff n

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ p = q ↔ ∀ (n : ℕ), p.coeff n = q.coeff n

Tactic:
rcases p with ⟨f : ℕ →₀ R⟩

Result:
case ofFinsupp
R : Type u
inst✝ : Semiring R
q : R[X]
f : ℕ →₀ R
⊢ { toFinsupp := f } = q ↔ ∀ (n : ℕ), { toFinsupp := f }.coeff n = q.coeff n

Proof state:
case ofFinsupp.ofFinsupp
R : Type u
inst✝ : Semiring R
f g : ℕ →₀ R
⊢ { toFinsupp := f } = { toFinsupp := g } ↔ ∀ (n : ℕ), { toFinsupp := f }.coeff n = { toFinsupp := g }.coeff n

Tactic:
simpa [coeff] using DFunLike.ext_iff (f := f) (g := g)

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
private lemma expDegree_cast {n : ℕ} (hn : n ≠ 0) :
    2 * (expDegree n : ℤ) = n ^ 2 - if Even n then 4 else 1

Proof state:
case intro.inr
n : ℕ
hn : 2 * n + 1 ≠ 0
⊢ 2 * ↑(WeierstrassCurve.expDegree (2 * n + 1)) = ↑(2 * n + 1) ^ 2 - if Even (2 * n + 1) then 4 else 1

Tactic:
push_cast [expDegree, show (2 * n + 1) ^ 2 = 2 * (2 * n * (n + 1)) + 1 by ring1,
  n.not_even_two_mul_add_one, Nat.add_sub_cancel, Nat.mul_div_cancel_left _ two_pos]

Result:
case intro.inr
n : ℕ
hn : 2 * n + 1 ≠ 0
⊢ 2 * (2 * ↑n * (↑n + 1)) = (2 * ↑n + 1) ^ 2 - 1

Proof state:
n : ℕ
hn : n ≠ 0
⊢ 2 * ↑(WeierstrassCurve.expDegree n) = ↑n ^ 2 - if Even n then 4 else 1

Tactic:
rcases n.even_or_odd' with ⟨n, rfl | rfl⟩

Result:
case intro.inl
n : ℕ
hn : 2 * n ≠ 0
⊢ 2 * ↑(WeierstrassCurve.expDegree (2 * n)) = ↑(2 * n) ^ 2 - if Even (2 * n) then 4 else 1

case intro.inr
n : ℕ
hn : 2 * n + 1 ≠ 0
⊢ 2 * ↑(WeierstrassCurve.expDegree (2 * n + 1)) = ↑(2 * n + 1) ^ 2 - if Even (2 * n + 1) then 4 else 1

Proof state:
case intro.inl.succ
n : ℕ
hn : 2 * (n + 1) ≠ 0
⊢ 2 * (2 * ↑n * (↑n + 2)) = (2 * (↑n + 1)) ^ 2 - 4

Tactic:
ring1

Result:
no goals

Proof state:
n : ℕ
hn : 2 * n + 1 ≠ 0
⊢ (2 * n + 1) ^ 2 = 2 * (2 * n * (n + 1)) + 1

Tactic:
ring1

Result:
no goals

Proof state:
case intro.inr
n : ℕ
hn : 2 * n + 1 ≠ 0
⊢ 2 * (2 * ↑n * (↑n + 1)) = (2 * ↑n + 1) ^ 2 - 1

Tactic:
ring1

Result:
no goals

Proof state:
case intro.inl.zero
hn : 2 * 0 ≠ 0
⊢ 2 * ↑(WeierstrassCurve.expDegree (2 * 0)) = ↑(2 * 0) ^ 2 - if Even (2 * 0) then 4 else 1

Tactic:
contradiction

Result:
no goals

Proof state:
n : ℕ
hn : 2 * (n + 1) ≠ 0
⊢ (2 * (n + 1)) ^ 2 = 2 * (2 * n * (n + 2)) + 4

Tactic:
ring1

Result:
no goals

Proof state:
case intro.inl.succ
n : ℕ
hn : 2 * (n + 1) ≠ 0
⊢ 2 * ↑(WeierstrassCurve.expDegree (2 * (n + 1))) = ↑(2 * (n + 1)) ^ 2 - if Even (2 * (n + 1)) then 4 else 1

Tactic:
push_cast [expDegree, show (2 * (n + 1)) ^ 2 = 2 * (2 * n * (n + 2)) + 4 by ring1, even_two_mul,
  Nat.add_sub_cancel, Nat.mul_div_cancel_left _ two_pos]

Result:
case intro.inl.succ
n : ℕ
hn : 2 * (n + 1) ≠ 0
⊢ 2 * (2 * ↑n * (↑n + 2)) = (2 * (↑n + 1)) ^ 2 - 4

Proof state:
case intro.inl
n : ℕ
hn : 2 * n ≠ 0
⊢ 2 * ↑(WeierstrassCurve.expDegree (2 * n)) = ↑(2 * n) ^ 2 - if Even (2 * n) then 4 else 1

Tactic:
rcases n with _ | n

Result:
case intro.inl.zero
hn : 2 * 0 ≠ 0
⊢ 2 * ↑(WeierstrassCurve.expDegree (2 * 0)) = ↑(2 * 0) ^ 2 - if Even (2 * 0) then 4 else 1

case intro.inl.succ
n : ℕ
hn : 2 * (n + 1) ≠ 0
⊢ 2 * ↑(WeierstrassCurve.expDegree (2 * (n + 1))) = ↑(2 * (n + 1)) ^ 2 - if Even (2 * (n + 1)) then 4 else 1
-- Mathlib/RingTheory/Nilpotent/Basic.lean
theorem zero_isRadical_iff [MonoidWithZero R] : IsRadical (0 : R) ↔ IsReduced R

Proof state:
R : Type u_1
inst✝ : MonoidWithZero R
⊢ IsRadical 0 ↔ IsReduced R

Tactic:
simp_rw [isReduced_iff, IsNilpotent, exists_imp, ← zero_dvd_iff]

Result:
R : Type u_1
inst✝ : MonoidWithZero R
⊢ IsRadical 0 ↔ ∀ (x : R) (x_1 : ℕ), 0 ∣ x ^ x_1 → 0 ∣ x

Proof state:
R : Type u_1
inst✝ : MonoidWithZero R
⊢ IsRadical 0 ↔ ∀ (x : R) (x_1 : ℕ), 0 ∣ x ^ x_1 → 0 ∣ x

Tactic:
exact forall_swap

Result:
no goals
-- Mathlib/Data/Real/GoldenRatio.lean
theorem fib_isSol_fibRec : fibRec.IsSolution (fun x => x.fib : ℕ → α)

Proof state:
α : Type u_1
inst✝ : CommSemiring α
⊢ { order := 2, coeffs := ![1, 1] }.IsSolution fun x => ↑(Nat.fib x)

Tactic:
intro n

Result:
α : Type u_1
inst✝ : CommSemiring α
n : ℕ
⊢ (fun x => ↑(Nat.fib x)) (n + { order := 2, coeffs := ![1, 1] }.order) =
    ∑ i : Fin { order := 2, coeffs := ![1, 1] }.order,
      { order := 2, coeffs := ![1, 1] }.coeffs i * (fun x => ↑(Nat.fib x)) (n + ↑i)

Proof state:
α : Type u_1
inst✝ : CommSemiring α
⊢ fibRec.IsSolution fun x => ↑(Nat.fib x)

Tactic:
rw [fibRec]

Result:
α : Type u_1
inst✝ : CommSemiring α
⊢ { order := 2, coeffs := ![1, 1] }.IsSolution fun x => ↑(Nat.fib x)

Proof state:
α : Type u_1
inst✝ : CommSemiring α
n : ℕ
⊢ ↑(Nat.fib (n + 1) + Nat.fib n) = ∑ x : Fin 2, ![1, 1] x * ↑(Nat.fib (n + ↑x))

Tactic:
simp [Finset.sum_fin_eq_sum_range, Finset.sum_range_succ']

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommSemiring α
n : ℕ
⊢ (fun x => ↑(Nat.fib x)) (n + { order := 2, coeffs := ![1, 1] }.order) =
    ∑ i : Fin { order := 2, coeffs := ![1, 1] }.order,
      { order := 2, coeffs := ![1, 1] }.coeffs i * (fun x => ↑(Nat.fib x)) (n + ↑i)

Tactic:
simp only

Result:
α : Type u_1
inst✝ : CommSemiring α
n : ℕ
⊢ ↑(Nat.fib (n + 2)) = ∑ x : Fin 2, ![1, 1] x * ↑(Nat.fib (n + ↑x))

Proof state:
α : Type u_1
inst✝ : CommSemiring α
n : ℕ
⊢ ↑(Nat.fib (n + 2)) = ∑ x : Fin 2, ![1, 1] x * ↑(Nat.fib (n + ↑x))

Tactic:
rw [Nat.fib_add_two, add_comm]

Result:
α : Type u_1
inst✝ : CommSemiring α
n : ℕ
⊢ ↑(Nat.fib (n + 1) + Nat.fib n) = ∑ x : Fin 2, ![1, 1] x * ↑(Nat.fib (n + ↑x))
-- Mathlib/Probability/StrongLaw.lean
theorem strong_law_aux7 :
    ∀ᵐ ω, Tendsto (fun n : ℕ => (∑ i ∈ range n, X i ω) / n) atTop (𝓝 𝔼[X 0])

Proof state:
case intro.intro.intro
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g => IndepFun f g ℙ) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℕ → ℝ
cone : ∀ (n : ℕ), 1 < c n
clim : Tendsto c atTop (𝓝 1)
this :
  ∀ (k : ℕ), ∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) / ↑⌊c k ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))
⊢ ∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (a : Ω), X 0 a))

Tactic:
filter_upwards [ae_all_iff.2 this] with ω hω

Result:
case h
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g => IndepFun f g ℙ) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℕ → ℝ
cone : ∀ (n : ℕ), 1 < c n
clim : Tendsto c atTop (𝓝 1)
this :
  ∀ (k : ℕ), ∀ᵐ (ω : Ω), Tendsto (fun n => (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) / ↑⌊c k ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))
ω : Ω
hω : ∀ (i : ℕ), Tendsto (fun n => (∑ i ∈ range ⌊c i ^ n⌋₊, X i ω) / ↑⌊c i ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))
⊢ Tendsto (fun n => (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (a : Ω), X 0 a))
-- Mathlib/Order/Filter/Basic.lean
lemma skolem {ι : Type*} {α : ι → Type*} [∀ i, Nonempty (α i)]
    {P : ∀ i : ι, α i → Prop} {F : Filter ι} :
    (∀ᶠ i in F, ∃ b, P i b) ↔ ∃ b : (Π i, α i), ∀ᶠ i in F, P i (b i)

Proof state:
ι : Type u_2
α : ι → Type u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
P : (i : ι) → α i → Prop
F : Filter ι
⊢ (∀ᶠ (i : ι) in F, ∃ b, P i b) ↔ ∃ b, ∀ᶠ (i : ι) in F, P i (b i)

Tactic:
refine ⟨fun H ↦ ?_, fun ⟨b, hb⟩ ↦ hb.mp (.of_forall fun x a ↦ ⟨_, a⟩)⟩

Result:
ι : Type u_2
α : ι → Type u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
P : (i : ι) → α i → Prop
F : Filter ι
H : ∀ᶠ (i : ι) in F, ∃ b, P i b
⊢ ∃ b, ∀ᶠ (i : ι) in F, P i (b i)

Proof state:
ι : Type u_2
α : ι → Type u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
P : (i : ι) → α i → Prop
F : Filter ι
⊢ (∀ᶠ (i : ι) in F, ∃ b, P i b) ↔ ∃ b, ∀ᶠ (i : ι) in F, P i (b i)

Tactic:
classical
refine ⟨fun H ↦ ?_, fun ⟨b, hb⟩ ↦ hb.mp (.of_forall fun x a ↦ ⟨_, a⟩)⟩
refine ⟨fun i ↦ if h : ∃ b, P i b then h.choose else Nonempty.some inferInstance, ?_⟩
filter_upwards [H] with i hi
exact dif_pos hi ▸ hi.choose_spec

Result:
no goals

Proof state:
case h
ι : Type u_2
α : ι → Type u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
P : (i : ι) → α i → Prop
F : Filter ι
H : ∀ᶠ (i : ι) in F, ∃ b, P i b
i : ι
hi : ∃ b, P i b
⊢ P i (if h : ∃ b, P i b then h.choose else ⋯.some)

Tactic:
exact dif_pos hi ▸ hi.choose_spec

Result:
no goals

Proof state:
ι : Type u_2
α : ι → Type u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
P : (i : ι) → α i → Prop
F : Filter ι
H : ∀ᶠ (i : ι) in F, ∃ b, P i b
⊢ ∀ᶠ (i : ι) in F, P i ((fun i => if h : ∃ b, P i b then h.choose else ⋯.some) i)

Tactic:
filter_upwards [H] with i hi

Result:
case h
ι : Type u_2
α : ι → Type u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
P : (i : ι) → α i → Prop
F : Filter ι
H : ∀ᶠ (i : ι) in F, ∃ b, P i b
i : ι
hi : ∃ b, P i b
⊢ P i (if h : ∃ b, P i b then h.choose else ⋯.some)

Proof state:
ι : Type u_2
α : ι → Type u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
P : (i : ι) → α i → Prop
F : Filter ι
H : ∀ᶠ (i : ι) in F, ∃ b, P i b
⊢ ∃ b, ∀ᶠ (i : ι) in F, P i (b i)

Tactic:
refine ⟨fun i ↦ if h : ∃ b, P i b then h.choose else Nonempty.some inferInstance, ?_⟩

Result:
ι : Type u_2
α : ι → Type u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
P : (i : ι) → α i → Prop
F : Filter ι
H : ∀ᶠ (i : ι) in F, ∃ b, P i b
⊢ ∀ᶠ (i : ι) in F, P i ((fun i => if h : ∃ b, P i b then h.choose else ⋯.some) i)
-- Mathlib/Geometry/RingedSpace/OpenImmersion.lean
theorem invApp_app (U : Opens X) :
    invApp f U ≫ f.c.app (op (opensFunctor f |>.obj U)) = X.presheaf.map
      (eqToHom (by simp [Opens.map, Set.preimage_image_eq _ H.base_open.injective]))

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑X
⊢ invApp f U ≫ f.c.app (op ((opensFunctor f).obj U)) = X.presheaf.map (eqToHom ⋯)

Tactic:
rw [invApp, Category.assoc, IsIso.inv_hom_id, Category.comp_id]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑X
⊢ op U = (Opens.map f.base).op.obj (op ((opensFunctor f).obj U))

Tactic:
simp [Opens.map, Set.preimage_image_eq _ H.base_open.injective]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem map_id (C : ConnectedComponent G) : C.map Hom.id = C

Proof state:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
⊢ ∀ (v : V), map Hom.id (G.connectedComponentMk v) = G.connectedComponentMk v

Tactic:
exact fun _ => rfl

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
⊢ map Hom.id C = C

Tactic:
refine C.ind ?_

Result:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
⊢ ∀ (v : V), map Hom.id (G.connectedComponentMk v) = G.connectedComponentMk v
-- Mathlib/Data/Multiset/Powerset.lean
theorem powersetCard_map {β : Type*} (f : α → β) (n : ℕ) (s : Multiset α) :
    powersetCard n (s.map f) = (powersetCard n s).map (map f)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
n : ℕ
s : Multiset α
⊢ powersetCard n (map f s) = map (map f) (powersetCard n s)

Tactic:
induction' s using Multiset.induction with t s ih generalizing n

Result:
case empty
α : Type u_1
β : Type u_2
f : α → β
n : ℕ
⊢ powersetCard n (map f 0) = map (map f) (powersetCard n 0)

case cons
α : Type u_1
β : Type u_2
f : α → β
t : α
s : Multiset α
ih : ∀ (n : ℕ), powersetCard n (map f s) = map (map f) (powersetCard n s)
n : ℕ
⊢ powersetCard n (map f (t ::ₘ s)) = map (map f) (powersetCard n (t ::ₘ s))

Proof state:
case empty
α : Type u_1
β : Type u_2
f : α → β
n : ℕ
⊢ powersetCard n (map f 0) = map (map f) (powersetCard n 0)

Tactic:
cases n <;> simp [powersetCard_zero_left, powersetCard_zero_right]

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → β
t : α
s : Multiset α
ih : ∀ (n : ℕ), powersetCard n (map f s) = map (map f) (powersetCard n s)
n : ℕ
⊢ powersetCard n (map f (t ::ₘ s)) = map (map f) (powersetCard n (t ::ₘ s))

Tactic:
cases n <;> simp [ih, map_comp_cons]

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
lemma IsDynCoverOf.of_le {T : X → X} {F : Set X} {U : Set (X × X)} {m n : ℕ} (m_n : m ≤ n)
    {s : Set X} (h : IsDynCoverOf T F U n s) :
    IsDynCoverOf T F U m s

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
m n : ℕ
m_n : m ≤ n
s : Set X
h : IsDynCoverOf T F U n s
⊢ IsDynCoverOf T F U m s

Tactic:
exact Subset.trans (c := ⋃ x ∈ s, ball x (dynEntourage T U m)) h
  (iUnion₂_mono fun x _ ↦ ball_mono (dynEntourage_antitone T U m_n) x)

Result:
no goals