harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/FiniteType.lean
theorem support_gen_of_gen {S : Set R[M]} (hS : Algebra.adjoin R S = ⊤) :
    Algebra.adjoin R (⋃ f ∈ S, of' R M '' (f.support : Set M)) = ⊤

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set R[M]
hS : adjoin R S = ⊤
f : R[M]
hf : f ∈ S
⊢ f ∈ ↑(adjoin R (⋃ f ∈ S, of' R M '' ↑f.support))

Tactic:
have hincl :
  of' R M '' f.support ⊆ ⋃ (g : R[M]) (_ : g ∈ S), of' R M '' g.support := by
  intro s hs
  exact Set.mem_iUnion₂.2 ⟨f, ⟨hf, hs⟩⟩

Result:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set R[M]
hS : adjoin R S = ⊤
f : R[M]
hf : f ∈ S
hincl : of' R M '' ↑f.support ⊆ ⋃ g ∈ S, of' R M '' ↑g.support
⊢ f ∈ ↑(adjoin R (⋃ f ∈ S, of' R M '' ↑f.support))

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set R[M]
hS : adjoin R S = ⊤
f : R[M]
hf : f ∈ S
hincl : of' R M '' ↑f.support ⊆ ⋃ g ∈ S, of' R M '' ↑g.support
⊢ f ∈ ↑(adjoin R (⋃ f ∈ S, of' R M '' ↑f.support))

Tactic:
exact adjoin_mono hincl (mem_adjoin_support f)

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set R[M]
hS : adjoin R S = ⊤
⊢ adjoin R (⋃ f ∈ S, of' R M '' ↑f.support) = ⊤

Tactic:
refine le_antisymm le_top ?_

Result:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set R[M]
hS : adjoin R S = ⊤
⊢ ⊤ ≤ adjoin R (⋃ f ∈ S, of' R M '' ↑f.support)

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set R[M]
hS : adjoin R S = ⊤
f : R[M]
hf : f ∈ S
⊢ of' R M '' ↑f.support ⊆ ⋃ g ∈ S, of' R M '' ↑g.support

Tactic:
intro s hs

Result:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set R[M]
hS : adjoin R S = ⊤
f : R[M]
hf : f ∈ S
s : R[M]
hs : s ∈ of' R M '' ↑f.support
⊢ s ∈ ⋃ g ∈ S, of' R M '' ↑g.support

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set R[M]
hS : adjoin R S = ⊤
⊢ S ⊆ ↑(adjoin R (⋃ f ∈ S, of' R M '' ↑f.support))

Tactic:
intro f hf

Result:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set R[M]
hS : adjoin R S = ⊤
f : R[M]
hf : f ∈ S
⊢ f ∈ ↑(adjoin R (⋃ f ∈ S, of' R M '' ↑f.support))

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set R[M]
hS : adjoin R S = ⊤
f : R[M]
hf : f ∈ S
s : R[M]
hs : s ∈ of' R M '' ↑f.support
⊢ s ∈ ⋃ g ∈ S, of' R M '' ↑g.support

Tactic:
exact Set.mem_iUnion₂.2 ⟨f, ⟨hf, hs⟩⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set R[M]
hS : adjoin R S = ⊤
⊢ ⊤ ≤ adjoin R (⋃ f ∈ S, of' R M '' ↑f.support)

Tactic:
rw [← hS, adjoin_le_iff]

Result:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set R[M]
hS : adjoin R S = ⊤
⊢ S ⊆ ↑(adjoin R (⋃ f ∈ S, of' R M '' ↑f.support))
-- Mathlib/Algebra/CharP/Lemmas.lean
lemma Nat.Prime.dvd_add_pow_sub_pow_of_dvd (hpri : p.Prime) {r : R} (h₁ : r ∣ x ^ p)
    (h₂ : r ∣ p * x) : r ∣ (x + y) ^ p - y ^ p

Proof state:
R : Type u_1
inst✝ : CommRing R
x y : R
p : ℕ
hpri : Prime p
r : R
h₁ : r ∣ x ^ p
h₂ : r ∣ ↑p * x
⊢ r ∣ (x + y) ^ p - y ^ p

Tactic:
rw [add_pow_prime_eq hpri, add_right_comm, add_assoc, add_sub_assoc, add_sub_cancel_right]

Result:
R : Type u_1
inst✝ : CommRing R
x y : R
p : ℕ
hpri : Prime p
r : R
h₁ : r ∣ x ^ p
h₂ : r ∣ ↑p * x
⊢ r ∣ x ^ p + ↑p * ∑ k ∈ Ioo 0 p, x ^ k * y ^ (p - k) * ↑(p.choose k / p)

Proof state:
R : Type u_1
inst✝ : CommRing R
x y : R
p : ℕ
hpri : Prime p
r : R
h₁ : r ∣ x ^ p
h₂ : r ∣ ↑p * x
⊢ ∀ i ∈ Ioo 0 p, x ∣ x ^ i * y ^ (p - i) * ↑(p.choose i / p)

Tactic:
simp only [Finset.mem_Ioo, and_imp, mul_assoc]

Result:
R : Type u_1
inst✝ : CommRing R
x y : R
p : ℕ
hpri : Prime p
r : R
h₁ : r ∣ x ^ p
h₂ : r ∣ ↑p * x
⊢ ∀ (i : ℕ), 0 < i → i < p → x ∣ x ^ i * (y ^ (p - i) * ↑(p.choose i / p))

Proof state:
R : Type u_1
inst✝ : CommRing R
x y : R
p : ℕ
hpri : Prime p
r : R
h₁ : r ∣ x ^ p
h₂ : r ∣ ↑p * x
⊢ r ∣ x ^ p + ↑p * ∑ k ∈ Ioo 0 p, x ^ k * y ^ (p - k) * ↑(p.choose k / p)

Tactic:
apply dvd_add h₁ (h₂.trans <| mul_dvd_mul_left _ <| Finset.dvd_sum _)

Result:
R : Type u_1
inst✝ : CommRing R
x y : R
p : ℕ
hpri : Prime p
r : R
h₁ : r ∣ x ^ p
h₂ : r ∣ ↑p * x
⊢ ∀ i ∈ Ioo 0 p, x ∣ x ^ i * y ^ (p - i) * ↑(p.choose i / p)

Proof state:
R : Type u_1
inst✝ : CommRing R
x y : R
p : ℕ
hpri : Prime p
r : R
h₁ : r ∣ x ^ p
h₂ : r ∣ ↑p * x
i : ℕ
hi0 : 0 < i
a✝ : i < p
⊢ x ∣ x ^ i * (y ^ (p - i) * ↑(p.choose i / p))

Tactic:
exact dvd_mul_of_dvd_left (dvd_rfl.pow hi0.ne') _

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
x y : R
p : ℕ
hpri : Prime p
r : R
h₁ : r ∣ x ^ p
h₂ : r ∣ ↑p * x
⊢ ∀ (i : ℕ), 0 < i → i < p → x ∣ x ^ i * (y ^ (p - i) * ↑(p.choose i / p))

Tactic:
intro i hi0 _

Result:
R : Type u_1
inst✝ : CommRing R
x y : R
p : ℕ
hpri : Prime p
r : R
h₁ : r ∣ x ^ p
h₂ : r ∣ ↑p * x
i : ℕ
hi0 : 0 < i
a✝ : i < p
⊢ x ∣ x ^ i * (y ^ (p - i) * ↑(p.choose i / p))
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem mul {β} [MonoidWithZero β] {f g : α →ₛ β} (hf : f.FinMeasSupp μ)
    (hg : g.FinMeasSupp μ) : (f * g).FinMeasSupp μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝ : MonoidWithZero β
f g : α →ₛ β
hf : f.FinMeasSupp μ
hg : g.FinMeasSupp μ
⊢ (f * g).FinMeasSupp μ

Tactic:
rw [mul_eq_map₂]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝ : MonoidWithZero β
f g : α →ₛ β
hf : f.FinMeasSupp μ
hg : g.FinMeasSupp μ
⊢ (map (fun p => p.1 * p.2) (f.pair g)).FinMeasSupp μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝ : MonoidWithZero β
f g : α →ₛ β
hf : f.FinMeasSupp μ
hg : g.FinMeasSupp μ
⊢ (map (fun p => p.1 * p.2) (f.pair g)).FinMeasSupp μ

Tactic:
exact hf.map₂ hg (zero_mul 0)

Result:
no goals
-- Mathlib/GroupTheory/Index.lean
theorem index_comap (f : G' →* G) :
    (H.comap f).index = H.relindex f.range :=
  Eq.trans (congr_arg index (by rfl))
    ((H.subgroupOf f.range).index_comap_of_surjective f.rangeRestrict_surjective)

Proof state:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
⊢ comap f H = comap f.rangeRestrict (H.subgroupOf f.range)

Tactic:
rfl

Result:
no goals
-- Mathlib/Logic/Lemmas.lean
theorem dite_dite_distrib_left {a : p → α} {b : ¬p → q → α} {c : ¬p → ¬q → α} :
    (dite p a fun hp ↦ dite q (b hp) (c hp)) =
      dite q (fun hq ↦ (dite p a) fun hp ↦ b hp hq) fun hq ↦ (dite p a) fun hp ↦ c hp hq

Proof state:
α : Sort u_1
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
⊢ (dite p a fun hp => dite q (b hp) (c hp)) = if hq : q then dite p a fun hp => b hp hq else dite p a fun hp => c hp hq

Tactic:
split_ifs <;> rfl

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem isRightInversion_mul_left_iff {w : W} :
    cs.IsRightInversion (w * t) t ↔ ¬cs.IsRightInversion w t

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
⊢ cs.length w < cs.length (w * t) ↔ cs.length w ≤ cs.length (w * t)

Tactic:
constructor

Result:
case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
⊢ cs.length w < cs.length (w * t) → cs.length w ≤ cs.length (w * t)

case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
⊢ cs.length w ≤ cs.length (w * t) → cs.length w < cs.length (w * t)

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
⊢ cs.IsRightInversion (w * t) t ↔ ¬cs.IsRightInversion w t

Tactic:
unfold IsRightInversion

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
⊢ cs.IsReflection t ∧ cs.length (w * t * t) < cs.length (w * t) ↔ ¬(cs.IsReflection t ∧ cs.length (w * t) < cs.length w)

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
⊢ cs.IsReflection t ∧ cs.length (w * t * t) < cs.length (w * t) ↔ ¬(cs.IsReflection t ∧ cs.length (w * t) < cs.length w)

Tactic:
simp only [mul_assoc, ht.inv, ht.mul_self, mul_one, ht, true_and, not_lt]

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
⊢ cs.length w < cs.length (w * t) ↔ cs.length w ≤ cs.length (w * t)

Proof state:
case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
⊢ cs.length w < cs.length (w * t) → cs.length w ≤ cs.length (w * t)

Tactic:
exact le_of_lt

Result:
no goals
-- Mathlib/Analysis/Convex/Hull.lean
theorem convexHull_pair (x y : E) : convexHull 𝕜 {x, y} = segment 𝕜 x y

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x y : E
⊢ {x, y} ⊆ segment 𝕜 x y

Tactic:
rw [insert_subset_iff, singleton_subset_iff]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x y : E
⊢ x ∈ segment 𝕜 x y ∧ y ∈ segment 𝕜 x y

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x y : E
⊢ x ∈ segment 𝕜 x y ∧ y ∈ segment 𝕜 x y

Tactic:
exact ⟨left_mem_segment _ _ _, right_mem_segment _ _ _⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x y : E
⊢ (convexHull 𝕜) {x, y} = segment 𝕜 x y

Tactic:
refine (convexHull_min ?_ <| convex_segment _ _).antisymm
  (segment_subset_convexHull (mem_insert _ _) <| subset_insert _ _ <| mem_singleton _)

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x y : E
⊢ {x, y} ⊆ segment 𝕜 x y
-- Mathlib/Data/Fin/Basic.lean
theorem modNat_rev (i : Fin (m * n)) : i.rev.modNat = i.modNat.rev

Proof state:
n m : ℕ
i : Fin (m * n)
⊢ i.rev.modNat = i.modNat.rev

Tactic:
ext

Result:
case h
n m : ℕ
i : Fin (m * n)
⊢ ↑i.rev.modNat = ↑i.modNat.rev

Proof state:
n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ n - (↑i % n + 1) < n

Tactic:
exact i.modNat.rev.is_lt

Result:
no goals

Proof state:
case h
n m : ℕ
i : Fin (m * n)
⊢ ↑i.rev.modNat = ↑i.modNat.rev

Tactic:
have H₁ : i % n + 1 ≤ n := i.modNat.is_lt

Result:
case h
n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
⊢ ↑i.rev.modNat = ↑i.modNat.rev

Proof state:
case h
n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ (m * n - (↑i + 1)) % n = n - (↑i % n + 1)

Tactic:
calc
  (m * n - (i + 1)) % n = (m * n - ((i / n) * n + i % n + 1)) % n := by rw [Nat.div_add_mod']
  _ = ((m - i / n - 1) * n + (n - (i % n + 1))) % n := by
    rw [Nat.mul_sub_right_distrib, Nat.one_mul, Nat.sub_add_sub_cancel _ H₁,
      Nat.mul_sub_right_distrib, Nat.sub_sub, Nat.add_assoc]
    exact Nat.le_mul_of_pos_left _ <| Nat.le_sub_of_add_le' H₂
  _ = n - (i % n + 1) := by
    rw [Nat.mul_comm, Nat.mul_add_mod, Nat.mod_eq_of_lt]; exact i.modNat.rev.is_lt

Result:
no goals

Proof state:
n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ (m * n - (↑i + 1)) % n = (m * n - (↑i / n * n + ↑i % n + 1)) % n

Tactic:
rw [Nat.div_add_mod']

Result:
no goals

Proof state:
n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ ((m - ↑i / n - 1) * n + (n - (↑i % n + 1))) % n = n - (↑i % n + 1)

Tactic:
rw [Nat.mul_comm, Nat.mul_add_mod, Nat.mod_eq_of_lt]

Result:
n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ n - (↑i % n + 1) < n

Proof state:
n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ n ≤ (m - ↑i / n) * n

Tactic:
exact Nat.le_mul_of_pos_left _ <| Nat.le_sub_of_add_le' H₂

Result:
no goals

Proof state:
case h
n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ ↑i.rev.modNat = ↑i.modNat.rev

Tactic:
simp only [coe_modNat, val_rev]

Result:
case h
n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ (m * n - (↑i + 1)) % n = n - (↑i % n + 1)

Proof state:
n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ (m * n - (↑i / n * n + ↑i % n + 1)) % n = ((m - ↑i / n - 1) * n + (n - (↑i % n + 1))) % n

Tactic:
rw [Nat.mul_sub_right_distrib, Nat.one_mul, Nat.sub_add_sub_cancel _ H₁,
  Nat.mul_sub_right_distrib, Nat.sub_sub, Nat.add_assoc]

Result:
n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ n ≤ (m - ↑i / n) * n

Proof state:
case h
n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
⊢ ↑i.rev.modNat = ↑i.modNat.rev

Tactic:
have H₂ : i / n < m := i.divNat.is_lt

Result:
case h
n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ ↑i.rev.modNat = ↑i.modNat.rev
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem spanSingleton_one : spanSingleton S (1 : P) = 1

Proof state:
case a
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x✝ : P
⊢ ∀ (a : R), a • 1 = x✝ ↔ (algebraMap R P) a = x✝

Tactic:
intro x'

Result:
case a
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x✝ : P
x' : R
⊢ x' • 1 = x✝ ↔ (algebraMap R P) x' = x✝

Proof state:
case a
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x✝ : P
x' : R
⊢ x' • 1 = x✝ ↔ (algebraMap R P) x' = x✝

Tactic:
rw [Algebra.smul_def, mul_one]

Result:
no goals

Proof state:
case a
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x✝ : P
⊢ x✝ ∈ spanSingleton S 1 ↔ x✝ ∈ 1

Tactic:
refine (mem_spanSingleton S).trans ((exists_congr ?_).trans (mem_one_iff S).symm)

Result:
case a
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x✝ : P
⊢ ∀ (a : R), a • 1 = x✝ ↔ (algebraMap R P) a = x✝

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
⊢ spanSingleton S 1 = 1

Tactic:
ext

Result:
case a
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x✝ : P
⊢ x✝ ∈ spanSingleton S 1 ↔ x✝ ∈ 1
-- Mathlib/Analysis/RCLike/Inner.lean
@[simp] lemma wInner_cWeight_const_right (f : ι → 𝕜) (a : 𝕜) :
    ⟪f, const _ a⟫ₙ_[𝕜] = (𝔼 i, conj (f i)) * a

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
f : ι → 𝕜
a : 𝕜
⊢ wInner cWeight f (const ι a) = (𝔼 i : ι, (starRingEnd 𝕜) (f i)) * a

Tactic:
simp [wInner_cWeight_eq_expect, expect_mul]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Spectrum.lean
theorem conj_eigenvalue_eq_self (hT : T.IsSymmetric) {μ : 𝕜} (hμ : HasEigenvalue T μ) :
    conj μ = μ

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ : 𝕜
hμ : HasEigenvalue T μ
⊢ (starRingEnd 𝕜) μ = μ

Tactic:
obtain ⟨v, hv₁, hv₂⟩ := hμ.exists_hasEigenvector

Result:
case intro.intro
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ : 𝕜
hμ : HasEigenvalue T μ
v : E
hv₁ : v ∈ (genEigenspace T μ) 1
hv₂ : v ≠ 0
⊢ (starRingEnd 𝕜) μ = μ

Proof state:
case intro.intro
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ : 𝕜
hμ : HasEigenvalue T μ
v : E
hv₁ : T v = μ • v
hv₂ : v ≠ 0
⊢ (starRingEnd 𝕜) μ = μ

Tactic:
simpa [hv₂, inner_smul_left, inner_smul_right, hv₁] using hT v v

Result:
no goals

Proof state:
case intro.intro
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ : 𝕜
hμ : HasEigenvalue T μ
v : E
hv₁ : v ∈ (genEigenspace T μ) 1
hv₂ : v ≠ 0
⊢ (starRingEnd 𝕜) μ = μ

Tactic:
rw [mem_eigenspace_iff] at hv₁

Result:
case intro.intro
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ : 𝕜
hμ : HasEigenvalue T μ
v : E
hv₁ : T v = μ • v
hv₂ : v ≠ 0
⊢ (starRingEnd 𝕜) μ = μ
-- Mathlib/Algebra/Homology/Embedding/TruncGE.lean
lemma restrictionToTruncGE'_hasLift : e.HasLift (K.restrictionToTruncGE' e)

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : e.BoundaryGE j
i' : ι'
x✝ : c'.Rel i' (e.f j)
⊢ K.d i' (e.f j) ≫ (K.restrictionXIso e ⋯).hom ≫ K.pOpcycles (e.f j) ≫ (K.truncGE'XIsoOpcycles e ⋯ hj).inv = 0

Tactic:
simp [restrictionXIso]

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : e.BoundaryGE j
i' : ι'
x✝ : c'.Rel i' (e.f j)
⊢ K.d i' (e.f j) ≫ restrictionToTruncGE'.f K e j = 0

Tactic:
rw [restrictionToTruncGE'.f_eq_iso_hom_pOpcycles_iso_inv K e rfl hj]

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : e.BoundaryGE j
i' : ι'
x✝ : c'.Rel i' (e.f j)
⊢ K.d i' (e.f j) ≫ (K.restrictionXIso e ⋯).hom ≫ K.pOpcycles (e.f j) ≫ (K.truncGE'XIsoOpcycles e ⋯ hj).inv = 0

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : e.BoundaryGE j
i' : ι'
x✝ : c'.Rel i' (e.f j)
⊢ K.d i' (e.f j) ≫ (K.restrictionToTruncGE' e).f j = 0

Tactic:
dsimp [restrictionToTruncGE']

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : e.BoundaryGE j
i' : ι'
x✝ : c'.Rel i' (e.f j)
⊢ K.d i' (e.f j) ≫ restrictionToTruncGE'.f K e j = 0

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
⊢ e.HasLift (K.restrictionToTruncGE' e)

Tactic:
intro j hj i' _

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : e.BoundaryGE j
i' : ι'
x✝ : c'.Rel i' (e.f j)
⊢ K.d i' (e.f j) ≫ (K.restrictionToTruncGE' e).f j = 0
-- Mathlib/Analysis/Asymptotics/ExpGrowth.lean
lemma expGrowthSup_sum {α : Type*} (u : α → ℕ → ℝ≥0∞) (s : Finset α) :
    expGrowthSup (∑ x ∈ s, u x) = ⨆ x ∈ s, expGrowthSup (u x)

Proof state:
case insert
α : Type u_1
u : α → ℕ → ℝ≥0∞
a : α
t : Finset α
a_t : a ∉ t
ha : expGrowthSup (∑ x ∈ t, u x) = ⨆ x ∈ t, expGrowthSup (u x)
⊢ expGrowthSup (∑ x ∈ insert a t, u x) = ⨆ x ∈ insert a t, expGrowthSup (u x)

Tactic:
rw [Finset.sum_insert a_t, expGrowthSup_add, ← Finset.iSup_coe,
Finset.coe_insert a t, iSup_insert, Finset.iSup_coe, ha]

Result:
no goals

Proof state:
α : Type u_1
u : α → ℕ → ℝ≥0∞
s : Finset α
⊢ expGrowthSup (∑ x ∈ s, u x) = ⨆ x ∈ s, expGrowthSup (u x)

Tactic:
induction s using Finset.induction_on with
| empty => rw [Finset.sum_empty, ← Finset.iSup_coe, Finset.coe_empty, iSup_emptyset,
  expGrowthSup_zero]
| @insert a t a_t ha => rw [Finset.sum_insert a_t, expGrowthSup_add, ← Finset.iSup_coe,
  Finset.coe_insert a t, iSup_insert, Finset.iSup_coe, ha]

Result:
no goals

Proof state:
α : Type u_1
u : α → ℕ → ℝ≥0∞
s : Finset α
⊢ expGrowthSup (∑ x ∈ s, u x) = ⨆ x ∈ s, expGrowthSup (u x)

Tactic:
classical
induction s using Finset.induction_on with
| empty => rw [Finset.sum_empty, ← Finset.iSup_coe, Finset.coe_empty, iSup_emptyset,
  expGrowthSup_zero]
| @insert a t a_t ha => rw [Finset.sum_insert a_t, expGrowthSup_add, ← Finset.iSup_coe,
  Finset.coe_insert a t, iSup_insert, Finset.iSup_coe, ha]

Result:
no goals

Proof state:
case empty
α : Type u_1
u : α → ℕ → ℝ≥0∞
⊢ expGrowthSup (∑ x ∈ ∅, u x) = ⨆ x ∈ ∅, expGrowthSup (u x)

Tactic:
rw [Finset.sum_empty, ← Finset.iSup_coe, Finset.coe_empty, iSup_emptyset,
expGrowthSup_zero]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Content.lean
theorem content_C_mul (r : R) (p : R[X]) : (C r * p).content = normalize r * p.content

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (C r * p).support.gcd (C r * p).coeff = p.support.gcd fun x => r * p.coeff x

Tactic:
refine congr (congr rfl ?_) ?_ <;> ext <;> simp [h0, mem_support_iff]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (C r * p).content = normalize r * p.content

Tactic:
rw [content]

Result:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (C r * p).support.gcd (C r * p).coeff = normalize r * p.content

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (C r * p).support.gcd (C r * p).coeff = normalize r * p.content

Tactic:
rw [content]

Result:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (C r * p).support.gcd (C r * p).coeff = normalize r * p.support.gcd p.coeff

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (C r * p).support.gcd (C r * p).coeff = normalize r * p.support.gcd p.coeff

Tactic:
rw [← Finset.gcd_mul_left]

Result:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (C r * p).support.gcd (C r * p).coeff = p.support.gcd fun x => r * p.coeff x

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
⊢ (C r * p).content = normalize r * p.content

Tactic:
by_cases h0 : r = 0

Result:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : r = 0
⊢ (C r * p).content = normalize r * p.content

case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (C r * p).content = normalize r * p.content

Proof state:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : r = 0
⊢ (C r * p).content = normalize r * p.content

Tactic:
simp [h0]

Result:
no goals