harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Seq/WSeq.lean
theorem map_id (s : WSeq α) : map id s = s

Proof state:
α : Type u
s : WSeq α
⊢ map id s = s

Tactic:
simp [map]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_eq_single_of_mem {s : Finset α} {f : α → β} (a : α) (h : a ∈ s)
    (h₀ : ∀ b ∈ s, b ≠ a → f b = 1) : ∏ x ∈ s, f x = f a

Proof state:
case refine_1
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
h : a ∈ s
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
this : DecidableEq α
a✝ : α
H : a✝ ∈ {a}
⊢ a✝ ∈ s

Tactic:
rwa [mem_singleton.1 H]

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
h : a ∈ s
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
this : DecidableEq α
⊢ ∏ x ∈ s, f x = ∏ x ∈ {a}, f x

Tactic:
refine (prod_subset ?_ ?_).symm

Result:
case refine_1
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
h : a ∈ s
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
this : DecidableEq α
⊢ {a} ⊆ s

case refine_2
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
h : a ∈ s
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
this : DecidableEq α
⊢ ∀ x ∈ s, x ∉ {a} → f x = 1

Proof state:
case refine_1
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
h : a ∈ s
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
this : DecidableEq α
⊢ {a} ⊆ s

Tactic:
intro _ H

Result:
case refine_1
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
h : a ∈ s
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
this : DecidableEq α
a✝ : α
H : a✝ ∈ {a}
⊢ a✝ ∈ s

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
h : a ∈ s
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
⊢ ∏ x ∈ s, f x = f a

Tactic:
haveI := Classical.decEq α

Result:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
h : a ∈ s
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
this : DecidableEq α
⊢ ∏ x ∈ s, f x = f a

Proof state:
case refine_2
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
h : a ∈ s
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
this : DecidableEq α
⊢ ∀ x ∈ s, x ∉ {a} → f x = 1

Tactic:
simpa only [mem_singleton]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem add_eq_left {a b : Cardinal} (ha : ℵ₀ ≤ a) (hb : b ≤ a) : a + b = a

Proof state:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : b ≤ a
⊢ a + b = a

Tactic:
rw [add_eq_max ha, max_eq_left hb]

Result:
no goals
-- Mathlib/Algebra/Algebra/Tower.lean
theorem algebraMap_eq : algebraMap R A = (algebraMap S A).comp (algebraMap R S) :=
  RingHom.ext fun x => by
    simp_rw [RingHom.comp_apply, Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]

Proof state:
R : Type u
S : Type v
A : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
x : R
⊢ (algebraMap R A) x = ((algebraMap S A).comp (algebraMap R S)) x

Tactic:
simp_rw [RingHom.comp_apply, Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem cthickening_empty (δ : ℝ) : cthickening δ (∅ : Set α) = ∅

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
⊢ cthickening δ ∅ = ∅

Tactic:
simp only [cthickening, ENNReal.ofReal_ne_top, setOf_false, infEdist_empty, top_le_iff]

Result:
no goals
-- Mathlib/Data/Nat/Size.lean
theorem size_eq_zero {n : ℕ} : size n = 0 ↔ n = 0

Proof state:
n : ℕ
⊢ n.size = 0 ↔ n = 0

Tactic:
simpa [Nat.pos_iff_ne_zero, not_iff_not] using size_pos

Result:
no goals
-- Mathlib/Data/List/Lex.lean
theorem lt_iff_lex_lt [LinearOrder α] (l l' : List α) : List.lt l l' ↔ Lex (· < ·) l l'

Proof state:
α : Type u
inst✝ : LinearOrder α
l l' : List α
⊢ l.lt l' ↔ Lex (fun x1 x2 => x1 < x2) l l'

Tactic:
rw [List.lt]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean
theorem collinear_iff_eq_or_eq_or_sin_eq_zero {p₁ p₂ p₃ : P} :
    Collinear ℝ ({p₁, p₂, p₃} : Set P) ↔ p₁ = p₂ ∨ p₃ = p₂ ∨ Real.sin (∠ p₁ p₂ p₃) = 0

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
⊢ Collinear ℝ {p₁, p₂, p₃} ↔ p₁ = p₂ ∨ p₃ = p₂ ∨ sin (∠ p₁ p₂ p₃) = 0

Tactic:
rw [sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi,
  collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi]

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem inf_prod {f₁ f₂ : Filter α} : (f₁ ⊓ f₂) ×ˢ g = (f₁ ×ˢ g) ⊓ (f₂ ×ˢ g)

Proof state:
α : Type u_1
β : Type u_2
g : Filter β
f₁ f₂ : Filter α
⊢ (f₁ ⊓ f₂) ×ˢ g = f₁ ×ˢ g ⊓ f₂ ×ˢ g

Tactic:
rw [prod_inf_prod, inf_idem]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem getElem?_take_of_succ {l : List α} {n : Nat} : (l.take (n + 1))[n]? = l[n]?

Proof state:
α : Type u_1
l : List α
n : Nat
⊢ (take (n + 1) l)[n]? = l[n]?

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Order/IntermediateValue.lean
theorem IsPreconnected.intermediate_value₂_eventually₁ {s : Set X} (hs : IsPreconnected s) {a : X}
    {l : Filter X} (ha : a ∈ s) [NeBot l] (hl : l ≤ 𝓟 s) {f g : X → α} (hf : ContinuousOn f s)
    (hg : ContinuousOn g s) (ha' : f a ≤ g a) (he : g ≤ᶠ[l] f) : ∃ x ∈ s, f x = g x

Proof state:
X : Type u
α : Type v
inst✝⁴ : TopologicalSpace X
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a : X
l : Filter X
ha : a ∈ s
inst✝ : l.NeBot
hl : l ≤ 𝓟 s
f g : X → α
hf : ContinuousOn f s
hg : ContinuousOn g s
ha' : f a ≤ g a
he : g ≤ᶠ[l] f
⊢ ∃ x ∈ s, f x = g x

Tactic:
rw [continuousOn_iff_continuous_restrict] at hf hg

Result:
X : Type u
α : Type v
inst✝⁴ : TopologicalSpace X
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a : X
l : Filter X
ha : a ∈ s
inst✝ : l.NeBot
hl : l ≤ 𝓟 s
f g : X → α
hf : Continuous (s.restrict f)
hg : Continuous (s.restrict g)
ha' : f a ≤ g a
he : g ≤ᶠ[l] f
⊢ ∃ x ∈ s, f x = g x

Proof state:
case intro
X : Type u
α : Type v
inst✝⁴ : TopologicalSpace X
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a : X
l : Filter X
ha : a ∈ s
inst✝ : l.NeBot
hl : l ≤ 𝓟 s
f g : X → α
hf : Continuous (s.restrict f)
hg : Continuous (s.restrict g)
ha' : f a ≤ g a
he : g ≤ᶠ[l] f
b : ↑s
h : s.restrict f b = s.restrict g b
⊢ ∃ x ∈ s, f x = g x

Tactic:
exact ⟨b, b.prop, h⟩

Result:
no goals

Proof state:
X : Type u
α : Type v
inst✝⁴ : TopologicalSpace X
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a : X
l : Filter X
ha : a ∈ s
inst✝ : l.NeBot
hl : l ≤ 𝓟 s
f g : X → α
hf : Continuous (s.restrict f)
hg : Continuous (s.restrict g)
ha' : f a ≤ g a
he : g ≤ᶠ[l] f
⊢ ∃ x ∈ s, f x = g x

Tactic:
obtain ⟨b, h⟩ :=
  @intermediate_value_univ₂_eventually₁ _ _ _ _ _ _ (Subtype.preconnectedSpace hs) ⟨a, ha⟩ _
    (comap_coe_neBot_of_le_principal hl) _ _ hf hg ha' (he.comap _)

Result:
case intro
X : Type u
α : Type v
inst✝⁴ : TopologicalSpace X
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a : X
l : Filter X
ha : a ∈ s
inst✝ : l.NeBot
hl : l ≤ 𝓟 s
f g : X → α
hf : Continuous (s.restrict f)
hg : Continuous (s.restrict g)
ha' : f a ≤ g a
he : g ≤ᶠ[l] f
b : ↑s
h : s.restrict f b = s.restrict g b
⊢ ∃ x ∈ s, f x = g x
-- Mathlib/GroupTheory/Torsion.lean
theorem not_isTorsion_iff : ¬IsTorsion G ↔ ∃ g : G, ¬IsOfFinOrder g

Proof state:
G : Type u_1
inst✝ : Monoid G
⊢ ¬IsTorsion G ↔ ∃ g, ¬IsOfFinOrder g

Tactic:
rw [IsTorsion, not_forall]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_erase_le [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
    (m.erase k).size ≤ m.size

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k : α
⊢ (m.erase k).size ≤ m.size

Tactic:
simp_to_raw using Raw₀.size_erase_le

Result:
no goals
-- Mathlib/Order/Irreducible.lean
theorem supPrime_iff_not_isMin : SupPrime a ↔ ¬IsMin a :=
  and_iff_left <| by simp

Proof state:
α : Type u_2
inst✝ : LinearOrder α
a : α
⊢ ∀ ⦃b c : α⦄, a ≤ b ⊔ c → a ≤ b ∨ a ≤ c

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
theorem of_comp (hf : Continuous f) (hg : Continuous g)
    (hgf : IsQuotientMap (g ∘ f)) : IsQuotientMap g :=
  ⟨hgf.1.of_comp,
    le_antisymm
      (by rw [hgf.eq_coinduced, ← coinduced_compose]; exact coinduced_mono hf.coinduced_le)
      hg.coinduced_le⟩

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hf : Continuous f
hg : Continuous g
hgf : IsQuotientMap (g ∘ f)
⊢ inst✝ ≤ coinduced g inst✝¹

Tactic:
rw [hgf.eq_coinduced, ← coinduced_compose]

Result:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hf : Continuous f
hg : Continuous g
hgf : IsQuotientMap (g ∘ f)
⊢ coinduced g (coinduced f inst✝²) ≤ coinduced g inst✝¹

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hf : Continuous f
hg : Continuous g
hgf : IsQuotientMap (g ∘ f)
⊢ coinduced g (coinduced f inst✝²) ≤ coinduced g inst✝¹

Tactic:
exact coinduced_mono hf.coinduced_le

Result:
no goals
-- Mathlib/Topology/Order/LowerUpperTopology.lean
theorem tendsto_nhds_iff_lt {β : Type*} {f : β → α} {l : Filter β} {x : α} :
    Filter.Tendsto f l (𝓝 x) ↔ ∀ y, x < y → ∀ᶠ z in l, f z < y

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
β : Type u_3
f : β → α
l : Filter β
x : α
⊢ Filter.Tendsto f l (𝓝 x) ↔ ∀ (y : α), x < y → ∀ᶠ (z : β) in l, f z < y

Tactic:
simp only [tendsto_nhds_iff_not_le, not_le]

Result:
no goals
-- Mathlib/Data/Finset/Erase.lean
theorem eq_of_mem_of_not_mem_erase (hs : b ∈ s) (hsa : b ∉ s.erase a) : b = a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
hs : b ∈ s
hsa : b ≠ a → b ∉ s
⊢ b = a

Tactic:
exact not_imp_not.mp hsa hs

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
hs : b ∈ s
hsa : b ∉ s.erase a
⊢ b = a

Tactic:
rw [mem_erase, not_and] at hsa

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
hs : b ∈ s
hsa : b ≠ a → b ∉ s
⊢ b = a
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem map_toSubring : (p.toSubring T hp).map (Subring.subtype T) = p

Proof state:
case a
R : Type u
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
n : ℕ
⊢ (map T.subtype (p.toSubring T hp)).coeff n = p.coeff n

Tactic:
simp [coeff_map]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
⊢ map T.subtype (p.toSubring T hp) = p

Tactic:
ext n

Result:
case a
R : Type u
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
n : ℕ
⊢ (map T.subtype (p.toSubring T hp)).coeff n = p.coeff n
-- Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
protected lemma map_smul (x : R[X]) (y : W.CoordinateRing) :
    map W f (x • y) = x.map f • map W f y

Proof state:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
W : Affine R
f : R →+* S
x : R[X]
y : W.CoordinateRing
⊢ (map W f) (x • y) = Polynomial.map f x • (map W f) y

Tactic:
rw [smul, _root_.map_mul, map_mk, map_C, smul]

Result:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
W : Affine R
f : R →+* S
x : R[X]
y : W.CoordinateRing
⊢ (mk (WeierstrassCurve.map W f)) (C ((mapRingHom f) x)) * (map W f) y =
    (mk (WeierstrassCurve.map W f).toAffine) (C (Polynomial.map f x)) * (map W f) y

Proof state:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
W : Affine R
f : R →+* S
x : R[X]
y : W.CoordinateRing
⊢ (mk (WeierstrassCurve.map W f)) (C ((mapRingHom f) x)) * (map W f) y =
    (mk (WeierstrassCurve.map W f).toAffine) (C (Polynomial.map f x)) * (map W f) y

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Nat/Prime/Int.lean
/-- Two prime powers with positive exponents are equal only when the primes and the
exponents are equal. -/
lemma Prime.pow_inj {p q m n : ℕ} (hp : p.Prime) (hq : q.Prime)
    (h : p ^ (m + 1) = q ^ (n + 1)) : p = q ∧ m = n

Proof state:
p q m n : ℕ
hp : Prime p
hq : Prime q
h : p ^ (m + 1) = q ^ (n + 1)
H : p = q
⊢ p = q ∧ m = n

Tactic:
exact ⟨H, succ_inj'.mp <| Nat.pow_right_injective hq.two_le (H ▸ h)⟩

Result:
no goals

Proof state:
p q m n : ℕ
hp : Prime p
hq : Prime q
h : p ^ (m + 1) = q ^ (n + 1)
⊢ p = q ∧ m = n

Tactic:
have H := dvd_antisymm (Prime.dvd_of_dvd_pow hp <| h ▸ dvd_pow_self p (succ_ne_zero m))
  (Prime.dvd_of_dvd_pow hq <| h.symm ▸ dvd_pow_self q (succ_ne_zero n))

Result:
p q m n : ℕ
hp : Prime p
hq : Prime q
h : p ^ (m + 1) = q ^ (n + 1)
H : p = q
⊢ p = q ∧ m = n
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma baseChange_polynomialX : (W'.baseChange B).toJacobian.polynomialX =
    MvPolynomial.map f (W'.baseChange A).toJacobian.polynomialX

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Jacobian R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (baseChange W' B).toJacobian.polynomialX = (MvPolynomial.map ↑f) (baseChange W' A).toJacobian.polynomialX

Tactic:
rw [← map_polynomialX, map_baseChange]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem norm_fderiv_iteratedFDeriv {n : ℕ} :
    ‖fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x‖ = ‖iteratedFDeriv 𝕜 (n + 1) f x‖

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ
⊢ ‖fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x‖ = ‖iteratedFDeriv 𝕜 (n + 1) f x‖

Tactic:
rw [iteratedFDeriv_succ_eq_comp_left, comp_apply, LinearIsometryEquiv.norm_map]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem infsep_pos : 0 < s.infsep ↔ 0 < s.einfsep ∧ s.einfsep < ∞

Proof state:
α : Type u_1
inst✝ : EDist α
s : Set α
⊢ 0 < s.infsep ↔ 0 < s.einfsep ∧ s.einfsep < ⊤

Tactic:
simp_rw [infsep, ENNReal.toReal_pos_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem associator_naturality_right (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h') :
    (f ≫ g) ◁ η ≫ (α_ f g h').hom = (α_ f g h).hom ≫ f ◁ g ◁ η

Proof state:
B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g : b ⟶ c
h h' : c ⟶ d
η : h ⟶ h'
⊢ (f ≫ g) ◁ η ≫ (α_ f g h').hom = (α_ f g h).hom ≫ f ◁ g ◁ η

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma negDblY_smul (P : Fin 3 → R) (u : R) : W'.negDblY (u • P) = (u ^ 4) ^ 3 * W'.negDblY P

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ W'.negDblY (u • P) = (u ^ 4) ^ 3 * W'.negDblY P

Tactic:
simp only [negDblY, dblU_smul, dblX_smul, negY_smul, smul_fin3_ext]

Result:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ -(u ^ 4 * W'.dblU P) * ((u ^ 4) ^ 2 * W'.dblX P - u ^ 2 * P x * (u ^ 3 * P y - u ^ 3 * W'.negY P) ^ 2) +
      u ^ 3 * P y * (u ^ 3 * P y - u ^ 3 * W'.negY P) ^ 3 =
    (u ^ 4) ^ 3 * (-W'.dblU P * (W'.dblX P - P x * (P y - W'.negY P) ^ 2) + P y * (P y - W'.negY P) ^ 3)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ -(u ^ 4 * W'.dblU P) * ((u ^ 4) ^ 2 * W'.dblX P - u ^ 2 * P x * (u ^ 3 * P y - u ^ 3 * W'.negY P) ^ 2) +
      u ^ 3 * P y * (u ^ 3 * P y - u ^ 3 * W'.negY P) ^ 3 =
    (u ^ 4) ^ 3 * (-W'.dblU P * (W'.dblX P - P x * (P y - W'.negY P) ^ 2) + P y * (P y - W'.negY P) ^ 3)

Tactic:
ring1

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
lemma connected_iff_forall_exists_walk_subgraph (H : G.Subgraph) :
    H.Connected ↔
      H.verts.Nonempty ∧
        ∀ {u v}, u ∈ H.verts → v ∈ H.verts → ∃ p : G.Walk u v, p.toSubgraph ≤ H

Proof state:
V : Type u
G : SimpleGraph V
H : G.Subgraph
⊢ H.Connected ↔ H.verts.Nonempty ∧ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, p.toSubgraph ≤ H

Tactic:
rw [H.connected_iff, preconnected_iff_forall_exists_walk_subgraph, and_comm]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
theorem mul_self_div_self (a : G₀) : a * a / a = a

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a * a / a = a

Tactic:
rw [div_eq_mul_inv, mul_self_mul_inv a]

Result:
no goals
-- Mathlib/Data/Fintype/Sets.lean
theorem toFinset_image [DecidableEq β] (f : α → β) (s : Set α) [Fintype s] [Fintype (f '' s)] :
    (f '' s).toFinset = s.toFinset.image f :=
  Finset.coe_injective <| by simp

Proof state:
α : Type u_1
β : Type u_2
inst✝² : DecidableEq β
f : α → β
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑(f '' s)
⊢ ↑(f '' s).toFinset = ↑(Finset.image f s.toFinset)

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem zero_equiv_neg_iff {x : PGame} : (0 ≈ -x) ↔ (0 ≈ x)

Proof state:
x : PGame
⊢ 0 ≈ -x ↔ 0 ≈ x

Tactic:
rw [← neg_equiv_iff, neg_zero]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem S_eq (n : ℤ) : S R n = X * S R (n - 1) - S R (n - 2)

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ S R n = X * S R (n - 1) - S R (n - 2)

Tactic:
linear_combination (norm := ring_nf) S_add_two R (n - 2)

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem HasDerivWithinAt.finset_prod (hf : ∀ i ∈ u, HasDerivWithinAt (f i) (f' i) s x) :
    HasDerivWithinAt (∏ i ∈ u, f i ·) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) s x

Proof state:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_2
inst✝² : DecidableEq ι
𝔸' : Type u_3
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
f' : ι → 𝔸'
hf : ∀ i ∈ u, HasDerivWithinAt (f i) (f' i) s x
⊢ HasDerivWithinAt (fun x => ∏ i ∈ u, f i x) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) s x

Tactic:
simpa [ContinuousLinearMap.sum_apply, ContinuousLinearMap.smul_apply] using
  (HasFDerivWithinAt.finset_prod (fun i hi ↦ (hf i hi).hasFDerivWithinAt)).hasDerivWithinAt

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Veblen.lean
theorem veblen_zero_strictMono : StrictMono (veblen · 0) :=
  veblenWith_zero_strictMono (isNormal_opow one_lt_omega0) (by simp)

Proof state:
⊢ 0 < ω ^ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem aroots_X_sub_C [CommRing S] [IsDomain S] [Algebra T S]
    (r : T) : aroots (X - C r) S = {algebraMap T S r}

Proof state:
S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
r : T
⊢ (X - C r).aroots S = {(algebraMap T S) r}

Tactic:
rw [aroots_def, Polynomial.map_sub, map_X, map_C, roots_X_sub_C]

Result:
no goals
-- Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
theorem exists_irreducible : ∃ ϖ : R, Irreducible ϖ

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
⊢ ∃ ϖ, maximalIdeal R = span {ϖ}

Tactic:
exact (IsPrincipalIdealRing.principal <| maximalIdeal R).principal

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
⊢ ∃ ϖ, Irreducible ϖ

Tactic:
simp_rw [irreducible_iff_uniformizer]

Result:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
⊢ ∃ ϖ, maximalIdeal R = span {ϖ}
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem c₆_of_isShortNF : W.c₆ = -864 * W.a₆

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsShortNF
⊢ W.c₆ = -864 * W.a₆

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Mod.lean
theorem mod_mul {a b x : Nat} : x % (a * b) = x % a + a * (x / a % b)

Proof state:
a b x : Nat
⊢ x % (a * b) = x % a + a * (x / a % b)

Tactic:
rw [Nat.add_comm, ← Nat.div_add_mod (x % (a*b)) a, Nat.mod_mul_right_mod,
  Nat.mod_mul_right_div_self]

Result:
no goals
-- Mathlib/Analysis/PSeries.lean
theorem summable_one_div_nat_pow {p : ℕ} :
    Summable (fun n => 1 / (n : ℝ) ^ p : ℕ → ℝ) ↔ 1 < p

Proof state:
p : ℕ
⊢ (Summable fun n => 1 / ↑n ^ p) ↔ 1 < p

Tactic:
simp only [one_div, Real.summable_nat_pow_inv]

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem and_symm_right {α : Sort*} (a b : α) (p : Prop) : p ∧ a = b ↔ p ∧ b = a

Proof state:
α : Sort u_1
a b : α
p : Prop
⊢ p ∧ a = b ↔ p ∧ b = a

Tactic:
simp [eq_comm]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
theorem IsUniformInducing.cauchy_map_iff {f : α → β} (hf : IsUniformInducing f) {F : Filter α} :
    Cauchy (map f F) ↔ Cauchy F

Proof state:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
hf : IsUniformInducing f
F : Filter α
⊢ Cauchy (map f F) ↔ Cauchy F

Tactic:
simp only [Cauchy, map_neBot_iff, prod_map_map_eq, map_le_iff_le_comap, ← hf.comap_uniformity]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem max?_mem {t : RBNode α} (h : t.max? = some a) : a ∈ t

Proof state:
α : Type u_1
a : α
t : RBNode α
h : t.max? = some a
⊢ a ∈ t

Tactic:
simpa using min?_mem ((min?_reverse _).trans h)

Result:
no goals
-- Mathlib/Topology/Algebra/GroupWithZero.lean
theorem Continuous.div₀ (hf : Continuous f) (hg : Continuous g) (h₀ : ∀ x, g x ≠ 0) :
    Continuous (fun x => f x / g x)

Proof state:
α : Type u_1
G₀ : Type u_3
inst✝⁴ : GroupWithZero G₀
inst✝³ : TopologicalSpace G₀
inst✝² : HasContinuousInv₀ G₀
inst✝¹ : ContinuousMul G₀
f g : α → G₀
inst✝ : TopologicalSpace α
hf : Continuous f
hg : Continuous g
h₀ : ∀ (x : α), g x ≠ 0
⊢ Continuous fun x => f x / g x

Tactic:
simpa only [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Basic.lean
theorem seqLeft_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x <* y = x >>= fun a => y >>= fun _ => pure a

Proof state:
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
y : m β
⊢ const β <$> x <*> y = do
    let a ← x
    let _ ← y
    pure a

Tactic:
simp only [map_eq_pure_bind, seq_eq_bind_map, bind_assoc, pure_bind, const_apply]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
y : m β
⊢ x <* y = do
    let a ← x
    let _ ← y
    pure a

Tactic:
rw [seqLeft_eq]

Result:
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
y : m β
⊢ const β <$> x <*> y = do
    let a ← x
    let _ ← y
    pure a
-- Mathlib/Algebra/Polynomial/Eval/Coeff.lean
theorem eval₂_map [Semiring T] (g : S →+* T) (x : T) :
    (p.map f).eval₂ g x = p.eval₂ (g.comp f) x

Proof state:
R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
p : R[X]
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Semiring T
g : S →+* T
x : T
⊢ eval₂ g x (map f p) = eval₂ (g.comp f) x p

Tactic:
rw [eval₂_eq_eval_map, eval₂_eq_eval_map, map_map]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem monic_of_degree_le (n : ℕ) (H1 : degree p ≤ n) (H2 : coeff p n = 1) : Monic p :=
  Decidable.byCases
    (fun H : degree p < n => eq_of_zero_eq_one (H2 ▸ (coeff_eq_zero_of_degree_lt H).symm) _ _)
    fun H : ¬degree p < n => by
    rwa [Monic, Polynomial.leadingCoeff, natDegree, (lt_or_eq_of_le H1).resolve_left H]

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
H1 : p.degree ≤ ↑n
H2 : p.coeff n = 1
H : ¬p.degree < ↑n
⊢ p.Monic

Tactic:
rwa [Monic, Polynomial.leadingCoeff, natDegree, (lt_or_eq_of_le H1).resolve_left H]

Result:
no goals