harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Real/ConjExponents.lean
@[symm]
protected lemma symm : q.IsConjExponent p where
  one_lt

Proof state:
p q : ℝ≥0
h : p.IsConjExponent q
⊢ q⁻¹ + p⁻¹ = 1

Tactic:
simpa [add_comm] using h.inv_add_inv_conj

Result:
no goals

Proof state:
p q : ℝ≥0
h : p.IsConjExponent q
⊢ 1 < q

Tactic:
rw [h.conj_eq]

Result:
p q : ℝ≥0
h : p.IsConjExponent q
⊢ 1 < p / (p - 1)

Proof state:
p q : ℝ≥0
h : p.IsConjExponent q
⊢ 1 < p / (p - 1)

Tactic:
exact (one_lt_div h.sub_one_pos).mpr (tsub_lt_self h.pos zero_lt_one)

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma le_mul_self : ∀ n : ℕ, n ≤ n * n
  | 0 => Nat.le_refl _
  | n + 1 => by simp [Nat.mul_add]

Proof state:
n : ℕ
⊢ n + 1 ≤ (n + 1) * (n + 1)

Tactic:
simp [Nat.mul_add]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem finite_int_prime_iff {a : ℤ} : FiniteMultiplicity (p : ℤ) a ↔ a ≠ 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
⊢ FiniteMultiplicity (↑p) a ↔ a ≠ 0

Tactic:
simp [Int.finiteMultiplicity_iff, hp.1.ne_one]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean
theorem H1Map_comp {G H K : Type u} [Group G] [Group H] [Group K]
    {A : Rep k K} {B : Rep k H} {C : Rep k G} (f : H →* K) (g : G →* H)
    (φ : (Action.res _ f).obj A ⟶ B) (ψ : (Action.res _ g).obj B ⟶ C) :
    H1Map (f.comp g) ((Action.res _ g).map φ ≫ ψ) = H1Map f φ ≫ H1Map g ψ

Proof state:
k : Type u
inst✝³ : CommRing k
G H K : Type u
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group K
A : Rep k K
B : Rep k H
C : Rep k G
f : H →* K
g : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
ψ : (Action.res (ModuleCat k) g).obj B ⟶ C
⊢ H1Map (f.comp g) ((Action.res (ModuleCat k) g).map φ ≫ ψ) = H1Map f φ ≫ H1Map g ψ

Tactic:
simpa [H1Map, shortComplexH1, mapShortComplexH1_comp] using leftHomologyMap'_comp ..

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem xor_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
    (lhs' ^^ rhs') = (lhs ^^ rhs)

Proof state:
lhs rhs lhs' rhs' : Bool
h1 : lhs' = lhs
h2 : rhs' = rhs
⊢ (lhs' ^^ rhs') = (lhs ^^ rhs)

Tactic:
simp[*]

Result:
no goals
-- Mathlib/CategoryTheory/FiberedCategory/HomLift.lean
lemma eq_of_isHomLift {a b : 𝒳} (f : p.obj a ⟶ p.obj b) (φ : a ⟶ b) [p.IsHomLift f φ] :
    f = p.map φ

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

Tactic:
simp only [fac p f φ, eqToHom_refl, comp_id, id_comp]

Result:
no goals
-- Mathlib/Algebra/EuclideanDomain/Basic.lean
theorem mul_div_cancel' {a b : R} (hb : b ≠ 0) (hab : b ∣ a) : b * (a / b) = a

Proof state:
R : Type u
inst✝ : EuclideanDomain R
a b : R
hb : b ≠ 0
hab : b ∣ a
⊢ b * (a / b) = a

Tactic:
rw [← mul_div_assoc _ hab, mul_div_cancel_left₀ _ hb]

Result:
no goals
-- Mathlib/Algebra/Group/Fin/Tuple.lean
@[simp] lemma smul_cons (x : M) (y : α) (v : Fin n → α) :
    x • vecCons y v = vecCons (x • y) (x • v)

Proof state:
case h
α : Type u_1
M : Type u_2
n : ℕ
inst✝ : SMul M α
x : M
y : α
v : Fin n → α
i : Fin n.succ
⊢ (x • vecCons y v) i = vecCons (x • y) (x • v) i

Tactic:
refine i.cases ?_ ?_ <;> simp

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
n : ℕ
inst✝ : SMul M α
x : M
y : α
v : Fin n → α
⊢ x • vecCons y v = vecCons (x • y) (x • v)

Tactic:
ext i

Result:
case h
α : Type u_1
M : Type u_2
n : ℕ
inst✝ : SMul M α
x : M
y : α
v : Fin n → α
i : Fin n.succ
⊢ (x • vecCons y v) i = vecCons (x • y) (x • v) i
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_mono_interval {c d} (hca : c ≤ a) (hab : a ≤ b) (hbd : b ≤ d)
    (hf : 0 ≤ᵐ[μ.restrict (Ioc c d)] f) (hfi : IntervalIntegrable f μ c d) :
    (∫ x in a..b, f x ∂μ) ≤ ∫ x in c..d, f x ∂μ

Proof state:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
c d : ℝ
hca : c ≤ a
hab : a ≤ b
hbd : b ≤ d
hf : 0 ≤ᶠ[ae (μ.restrict (Ioc c d))] f
hfi : IntervalIntegrable f μ c d
⊢ ∫ (x : ℝ) in a..b, f x ∂μ ≤ ∫ (x : ℝ) in c..d, f x ∂μ

Tactic:
rw [integral_of_le hab, integral_of_le (hca.trans (hab.trans hbd))]

Result:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
c d : ℝ
hca : c ≤ a
hab : a ≤ b
hbd : b ≤ d
hf : 0 ≤ᶠ[ae (μ.restrict (Ioc c d))] f
hfi : IntervalIntegrable f μ c d
⊢ ∫ (x : ℝ) in Ioc a b, f x ∂μ ≤ ∫ (x : ℝ) in Ioc c d, f x ∂μ

Proof state:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
c d : ℝ
hca : c ≤ a
hab : a ≤ b
hbd : b ≤ d
hf : 0 ≤ᶠ[ae (μ.restrict (Ioc c d))] f
hfi : IntervalIntegrable f μ c d
⊢ ∫ (x : ℝ) in Ioc a b, f x ∂μ ≤ ∫ (x : ℝ) in Ioc c d, f x ∂μ

Tactic:
exact setIntegral_mono_set hfi.1 hf (Ioc_subset_Ioc hca hbd).eventuallyLE

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem reverse_setRed {t : RBNode α} : (setRed t).reverse = setRed t.reverse

Proof state:
α : Type u_1
t : RBNode α
⊢ (match t with
      | node c a v b => node red a v b
      | nil => nil).reverse =
    match t.reverse with
    | node c a v b => node red a v b
    | nil => nil

Tactic:
split <;> simp

Result:
no goals

Proof state:
α : Type u_1
t : RBNode α
⊢ t.setRed.reverse = t.reverse.setRed

Tactic:
unfold setRed

Result:
α : Type u_1
t : RBNode α
⊢ (match t with
      | node c a v b => node red a v b
      | nil => nil).reverse =
    match t.reverse with
    | node c a v b => node red a v b
    | nil => nil
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem rank_span_finset_le (s : Finset M) : Module.rank R (span R (s : Set M)) ≤ s.card

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
s : Finset M
⊢ Module.rank R ↥(span R ↑s) ≤ ↑s.card

Tactic:
simpa using rank_span_le s.toSet

Result:
no goals
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem EqOnSource.target_eq {e e' : PartialEquiv α β} (h : e ≈ e') : e.target = e'.target

Proof state:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
⊢ e.target = e'.target

Tactic:
simp only [← image_source_eq_target, ← source_eq h, h.2.image_eq]

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem coprime_add_mul_left_right (m n k : ℕ) : Coprime m (n + m * k) ↔ Coprime m n

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

Tactic:
rw [Coprime, Coprime, gcd_add_mul_left_right]

Result:
no goals
-- Mathlib/Topology/Order.lean
@[simp]
lemma generateFrom_insert_empty {α : Type*} {s : Set (Set α)} :
    generateFrom (insert ∅ s) = generateFrom s

Proof state:
α : Type u_1
s : Set (Set α)
⊢ generateFrom (insert ∅ s) = generateFrom s

Tactic:
rw [← sUnion_empty]

Result:
α : Type u_1
s : Set (Set α)
⊢ generateFrom (insert (⋃₀ ∅) s) = generateFrom s

Proof state:
α : Type u_1
s : Set (Set α)
⊢ generateFrom (insert (⋃₀ ∅) s) = generateFrom s

Tactic:
exact generateFrom_insert_of_generateOpen (.sUnion ∅ (fun s_1 a ↦ False.elim a))

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
theorem mk0_one (h := one_ne_zero) : mk0 (1 : G₀) h = 1

Proof state:
case a
G₀ : Type u_3
inst✝ : GroupWithZero G₀
h : optParam (1 ≠ 0) ⋯
⊢ ↑(mk0 1 h) = ↑1

Tactic:
rfl

Result:
no goals

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
h : optParam (1 ≠ 0) ⋯
⊢ mk0 1 h = 1

Tactic:
ext

Result:
case a
G₀ : Type u_3
inst✝ : GroupWithZero G₀
h : optParam (1 ≠ 0) ⋯
⊢ ↑(mk0 1 h) = ↑1
-- Mathlib/MeasureTheory/PiSystem.lean
theorem IsPiSystem.comap {α β} {S : Set (Set β)} (h_pi : IsPiSystem S) (f : α → β) :
    IsPiSystem { s : Set α | ∃ t ∈ S, f ⁻¹' t = s }

Proof state:
α : Type u_3
β : Type u_4
S : Set (Set β)
h_pi : IsPiSystem S
f : α → β
⊢ IsPiSystem {s | ∃ t ∈ S, f ⁻¹' t = s}

Tactic:
rintro _ ⟨s, hs_mem, rfl⟩ _ ⟨t, ht_mem, rfl⟩ hst

Result:
case intro.intro.intro.intro
α : Type u_3
β : Type u_4
S : Set (Set β)
h_pi : IsPiSystem S
f : α → β
s : Set β
hs_mem : s ∈ S
t : Set β
ht_mem : t ∈ S
hst : (f ⁻¹' s ∩ f ⁻¹' t).Nonempty
⊢ f ⁻¹' s ∩ f ⁻¹' t ∈ {s | ∃ t ∈ S, f ⁻¹' t = s}

Proof state:
case intro.intro.intro.intro
α : Type u_3
β : Type u_4
S : Set (Set β)
h_pi : IsPiSystem S
f : α → β
s : Set β
hs_mem : s ∈ S
t : Set β
ht_mem : t ∈ S
hst : (f ⁻¹' s ∩ f ⁻¹' t).Nonempty
⊢ f ⁻¹' s ∩ f ⁻¹' t ∈ {s | ∃ t ∈ S, f ⁻¹' t = s}

Tactic:
rw [← Set.preimage_inter] at hst ⊢

Result:
case intro.intro.intro.intro
α : Type u_3
β : Type u_4
S : Set (Set β)
h_pi : IsPiSystem S
f : α → β
s : Set β
hs_mem : s ∈ S
t : Set β
ht_mem : t ∈ S
hst : (f ⁻¹' (s ∩ t)).Nonempty
⊢ f ⁻¹' (s ∩ t) ∈ {s | ∃ t ∈ S, f ⁻¹' t = s}

Proof state:
case intro.intro.intro.intro
α : Type u_3
β : Type u_4
S : Set (Set β)
h_pi : IsPiSystem S
f : α → β
s : Set β
hs_mem : s ∈ S
t : Set β
ht_mem : t ∈ S
hst : (f ⁻¹' (s ∩ t)).Nonempty
⊢ f ⁻¹' (s ∩ t) ∈ {s | ∃ t ∈ S, f ⁻¹' t = s}

Tactic:
exact ⟨s ∩ t, h_pi s hs_mem t ht_mem (nonempty_of_nonempty_preimage hst), rfl⟩

Result:
no goals
-- Mathlib/Data/Sign.lean
theorem neg_one_lt_iff {a : SignType} : -1 < a ↔ 0 ≤ a

Proof state:
a : SignType
⊢ -1 < a ↔ 0 ≤ a

Tactic:
cases a <;> decide

Result:
no goals
-- Mathlib/Analysis/Complex/ReImTopology.lean
theorem closure_setOf_lt_re (a : ℝ) : closure { z : ℂ | a < z.re } = { z | a ≤ z.re }

Proof state:
a : ℝ
⊢ closure {z | a < z.re} = {z | a ≤ z.re}

Tactic:
simpa only [closure_Ioi] using closure_preimage_re (Ioi a)

Result:
no goals
-- Mathlib/RingTheory/Flat/EquationalCriterion.lean
theorem sum_smul_eq_zero_of_isTrivialRelation (h : IsTrivialRelation f x) :
    ∑ i, f i • x i = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
f : ι → R
x : ι → M
h : IsTrivialRelation f x
⊢ ∑ i : ι, f i • x i = 0

Tactic:
simpa using
  congr_arg (TensorProduct.lid R M) <|
    sum_tmul_eq_zero_of_vanishesTrivially R (isTrivialRelation_iff_vanishesTrivially.mp h)

Result:
no goals
-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean
theorem constant_on {f : α → E} {s : Set α} (hf : (f '' s).Subsingleton) :
    eVariationOn f s = 0

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : (f '' s).Subsingleton
x : α
xs : x ∈ s
y : α
ys : y ∈ s
⊢ edist (f x) (f y) = 0

Tactic:
rw [hf ⟨x, xs, rfl⟩ ⟨y, ys, rfl⟩, edist_self]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : (f '' s).Subsingleton
⊢ eVariationOn f s = 0

Tactic:
rw [eq_zero_iff]

Result:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : (f '' s).Subsingleton
⊢ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : (f '' s).Subsingleton
⊢ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0

Tactic:
rintro x xs y ys

Result:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : (f '' s).Subsingleton
x : α
xs : x ∈ s
y : α
ys : y ∈ s
⊢ edist (f x) (f y) = 0
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem get?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
    get? (m.insertIfNew k v) a = if k == a ∧ ¬k ∈ m then some v else get? m a

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k a : α
v : β
⊢ get? (m.insertIfNew k v) a = if (k == a) = true ∧ ¬k ∈ m then some v else get? m a

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true]

Result:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k a : α
v : β
⊢ get? (m.insertIfNew k v) a = if (k == a) = true ∧ m.contains k = false then some v else get? m a

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k a : α
v : β
⊢ get? (m.insertIfNew k v) a = if (k == a) = true ∧ m.contains k = false then some v else get? m a

Tactic:
exact Raw₀.Const.get?_insertIfNew ⟨m.1, _⟩ m.2

Result:
no goals
-- Mathlib/Analysis/Complex/ReImTopology.lean
protected lemma TendstoUniformlyOn.im {f : ι → α → ℂ} {p : Filter ι} {g : α → ℂ} {K : Set α}
    (hf : TendstoUniformlyOn f g p K) :
    TendstoUniformlyOn (fun n x => (f n x).im) (fun y => (g y).im) p K

Proof state:
α : Type u_1
ι : Type u_2
f : ι → α → ℂ
p : Filter ι
g : α → ℂ
K : Set α
hf : TendstoUniformlyOn f g p K
⊢ TendstoUniformlyOn (fun n x => (f n x).im) (fun y => (g y).im) p K

Tactic:
apply UniformContinuous.comp_tendstoUniformlyOn uniformlyContinuous_im hf

Result:
no goals
-- Mathlib/Tactic/PNatToNat.lean
@[pnat_to_nat_coe]
lemma coe_le_coe (m n : PNat) : m ≤ n ↔ (m : ℕ) ≤ (n : ℕ)

Proof state:
m n : ℕ+
⊢ m ≤ n ↔ ↑m ≤ ↑n

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/UnitTrinomial.lean
theorem card_support_eq_three (hp : p.IsUnitTrinomial) : #p.support = 3

Proof state:
p : ℤ[X]
hp : p.IsUnitTrinomial
⊢ #p.support = 3

Tactic:
obtain ⟨k, m, n, hkm, hmn, u, v, w, rfl⟩ := hp

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ #(trinomial k m n ↑u ↑v ↑w).support = 3

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ #(trinomial k m n ↑u ↑v ↑w).support = 3

Tactic:
exact card_support_trinomial hkm hmn u.ne_zero v.ne_zero w.ne_zero

Result:
no goals
-- Mathlib/Data/Finset/Union.lean
lemma biUnion_subset {s' : Finset β} : s.biUnion t ⊆ s' ↔ ∀ x ∈ s, t x ⊆ s'

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst✝ : DecidableEq β
s' : Finset β
⊢ s.biUnion t ⊆ s' ↔ ∀ x ∈ s, t x ⊆ s'

Tactic:
simp only [subset_iff, mem_biUnion]

Result:
α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst✝ : DecidableEq β
s' : Finset β
⊢ (∀ ⦃x : β⦄, (∃ a ∈ s, x ∈ t a) → x ∈ s') ↔ ∀ x ∈ s, ∀ ⦃x_1 : β⦄, x_1 ∈ t x → x_1 ∈ s'

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst✝ : DecidableEq β
s' : Finset β
⊢ (∀ ⦃x : β⦄, (∃ a ∈ s, x ∈ t a) → x ∈ s') ↔ ∀ x ∈ s, ∀ ⦃x_1 : β⦄, x_1 ∈ t x → x_1 ∈ s'

Tactic:
exact ⟨fun H a ha b hb ↦ H ⟨a, ha, hb⟩, fun H b ⟨a, ha, hb⟩ ↦ H a ha hb⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem natAbs_mul (a b : Int) : natAbs (a * b) = natAbs a * natAbs b

Proof state:
a b : Int
⊢ (a * b).natAbs = a.natAbs * b.natAbs

Tactic:
cases a <;> cases b <;>
  simp only [← Int.mul_def, Int.mul, natAbs_negOfNat] <;> simp only [natAbs]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma b₈_of_char_two :
    W.b₈ = W.a₁ ^ 2 * W.a₆ + W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 + W.a₄ ^ 2

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ W.b₈ = W.a₁ ^ 2 * W.a₆ + W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 + W.a₄ ^ 2

Tactic:
rw [b₈]

Result:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ W.a₁ ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2 =
    W.a₁ ^ 2 * W.a₆ + W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 + W.a₄ ^ 2

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ W.a₁ ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2 =
    W.a₁ ^ 2 * W.a₆ + W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 + W.a₄ ^ 2

Tactic:
linear_combination (2 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ - W.a₄ ^ 2) * CharP.cast_eq_zero R 2

Result:
no goals
-- Mathlib/Algebra/Order/AddGroupWithTop.lean
@[simp]
lemma sub_eq_top_iff {a b : WithTop α} : a - b = ⊤ ↔ (a = ⊤ ∨ b = ⊤)

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b : WithTop α
⊢ a - b = ⊤ ↔ a = ⊤ ∨ b = ⊤

Tactic:
cases a <;> cases b <;> simp [← coe_sub]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean
/-- The zero locus of a set of sections over a compact open of a scheme is `X` if and only if
`s` is contained in the nilradical of `Γ(X, U)`. -/
lemma Scheme.zeroLocus_eq_top_iff_subset_nilradical_of_isCompact {X : Scheme.{u}} {U : X.Opens}
    (hU : IsCompact (U : Set X)) (s : Set Γ(X, U)) :
    X.zeroLocus s = ⊤ ↔ s ⊆ nilradical Γ(X, U)

Proof state:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
s : Set ↑Γ(X, U)
⊢ X.zeroLocus s = ⊤ ↔ s ⊆ ↑(nilradical ↑Γ(X, U))

Tactic:
simp [Scheme.zeroLocus_def, ← Scheme.isNilpotent_iff_basicOpen_eq_bot_of_isCompact hU,
  ← mem_nilradical, Set.subset_def]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma negDblY_of_Y_eq' [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hQz : Q z ≠ 0)
    (hx : P x * Q z = Q x * P z) (hy : P y * Q z = Q y * P z) (hy' : P y * Q z = W'.negY Q * P z) :
    W'.negDblY P * P z ^ 2 = -eval P W'.polynomialX ^ 3

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ -(eval P) W'.polynomialX *
        ((eval P) W'.polynomialX ^ 2 - W'.a₁ * (eval P) W'.polynomialX * P z * (W'.negY P - W'.negY P) -
              W'.a₂ * P z ^ 2 * (W'.negY P - W'.negY P) ^ 2 -
            2 * P x * P z * (W'.negY P - W'.negY P) ^ 2 -
          P x * P z * (W'.negY P - W'.negY P) ^ 2) +
      W'.negY P * P z ^ 2 * (W'.negY P - W'.negY P) ^ 3 =
    -(eval P) W'.polynomialX ^ 3

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ W'.negDblY P * P z ^ 2 = -(eval P) W'.polynomialX ^ 3

Tactic:
rw [negDblY_eq' hP, Y_eq_negY_of_Y_eq hQz hx hy hy']

Result:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ -(eval P) W'.polynomialX *
        ((eval P) W'.polynomialX ^ 2 - W'.a₁ * (eval P) W'.polynomialX * P z * (W'.negY P - W'.negY P) -
              W'.a₂ * P z ^ 2 * (W'.negY P - W'.negY P) ^ 2 -
            2 * P x * P z * (W'.negY P - W'.negY P) ^ 2 -
          P x * P z * (W'.negY P - W'.negY P) ^ 2) +
      W'.negY P * P z ^ 2 * (W'.negY P - W'.negY P) ^ 3 =
    -(eval P) W'.polynomialX ^ 3
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem add_sub_of_le {a b : Nat} (h : a ≤ b) : a + (b - a) = b

Proof state:
a b : Nat
h : a ≤ b
⊢ a + (b - a) = b

Tactic:
induction a with
| zero => simp
| succ a ih =>
  have hne : b - a ≠ 0 := Nat.sub_ne_zero_of_lt h
  have : a ≤ b := Nat.le_of_succ_le h
  rw [sub_succ, Nat.succ_add, ← Nat.add_succ, Nat.succ_pred hne, ih this]

Result:
no goals

Proof state:
case zero
b : Nat
h : 0 ≤ b
⊢ 0 + (b - 0) = b

Tactic:
simp

Result:
no goals

Proof state:
case succ
b a : Nat
ih : a ≤ b → a + (b - a) = b
h : a + 1 ≤ b
hne : b - a ≠ 0
⊢ a + 1 + (b - (a + 1)) = b

Tactic:
have : a ≤ b := Nat.le_of_succ_le h

Result:
case succ
b a : Nat
ih : a ≤ b → a + (b - a) = b
h : a + 1 ≤ b
hne : b - a ≠ 0
this : a ≤ b
⊢ a + 1 + (b - (a + 1)) = b

Proof state:
case succ
b a : Nat
ih : a ≤ b → a + (b - a) = b
h : a + 1 ≤ b
⊢ a + 1 + (b - (a + 1)) = b

Tactic:
have hne : b - a ≠ 0 := Nat.sub_ne_zero_of_lt h

Result:
case succ
b a : Nat
ih : a ≤ b → a + (b - a) = b
h : a + 1 ≤ b
hne : b - a ≠ 0
⊢ a + 1 + (b - (a + 1)) = b

Proof state:
case succ
b a : Nat
ih : a ≤ b → a + (b - a) = b
h : a + 1 ≤ b
hne : b - a ≠ 0
this : a ≤ b
⊢ a + 1 + (b - (a + 1)) = b

Tactic:
rw [sub_succ, Nat.succ_add, ← Nat.add_succ, Nat.succ_pred hne, ih this]

Result:
no goals
-- Mathlib/Computability/PartrecCode.lean
theorem const_inj : ∀ {n₁ n₂}, Nat.Partrec.Code.const n₁ = Nat.Partrec.Code.const n₂ → n₁ = n₂
  | 0, 0, _ => by simp
  | n₁ + 1, n₂ + 1, h => by
    dsimp [Nat.Partrec.Code.const] at h
    injection h with h₁ h₂
    simp only [const_inj h₂]

Proof state:
n₁ n₂ : ℕ
h : succ.comp (Code.const n₁) = succ.comp (Code.const n₂)
⊢ n₁ + 1 = n₂ + 1

Tactic:
injection h with h₁ h₂

Result:
n₁ n₂ : ℕ
h₁ : succ = succ
h₂ : Code.const n₁ = Code.const n₂
⊢ n₁ + 1 = n₂ + 1

Proof state:
n₁ n₂ : ℕ
h : Code.const (n₁ + 1) = Code.const (n₂ + 1)
⊢ n₁ + 1 = n₂ + 1

Tactic:
dsimp [Nat.Partrec.Code.const] at h

Result:
n₁ n₂ : ℕ
h : succ.comp (Code.const n₁) = succ.comp (Code.const n₂)
⊢ n₁ + 1 = n₂ + 1

Proof state:
x✝ : Code.const 0 = Code.const 0
⊢ 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
n₁ n₂ : ℕ
h₁ : succ = succ
h₂ : Code.const n₁ = Code.const n₂
⊢ n₁ + 1 = n₂ + 1

Tactic:
simp only [const_inj h₂]

Result:
no goals
-- Mathlib/RingTheory/PiTensorProduct.lean
lemma smul_tprod_mul_smul_tprod (r s : R) (x y : Π i, A i) :
    (r • tprod R x) * (s • tprod R y) = (r * s) • tprod R (x * y)

Proof state:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonUnitalNonAssocSemiring (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)
r s : R
x y : (i : ι) → A i
⊢ r • (tprod R) x * s • (tprod R) y = (r * s) • (tprod R) (x * y)

Tactic:
simp only [mul_def, map_smul, LinearMap.smul_apply, mul_tprod_tprod, mul_comm r s, mul_smul]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
theorem sub_dvd_eval_sub (a b : R) (p : R[X]) : a - b ∣ p.eval a - p.eval b

Proof state:
R : Type u
inst✝ : CommRing R
a b : R
p : R[X]
⊢ a - b ∣ eval a p - eval b p

Tactic:
suffices X - C b ∣ p - C (p.eval b) by
  simpa only [coe_evalRingHom, eval_sub, eval_X, eval_C] using (evalRingHom a).map_dvd this

Result:
R : Type u
inst✝ : CommRing R
a b : R
p : R[X]
⊢ X - C b ∣ p - C (eval b p)

Proof state:
R : Type u
inst✝ : CommRing R
a b : R
p : R[X]
this : X - C b ∣ p - C (eval b p)
⊢ a - b ∣ eval a p - eval b p

Tactic:
simpa only [coe_evalRingHom, eval_sub, eval_X, eval_C] using (evalRingHom a).map_dvd this

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
a b : R
p : R[X]
⊢ X - C b ∣ p - C (eval b p)

Tactic:
simp [dvd_iff_isRoot]

Result:
no goals
-- Mathlib/Algebra/Homology/ComplexShape.lean
lemma prev_eq_self (c : ComplexShape ι) (j : ι) (hj : ¬ c.Rel (c.prev j) j) :
    c.prev j = j :=
  c.prev_eq_self' j (fun k hk' => hj (by simpa only [c.prev_eq' hk'] using hk'))

Proof state:
ι : Type u_1
c : ComplexShape ι
j : ι
hj : ¬c.Rel (c.prev j) j
k : ι
hk' : c.Rel k j
⊢ c.Rel (c.prev j) j

Tactic:
simpa only [c.prev_eq' hk'] using hk'

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Veblen.lean
theorem isNormal_veblenWith (o : Ordinal) : IsNormal (veblenWith f o)

Proof state:
case inr
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
h : o ≠ 0
⊢ IsNormal (veblenWith f o)

Tactic:
exact isNormal_veblenWith' f h

Result:
no goals

Proof state:
case inl
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
⊢ IsNormal (veblenWith f 0)

Tactic:
rwa [veblenWith_zero]

Result:
no goals

Proof state:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
⊢ IsNormal (veblenWith f o)

Tactic:
obtain rfl | h := eq_or_ne o 0

Result:
case inl
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
⊢ IsNormal (veblenWith f 0)

case inr
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
h : o ≠ 0
⊢ IsNormal (veblenWith f o)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem_concat_length : ∀ (l : List α) (a : α) (i) (_ : i = l.length) (w), (l ++ [a])[i]'w = a
  | [], a, _, h, _ => by subst h; simp
  | _ :: l, a, _, h, _ => by simp [getElem_concat_length, h]

Proof state:
α : Type u_1
a : α
x✝¹ : Nat
h : x✝¹ = [].length
x✝ : x✝¹ < ([] ++ [a]).length
⊢ ([] ++ [a])[x✝¹] = a

Tactic:
subst h

Result:
α : Type u_1
a : α
x✝ : [].length < ([] ++ [a]).length
⊢ ([] ++ [a])[[].length] = a

Proof state:
α : Type u_1
head✝ : α
l : List α
a : α
x✝¹ : Nat
h : x✝¹ = (head✝ :: l).length
x✝ : x✝¹ < (head✝ :: l ++ [a]).length
⊢ (head✝ :: l ++ [a])[x✝¹] = a

Tactic:
simp [getElem_concat_length, h]

Result:
no goals

Proof state:
α : Type u_1
a : α
x✝ : [].length < ([] ++ [a]).length
⊢ ([] ++ [a])[[].length] = a

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem inf_eq_bot_iff {f g : Filter α} : f ⊓ g = ⊥ ↔ ∃ U ∈ f, ∃ V ∈ g, U ∩ V = ∅

Proof state:
α : Type u
f g : Filter α
⊢ f ⊓ g = ⊥ ↔ ∃ U ∈ f, ∃ V ∈ g, U ∩ V = ∅

Tactic:
simp only [← disjoint_iff, Filter.disjoint_iff, Set.disjoint_iff_inter_eq_empty]

Result:
no goals