harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Trace.lean
@[simp]
lemma trace_lie {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] (f g : Module.End R M) :
    trace R M ⁅f, g⁆ = 0

Proof state:
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
⊢ (trace R M) (g * f) - (trace R M) (g * f) = 0

Tactic:
exact sub_self _

Result:
no goals

Proof state:
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
⊢ (trace R M) ⁅f, g⁆ = 0

Tactic:
rw [Ring.lie_def, map_sub, trace_mul_comm]

Result:
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
⊢ (trace R M) (g * f) - (trace R M) (g * f) = 0
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cosh_sub : cosh (x - y) = cosh x * cosh y - sinh x * sinh y

Proof state:
x y : ℂ
⊢ cosh (x - y) = cosh x * cosh y - sinh x * sinh y

Tactic:
simp [sub_eq_add_neg, cosh_add, sinh_neg, cosh_neg]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
@[simp]
lemma root_eq_neg_iff :
    P.root i = - P.root j ↔ j = P.reflection_perm i i

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
h : P.root i = -P.root j
⊢ P.root j = P.root ((P.reflection_perm i) i)

Tactic:
rw [root_reflection_perm, reflection_apply_self, h, neg_neg]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
h : j = (P.reflection_perm i) i
⊢ P.root i = -P.root j

Tactic:
simp [h]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
⊢ P.root i = -P.root j ↔ j = (P.reflection_perm i) i

Tactic:
refine ⟨fun h ↦ P.root.injective ?_, fun h ↦ by simp [h]⟩

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
h : P.root i = -P.root j
⊢ P.root j = P.root ((P.reflection_perm i) i)
-- Mathlib/Data/Complex/Norm.lean
theorem norm_mul (z w : ℂ) : ‖z * w‖ = ‖z‖ * ‖w‖

Proof state:
z w : ℂ
⊢ ‖z * w‖ = ‖z‖ * ‖w‖

Tactic:
rw [norm_def, norm_def, norm_def, normSq_mul, Real.sqrt_mul (normSq_nonneg _)]

Result:
no goals
-- Mathlib/SetTheory/Nimber/Basic.lean
theorem add_eq_zero {a b : Nimber} : a + b = 0 ↔ a = b

Proof state:
case mp.inr.inl
a : Nimber
hab : a + a = 0
⊢ a = a

Tactic:
rfl

Result:
no goals

Proof state:
case mp.inr.inr
a b : Nimber
hab : a + b = 0
h : b < a
hb : b + b = 0
⊢ a = b

Tactic:
rwa [← hb, add_left_inj] at hab

Result:
no goals

Proof state:
case mpr
a b : Nimber
hab : a = b
⊢ a + b ≤ 0

Tactic:
apply add_le_of_forall_ne <;>
simp_rw [ne_eq] <;>
intro x hx

Result:
case mpr.h₁
a b : Nimber
hab : a = b
x : Nimber
hx : x < a
⊢ ¬x + b = 0

case mpr.h₂
a b : Nimber
hab : a = b
x : Nimber
hx : x < b
⊢ ¬a + x = 0

Proof state:
case mp.inl
a b : Nimber
hab : a + b = 0
h : a < b
⊢ a = b

Tactic:
have ha : a + a = 0 := add_eq_zero.2 rfl

Result:
case mp.inl
a b : Nimber
hab : a + b = 0
h : a < b
ha : a + a = 0
⊢ a = b

Proof state:
case mpr.h₂
a b : Nimber
hab : a = b
x : Nimber
hx : x < b
⊢ ¬a + x = 0

Tactic:
rw [add_eq_zero, hab]

Result:
case mpr.h₂
a b : Nimber
hab : a = b
x : Nimber
hx : x < b
⊢ ¬b = x

Proof state:
case mp.inr.inr
a b : Nimber
hab : a + b = 0
h : b < a
⊢ a = b

Tactic:
have hb : b + b = 0 := add_eq_zero.2 rfl

Result:
case mp.inr.inr
a b : Nimber
hab : a + b = 0
h : b < a
hb : b + b = 0
⊢ a = b

Proof state:
case mpr
a b : Nimber
hab : a = b
⊢ a + b = 0

Tactic:
rw [← Nimber.le_zero]

Result:
case mpr
a b : Nimber
hab : a = b
⊢ a + b ≤ 0

Proof state:
case mp
a b : Nimber
hab : a + b = 0
⊢ a = b

Tactic:
obtain h | rfl | h := lt_trichotomy a b

Result:
case mp.inl
a b : Nimber
hab : a + b = 0
h : a < b
⊢ a = b

case mp.inr.inl
a : Nimber
hab : a + a = 0
⊢ a = a

case mp.inr.inr
a b : Nimber
hab : a + b = 0
h : b < a
⊢ a = b

Proof state:
case mpr.h₂
a b : Nimber
hab : a = b
x : Nimber
hx : x < b
⊢ ¬b = x

Tactic:
exact hx.ne'

Result:
no goals

Proof state:
case mpr.h₁
a b : Nimber
hab : a = b
x : Nimber
hx : x < a
⊢ ¬x + b = 0

Tactic:
rw [add_eq_zero, ← hab]

Result:
case mpr.h₁
a b : Nimber
hab : a = b
x : Nimber
hx : x < a
⊢ ¬x = a

Proof state:
a b : Nimber
⊢ a + b = 0 ↔ a = b

Tactic:
constructor <;>
  intro hab

Result:
case mp
a b : Nimber
hab : a + b = 0
⊢ a = b

case mpr
a b : Nimber
hab : a = b
⊢ a + b = 0

Proof state:
case mpr.h₁
a b : Nimber
hab : a = b
x : Nimber
hx : x < a
⊢ ¬x = a

Tactic:
exact hx.ne

Result:
no goals

Proof state:
case mp.inl
a b : Nimber
hab : a + b = 0
h : a < b
ha : a + a = 0
⊢ a = b

Tactic:
rwa [← ha, add_right_inj, eq_comm] at hab

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem eraseIdx_set_lt {l : Array α} {i : Nat} {w : i < l.size} {j : Nat} {a : α} (h : j < i) :
    (l.set i a).eraseIdx j (by simp; omega) = (l.eraseIdx j).set (i - 1) a (by simp; omega)

Proof state:
α : Type ?u.70214
l : Array α
i : Nat
w : i < l.size
j : Nat
a : α
h : j < i
⊢ j < l.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type ?u.70214
l : Array α
i : Nat
w : i < l.size
j : Nat
a : α
h : j < i
⊢ j < (l.set i a w).size

Tactic:
simp

Result:
α : Type ?u.70214
l : Array α
i : Nat
w : i < l.size
j : Nat
a : α
h : j < i
⊢ j < l.size

Proof state:
case mk
α : Type u_1
i j : Nat
a : α
h : j < i
l : List α
w : i < { toList := l }.size
⊢ ({ toList := l }.set i a w).eraseIdx j ⋯ = ({ toList := l }.eraseIdx j ⋯).set (i - 1) a ⋯

Tactic:
simp [List.eraseIdx_set_lt, *]

Result:
no goals

Proof state:
α : Type ?u.70214
l : Array α
i : Nat
w : i < l.size
j : Nat
a : α
h : j < i
⊢ i - 1 < (l.eraseIdx j ⋯).size

Tactic:
simp

Result:
α : Type ?u.70214
l : Array α
i : Nat
w : i < l.size
j : Nat
a : α
h : j < i
⊢ i - 1 < l.size - 1

Proof state:
α : Type u_1
l : Array α
i : Nat
w : i < l.size
j : Nat
a : α
h : j < i
⊢ (l.set i a w).eraseIdx j ⋯ = (l.eraseIdx j ⋯).set (i - 1) a ⋯

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
i j : Nat
a : α
h : j < i
l : List α
w : i < { toList := l }.size
⊢ ({ toList := l }.set i a w).eraseIdx j ⋯ = ({ toList := l }.eraseIdx j ⋯).set (i - 1) a ⋯

Proof state:
α : Type ?u.70214
l : Array α
i : Nat
w : i < l.size
j : Nat
a : α
h : j < i
⊢ i - 1 < l.size - 1

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/Analytic/OfScalars.lean
theorem ofScalars_series_eq_zero_of_scalar_zero : ofScalars E (0 : ℕ → 𝕜) = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : Ring E
inst✝² : Algebra 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalRing E
⊢ ofScalars E 0 = 0

Tactic:
simp [FormalMultilinearSeries.ext_iff]

Result:
no goals
-- Mathlib/Geometry/Euclidean/PerpBisector.lean
theorem inner_vsub_vsub_of_dist_eq_of_dist_eq {c₁ c₂ p₁ p₂ : P} (hc₁ : dist p₁ c₁ = dist p₂ c₁)
    (hc₂ : dist p₁ c₂ = dist p₂ c₂) : ⟪c₂ -ᵥ c₁, 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
c₁ c₂ p₁ p₂ : P
hc₁ : dist p₁ c₁ = dist p₂ c₁
hc₂ : dist p₁ c₂ = dist p₂ c₂
⊢ inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0

Tactic:
rw [← Submodule.mem_orthogonal_singleton_iff_inner_left, ← direction_perpBisector]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c₁ c₂ p₁ p₂ : P
hc₁ : dist p₁ c₁ = dist p₂ c₁
hc₂ : dist p₁ c₂ = dist p₂ c₂
⊢ c₂ -ᵥ c₁ ∈ (perpBisector p₁ p₂).direction

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c₁ c₂ p₁ p₂ : P
hc₁ : dist p₁ c₁ = dist p₂ c₁
hc₂ : dist p₁ c₂ = dist p₂ c₂
⊢ c₂ -ᵥ c₁ ∈ (perpBisector p₁ p₂).direction

Tactic:
apply vsub_mem_direction <;> rwa [mem_perpBisector_iff_dist_eq']

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Linearity.lean
@[simp]
lemma LSeries_neg (f : ℕ → ℂ) (s : ℂ) : LSeries (-f) s = -LSeries f s

Proof state:
f : ℕ → ℂ
s : ℂ
⊢ LSeries (-f) s = -LSeries f s

Tactic:
simp [LSeries, term_neg_apply, tsum_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldl_eq_foldr_reverse (l : Array α) (f : β → α → β) (b) :
    l.foldl f b = l.reverse.foldr (fun x y => f y x) b

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : β → α → β
b : β
⊢ foldl f b l = foldr (fun x y => f y x) b l.reverse

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Presentable/IsCardinalFiltered.lean
lemma isCardinalFiltered_aleph0_iff (J : Type u) [Category.{v} J] :
    IsCardinalFiltered J Cardinal.aleph0.{w} ↔ IsFiltered J

Proof state:
case mpr.nonempty_cocone
J : Type u
inst✝¹ : Category.{v, u} J
a✝ : IsFiltered J
A : Type w
inst✝ : SmallCategory A
F : A ⥤ J
hA : HasCardinalLT (Arrow A) Cardinal.aleph0
⊢ Nonempty (Cocone F)

Tactic:
rw [hasCardinalLT_aleph0_iff] at hA

Result:
case mpr.nonempty_cocone
J : Type u
inst✝¹ : Category.{v, u} J
a✝ : IsFiltered J
A : Type w
inst✝ : SmallCategory A
F : A ⥤ J
hA : Finite (Arrow A)
⊢ Nonempty (Cocone F)

Proof state:
case mpr.nonempty_cocone
J : Type u
inst✝ : Category.{v, u} J
a✝ : IsFiltered J
⊢ ∀ {A : Type w} [inst : SmallCategory A] (F : A ⥤ J), HasCardinalLT (Arrow A) Cardinal.aleph0 → Nonempty (Cocone F)

Tactic:
intro A _ F hA

Result:
case mpr.nonempty_cocone
J : Type u
inst✝¹ : Category.{v, u} J
a✝ : IsFiltered J
A : Type w
inst✝ : SmallCategory A
F : A ⥤ J
hA : HasCardinalLT (Arrow A) Cardinal.aleph0
⊢ Nonempty (Cocone F)

Proof state:
case mpr.nonempty_cocone
J : Type u
inst✝¹ : Category.{v, u} J
a✝ : IsFiltered J
A : Type w
inst✝ : SmallCategory A
F : A ⥤ J
hA : Finite (Arrow A)
⊢ Nonempty (Cocone F)

Tactic:
have := ((Arrow.finite_iff A).1 hA).some

Result:
case mpr.nonempty_cocone
J : Type u
inst✝¹ : Category.{v, u} J
a✝ : IsFiltered J
A : Type w
inst✝ : SmallCategory A
F : A ⥤ J
hA : Finite (Arrow A)
this : FinCategory A
⊢ Nonempty (Cocone F)

Proof state:
J : Type u
inst✝ : Category.{v, u} J
⊢ IsCardinalFiltered J Cardinal.aleph0 ↔ IsFiltered J

Tactic:
constructor

Result:
case mp
J : Type u
inst✝ : Category.{v, u} J
⊢ IsCardinalFiltered J Cardinal.aleph0 → IsFiltered J

case mpr
J : Type u
inst✝ : Category.{v, u} J
⊢ IsFiltered J → IsCardinalFiltered J Cardinal.aleph0

Proof state:
case mpr.nonempty_cocone
J : Type u
inst✝¹ : Category.{v, u} J
a✝ : IsFiltered J
A : Type w
inst✝ : SmallCategory A
F : A ⥤ J
hA : Finite (Arrow A)
this : FinCategory A
⊢ Nonempty (Cocone F)

Tactic:
exact ⟨IsFiltered.cocone F⟩

Result:
no goals

Proof state:
case mpr
J : Type u
inst✝ : Category.{v, u} J
a✝ : IsFiltered J
⊢ IsCardinalFiltered J Cardinal.aleph0

Tactic:
constructor

Result:
case mpr.nonempty_cocone
J : Type u
inst✝ : Category.{v, u} J
a✝ : IsFiltered J
⊢ ∀ {A : Type w} [inst : SmallCategory A] (F : A ⥤ J), HasCardinalLT (Arrow A) Cardinal.aleph0 → Nonempty (Cocone F)

Proof state:
case mpr
J : Type u
inst✝ : Category.{v, u} J
⊢ IsFiltered J → IsCardinalFiltered J Cardinal.aleph0

Tactic:
intro

Result:
case mpr
J : Type u
inst✝ : Category.{v, u} J
a✝ : IsFiltered J
⊢ IsCardinalFiltered J Cardinal.aleph0

Proof state:
case mp
J : Type u
inst✝ : Category.{v, u} J
a✝ : IsCardinalFiltered J Cardinal.aleph0
⊢ IsFiltered J

Tactic:
exact isFiltered_of_isCardinalDirected J Cardinal.aleph0

Result:
no goals

Proof state:
case mp
J : Type u
inst✝ : Category.{v, u} J
⊢ IsCardinalFiltered J Cardinal.aleph0 → IsFiltered J

Tactic:
intro

Result:
case mp
J : Type u
inst✝ : Category.{v, u} J
a✝ : IsCardinalFiltered J Cardinal.aleph0
⊢ IsFiltered J
-- Mathlib/MeasureTheory/PiSystem.lean
theorem has_union {s₁ s₂ : Set α} (h₁ : d.Has s₁) (h₂ : d.Has s₂) (h : Disjoint s₁ s₂) :
    d.Has (s₁ ∪ s₂)

Proof state:
α : Type u_3
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : d.Has s₁
h₂ : d.Has s₂
h : Disjoint s₁ s₂
⊢ d.Has (s₁ ∪ s₂)

Tactic:
rw [union_eq_iUnion]

Result:
α : Type u_3
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : d.Has s₁
h₂ : d.Has s₂
h : Disjoint s₁ s₂
⊢ d.Has (⋃ b, bif b then s₁ else s₂)

Proof state:
α : Type u_3
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : d.Has s₁
h₂ : d.Has s₂
h : Disjoint s₁ s₂
⊢ d.Has (⋃ b, bif b then s₁ else s₂)

Tactic:
exact d.has_iUnion (pairwise_disjoint_on_bool.2 h) (Bool.forall_bool.2 ⟨h₂, h₁⟩)

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem prod_mono : ∀ {a b : FactorSet α}, a ≤ b → a.prod ≤ b.prod
  | ⊤, b, h => by
    have : b = ⊤ := top_unique h
    rw [this, prod_top]
  | a, ⊤, _ => show a.prod ≤ (⊤ : FactorSet α).prod by simp
  | WithTop.some _, WithTop.some _, h =>
    prod_le_prod <| Multiset.map_le_map <| WithTop.coe_le_coe.1 <| h

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : FactorSet α
x✝ : a ≤ ⊤
⊢ a.prod ≤ ⊤.prod

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
b : FactorSet α
h : ⊤ ≤ b
⊢ ⊤.prod ≤ b.prod

Tactic:
have : b = ⊤ := top_unique h

Result:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
b : FactorSet α
h : ⊤ ≤ b
this : b = ⊤
⊢ ⊤.prod ≤ b.prod

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
b : FactorSet α
h : ⊤ ≤ b
this : b = ⊤
⊢ ⊤.prod ≤ b.prod

Tactic:
rw [this, prod_top]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem smul_map_volume_mul_left {a : ℝ} (h : a ≠ 0) :
    ENNReal.ofReal |a| • Measure.map (a * ·) volume = volume

Proof state:
case inl
a : ℝ
h✝ : a ≠ 0
p q : ℚ
h : a < 0
⊢ volume (Ioo ↑p ↑q) = (ofReal |a| • Measure.map (fun x => a * x) volume) (Ioo ↑p ↑q)

Tactic:
simp only [Real.volume_Ioo, Measure.smul_apply, ← ENNReal.ofReal_mul (le_of_lt <| neg_pos.2 h),
  Measure.map_apply (measurable_const_mul a) measurableSet_Ioo, neg_sub_neg, neg_mul,
  preimage_const_mul_Ioo_of_neg _ _ h, abs_of_neg h, mul_sub, smul_eq_mul,
  mul_div_cancel₀ _ (ne_of_lt h)]

Result:
no goals

Proof state:
a : ℝ
h : a ≠ 0
p q : ℚ
⊢ volume (Ioo ↑p ↑q) = (ofReal |a| • Measure.map (fun x => a * x) volume) (Ioo ↑p ↑q)

Tactic:
rcases lt_or_gt_of_ne h with h | h

Result:
case inl
a : ℝ
h✝ : a ≠ 0
p q : ℚ
h : a < 0
⊢ volume (Ioo ↑p ↑q) = (ofReal |a| • Measure.map (fun x => a * x) volume) (Ioo ↑p ↑q)

case inr
a : ℝ
h✝ : a ≠ 0
p q : ℚ
h : a > 0
⊢ volume (Ioo ↑p ↑q) = (ofReal |a| • Measure.map (fun x => a * x) volume) (Ioo ↑p ↑q)

Proof state:
case inr
a : ℝ
h✝ : a ≠ 0
p q : ℚ
h : a > 0
⊢ volume (Ioo ↑p ↑q) = (ofReal |a| • Measure.map (fun x => a * x) volume) (Ioo ↑p ↑q)

Tactic:
simp only [Real.volume_Ioo, Measure.smul_apply, ← ENNReal.ofReal_mul (le_of_lt h),
  Measure.map_apply (measurable_const_mul a) measurableSet_Ioo, preimage_const_mul_Ioo _ _ h,
  abs_of_pos h, mul_sub, mul_div_cancel₀ _ (ne_of_gt h), smul_eq_mul]

Result:
no goals

Proof state:
a : ℝ
h : a ≠ 0
⊢ ofReal |a| • Measure.map (fun x => a * x) volume = volume

Tactic:
refine (Real.measure_ext_Ioo_rat fun p q => ?_).symm

Result:
a : ℝ
h : a ≠ 0
p q : ℚ
⊢ volume (Ioo ↑p ↑q) = (ofReal |a| • Measure.map (fun x => a * x) volume) (Ioo ↑p ↑q)
-- Mathlib/Topology/Compactness/Lindelof.lean
theorem HereditarilyLindelof_LindelofSets [HereditarilyLindelofSpace X] (s : Set X) :
    IsLindelof s

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : HereditarilyLindelofSpace X
s : Set X
⊢ IsLindelof s

Tactic:
apply HereditarilyLindelofSpace.isHereditarilyLindelof_univ

Result:
case a
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : HereditarilyLindelofSpace X
s : Set X
⊢ s ⊆ univ

Proof state:
case a
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : HereditarilyLindelofSpace X
s : Set X
⊢ s ⊆ univ

Tactic:
exact subset_univ s

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Equal.lean
theorem BitVec.self_eq_add_right (a b : BitVec w) : (a == a + b) = (b == 0#w)

Proof state:
w : Nat
a b : BitVec w
⊢ (a == a + b) = (b == 0#w)

Tactic:
rw [Bool.eq_iff_iff]

Result:
w : Nat
a b : BitVec w
⊢ (a == a + b) = true ↔ (b == 0#w) = true

Proof state:
w : Nat
a b : BitVec w
⊢ (a == a + b) = true ↔ (b == 0#w) = true

Tactic:
simp

Result:
no goals
-- Mathlib/Tactic/ComputeDegree.lean
theorem natDegree_eq_of_le_of_coeff_ne_zero' {deg m o : ℕ} {c : R} {p : R[X]}
    (h_natDeg_le : natDegree p ≤ m) (coeff_eq : coeff p o = c)
    (coeff_ne_zero : c ≠ 0) (deg_eq_deg : m = deg) (coeff_eq_deg : o = deg) :
    natDegree p = deg

Proof state:
R : Type u_1
inst✝ : Semiring R
deg m o : ℕ
c : R
p : R[X]
h_natDeg_le : p.natDegree ≤ m
coeff_eq : p.coeff o = c
coeff_ne_zero : c ≠ 0
deg_eq_deg : m = deg
coeff_eq_deg : o = deg
⊢ p.natDegree = deg

Tactic:
subst coeff_eq deg_eq_deg coeff_eq_deg

Result:
R : Type u_1
inst✝ : Semiring R
o : ℕ
p : R[X]
coeff_ne_zero : p.coeff o ≠ 0
h_natDeg_le : p.natDegree ≤ o
⊢ p.natDegree = o

Proof state:
R : Type u_1
inst✝ : Semiring R
o : ℕ
p : R[X]
coeff_ne_zero : p.coeff o ≠ 0
h_natDeg_le : p.natDegree ≤ o
⊢ p.natDegree = o

Tactic:
exact natDegree_eq_of_le_of_coeff_ne_zero ‹_› ‹_›

Result:
no goals
-- Mathlib/Data/Nat/GCD/BigOperators.lean
theorem coprime_multiset_prod_left_iff {m : Multiset ℕ} {k : ℕ} :
    Coprime m.prod k ↔ ∀ n ∈ m, Coprime n k

Proof state:
m : Multiset ℕ
k : ℕ
⊢ m.prod.Coprime k ↔ ∀ n ∈ m, n.Coprime k

Tactic:
induction m using Quotient.inductionOn

Result:
case h
k : ℕ
a✝ : List ℕ
⊢ (Multiset.prod ⟦a✝⟧).Coprime k ↔ ∀ n ∈ ⟦a✝⟧, n.Coprime k

Proof state:
case h
k : ℕ
a✝ : List ℕ
⊢ (Multiset.prod ⟦a✝⟧).Coprime k ↔ ∀ n ∈ ⟦a✝⟧, n.Coprime k

Tactic:
simpa using coprime_list_prod_left_iff

Result:
no goals
-- Mathlib/AlgebraicGeometry/PointsPi.lean
lemma pointsPi_surjective_of_isAffine [IsAffine X] : Function.Surjective (pointsPi R X)

Proof state:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝ : IsAffine X
f : (i : ι) → Spec (R i) ⟶ X
⊢ ∃ a, pointsPi R X a = f

Tactic:
refine ⟨Spec.map (CommRingCat.ofHom
  (Pi.ringHom fun i ↦ (Spec.preimage (f i ≫ X.isoSpec.hom)).1)) ≫ X.isoSpec.inv, ?_⟩

Result:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝ : IsAffine X
f : (i : ι) → Spec (R i) ⟶ X
⊢ pointsPi R X
      (Spec.map (CommRingCat.ofHom (Pi.ringHom fun i => (Spec.preimage (f i ≫ X.isoSpec.hom)).hom')) ≫ X.isoSpec.inv) =
    f

Proof state:
case h
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝ : IsAffine X
f : (i : ι) → Spec (R i) ⟶ X
i : ι
⊢ Spec.map
      (CommRingCat.ofHom (Pi.ringHom fun i => (Spec.preimage (f i ≫ X.isoSpec.hom)).hom') ≫
        CommRingCat.ofHom (Pi.evalRingHom (fun x => ↑(R x)) i)) =
    f i ≫ X.isoSpec.hom

Tactic:
exact Spec.map_preimage _

Result:
no goals

Proof state:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝ : IsAffine X
⊢ Function.Surjective (pointsPi R X)

Tactic:
rintro f

Result:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝ : IsAffine X
f : (i : ι) → Spec (R i) ⟶ X
⊢ ∃ a, pointsPi R X a = f

Proof state:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝ : IsAffine X
f : (i : ι) → Spec (R i) ⟶ X
⊢ pointsPi R X
      (Spec.map (CommRingCat.ofHom (Pi.ringHom fun i => (Spec.preimage (f i ≫ X.isoSpec.hom)).hom')) ≫ X.isoSpec.inv) =
    f

Tactic:
ext i : 1

Result:
case h
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝ : IsAffine X
f : (i : ι) → Spec (R i) ⟶ X
i : ι
⊢ pointsPi R X
      (Spec.map (CommRingCat.ofHom (Pi.ringHom fun i => (Spec.preimage (f i ≫ X.isoSpec.hom)).hom')) ≫ X.isoSpec.inv)
      i =
    f i

Proof state:
case h
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝ : IsAffine X
f : (i : ι) → Spec (R i) ⟶ X
i : ι
⊢ pointsPi R X
      (Spec.map (CommRingCat.ofHom (Pi.ringHom fun i => (Spec.preimage (f i ≫ X.isoSpec.hom)).hom')) ≫ X.isoSpec.inv)
      i =
    f i

Tactic:
simp only [pointsPi, ← Spec.map_comp_assoc, Iso.comp_inv_eq]

Result:
case h
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝ : IsAffine X
f : (i : ι) → Spec (R i) ⟶ X
i : ι
⊢ Spec.map
      (CommRingCat.ofHom (Pi.ringHom fun i => (Spec.preimage (f i ≫ X.isoSpec.hom)).hom') ≫
        CommRingCat.ofHom (Pi.evalRingHom (fun x => ↑(R x)) i)) =
    f i ≫ X.isoSpec.hom
-- Mathlib/Data/Finset/NoncommProd.lean
theorem map_noncommProd_aux [MonoidHomClass F α β] (s : Multiset α)
    (comm : { x | x ∈ s }.Pairwise Commute) (f : F) : { x | x ∈ s.map f }.Pairwise Commute

Proof state:
case intro.intro.intro.intro
F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
s : Multiset α
comm : {x | x ∈ s}.Pairwise Commute
f : F
x : α
hx : x ∈ s
y : α
hy : y ∈ s
a✝ : f x ≠ f y
⊢ Commute (f x) (f y)

Tactic:
exact (comm.of_refl hx hy).map f

Result:
no goals

Proof state:
F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
s : Multiset α
comm : {x | x ∈ s}.Pairwise Commute
f : F
⊢ {x | x ∈ map (⇑f) s}.Pairwise Commute

Tactic:
simp only [Multiset.mem_map]

Result:
F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
s : Multiset α
comm : {x | x ∈ s}.Pairwise Commute
f : F
⊢ {x | ∃ a ∈ s, f a = x}.Pairwise Commute

Proof state:
F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
s : Multiset α
comm : {x | x ∈ s}.Pairwise Commute
f : F
⊢ {x | ∃ a ∈ s, f a = x}.Pairwise Commute

Tactic:
rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ _

Result:
case intro.intro.intro.intro
F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
s : Multiset α
comm : {x | x ∈ s}.Pairwise Commute
f : F
x : α
hx : x ∈ s
y : α
hy : y ∈ s
a✝ : f x ≠ f y
⊢ Commute (f x) (f y)
-- Mathlib/FieldTheory/RatFunc/AsPolynomial.lean
theorem eval_eq_zero_of_eval₂_denom_eq_zero {x : RatFunc K}
    (h : Polynomial.eval₂ f a (denom x) = 0) : eval f a x = 0

Proof state:
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x : RatFunc K
h : Polynomial.eval₂ f a x.denom = 0
⊢ eval f a x = 0

Tactic:
rw [eval, h, div_zero]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem mul_mem_nthRootsFinset
    {η₁ η₂ : R} (hη₁ : η₁ ∈ nthRootsFinset n R) (hη₂ : η₂ ∈ nthRootsFinset n R) :
    η₁ * η₂ ∈ nthRootsFinset n R

Proof state:
R : Type u
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
η₁ η₂ : R
hη₁ : η₁ ∈ nthRootsFinset n R
hη₂ : η₂ ∈ nthRootsFinset n R
⊢ η₁ * η₂ ∈ nthRootsFinset n R

Tactic:
cases n with
| zero =>
  simp only [nthRootsFinset_zero, not_mem_empty] at hη₁
| succ n =>
  rw [mem_nthRootsFinset n.succ_pos] at hη₁ hη₂ ⊢
  rw [mul_pow, hη₁, hη₂, one_mul]

Result:
no goals

Proof state:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
η₁ η₂ : R
n : ℕ
hη₁ : η₁ ^ n.succ = 1
hη₂ : η₂ ^ n.succ = 1
⊢ (η₁ * η₂) ^ n.succ = 1

Tactic:
rw [mul_pow, hη₁, hη₂, one_mul]

Result:
no goals

Proof state:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
η₁ η₂ : R
n : ℕ
hη₁ : η₁ ∈ nthRootsFinset (n + 1) R
hη₂ : η₂ ∈ nthRootsFinset (n + 1) R
⊢ η₁ * η₂ ∈ nthRootsFinset (n + 1) R

Tactic:
rw [mem_nthRootsFinset n.succ_pos] at hη₁ hη₂ ⊢

Result:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
η₁ η₂ : R
n : ℕ
hη₁ : η₁ ^ n.succ = 1
hη₂ : η₂ ^ n.succ = 1
⊢ (η₁ * η₂) ^ n.succ = 1

Proof state:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
η₁ η₂ : R
hη₁ : η₁ ∈ nthRootsFinset 0 R
hη₂ : η₂ ∈ nthRootsFinset 0 R
⊢ η₁ * η₂ ∈ nthRootsFinset 0 R

Tactic:
simp only [nthRootsFinset_zero, not_mem_empty] at hη₁

Result:
no goals