harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/MulChar/Basic.lean
lemma ringHomComp_mul (χ φ : MulChar R R') (f : R' →+* R'') :
    (χ * φ).ringHomComp f = χ.ringHomComp f * φ.ringHomComp f

Proof state:
case h
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
χ φ : MulChar R R'
f : R' →+* R''
a✝ : Rˣ
⊢ ((χ * φ).ringHomComp f) ↑a✝ = (χ.ringHomComp f * φ.ringHomComp f) ↑a✝

Tactic:
simp only [ringHomComp_apply, coeToFun_mul, Pi.mul_apply, map_mul]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
χ φ : MulChar R R'
f : R' →+* R''
⊢ (χ * φ).ringHomComp f = χ.ringHomComp f * φ.ringHomComp f

Tactic:
ext1

Result:
case h
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
χ φ : MulChar R R'
f : R' →+* R''
a✝ : Rˣ
⊢ ((χ * φ).ringHomComp f) ↑a✝ = (χ.ringHomComp f * φ.ringHomComp f) ↑a✝
-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem eLpNorm'_eq {p : ℝ} (f : α →ₛ F) (μ : Measure α) :
    eLpNorm' f p μ = (∑ y ∈ f.range, ‖y‖ₑ ^ p * μ (f ⁻¹' {y})) ^ (1 / p)

Proof state:
α : Type u_1
F : Type u_5
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup F
p : ℝ
f : α →ₛ F
μ : Measure α
⊢ (fun x => ‖f x‖ₑ ^ p) = ⇑(map (fun x => ‖x‖ₑ ^ p) f)

Tactic:
simp

Result:
α : Type u_1
F : Type u_5
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup F
p : ℝ
f : α →ₛ F
μ : Measure α
⊢ (fun x => ‖f x‖ₑ ^ p) = (fun x => ‖x‖ₑ ^ p) ∘ ⇑f

Proof state:
α : Type u_1
F : Type u_5
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup F
p : ℝ
f : α →ₛ F
μ : Measure α
h_map : (fun x => ‖f x‖ₑ ^ p) = ⇑(map (fun x => ‖x‖ₑ ^ p) f)
⊢ eLpNorm' (⇑f) p μ = (∑ y ∈ f.range, ‖y‖ₑ ^ p * μ (⇑f ⁻¹' {y})) ^ (1 / p)

Tactic:
rw [eLpNorm'_eq_lintegral_enorm, h_map, lintegral_eq_lintegral, map_lintegral]

Result:
no goals

Proof state:
α : Type u_1
F : Type u_5
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup F
p : ℝ
f : α →ₛ F
μ : Measure α
⊢ (fun x => ‖f x‖ₑ ^ p) = (fun x => ‖x‖ₑ ^ p) ∘ ⇑f

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem mem_const_vadd_affineSegment {x y z : P} (v : V) :
    v +ᵥ z ∈ affineSegment R (v +ᵥ x) (v +ᵥ y) ↔ z ∈ affineSegment R x y

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
v : V
⊢ v +ᵥ z ∈ affineSegment R (v +ᵥ x) (v +ᵥ y) ↔ z ∈ affineSegment R x y

Tactic:
rw [← affineSegment_const_vadd_image, (AddAction.injective v).mem_set_image]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem WithSeminorms.isVonNBounded_iff_finset_seminorm_bounded {s : Set E} (hp : WithSeminorms p) :
    Bornology.IsVonNBounded 𝕜 s ↔ ∀ I : Finset ι, ∃ r > 0, ∀ x ∈ s, I.sup p x < r

Proof state:
case mp.intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
h✝ : Absorbs 𝕜 ((I.sup p).ball 0 1) s
r : ℝ
hr : r > 0
a : 𝕜
ha : r < ‖a‖
h : s ⊆ (I.sup p).ball 0 ‖a‖
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r

Tactic:
refine ⟨‖a‖, lt_trans hr ha, ?_⟩

Result:
case mp.intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
h✝ : Absorbs 𝕜 ((I.sup p).ball 0 1) s
r : ℝ
hr : r > 0
a : 𝕜
ha : r < ‖a‖
h : s ⊆ (I.sup p).ball 0 ‖a‖
⊢ ∀ x ∈ s, (I.sup p) x < ‖a‖

Proof state:
case mp
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
h : Absorbs 𝕜 ((I.sup p).ball 0 1) s
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r

Tactic:
rcases h.exists_pos with ⟨r, hr, h⟩

Result:
case mp.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
h✝ : Absorbs 𝕜 ((I.sup p).ball 0 1) s
r : ℝ
hr : r > 0
h : ∀ (c : 𝕜), r ≤ ‖c‖ → s ⊆ c • (I.sup p).ball 0 1
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r
-- Mathlib/Logic/Relation.lean
theorem cases_head_iff : ReflTransGen r a b ↔ a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b

Proof state:
case mpr.inr.intro.intro
α : Type u_1
r : α → α → Prop
a b c : α
hac : r a c
hcb : ReflTransGen r c b
⊢ ReflTransGen r a b

Tactic:
exact head hac hcb

Result:
no goals

Proof state:
case mpr.inl
α : Type u_1
r : α → α → Prop
a : α
⊢ ReflTransGen r a a

Tactic:
rfl

Result:
no goals

Proof state:
case mpr
α : Type u_1
r : α → α → Prop
a b : α
⊢ (a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b) → ReflTransGen r a b

Tactic:
rintro (rfl | ⟨c, hac, hcb⟩)

Result:
case mpr.inl
α : Type u_1
r : α → α → Prop
a : α
⊢ ReflTransGen r a a

case mpr.inr.intro.intro
α : Type u_1
r : α → α → Prop
a b c : α
hac : r a c
hcb : ReflTransGen r c b
⊢ ReflTransGen r a b

Proof state:
α : Type u_1
r : α → α → Prop
a b : α
⊢ ReflTransGen r a b ↔ a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b

Tactic:
use cases_head

Result:
case mpr
α : Type u_1
r : α → α → Prop
a b : α
⊢ (a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b) → ReflTransGen r a b
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
theorem size_insertUnit {n : Nat} (units : Array (Literal (PosFin n)))
    (assignments : Array Assignment) (b : Bool) (l : Literal (PosFin n)) :
    (insertUnit (units, assignments, b) l).2.1.size = assignments.size

Proof state:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
b : Bool
l : Literal (PosFin n)
⊢ (insertUnit (units, assignments, b) l).snd.fst.size = assignments.size

Tactic:
simp only [insertUnit]

Result:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
b : Bool
l : Literal (PosFin n)
⊢ (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, b)
          else
            (units.push (l.fst, l.snd), assignments.modify l.fst.val (addAssignment l.snd),
              b || assignments[l.fst.val]! != unassigned)).snd.fst.size =
    assignments.size

Proof state:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
b : Bool
l : Literal (PosFin n)
⊢ (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, b)
          else
            (units.push (l.fst, l.snd), assignments.modify l.fst.val (addAssignment l.snd),
              b || assignments[l.fst.val]! != unassigned)).snd.fst.size =
    assignments.size

Tactic:
split <;> simp

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Prod.lean
theorem polar_prod (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) (x y : M₁ × M₂) :
    polar (Q₁.prod Q₂) x y = polar Q₁ x.1 y.1 + polar Q₂ x.2 y.2

Proof state:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup P
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
x y : M₁ × M₂
⊢ Q₁ (x.1 + y.1) + Q₂ (x.2 + y.2) - (Q₁ x.1 + Q₂ x.2) - (Q₁ y.1 + Q₂ y.2) =
    Q₁ (x.1 + y.1) - Q₁ x.1 - Q₁ y.1 + (Q₂ (x.2 + y.2) - Q₂ x.2 - Q₂ y.2)

Tactic:
abel

Result:
no goals

Proof state:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup P
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
x y : M₁ × M₂
⊢ polar (⇑(Q₁.prod Q₂)) x y = polar (⇑Q₁) x.1 y.1 + polar (⇑Q₂) x.2 y.2

Tactic:
dsimp [polar]

Result:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup P
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
x y : M₁ × M₂
⊢ Q₁ (x.1 + y.1) + Q₂ (x.2 + y.2) - (Q₁ x.1 + Q₂ x.2) - (Q₁ y.1 + Q₂ y.2) =
    Q₁ (x.1 + y.1) - Q₁ x.1 - Q₁ y.1 + (Q₂ (x.2 + y.2) - Q₂ x.2 - Q₂ y.2)
-- Mathlib/Analysis/Convex/Strict.lean
theorem StrictConvex.add_smul_mem (hs : StrictConvex 𝕜 s) (hx : x ∈ s) (hxy : x + y ∈ s)
    (hy : y ≠ 0) {t : 𝕜} (ht₀ : 0 < t) (ht₁ : t < 1) : x + t • y ∈ interior s

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x y : E
hs : StrictConvex 𝕜 s
hx : x ∈ s
hxy : x + y ∈ s
hy : y ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ (1 - t) • x + t • (x + y) ∈ interior s

Tactic:
exact hs hx hxy (fun h => hy <| add_left_cancel (a := x) (by rw [← h, add_zero]))
  (sub_pos_of_lt ht₁) ht₀ (sub_add_cancel 1 t)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x y : E
hs : StrictConvex 𝕜 s
hx : x ∈ s
hxy : x + y ∈ s
hy : y ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ x + t • y = (1 - t) • x + t • (x + y)

Tactic:
match_scalars <;> field_simp

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x y : E
hs : StrictConvex 𝕜 s
hx : x ∈ s
hxy : x + y ∈ s
hy : y ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ x + t • y ∈ interior s

Tactic:
rw [h]

Result:
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x y : E
hs : StrictConvex 𝕜 s
hx : x ∈ s
hxy : x + y ∈ s
hy : y ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ (1 - t) • x + t • (x + y) ∈ interior s

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x y : E
hs : StrictConvex 𝕜 s
hx : x ∈ s
hxy : x + y ∈ s
hy : y ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ x + t • y ∈ interior s

Tactic:
have h : x + t • y = (1 - t) • x + t • (x + y) := by match_scalars <;> field_simp

Result:
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x y : E
hs : StrictConvex 𝕜 s
hx : x ∈ s
hxy : x + y ∈ s
hy : y ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ x + t • y ∈ interior s

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x y : E
hs : StrictConvex 𝕜 s
hx : x ∈ s
hxy : x + y ∈ s
hy : y ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
h✝ : x + t • y = (1 - t) • x + t • (x + y)
h : x = x + y
⊢ x + y = x + 0

Tactic:
rw [← h, add_zero]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc (attr := simp)]
lemma LeftHomologyData.homologyπ_comp_homologyIso_hom (h : S.LeftHomologyData) :
    S.homologyπ ≫ h.homologyIso.hom = h.cyclesIso.hom ≫ h.π

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
⊢ S.homologyπ ≫ h.homologyIso.hom = h.cyclesIso.hom ≫ h.π

Tactic:
dsimp only [homologyπ, homologyIso]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
⊢ (S.leftHomologyπ ≫ S.leftHomologyIso.hom) ≫ (S.leftHomologyIso.symm ≪≫ h.leftHomologyIso).hom = h.cyclesIso.hom ≫ h.π

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
⊢ (S.leftHomologyπ ≫ S.leftHomologyIso.hom) ≫ (S.leftHomologyIso.symm ≪≫ h.leftHomologyIso).hom = h.cyclesIso.hom ≫ h.π

Tactic:
simp only [Iso.trans_hom, Iso.symm_hom, assoc, Iso.hom_inv_id_assoc,
  leftHomologyπ_comp_leftHomologyIso_hom]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Int.lean
theorem abs_ediv_le_abs : ∀ a b : ℤ, |a / b| ≤ |a| :=
  suffices ∀ (a : ℤ) (n : ℕ), |a / n| ≤ |a| from fun a b =>
    match b, eq_nat_or_neg b with
    | _, ⟨n, Or.inl rfl⟩ => this _ _
    | _, ⟨n, Or.inr rfl⟩ => by rw [Int.ediv_neg, abs_neg]; apply this
  fun a n => by
  rw [abs_eq_natAbs, abs_eq_natAbs];
  exact ofNat_le_ofNat_of_le
    (match a, n with
      | (m : ℕ), n => Nat.div_le_self _ _
      | -[m+1], 0 => Nat.zero_le _
      | -[m+1], n + 1 => Nat.succ_le_succ (Nat.div_le_self _ _))

Proof state:
this : ∀ (a : ℤ) (n : ℕ), |a / ↑n| ≤ |a|
a b : ℤ
n : ℕ
⊢ |a / -↑n| ≤ |a|

Tactic:
rw [Int.ediv_neg, abs_neg]

Result:
this : ∀ (a : ℤ) (n : ℕ), |a / ↑n| ≤ |a|
a b : ℤ
n : ℕ
⊢ |a / ↑n| ≤ |a|

Proof state:
a : ℤ
n : ℕ
⊢ ↑(a / ↑n).natAbs ≤ ↑a.natAbs

Tactic:
exact ofNat_le_ofNat_of_le
  (match a, n with
    | (m : ℕ), n => Nat.div_le_self _ _
    | -[m+1], 0 => Nat.zero_le _
    | -[m+1], n + 1 => Nat.succ_le_succ (Nat.div_le_self _ _))

Result:
no goals

Proof state:
this : ∀ (a : ℤ) (n : ℕ), |a / ↑n| ≤ |a|
a b : ℤ
n : ℕ
⊢ |a / ↑n| ≤ |a|

Tactic:
apply this

Result:
no goals

Proof state:
a : ℤ
n : ℕ
⊢ |a / ↑n| ≤ |a|

Tactic:
rw [abs_eq_natAbs, abs_eq_natAbs]

Result:
a : ℤ
n : ℕ
⊢ ↑(a / ↑n).natAbs ≤ ↑a.natAbs
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Roots.lean
theorem cyclotomic.irreducible {n : ℕ} (hpos : 0 < n) : Irreducible (cyclotomic n ℤ)

Proof state:
case hx
n : ℕ
hpos : 0 < n
⊢ IsIntegral ℤ (cexp (2 * ↑Real.pi * I / ↑n))

Tactic:
exact (isPrimitiveRoot_exp n hpos.ne').isIntegral hpos

Result:
no goals

Proof state:
n : ℕ
hpos : 0 < n
⊢ Irreducible (cyclotomic n ℤ)

Tactic:
rw [cyclotomic_eq_minpoly (isPrimitiveRoot_exp n hpos.ne') hpos]

Result:
n : ℕ
hpos : 0 < n
⊢ Irreducible (minpoly ℤ (cexp (2 * ↑Real.pi * I / ↑n)))

Proof state:
n : ℕ
hpos : 0 < n
⊢ Irreducible (minpoly ℤ (cexp (2 * ↑Real.pi * I / ↑n)))

Tactic:
apply minpoly.irreducible

Result:
case hx
n : ℕ
hpos : 0 < n
⊢ IsIntegral ℤ (cexp (2 * ↑Real.pi * I / ↑n))
-- Mathlib/Data/Nat/Init.lean
lemma eq_zero_of_le_div (hn : 2 ≤ n) (h : m ≤ m / n) : m = 0 :=
  eq_zero_of_mul_le hn <| by
    rw [Nat.mul_comm]; exact (Nat.le_div_iff_mul_le (Nat.lt_of_lt_of_le (by decide) hn)).1 h

Proof state:
m n : ℕ
hn : 2 ≤ n
h : m ≤ m / n
⊢ 0 < 2

Tactic:
decide

Result:
no goals

Proof state:
m n : ℕ
hn : 2 ≤ n
h : m ≤ m / n
⊢ n * m ≤ m

Tactic:
rw [Nat.mul_comm]

Result:
m n : ℕ
hn : 2 ≤ n
h : m ≤ m / n
⊢ m * n ≤ m

Proof state:
m n : ℕ
hn : 2 ≤ n
h : m ≤ m / n
⊢ m * n ≤ m

Tactic:
exact (Nat.le_div_iff_mul_le (Nat.lt_of_lt_of_le (by decide) hn)).1 h

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean
theorem sum_logEmbedding_component (x : (𝓞 K)ˣ) :
    ∑ w, logEmbedding K (Additive.ofMul x) w =
      - mult (w₀ : InfinitePlace K) * Real.log (w₀ (x : K))

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : ∑ w : InfinitePlace K, ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑x)) = 0
⊢ ∑ w : { w // w ≠ w₀ }, (logEmbedding K) (Additive.ofMul x) w = -↑w₀.mult * Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))

Tactic:
rw [Fintype.sum_eq_add_sum_subtype_ne _ w₀, add_comm, add_eq_zero_iff_eq_neg, ← neg_mul] at h

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h :
  ∑ i : { i // i ≠ w₀ }, ↑(↑i).mult * Real.log (↑i ((algebraMap (𝓞 K) K) ↑x)) =
    -↑w₀.mult * Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))
⊢ ∑ w : { w // w ≠ w₀ }, (logEmbedding K) (Additive.ofMul x) w = -↑w₀.mult * Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
⊢ ∑ w : { w // w ≠ w₀ }, (logEmbedding K) (Additive.ofMul x) w = -↑w₀.mult * Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))

Tactic:
have h := sum_mult_mul_log x

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : ∑ w : InfinitePlace K, ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑x)) = 0
⊢ ∑ w : { w // w ≠ w₀ }, (logEmbedding K) (Additive.ofMul x) w = -↑w₀.mult * Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h :
  ∑ i : { i // i ≠ w₀ }, ↑(↑i).mult * Real.log (↑i ((algebraMap (𝓞 K) K) ↑x)) =
    -↑w₀.mult * Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))
⊢ ∑ w : { w // w ≠ w₀ }, (logEmbedding K) (Additive.ofMul x) w = -↑w₀.mult * Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))

Tactic:
simpa [logEmbedding_component] using h

Result:
no goals
-- Mathlib/Data/List/NatAntidiagonal.lean
theorem map_swap_antidiagonal {n : ℕ} :
    (antidiagonal n).map Prod.swap = (antidiagonal n).reverse

Proof state:
n : ℕ
⊢ map (Prod.swap ∘ fun i => (i, n - i)) (range (n + 1)) =
    map ((fun i => (i, n - i)) ∘ fun x => 0 + (n + 1) - 1 - x) (range (n + 1))

Tactic:
apply map_congr_left

Result:
case h
n : ℕ
⊢ ∀ a ∈ range (n + 1), (Prod.swap ∘ fun i => (i, n - i)) a = ((fun i => (i, n - i)) ∘ fun x => 0 + (n + 1) - 1 - x) a

Proof state:
n : ℕ
⊢ map Prod.swap (antidiagonal n) = (antidiagonal n).reverse

Tactic:
rw [antidiagonal, map_map, ← List.map_reverse, range_eq_range', reverse_range', ←
  range_eq_range', map_map]

Result:
n : ℕ
⊢ map (Prod.swap ∘ fun i => (i, n - i)) (range (n + 1)) =
    map ((fun i => (i, n - i)) ∘ fun x => 0 + (n + 1) - 1 - x) (range (n + 1))

Proof state:
case h
n : ℕ
⊢ ∀ a ∈ range (n + 1), (Prod.swap ∘ fun i => (i, n - i)) a = ((fun i => (i, n - i)) ∘ fun x => 0 + (n + 1) - 1 - x) a

Tactic:
simp +contextual [Nat.sub_sub_self, Nat.lt_succ_iff]

Result:
no goals
-- Mathlib/Algebra/Regular/Basic.lean
theorem IsRightRegular.ne_zero [Nontrivial R] (ra : IsRightRegular a) : a ≠ 0

Proof state:
case intro.intro
R : Type u_1
inst✝¹ : MulZeroClass R
inst✝ : Nontrivial R
ra : IsRightRegular 0
x y : R
xy : x ≠ y
⊢ False

Tactic:
refine xy (ra (?_ : x * 0 = y * 0))

Result:
case intro.intro
R : Type u_1
inst✝¹ : MulZeroClass R
inst✝ : Nontrivial R
ra : IsRightRegular 0
x y : R
xy : x ≠ y
⊢ x * 0 = y * 0

Proof state:
R : Type u_1
inst✝¹ : MulZeroClass R
a : R
inst✝ : Nontrivial R
ra : IsRightRegular a
⊢ a ≠ 0

Tactic:
rintro rfl

Result:
R : Type u_1
inst✝¹ : MulZeroClass R
inst✝ : Nontrivial R
ra : IsRightRegular 0
⊢ False

Proof state:
R : Type u_1
inst✝¹ : MulZeroClass R
inst✝ : Nontrivial R
ra : IsRightRegular 0
⊢ False

Tactic:
rcases exists_pair_ne R with ⟨x, y, xy⟩

Result:
case intro.intro
R : Type u_1
inst✝¹ : MulZeroClass R
inst✝ : Nontrivial R
ra : IsRightRegular 0
x y : R
xy : x ≠ y
⊢ False

Proof state:
case intro.intro
R : Type u_1
inst✝¹ : MulZeroClass R
inst✝ : Nontrivial R
ra : IsRightRegular 0
x y : R
xy : x ≠ y
⊢ x * 0 = y * 0

Tactic:
rw [mul_zero, mul_zero]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Bounded.lean
theorem isVonNBounded_biUnion {ι : Type*} {I : Set ι} (hI : I.Finite) {s : ι → Set E} :
    IsVonNBounded 𝕜 (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, IsVonNBounded 𝕜 (s i)

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
ι : Type u_6
I : Set ι
hI : I.Finite
s : ι → Set E
x✝ : Finite ↑I
⊢ IsVonNBounded 𝕜 (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, IsVonNBounded 𝕜 (s i)

Tactic:
rw [biUnion_eq_iUnion, isVonNBounded_iUnion, Subtype.forall]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
ι : Type u_6
I : Set ι
hI : I.Finite
s : ι → Set E
⊢ IsVonNBounded 𝕜 (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, IsVonNBounded 𝕜 (s i)

Tactic:
have _ := hI.to_subtype

Result:
𝕜 : Type u_1
E : Type u_3
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
ι : Type u_6
I : Set ι
hI : I.Finite
s : ι → Set E
x✝ : Finite ↑I
⊢ IsVonNBounded 𝕜 (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, IsVonNBounded 𝕜 (s i)
-- Mathlib/Data/Real/Pointwise.lean
theorem Real.iInf_mul_of_nonneg (ha : 0 ≤ r) (f : ι → ℝ) : (⨅ i, f i) * r = ⨅ i, f i * r

Proof state:
ι : Sort u_1
r : ℝ
ha : 0 ≤ r
f : ι → ℝ
⊢ (⨅ i, f i) * r = ⨅ i, f i * r

Tactic:
simp only [Real.mul_iInf_of_nonneg ha, mul_comm]

Result:
no goals
-- Mathlib/Algebra/Module/Torsion.lean
theorem torsionBySet_univ : torsionBySet R M Set.univ = ⊥

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ torsionBySet R M Set.univ ≤ torsionBySet R M {1}

Tactic:
exact torsionBySet_le_torsionBySet_of_subset fun _ _ => trivial

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ torsionBySet R M Set.univ = ⊥

Tactic:
rw [eq_bot_iff, ← torsionBy_one, ← torsionBySet_singleton_eq]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ torsionBySet R M Set.univ ≤ torsionBySet R M {1}
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem isAlgebraic_nat [Nontrivial R] (n : ℕ) : IsAlgebraic R (n : A)

Proof state:
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
n : ℕ
⊢ IsAlgebraic R ↑n

Tactic:
rw [← map_natCast (_ : R →+* A) n]

Result:
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
n : ℕ
⊢ IsAlgebraic R (?m.37646 ↑n)

R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
n : ℕ
⊢ R →+* A

Proof state:
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
n : ℕ
⊢ IsAlgebraic R (?m.37646 ↑n)

R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
n : ℕ
⊢ R →+* A

Tactic:
exact isAlgebraic_algebraMap (Nat.cast n)

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean
theorem Module.End.finite_spectrum {K : Type v} {V : Type w} [Field K] [AddCommGroup V]
    [Module K V] [FiniteDimensional K V] (f : Module.End K V) :
    Set.Finite (spectrum K f)

Proof state:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
⊢ (spectrum K f).Finite

Tactic:
convert f.finite_hasEigenvalue

Result:
case h.e'_2.h.e
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
⊢ spectrum K = HasEigenvalue

Proof state:
case h.e'_2.h.e
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
⊢ spectrum K = HasEigenvalue

Tactic:
ext f x

Result:
case h.e'_2.h.e.h.h
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f✝ f : End K V
x : K
⊢ x ∈ spectrum K f ↔ x ∈ f.HasEigenvalue

Proof state:
case h.e'_2.h.e.h.h
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f✝ f : End K V
x : K
⊢ x ∈ spectrum K f ↔ x ∈ f.HasEigenvalue

Tactic:
exact Module.End.hasEigenvalue_iff_mem_spectrum.symm

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
theorem divisorsAntidiagonal_one : divisorsAntidiagonal 1 = {(1, 1)}

Proof state:
⊢ divisorsAntidiagonal 1 = {(1, 1)}

Tactic:
ext

Result:
case h
a✝ : ℕ × ℕ
⊢ a✝ ∈ divisorsAntidiagonal 1 ↔ a✝ ∈ {(1, 1)}

Proof state:
case h
a✝ : ℕ × ℕ
⊢ a✝ ∈ divisorsAntidiagonal 1 ↔ a✝ ∈ {(1, 1)}

Tactic:
simp [mul_eq_one, Prod.ext_iff]

Result:
no goals