harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Simproc.lean
theorem eq_add_le {a : Nat} (b : Nat) {c : Nat} (h : c ≤ a) : (a = b + c) = (b = a - c)

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

Tactic:
rw [@Eq.comm Nat a (b + c)]

Result:
a b c : Nat
h : c ≤ a
⊢ (b + c = a) = (b = a - c)

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

Tactic:
exact add_eq_le b h

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem splits_iff_card_roots (ha : P.a ≠ 0) :
    Splits φ P.toPoly ↔ Multiset.card (map φ P).roots = 3

Proof state:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
ha : P.a ≠ 0
⊢ Splits φ P.toPoly ↔ (map φ P).roots.card = 3

Tactic:
replace ha : (map φ P).a ≠ 0 := (_root_.map_ne_zero φ).mpr ha

Result:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
ha : (map φ P).a ≠ 0
⊢ Splits φ P.toPoly ↔ (map φ P).roots.card = 3

Proof state:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
ha : (map φ P).a ≠ 0
⊢ Splits φ P.toPoly ↔ (map φ P).roots.card = 3

Tactic:
nth_rw 1 [← RingHom.id_comp φ]

Result:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
ha : (map φ P).a ≠ 0
⊢ Splits ((RingHom.id K).comp φ) P.toPoly ↔ (map φ P).roots.card = 3

Proof state:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
ha : (map φ P).a ≠ 0
⊢ Splits ((RingHom.id K).comp φ) P.toPoly ↔ (map φ P).roots.card = 3

Tactic:
rw [roots, ← splits_map_iff, ← map_toPoly, Polynomial.splits_iff_card_roots,
  ← ((degree_eq_iff_natDegree_eq <| ne_zero_of_a_ne_zero ha).1 <| degree_of_a_ne_zero ha : _ = 3)]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Quotient.lean
theorem quotient_nhd_basis (S : AddSubgroup M) :
    (𝓝 (0 : M ⧸ S)).HasBasis (fun ε ↦ 0 < ε) fun ε ↦ { x | ‖x‖ < ε }

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
⊢ ∀ (ε : ℝ), mk '' ball 0 ε = {x | ‖x‖ < ε}

Tactic:
refine fun ε ↦ Set.ext <| forall_mk.2 fun x ↦ ?_

Result:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
ε : ℝ
x : M
⊢ ↑x ∈ mk '' ball 0 ε ↔ ↑x ∈ {x | ‖x‖ < ε}

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
this : ∀ (ε : ℝ), mk '' ball 0 ε = {x | ‖x‖ < ε}
⊢ (𝓝 0).HasBasis (fun ε => 0 < ε) fun ε => {x | ‖x‖ < ε}

Tactic:
rw [← QuotientAddGroup.mk_zero, nhds_eq, ← funext this]

Result:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
this : ∀ (ε : ℝ), mk '' ball 0 ε = {x | ‖x‖ < ε}
⊢ (Filter.map mk (𝓝 0)).HasBasis (fun ε => 0 < ε) fun x => mk '' ball 0 x

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
this : ∀ (ε : ℝ), mk '' ball 0 ε = {x | ‖x‖ < ε}
⊢ (Filter.map mk (𝓝 0)).HasBasis (fun ε => 0 < ε) fun x => mk '' ball 0 x

Tactic:
exact .map _ Metric.nhds_basis_ball

Result:
no goals

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
ε : ℝ
x : M
⊢ (∃ x_1 ∈ {x | ‖x‖ < ε}, ↑x_1 = ↑x) ↔ ∃ m, ↑m = ↑x ∧ ‖m‖ < ε

Tactic:
exact exists_congr fun _ ↦ and_comm

Result:
no goals

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
⊢ (𝓝 0).HasBasis (fun ε => 0 < ε) fun ε => {x | ‖x‖ < ε}

Tactic:
have : ∀ ε : ℝ, mk '' ball (0 : M) ε = { x : M ⧸ S | ‖x‖ < ε } := by
  refine fun ε ↦ Set.ext <| forall_mk.2 fun x ↦ ?_
  rw [ball_zero_eq, mem_setOf_eq, norm_lt_iff, mem_image]
  exact exists_congr fun _ ↦ and_comm

Result:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
this : ∀ (ε : ℝ), mk '' ball 0 ε = {x | ‖x‖ < ε}
⊢ (𝓝 0).HasBasis (fun ε => 0 < ε) fun ε => {x | ‖x‖ < ε}

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
ε : ℝ
x : M
⊢ ↑x ∈ mk '' ball 0 ε ↔ ↑x ∈ {x | ‖x‖ < ε}

Tactic:
rw [ball_zero_eq, mem_setOf_eq, norm_lt_iff, mem_image]

Result:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
ε : ℝ
x : M
⊢ (∃ x_1 ∈ {x | ‖x‖ < ε}, ↑x_1 = ↑x) ↔ ∃ m, ↑m = ↑x ∧ ‖m‖ < ε
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem tan_pi_div_six : tan (π / 6) = 1 / sqrt 3

Proof state:
⊢ tan (π / 6) = 1 / √3

Tactic:
rw [tan_eq_sin_div_cos, sin_pi_div_six, cos_pi_div_six]

Result:
⊢ 1 / 2 / (√3 / 2) = 1 / √3

Proof state:
⊢ 1 / 2 / (√3 / 2) = 1 / √3

Tactic:
ring

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/LpEquiv.lean
theorem equiv_lpPiLp_norm [Fintype α] (f : lp E p) : ‖Equiv.lpPiLp f‖ = ‖f‖

Proof state:
case inr.inr
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Fintype α
f : ↥(lp E p)
h : 0 < p.toReal
⊢ ‖Equiv.lpPiLp f‖ = ‖f‖

Tactic:
rw [PiLp.norm_eq_sum h, lp.norm_eq_tsum_rpow h, tsum_fintype]

Result:
case inr.inr
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Fintype α
f : ↥(lp E p)
h : 0 < p.toReal
⊢ (∑ i : α, ‖Equiv.lpPiLp f i‖ ^ p.toReal) ^ (1 / p.toReal) = (∑ b : α, ‖↑f b‖ ^ p.toReal) ^ (1 / p.toReal)

Proof state:
case inl
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Fintype α
f : ↥(lp E 0)
⊢ ‖Equiv.lpPiLp f‖ = ‖f‖

Tactic:
simp [Equiv.lpPiLp, PiLp.norm_eq_card, lp.norm_eq_card_dsupport]

Result:
no goals

Proof state:
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Fintype α
f : ↥(lp E p)
⊢ ‖Equiv.lpPiLp f‖ = ‖f‖

Tactic:
rcases p.trichotomy with (rfl | rfl | h)

Result:
case inl
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Fintype α
f : ↥(lp E 0)
⊢ ‖Equiv.lpPiLp f‖ = ‖f‖

case inr.inl
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Fintype α
f : ↥(lp E ⊤)
⊢ ‖Equiv.lpPiLp f‖ = ‖f‖

case inr.inr
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Fintype α
f : ↥(lp E p)
h : 0 < p.toReal
⊢ ‖Equiv.lpPiLp f‖ = ‖f‖

Proof state:
case inr.inl
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Fintype α
f : ↥(lp E ⊤)
⊢ ⨆ i, ‖Equiv.lpPiLp f i‖ = ⨆ i, ‖↑f i‖

Tactic:
rfl

Result:
no goals

Proof state:
case inr.inl
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Fintype α
f : ↥(lp E ⊤)
⊢ ‖Equiv.lpPiLp f‖ = ‖f‖

Tactic:
rw [PiLp.norm_eq_ciSup, lp.norm_eq_ciSup]

Result:
case inr.inl
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Fintype α
f : ↥(lp E ⊤)
⊢ ⨆ i, ‖Equiv.lpPiLp f i‖ = ⨆ i, ‖↑f i‖

Proof state:
case inr.inr
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Fintype α
f : ↥(lp E p)
h : 0 < p.toReal
⊢ (∑ i : α, ‖Equiv.lpPiLp f i‖ ^ p.toReal) ^ (1 / p.toReal) = (∑ b : α, ‖↑f b‖ ^ p.toReal) ^ (1 / p.toReal)

Tactic:
rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma baseChange_neg (P : Fin 3 → A) :
    (W'.baseChange B).toJacobian.neg (f ∘ P) = f ∘ (W'.baseChange A).toJacobian.neg P

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
P : Fin 3 → A
⊢ (baseChange W' B).toJacobian.neg (⇑f ∘ P) = ⇑f ∘ (baseChange W' A).toJacobian.neg P

Tactic:
rw [← RingHom.coe_coe, ← WeierstrassCurve.Jacobian.map_neg, map_baseChange]

Result:
no goals
-- Mathlib/Data/Real/ConjExponents.lean
protected lemma inv_inv (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) : a⁻¹.IsConjExponent b⁻¹ :=
  ⟨(one_lt_inv₀ ha).2 <| by linarith, by simpa only [inv_inv]⟩

Proof state:
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a < 1

Tactic:
linarith

Result:
no goals

Proof state:
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a⁻¹⁻¹ + b⁻¹⁻¹ = 1

Tactic:
simpa only [inv_inv]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem natCast_eq_last (n) : (n : Fin (n + 1)) = Fin.last n

Proof state:
n : ℕ
⊢ ↑n = last n

Tactic:
ext

Result:
case h
n : ℕ
⊢ ↑↑n = ↑(last n)

Proof state:
case h
n : ℕ
⊢ ↑↑n = ↑(last n)

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma add_smul_of_equiv {P Q : Fin 3 → R} (h : P ≈ Q) {u v : R} (hu : IsUnit u) (hv : IsUnit v) :
    W'.add (u • P) (v • Q) = u ^ 4 • W'.add P Q

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
h : P ≈ Q
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ W'.add (u • P) (v • Q) = u ^ 4 • W'.add P Q

Tactic:
rw [add_of_equiv <| (smul_equiv_smul P Q hu hv).mpr h, dblXYZ_smul, add_of_equiv h]

Result:
no goals
-- Mathlib/RingTheory/Localization/LocalizationLocalization.lean
theorem localization_localization_map_units [IsLocalization N T]
    (y : localizationLocalizationSubmodule M N) : IsUnit (algebraMap R T y)

Proof state:
case intro.intro
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
y : ↥(localizationLocalizationSubmodule M N)
y' : ↥N
z : ↥M
eq : (algebraMap R S) ↑y = ↑y' * (algebraMap R S) ↑z
⊢ IsUnit ((algebraMap S T) ↑y') ∧ IsUnit ((algebraMap S T) ((algebraMap R S) ↑z))

Tactic:
exact ⟨IsLocalization.map_units T y', (IsLocalization.map_units _ z).map (algebraMap S T)⟩

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
y : ↥(localizationLocalizationSubmodule M N)
y' : ↥N
z : ↥M
eq : (algebraMap R S) ↑y = ↑y' * (algebraMap R S) ↑z
⊢ IsUnit ((algebraMap R T) ↑y)

Tactic:
rw [IsScalarTower.algebraMap_apply R S T, eq, RingHom.map_mul, IsUnit.mul_iff]

Result:
case intro.intro
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
y : ↥(localizationLocalizationSubmodule M N)
y' : ↥N
z : ↥M
eq : (algebraMap R S) ↑y = ↑y' * (algebraMap R S) ↑z
⊢ IsUnit ((algebraMap S T) ↑y') ∧ IsUnit ((algebraMap S T) ((algebraMap R S) ↑z))

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
y : ↥(localizationLocalizationSubmodule M N)
⊢ IsUnit ((algebraMap R T) ↑y)

Tactic:
obtain ⟨y', z, eq⟩ := mem_localizationLocalizationSubmodule.mp y.prop

Result:
case intro.intro
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
y : ↥(localizationLocalizationSubmodule M N)
y' : ↥N
z : ↥M
eq : (algebraMap R S) ↑y = ↑y' * (algebraMap R S) ↑z
⊢ IsUnit ((algebraMap R T) ↑y)
-- Mathlib/LinearAlgebra/Quotient/Basic.lean
theorem factor_comp_mk (H : p ≤ p') : (factor H).comp (mkQ p) = mkQ p'

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
H : p ≤ p'
x : M
⊢ (factor H ∘ₗ p.mkQ) x = p'.mkQ x

Tactic:
rw [LinearMap.comp_apply, factor_mk]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
H : p ≤ p'
⊢ factor H ∘ₗ p.mkQ = p'.mkQ

Tactic:
ext x

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
H : p ≤ p'
x : M
⊢ (factor H ∘ₗ p.mkQ) x = p'.mkQ x
-- Mathlib/Topology/UnitInterval.lean
/-- Any open cover of the unit interval can be refined to a finite partition into subintervals. -/
lemma exists_monotone_Icc_subset_open_cover_unitInterval {ι} {c : ι → Set I}
    (hc₁ : ∀ i, IsOpen (c i)) (hc₂ : univ ⊆ ⋃ i, c i) : ∃ t : ℕ → I, t 0 = 0 ∧
      Monotone t ∧ (∃ n, ∀ m ≥ n, t m = 1) ∧ ∀ n, ∃ i, Icc (t n) (t (n + 1)) ⊆ c i

Proof state:
ι : Sort u_1
c : ι → Set ↑I
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : univ ⊆ ⋃ i, c i
⊢ ∃ t, ↑(t 0) = ↑0 ∧ Monotone t ∧ (∃ n, ∀ m ≥ n, ↑(t m) = ↑1) ∧ ∀ (n : ℕ), ∃ i, Icc (t n) (t (n + 1)) ⊆ c i

Tactic:
exact exists_monotone_Icc_subset_open_cover_Icc zero_le_one hc₁ hc₂

Result:
no goals

Proof state:
ι : Sort u_1
c : ι → Set ↑I
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : univ ⊆ ⋃ i, c i
⊢ ∃ t, t 0 = 0 ∧ Monotone t ∧ (∃ n, ∀ m ≥ n, t m = 1) ∧ ∀ (n : ℕ), ∃ i, Icc (t n) (t (n + 1)) ⊆ c i

Tactic:
simp_rw [← Subtype.coe_inj]

Result:
ι : Sort u_1
c : ι → Set ↑I
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : univ ⊆ ⋃ i, c i
⊢ ∃ t, ↑(t 0) = ↑0 ∧ Monotone t ∧ (∃ n, ∀ m ≥ n, ↑(t m) = ↑1) ∧ ∀ (n : ℕ), ∃ i, Icc (t n) (t (n + 1)) ⊆ c i
-- Mathlib/Data/Real/Sqrt.lean
theorem abs_le_sqrt (h : x ^ 2 ≤ y) : |x| ≤ √y

Proof state:
x y : ℝ
h : x ^ 2 ≤ y
⊢ |x| ≤ √y

Tactic:
rw [← sqrt_sq_eq_abs]

Result:
x y : ℝ
h : x ^ 2 ≤ y
⊢ √(x ^ 2) ≤ √y

Proof state:
x y : ℝ
h : x ^ 2 ≤ y
⊢ √(x ^ 2) ≤ √y

Tactic:
exact sqrt_le_sqrt h

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem lt_wf : @WellFounded PartENat (· < ·)

Proof state:
⊢ WellFounded fun a b => a < b

Tactic:
simp_rw [← withTopEquiv_lt]

Result:
⊢ WellFounded fun a b => withTopEquiv a < withTopEquiv b

Proof state:
⊢ WellFounded fun x1 x2 => x1 < x2

Tactic:
classical
  change WellFounded fun a b : PartENat => a < b
  simp_rw [← withTopEquiv_lt]
  exact InvImage.wf _ wellFounded_lt

Result:
no goals

Proof state:
⊢ WellFounded fun x1 x2 => x1 < x2

Tactic:
change WellFounded fun a b : PartENat => a < b

Result:
⊢ WellFounded fun a b => a < b

Proof state:
⊢ WellFounded fun a b => withTopEquiv a < withTopEquiv b

Tactic:
exact InvImage.wf _ wellFounded_lt

Result:
no goals
-- Mathlib/Tactic/Module.lean
theorem add_eq_eval {R₁ R₂ : Type*} [AddCommMonoid M] [Semiring R] [Module R M] [Semiring R₁]
    [Module R₁ M] [Semiring R₂] [Module R₂ M] {l₁ l₂ l : NF R M} {l₁' : NF R₁ M} {l₂' : NF R₂ M}
    {x₁ x₂ : M} (hx₁ : x₁ = l₁'.eval) (hx₂ : x₂ = l₂'.eval) (h₁ : l₁.eval = l₁'.eval)
    (h₂ : l₂.eval = l₂'.eval) (h : l₁.eval + l₂.eval = l.eval) :
    x₁ + x₂ = l.eval

Proof state:
R : Type u_2
M : Type u_3
R₁ : Type u_4
R₂ : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Semiring R
inst✝⁴ : Module R M
inst✝³ : Semiring R₁
inst✝² : Module R₁ M
inst✝¹ : Semiring R₂
inst✝ : Module R₂ M
l₁ l₂ l : NF R M
l₁' : NF R₁ M
l₂' : NF R₂ M
x₁ x₂ : M
hx₁ : x₁ = l₁'.eval
hx₂ : x₂ = l₂'.eval
h₁ : l₁.eval = l₁'.eval
h₂ : l₂.eval = l₂'.eval
h : l₁.eval + l₂.eval = l.eval
⊢ x₁ + x₂ = l.eval

Tactic:
rw [hx₁, hx₂, ← h₁, ← h₂, h]

Result:
no goals
-- Mathlib/SetTheory/Nimber/Field.lean
theorem mul_def (a b : Nimber) :
    a * b = sInf {x | ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = x}ᶜ

Proof state:
a b : Nimber
⊢ sInf {x | ∃ a' < a, ∃ b' < b, a'.mul b + a.mul b' + a'.mul b' = x}ᶜ =
    sInf {x | ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = x}ᶜ

Tactic:
rfl

Result:
no goals

Proof state:
a b : Nimber
⊢ a.mul b = sInf {x | ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = x}ᶜ

Tactic:
rw [Nimber.mul]

Result:
a b : Nimber
⊢ sInf {x | ∃ a', ∃ (_ : a' < a), ∃ b', ∃ (_ : b' < b), a'.mul b + a.mul b' + a'.mul b' = x}ᶜ =
    sInf {x | ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = x}ᶜ

Proof state:
a b : Nimber
⊢ a * b = sInf {x | ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = x}ᶜ

Tactic:
change Nimber.mul a b = _

Result:
a b : Nimber
⊢ a.mul b = sInf {x | ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = x}ᶜ

Proof state:
a b : Nimber
⊢ sInf {x | ∃ a', ∃ (_ : a' < a), ∃ b', ∃ (_ : b' < b), a'.mul b + a.mul b' + a'.mul b' = x}ᶜ =
    sInf {x | ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = x}ᶜ

Tactic:
simp_rw [exists_prop]

Result:
a b : Nimber
⊢ sInf {x | ∃ a' < a, ∃ b' < b, a'.mul b + a.mul b' + a'.mul b' = x}ᶜ =
    sInf {x | ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = x}ᶜ
-- Mathlib/Algebra/Lie/Normalizer.lean
theorem mem_normalizer_iff (x : L) : x ∈ H.normalizer ↔ ∀ y : L, y ∈ H → ⁅x, y⁆ ∈ H

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x : L
⊢ (∀ y ∈ H, ⁅y, x⁆ ∈ H) ↔ ∀ y ∈ H, ⁅x, y⁆ ∈ H

Tactic:
refine forall₂_congr fun y hy => ?_

Result:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x y : L
hy : y ∈ H
⊢ ⁅y, x⁆ ∈ H ↔ ⁅x, y⁆ ∈ H

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x y : L
hy : y ∈ H
⊢ ⁅y, x⁆ ∈ H ↔ ⁅x, y⁆ ∈ H

Tactic:
rw [← lie_skew, neg_mem_iff (G := L)]

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x : L
⊢ x ∈ H.normalizer ↔ ∀ y ∈ H, ⁅x, y⁆ ∈ H

Tactic:
rw [mem_normalizer_iff']

Result:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x : L
⊢ (∀ y ∈ H, ⁅y, x⁆ ∈ H) ↔ ∀ y ∈ H, ⁅x, y⁆ ∈ H
-- Mathlib/Order/GaloisConnection/Basic.lean
theorem sInf_image2_eq_sInf_sInf (h₁ : ∀ b, GaloisConnection (l₁ b) (swap u b))
    (h₂ : ∀ a, GaloisConnection (l₂ a) (u a)) : sInf (image2 u s t) = u (sInf s) (sInf t)

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : CompleteLattice γ
s : Set α
t : Set β
u : α → β → γ
l₁ : β → γ → α
l₂ : α → γ → β
h₁ : ∀ (b : β), GaloisConnection (l₁ b) (swap u b)
h₂ : ∀ (a : α), GaloisConnection (l₂ a) (u a)
⊢ sInf (image2 u s t) = u (sInf s) (sInf t)

Tactic:
simp_rw [sInf_image2, ← (h₂ _).u_sInf, ← (h₁ _).u_sInf]

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem _root_.Measurable.sub_stronglyMeasurable
    {α E : Type*} {_ : MeasurableSpace α} [AddCommGroup E] [TopologicalSpace E]
    [MeasurableSpace E] [BorelSpace E] [ContinuousAdd E] [ContinuousNeg E] [PseudoMetrizableSpace E]
    {g f : α → E} (hg : Measurable g) (hf : StronglyMeasurable f) :
    Measurable (g - f)

Proof state:
α : Type u_5
E : Type u_6
x✝ : MeasurableSpace α
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : ContinuousAdd E
inst✝¹ : ContinuousNeg E
inst✝ : PseudoMetrizableSpace E
g f : α → E
hg : Measurable g
hf : StronglyMeasurable f
⊢ Measurable (g - f)

Tactic:
rw [sub_eq_add_neg]

Result:
α : Type u_5
E : Type u_6
x✝ : MeasurableSpace α
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : ContinuousAdd E
inst✝¹ : ContinuousNeg E
inst✝ : PseudoMetrizableSpace E
g f : α → E
hg : Measurable g
hf : StronglyMeasurable f
⊢ Measurable (g + -f)

Proof state:
α : Type u_5
E : Type u_6
x✝ : MeasurableSpace α
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : ContinuousAdd E
inst✝¹ : ContinuousNeg E
inst✝ : PseudoMetrizableSpace E
g f : α → E
hg : Measurable g
hf : StronglyMeasurable f
⊢ Measurable (g + -f)

Tactic:
exact hg.add_stronglyMeasurable hf.neg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
    m.contains a = false → m.getKey? a = none

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
a : α
⊢ m.contains a = false → m.getKey? a = none

Tactic:
simp_to_raw using Raw₀.getKey?_eq_none

Result:
no goals
-- Mathlib/Topology/Compactness/Lindelof.lean
theorem IsLindelof.union (hs : IsLindelof s) (ht : IsLindelof t) : IsLindelof (s ∪ t)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsLindelof t
⊢ IsLindelof (⋃ b, bif b then s else t)

Tactic:
exact isLindelof_iUnion fun b => by cases b <;> assumption

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsLindelof t
b : Bool
⊢ IsLindelof (bif b then s else t)

Tactic:
cases b <;> assumption

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsLindelof t
⊢ IsLindelof (s ∪ t)

Tactic:
rw [union_eq_iUnion]

Result:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsLindelof t
⊢ IsLindelof (⋃ b, bif b then s else t)
-- Mathlib/Order/Minimal.lean
theorem minimal_iff_forall_lt : Minimal P x ↔ P x ∧ ∀ ⦃y⦄, y < x → ¬ P y

Proof state:
α : Type u_1
P : α → Prop
x : α
inst✝ : Preorder α
⊢ Minimal P x ↔ P x ∧ ∀ ⦃y : α⦄, y < x → ¬P y

Tactic:
simp [Minimal, lt_iff_le_not_le, not_imp_not, imp.swap]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem get_tail (l : List α) (i) (h : i < l.tail.length)
    (h' : i + 1 < l.length := (by simp only [length_tail] at h; omega)) :
    l.tail.get ⟨i, h⟩ = l.get ⟨i + 1, h'⟩

Proof state:
α : Type u
l : List α
i : ℕ
h : i < l.tail.length
h' : optParam (i + 1 < l.length) ⋯
⊢ l.tail.get ⟨i, h⟩ = l.get ⟨i + 1, h'⟩

Tactic:
cases l <;> [cases h; rfl]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l₁ l₂ l : List α
i : ℕ
h : i < l.length - 1
⊢ i + 1 < l.length

Tactic:
omega

Result:
no goals

Proof state:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l₁ l₂ l : List α
i : ℕ
h : i < l.tail.length
⊢ i + 1 < l.length

Tactic:
simp only [length_tail] at h

Result:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l₁ l₂ l : List α
i : ℕ
h : i < l.length - 1
⊢ i + 1 < l.length
-- Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
theorem coevaluation_comp_leftAdjointMate {X Y : C} [HasLeftDual X] [HasLeftDual Y] (f : X ⟶ Y) :
    η_ (ᘁY) Y ≫ (ᘁf) ▷ Y = η_ (ᘁX) X ≫ (ᘁX) ◁ f

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
⊢ (tensorRightHomEquiv (𝟙_ C) (ᘁY) Y ᘁX).symm (η_ (ᘁY) Y ≫ (ᘁf) ▷ Y) =
    (tensorRightHomEquiv (𝟙_ C) (ᘁY) Y ᘁX).symm (η_ (ᘁX) X ≫ ᘁX ◁ f)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
⊢ η_ (ᘁY) Y ≫ (ᘁf) ▷ Y = η_ (ᘁX) X ≫ ᘁX ◁ f

Tactic:
apply_fun (tensorRightHomEquiv _ (ᘁY) Y _).symm

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
⊢ (tensorRightHomEquiv (𝟙_ C) (ᘁY) Y ᘁX).symm (η_ (ᘁY) Y ≫ (ᘁf) ▷ Y) =
    (tensorRightHomEquiv (𝟙_ C) (ᘁY) Y ᘁX).symm (η_ (ᘁX) X ≫ ᘁX ◁ f)
-- Mathlib/Algebra/GroupWithZero/Pointwise/Set/Basic.lean
lemma Nonempty.zero_div (hs : s.Nonempty) : 0 / s = 0 :=
  s.zero_div_subset.antisymm <| by simpa [mem_div] using hs

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

Tactic:
simpa [mem_div] using hs

Result:
no goals
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem choose_le_succ (a c : ℕ) : choose a c ≤ choose a.succ c

Proof state:
a c : ℕ
⊢ a.choose c ≤ a.succ.choose c

Tactic:
cases c <;> simp [Nat.choose_succ_succ]

Result:
no goals
-- Mathlib/NumberTheory/FactorisationProperties.lean
theorem deficient_or_perfect_or_abundant (hn : 0 ≠ n) :
    Deficient n ∨ Abundant n ∨ Perfect n

Proof state:
n : ℕ
hn : 0 ≠ n
⊢ ∑ i ∈ n.properDivisors, i < n ∨ n < ∑ i ∈ n.properDivisors, i ∨ ∑ i ∈ n.properDivisors, i = n ∧ 0 < n

Tactic:
omega

Result:
no goals

Proof state:
n : ℕ
hn : 0 ≠ n
⊢ n.Deficient ∨ n.Abundant ∨ n.Perfect

Tactic:
dsimp only [Perfect, Abundant, Deficient]

Result:
n : ℕ
hn : 0 ≠ n
⊢ ∑ i ∈ n.properDivisors, i < n ∨ n < ∑ i ∈ n.properDivisors, i ∨ ∑ i ∈ n.properDivisors, i = n ∧ 0 < n