harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem sup_iterate_eq_nfp (f : Ordinal.{u} → Ordinal.{u}) (a : Ordinal.{u}) :
    (sup fun n : ℕ => f^[n] a) = nfp f a

Proof state:
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ (sup fun n => f^[n] a) = nfp f a

Tactic:
refine le_antisymm ?_ (sup_le fun l => ?_)

Result:
case refine_1
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ (sup fun n => f^[n] a) ≤ nfp f a

case refine_2
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
l : List Unit
⊢ List.foldr (fun x => f) a l ≤ sup fun n => f^[n] a

Proof state:
case refine_1
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ (sup fun n => f^[n] a) ≤ nfp f a

Tactic:
rw [sup_le_iff]

Result:
case refine_1
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ ∀ (i : ℕ), f^[i] a ≤ nfp f a

Proof state:
case refine_1
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ ∀ (i : ℕ), f^[i] a ≤ nfp f a

Tactic:
intro n

Result:
case refine_1
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
n : ℕ
⊢ f^[n] a ≤ nfp f a

Proof state:
case refine_2
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
l : List Unit
⊢ List.foldr (fun x => f) a l ≤ sup fun n => f^[n] a

Tactic:
rw [List.foldr_const f a l]

Result:
case refine_2
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
l : List Unit
⊢ f^[l.length] a ≤ sup fun n => f^[n] a

Proof state:
case refine_1
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
n : ℕ
⊢ f^[n] a ≤ nfp f a

Tactic:
rw [← List.length_replicate n Unit.unit, ← List.foldr_const f a]

Result:
case refine_1
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
n : ℕ
⊢ List.foldr (fun x => f) a (List.replicate n ()) ≤ nfp f a

Proof state:
case refine_2
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
l : List Unit
⊢ f^[l.length] a ≤ sup fun n => f^[n] a

Tactic:
exact le_sup _ _

Result:
no goals

Proof state:
case refine_1
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
n : ℕ
⊢ List.foldr (fun x => f) a (List.replicate n ()) ≤ nfp f a

Tactic:
apply le_sup

Result:
no goals
-- Mathlib/Computability/PostTuringMachine.lean
theorem supportsStmt_move {S : Finset (Λ' Γ Λ σ)} {d : Dir} {q : Stmt Bool (Λ' Γ Λ σ) σ} :
    SupportsStmt S (move n d q) = SupportsStmt S q

Proof state:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
S : Finset (Λ' Γ Λ σ)
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
⊢ ∀ {i : ℕ}, SupportsStmt S ((Stmt.move d)^[i] q) = SupportsStmt S q

Tactic:
intro i

Result:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
S : Finset (Λ' Γ Λ σ)
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
⊢ SupportsStmt S ((Stmt.move d)^[i] q) = SupportsStmt S q

Proof state:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
S : Finset (Λ' Γ Λ σ)
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
⊢ SupportsStmt S (move n d q) = SupportsStmt S q

Tactic:
suffices ∀ {i}, SupportsStmt S ((Stmt.move d)^[i] q) = _ from this

Result:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
S : Finset (Λ' Γ Λ σ)
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
⊢ ∀ {i : ℕ}, SupportsStmt S ((Stmt.move d)^[i] q) = SupportsStmt S q

Proof state:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
S : Finset (Λ' Γ Λ σ)
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
i : ℕ
⊢ SupportsStmt S ((Stmt.move d)^[i] q) = SupportsStmt S q

Tactic:
induction i generalizing q <;> simp only [*, iterate]

Result:
case succ
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
S : Finset (Λ' Γ Λ σ)
d : Dir
n✝ : ℕ
a✝ : ∀ {q : Stmt Bool (Λ' Γ Λ σ) σ}, SupportsStmt S ((Stmt.move d)^[n✝] q) = SupportsStmt S q
q : Stmt Bool (Λ' Γ Λ σ) σ
⊢ SupportsStmt S (Stmt.move d q) = SupportsStmt S q

Proof state:
case succ
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
S : Finset (Λ' Γ Λ σ)
d : Dir
n✝ : ℕ
a✝ : ∀ {q : Stmt Bool (Λ' Γ Λ σ) σ}, SupportsStmt S ((Stmt.move d)^[n✝] q) = SupportsStmt S q
q : Stmt Bool (Λ' Γ Λ σ) σ
⊢ SupportsStmt S (Stmt.move d q) = SupportsStmt S q

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup_bot (s : Finset β) : (s.sup fun _ => ⊥) = (⊥ : α)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
⊢ (s.sup fun x => ⊥) = ⊥

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Result:
case inl
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
⊢ (∅.sup fun x => ⊥) = ⊥

case inr
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
hs : s.Nonempty
⊢ (s.sup fun x => ⊥) = ⊥

Proof state:
case inl
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
⊢ (∅.sup fun x => ⊥) = ⊥

Tactic:
exact sup_empty

Result:
no goals

Proof state:
case inr
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
hs : s.Nonempty
⊢ (s.sup fun x => ⊥) = ⊥

Tactic:
exact sup_const hs _

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean
lemma arrowSucc_extendToSucc :
    arrowSucc (extendToSucc hj F τ) j (Order.lt_succ_of_not_isMax hj) =
      Arrow.mk τ

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
⊢ arrowSucc (extendToSucc hj F τ) j ⋯ = Arrow.mk τ

Tactic:
simp [arrowSucc, arrowMap, extendToSucc_map_le_succ, extendToSuccObjIso,
  extendToSucc.objIso, extendToSuccObjSuccIso, extendToSucc.objSuccIso]

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem add_iInf {a : ℝ≥0∞} : a + iInf f = ⨅ b, a + f b

Proof state:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ a + iInf f = ⨅ b, a + f b

Tactic:
rw [add_comm, iInf_add]

Result:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ ⨅ i, f i + a = ⨅ b, a + f b

Proof state:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ ⨅ i, f i + a = ⨅ b, a + f b

Tactic:
simp [add_comm]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem SeminormFamily.withSeminorms_iff_nhds_eq_iInf [IsTopologicalAddGroup E]
    (p : SeminormFamily 𝕜 E ι) : WithSeminorms p ↔ (𝓝 (0 : E)) = ⨅ i, (𝓝 0).comap (p i)

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ WithSeminorms p ↔ 𝓝 0 = ⨅ i, comap (⇑(p i)) (𝓝 0)

Tactic:
rw [← p.filter_eq_iInf]

Result:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ WithSeminorms p ↔ 𝓝 0 = AddGroupFilterBasis.toFilterBasis.filter

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
h : WithSeminorms p
⊢ 𝓝 0 = AddGroupFilterBasis.toFilterBasis.filter

Tactic:
exact AddGroupFilterBasis.nhds_zero_eq _

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ WithSeminorms p ↔ 𝓝 0 = AddGroupFilterBasis.toFilterBasis.filter

Tactic:
refine ⟨fun h => ?_, p.withSeminorms_of_nhds⟩

Result:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
h : WithSeminorms p
⊢ 𝓝 0 = AddGroupFilterBasis.toFilterBasis.filter
-- Mathlib/Data/Set/Function.lean
theorem apply_piecewise₂ {δ' δ'' : α → Sort*} (f' g' : ∀ i, δ' i) (h : ∀ i, δ i → δ' i → δ'' i)
    {x : α} :
    h x (s.piecewise f g x) (s.piecewise f' g' x) =
      s.piecewise (fun x => h x (f x) (f' x)) (fun x => h x (g x) (g' x)) x

Proof state:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_8
δ'' : α → Sort u_9
f' g' : (i : α) → δ' i
h : (i : α) → δ i → δ' i → δ'' i
x : α
⊢ h x (s.piecewise f g x) (s.piecewise f' g' x) = s.piecewise (fun x => h x (f x) (f' x)) (fun x => h x (g x) (g' x)) x

Tactic:
by_cases hx : x ∈ s <;> simp [hx]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_sub_pi_div_two (x : ℂ) : sin (x - π / 2) = -cos x

Proof state:
x : ℂ
⊢ sin (x - ↑π / 2) = -cos x

Tactic:
simp [sub_eq_add_neg, sin_add]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finsubgraph.lean
theorem singletonFinsubgraph_le_adj_left {u v : V} {e : G.Adj u v} :
    singletonFinsubgraph u ≤ finsubgraphOfAdj e

Proof state:
V : Type u
G : SimpleGraph V
u v : V
e : G.Adj u v
⊢ singletonFinsubgraph u ≤ finsubgraphOfAdj e

Tactic:
simp [singletonFinsubgraph, finsubgraphOfAdj]

Result:
no goals
-- Mathlib/Topology/Sheaves/Presheaf.lean
theorem toPushforwardOfIso_app {X Y : TopCat} (H₁ : X ≅ Y) {ℱ : X.Presheaf C} {𝒢 : Y.Presheaf C}
    (H₂ : H₁.hom _* ℱ ⟶ 𝒢) (U : (Opens X)ᵒᵖ) :
    (toPushforwardOfIso H₁ H₂).app U =
      ℱ.map (eqToHom (by simp [Opens.map, Set.preimage_preimage])) ≫
        H₂.app (op ((Opens.map H₁.inv).obj (unop U)))

Proof state:
C : Type u_1
inst✝ : Category.{u_5, u_1} C
X Y : TopCat
H₁ : X ≅ Y
ℱ : Presheaf C X
𝒢 : Presheaf C Y
H₂ : (pushforward C H₁.hom).obj ℱ ⟶ 𝒢
U : (Opens ↑X)ᵒᵖ
⊢ (toPushforwardOfIso H₁ H₂).app U = ℱ.map (eqToHom ⋯) ≫ H₂.app (op ((Opens.map H₁.inv).obj (unop U)))

Tactic:
simp [toPushforwardOfIso, Adjunction.homEquiv_unit]

Result:
no goals

Proof state:
C✝ : Type u
inst✝³ : Category.{v, u} C✝
X✝ : TopCat
C : Type u_1
inst✝² : Category.{?u.61790, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X Y : TopCat
H₁ : X ≅ Y
ℱ : Presheaf C X
𝒢 : Presheaf C Y
H₂ : (pushforward C H₁.hom).obj ℱ ⟶ 𝒢
U : (Opens ↑X)ᵒᵖ
⊢ U = (Opens.map H₁.hom).op.obj (op ((Opens.map H₁.inv).obj (unop U)))

Tactic:
simp [Opens.map, Set.preimage_preimage]

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Defs.lean
theorem induction_on' {P : RatFunc K → Prop} :
    ∀ (x : RatFunc K) (_pq : ∀ (p q : K[X]) (_ : q ≠ 0), P (RatFunc.mk p q)), P x
  | ⟨x⟩, f =>
    Localization.induction_on x fun ⟨p, q⟩ => by
      simpa only [mk_coe_def, Localization.mk_eq_mk'] using
        f p q (mem_nonZeroDivisors_iff_ne_zero.mp q.2)

Proof state:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
P : RatFunc K → Prop
x : FractionRing K[X]
f : ∀ (p q : K[X]), q ≠ 0 → P (RatFunc.mk p q)
x✝ : K[X] × ↥K[X]⁰
p : K[X]
q : ↥K[X]⁰
⊢ P { toFractionRing := Localization.mk (p, q).1 (p, q).2 }

Tactic:
simpa only [mk_coe_def, Localization.mk_eq_mk'] using
  f p q (mem_nonZeroDivisors_iff_ne_zero.mp q.2)

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem div_eq_zero_iff : a / b = 0 ↔ a = 0 ∨ b = ∞

Proof state:
a b : ℝ≥0∞
⊢ a / b = 0 ↔ a = 0 ∨ b = ⊤

Tactic:
simp [div_eq_mul_inv]

Result:
no goals
-- Mathlib/Data/Rel.lean
theorem Equiv.graph_inv (f : α ≃ β) : (f.symm : β → α).graph = Rel.inv (f : α → β).graph

Proof state:
case a.h.a
α : Type u_1
β : Type u_2
f : α ≃ β
x : β
y : α
⊢ Function.graph (⇑f.symm) x y ↔ (Function.graph ⇑f).inv x y

Tactic:
aesop (add norm Rel.inv_def)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α ≃ β
⊢ Function.graph ⇑f.symm = (Function.graph ⇑f).inv

Tactic:
ext x y

Result:
case a.h.a
α : Type u_1
β : Type u_2
f : α ≃ β
x : β
y : α
⊢ Function.graph (⇑f.symm) x y ↔ (Function.graph ⇑f).inv x y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem zipWith_eq_zipWith_take_min (l₁ : Array α) (l₂ : Array β) :
    zipWith f l₁ l₂ = zipWith f (l₁.take (min l₁.size l₂.size)) (l₂.take (min l₁.size l₂.size))

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
α✝ : Type u_3
f : α → β → α✝
toList✝¹ : List α
toList✝ : List β
⊢ List.zipWith f toList✝¹ toList✝ =
    List.zipWith f (List.take (min toList✝¹.length toList✝.length) toList✝¹)
      (List.take (min toList✝¹.length toList✝.length) toList✝)

Tactic:
rw [List.zipWith_eq_zipWith_take_min]

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
α✝ : Type u_3
f : α → β → α✝
l₂ : Array β
toList✝ : List α
⊢ zipWith f { toList := toList✝ } l₂ =
    zipWith f ({ toList := toList✝ }.take (min { toList := toList✝ }.size l₂.size))
      (l₂.take (min { toList := toList✝ }.size l₂.size))

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
β : Type u_2
α✝ : Type u_3
f : α → β → α✝
toList✝¹ : List α
toList✝ : List β
⊢ zipWith f { toList := toList✝¹ } { toList := toList✝ } =
    zipWith f ({ toList := toList✝¹ }.take (min { toList := toList✝¹ }.size { toList := toList✝ }.size))
      ({ toList := toList✝ }.take (min { toList := toList✝¹ }.size { toList := toList✝ }.size))

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
α✝ : Type u_3
f : α → β → α✝
toList✝¹ : List α
toList✝ : List β
⊢ zipWith f { toList := toList✝¹ } { toList := toList✝ } =
    zipWith f ({ toList := toList✝¹ }.take (min { toList := toList✝¹ }.size { toList := toList✝ }.size))
      ({ toList := toList✝ }.take (min { toList := toList✝¹ }.size { toList := toList✝ }.size))

Tactic:
simp

Result:
case mk.mk
α : Type u_1
β : Type u_2
α✝ : Type u_3
f : α → β → α✝
toList✝¹ : List α
toList✝ : List β
⊢ List.zipWith f toList✝¹ toList✝ =
    List.zipWith f (List.take (min toList✝¹.length toList✝.length) toList✝¹)
      (List.take (min toList✝¹.length toList✝.length) toList✝)

Proof state:
α : Type u_1
β : Type u_2
α✝ : Type u_3
f : α → β → α✝
l₁ : Array α
l₂ : Array β
⊢ zipWith f l₁ l₂ = zipWith f (l₁.take (min l₁.size l₂.size)) (l₂.take (min l₁.size l₂.size))

Tactic:
cases l₁

Result:
case mk
α : Type u_1
β : Type u_2
α✝ : Type u_3
f : α → β → α✝
l₂ : Array β
toList✝ : List α
⊢ zipWith f { toList := toList✝ } l₂ =
    zipWith f ({ toList := toList✝ }.take (min { toList := toList✝ }.size l₂.size))
      (l₂.take (min { toList := toList✝ }.size l₂.size))
-- Mathlib/Data/List/Infix.lean
theorem IsPrefix.flatten {l₁ l₂ : List (List α)} (h : l₁ <+: l₂) :
    l₁.flatten <+: l₂.flatten

Proof state:
α : Type u_1
l₁ l₂ : List (List α)
h : l₁ <+: l₂
⊢ l₁.flatten <+: l₂.flatten

Tactic:
rcases h with ⟨l, rfl⟩

Result:
case intro
α : Type u_1
l₁ l : List (List α)
⊢ l₁.flatten <+: (l₁ ++ l).flatten

Proof state:
case intro
α : Type u_1
l₁ l : List (List α)
⊢ l₁.flatten <+: (l₁ ++ l).flatten

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addX_self {P : Fin 3 → R} (hP : W'.Equation P) : W'.addX P P = 0

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.addX P P = 0

Tactic:
linear_combination (norm := (rw [addX]; ring1)) -2 * P z ^ 2 * (equation_iff _).mp hP

Result:
no goals

Proof state:
case a.a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ P x * P x ^ 2 * P z ^ 2 - 2 * P y * P y * P z * P z + P x ^ 2 * P x * P z ^ 2 - W'.a₁ * P x * P y * P z ^ 2 * P z -
                      W'.a₁ * P y * P x * P z * P z ^ 2 +
                    2 * W'.a₂ * P x * P x * P z ^ 2 * P z ^ 2 -
                  W'.a₃ * P y * P z ^ 4 * P z -
                W'.a₃ * P y * P z * P z ^ 4 +
              W'.a₄ * P x * P z ^ 4 * P z ^ 2 +
            W'.a₄ * P x * P z ^ 2 * P z ^ 4 +
          2 * W'.a₆ * P z ^ 4 * P z ^ 4 +
        -2 * P z ^ 2 * 0 -
      (0 +
        -2 * P z ^ 2 *
          (P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
            (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6))) =
    0

Tactic:
ring1

Result:
no goals

Proof state:
case a.a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.addX P P + -2 * P z ^ 2 * 0 -
      (0 +
        -2 * P z ^ 2 *
          (P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
            (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6))) =
    0

Tactic:
rw [addX]

Result:
case a.a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ P x * P x ^ 2 * P z ^ 2 - 2 * P y * P y * P z * P z + P x ^ 2 * P x * P z ^ 2 - W'.a₁ * P x * P y * P z ^ 2 * P z -
                      W'.a₁ * P y * P x * P z * P z ^ 2 +
                    2 * W'.a₂ * P x * P x * P z ^ 2 * P z ^ 2 -
                  W'.a₃ * P y * P z ^ 4 * P z -
                W'.a₃ * P y * P z * P z ^ 4 +
              W'.a₄ * P x * P z ^ 4 * P z ^ 2 +
            W'.a₄ * P x * P z ^ 2 * P z ^ 4 +
          2 * W'.a₆ * P z ^ 4 * P z ^ 4 +
        -2 * P z ^ 2 * 0 -
      (0 +
        -2 * P z ^ 2 *
          (P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
            (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6))) =
    0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_append_right {a : Vector α n} {b : Vector α m} {i : Nat} (h : i < n + m) (hi : n ≤ i) :
    (a ++ b)[i] = b[i - n]

Proof state:
α : Type u_1
n m : Nat
a : Vector α n
b : Vector α m
i : Nat
h : i < n + m
hi : n ≤ i
⊢ ¬i < n

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
n m : Nat
a : Vector α n
b : Vector α m
i : Nat
h : i < n + m
hi : n ≤ i
⊢ (a ++ b)[i] = b[i - n]

Tactic:
rw [getElem_append, dif_neg (by omega)]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/House.lean
theorem house_sum_le_sum_house {ι : Type*} (s : Finset ι) (α : ι → K) :
    house (∑ i ∈ s, α i) ≤ ∑ i ∈ s, house (α i)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ι : Type u_2
s : Finset ι
α : ι → K
⊢ ‖∑ x ∈ s, (canonicalEmbedding K) (α x)‖ ≤ ∑ x ∈ s, ‖(canonicalEmbedding K) (α x)‖

Tactic:
apply norm_sum_le_of_le

Result:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ι : Type u_2
s : Finset ι
α : ι → K
⊢ ∀ b ∈ s, ‖(canonicalEmbedding K) (α b)‖ ≤ ‖(canonicalEmbedding K) (α b)‖

Proof state:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ι : Type u_2
s : Finset ι
α : ι → K
b✝ : ι
a✝ : b✝ ∈ s
⊢ ‖(canonicalEmbedding K) (α b✝)‖ ≤ ‖(canonicalEmbedding K) (α b✝)‖

Tactic:
rfl

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ι : Type u_2
s : Finset ι
α : ι → K
⊢ house (∑ i ∈ s, α i) ≤ ∑ i ∈ s, house (α i)

Tactic:
simp only [house, map_sum]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ι : Type u_2
s : Finset ι
α : ι → K
⊢ ‖∑ x ∈ s, (canonicalEmbedding K) (α x)‖ ≤ ∑ x ∈ s, ‖(canonicalEmbedding K) (α x)‖

Proof state:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ι : Type u_2
s : Finset ι
α : ι → K
⊢ ∀ b ∈ s, ‖(canonicalEmbedding K) (α b)‖ ≤ ‖(canonicalEmbedding K) (α b)‖

Tactic:
intros

Result:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ι : Type u_2
s : Finset ι
α : ι → K
b✝ : ι
a✝ : b✝ ∈ s
⊢ ‖(canonicalEmbedding K) (α b✝)‖ ≤ ‖(canonicalEmbedding K) (α b✝)‖
-- Mathlib/CategoryTheory/FiberedCategory/HomLift.lean
lemma fac : f = eqToHom (domain_eq p f φ).symm ≫ p.map φ ≫ eqToHom (codomain_eq p f φ)

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsHomLift f φ
⊢ f = eqToHom ⋯ ≫ p.map φ ≫ eqToHom ⋯

Tactic:
subst_hom_lift p f φ

Result:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsHomLift (p.map φ) φ
⊢ p.map φ = eqToHom ⋯ ≫ p.map φ ≫ eqToHom ⋯

Proof state:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsHomLift (p.map φ) φ
⊢ p.map φ = eqToHom ⋯ ≫ p.map φ ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/Rademacher.lean
theorem ae_differentiableWithinAt {f : E → F} (hf : LipschitzOnWith C f s)
    (hs : MeasurableSet s) :
    ∀ᵐ x ∂(μ.restrict s), DifferentiableWithinAt ℝ f s x

Proof state:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
C : ℝ≥0
s : Set E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : FiniteDimensional ℝ F
inst✝ : μ.IsAddHaarMeasure
f : E → F
hf : LipschitzOnWith C f s
hs : MeasurableSet s
⊢ ∀ᵐ (x : E) ∂μ.restrict s, DifferentiableWithinAt ℝ f s x

Tactic:
rw [ae_restrict_iff' hs]

Result:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
C : ℝ≥0
s : Set E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : FiniteDimensional ℝ F
inst✝ : μ.IsAddHaarMeasure
f : E → F
hf : LipschitzOnWith C f s
hs : MeasurableSet s
⊢ ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x

Proof state:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
C : ℝ≥0
s : Set E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : FiniteDimensional ℝ F
inst✝ : μ.IsAddHaarMeasure
f : E → F
hf : LipschitzOnWith C f s
hs : MeasurableSet s
⊢ ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x

Tactic:
exact hf.ae_differentiableWithinAt_of_mem

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem coprime_add_self_left {m n : ℕ} : Coprime (m + n) n ↔ Coprime m n

Proof state:
m n : ℕ
⊢ (m + n).Coprime n ↔ m.Coprime n

Tactic:
rw [Coprime, Coprime, gcd_add_self_left]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem exists_nested_lieIdeal_coe_eq_iff {K' : LieSubalgebra R L} (h : K ≤ K') :
    (∃ I : LieIdeal R K', ↑I = ofLe h) ↔ ∀ x y : L, x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K

Proof state:
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
⊢ (∀ (x y : ↥K'), ↑y ∈ K → ⁅↑x, ↑y⁆ ∈ K) → ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K

Tactic:
intro h' x y hx hy

Result:
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
h' : ∀ (x y : ↥K'), ↑y ∈ K → ⁅↑x, ↑y⁆ ∈ K
x y : L
hx : x ∈ K'
hy : y ∈ K
⊢ ⁅x, y⁆ ∈ K

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
⊢ (∃ I, LieIdeal.toLieSubalgebra R (↥K') I = ofLe h) ↔ ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K

Tactic:
simp only [exists_lieIdeal_coe_eq_iff, coe_bracket, mem_ofLe]

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
⊢ (∀ (x y : ↥K'), ↑y ∈ K → ⁅↑x, ↑y⁆ ∈ K) ↔ ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K

Proof state:
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
h' : ∀ (x y : ↥K'), ↑y ∈ K → ⁅↑x, ↑y⁆ ∈ K
x y : L
hx : x ∈ K'
hy : y ∈ K
⊢ ⁅x, y⁆ ∈ K

Tactic:
exact h' ⟨x, hx⟩ ⟨y, h hy⟩ hy

Result:
no goals

Proof state:
case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
⊢ (∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K) → ∀ (x y : ↥K'), ↑y ∈ K → ⁅↑x, ↑y⁆ ∈ K

Tactic:
rintro h' ⟨x, hx⟩ ⟨y, hy⟩ hy'

Result:
case mpr.mk.mk
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
h' : ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K
x : L
hx : x ∈ K'
y : L
hy : y ∈ K'
hy' : ↑⟨y, hy⟩ ∈ K
⊢ ⁅↑⟨x, hx⟩, ↑⟨y, hy⟩⁆ ∈ K

Proof state:
case mpr.mk.mk
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
h' : ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K
x : L
hx : x ∈ K'
y : L
hy : y ∈ K'
hy' : ↑⟨y, hy⟩ ∈ K
⊢ ⁅↑⟨x, hx⟩, ↑⟨y, hy⟩⁆ ∈ K

Tactic:
exact h' x y hx hy'

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
⊢ (∀ (x y : ↥K'), ↑y ∈ K → ⁅↑x, ↑y⁆ ∈ K) ↔ ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K

Tactic:
constructor

Result:
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
⊢ (∀ (x y : ↥K'), ↑y ∈ K → ⁅↑x, ↑y⁆ ∈ K) → ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K

case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
⊢ (∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K) → ∀ (x y : ↥K'), ↑y ∈ K → ⁅↑x, ↑y⁆ ∈ K