mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
y' : M
hy'✝ : y' ∈ (f.extendFun hx).domain
hy' : y' ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = y'
k : K
hk : k • x = b
⊢ toLex ((truncLTLinearMap K c) (ofLex (↑↑f ⟨a, ha⟩))) +
      (RingHom.id K) k • toLex ((truncLTLinearMap K c) (ofLex (f.eval x))) ∈
    ((↑f).supSpanSingleton x (f.eval x) hx).toFun.range

Tactic:
refine Submodule.add_mem _ ?_ (Submodule.smul_mem _ _ ?_)

Goal state after:
case refine_1
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
y' : M
hy'✝ : y' ∈ (f.extendFun hx).domain
hy' : y' ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = y'
k : K
hk : k • x = b
⊢ toLex ((truncLTLinearMap K c) (ofLex (↑↑f ⟨a, ha⟩))) ∈ ((↑f).supSpanSingleton x (f.eval x) hx).toFun.range

case refine_2
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
y' : M
hy'✝ : y' ∈ (f.extendFun hx).domain
hy' : y' ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = y'
k : K
hk : k • x = b
⊢ toLex ((truncLTLinearMap K c) (ofLex (f.eval x))) ∈ ((↑f).supSpanSingleton x (f.eval x) hx).toFun.range
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case a
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
⊢ f ≤ f.extend hx

Tactic:
change f.val ≤ (f.extend hx).val
    simpa [extend, extendFun] using! LinearPMap.left_le_sup _ _ _

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
r : R
⊢ (C r).natDegree < 1

Tactic:
rw [natDegree_C]; exact zero_lt_one

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
r : R
⊢ (C r).natDegree < 1

Tactic:
rw [natDegree_C]; exact zero_lt_one

Goal state after:
Module: Mathlib.Algebra.Polynomial.CoeffMem

Goal state before:
pp: case neg
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : ¬q.Monic
⊢ p.coeff i ∈ Mq ^ deg(p) * Mp

Tactic:
· rw [← one_mul (p.coeff i), ← one_pow p.natDegree]
    exact Submodule.mul_mem_mul (Submodule.pow_mem_pow Mq hq' _) (hp i)

Goal state after:
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ (p * q).mirror = p.mirror * q.mirror

Tactic:
rw [mirror, mirror, mirror, reverse_mul_of_domain, natTrailingDegree_mul hp hq, pow_add]

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ p.reverse * q.reverse * (X ^ p.natTrailingDegree * X ^ q.natTrailingDegree) =
    p.reverse * X ^ p.natTrailingDegree * (q.reverse * X ^ q.natTrailingDegree)
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
c : ℕ → R[X]
h :
  ∀ (k : ℕ),
    (c k).natDegree ≤ p.natDegree - q ∧
      ∀ (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
⊢ ∃ gp,
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) (sumIDeriv p) = q ! • (aeval r) gp

Tactic:
choose c_le hc using h

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
c : ℕ → R[X]
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - q
hc : ∀ (k : ℕ) (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
⊢ ∃ gp,
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) (sumIDeriv p) = q ! • (aeval r) gp
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case inr
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
h : p * p.mirror = q.mirror * q.mirror.mirror
hq : q.mirror = trinomial k (n - m' + k) n ↑u ↑v ↑w
hmul : ↑w * ↑u = ↑u * ↑w
⊢ q = p.mirror ∨ q.mirror = p.mirror

Tactic:
← mirror_eq_iff

Goal state after:
case inr
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
h : p * p.mirror = q.mirror * q.mirror.mirror
hq : q.mirror = trinomial k (n - m' + k) n ↑u ↑v ↑w
hmul : ↑w * ↑u = ↑u * ↑w
⊢ q.mirror = p ∨ q.mirror = p.mirror
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case isTrue.isTrue.cons
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h : 0 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
c₀ : R
cs : List R
hcs✝ : ((X - C η) * P).coeffList = P.leadingCoeff :: c₀ :: cs
hecs : ((X - C η) * P.eraseLead).coeffList = P.nextCoeff :: cs
h✝¹ : decide (SignType.sign c₀ ≠ 0) = true
h✝ : 1 ≠ SignType.sign c₀
r : SignType
rs : List SignType
hcs : List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs) = r :: rs
⊢ (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1 (r :: rs)).length ≤
    (1 :: List.destutter' (fun x1 x2 ↦ x1 ≠ x2) (SignType.sign c₀) (r :: rs)).length

Tactic:
rw [← List.destutter_cons', ← List.destutter_cons']
    grind [List.destutter_cons_cons]

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : CommSemiring R
z w : R
⊢ (algebraMap R (QuadraticAlgebra R a b)) z ∣ (algebraMap R (QuadraticAlgebra R a b)) w ↔ z ∣ w

Tactic:
algebraMap_dvd_iff

Goal state after:
R : Type u_1
a b : R
inst✝ : CommSemiring R
z w : R
⊢ z ∣ ((algebraMap R (QuadraticAlgebra R a b)) w).re ∧ z ∣ ((algebraMap R (QuadraticAlgebra R a b)) w).im ↔ z ∣ w
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
hz : z ∈ (QuadraticAlgebra R a b)⁰
⊢ norm z ∈ R⁰

Tactic:
← algebraMap_mem_nonZeroDivisors_iff,

Goal state after:
case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
hz : z ∈ (QuadraticAlgebra R a b)⁰
⊢ (algebraMap R (QuadraticAlgebra R ?m.89 ?m.90)) (norm z) ∈ (QuadraticAlgebra R ?m.89 ?m.90)⁰

R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
hz : z ∈ (QuadraticAlgebra R a b)⁰
⊢ R

R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
hz : z ∈ (QuadraticAlgebra R a b)⁰
⊢ R
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case succ.inr.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : ∀ m < d + 1, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : SignType.sign P.nextCoeff = 1
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations

Tactic:
have h₁ : nextCoeff P ≠ 0 := by simp [← sign_ne_zero, hs_nC]

Goal state after:
case succ.inr.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : ∀ m < d + 1, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : SignType.sign P.nextCoeff = 1
h₁ : P.nextCoeff ≠ 0
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case succ.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : ∀ m < d + 1, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : SignType.sign P.nextCoeff = -1
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations

Tactic:
have h₁ : nextCoeff P ≠ 0 := by simp [← sign_ne_zero, hs_nC]

Goal state after:
case succ.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : ∀ m < d + 1, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : SignType.sign P.nextCoeff = -1
h₁ : P.nextCoeff ≠ 0
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case succ
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : inst₁.toAddMonoid = inst₂.toAddMonoid
h_zero' : inst₁.toZero = inst₂.toZero
h_one' : inst₁.toOne = inst₂.toOne
n : ℕ
h : ↑n = ↑n
⊢ ↑n + 1 = ↑n + 1

Tactic:
h_add

Goal state after:
case succ
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : inst₁.toAddMonoid = inst₂.toAddMonoid
h_zero' : inst₁.toZero = inst₂.toZero
h_one' : inst₁.toOne = inst₂.toOne
n : ℕ
h : ↑n = ↑n
⊢ ↑n + 1 = ↑n + 1
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : inst₁.toAddMonoid = inst₂.toAddMonoid
h_zero' : inst₁.toZero = inst₂.toZero
h_one' : inst₁.toOne = inst₂.toOne
n : ℕ
⊢ ↑n = ↑n

Tactic:
induction n with
    | zero => rewrite [inst₁.natCast_zero, inst₂.natCast_zero]
              exact congrArg (@Zero.zero R) h_zero'
    | succ n h => rw [inst₁.natCast_succ, inst₂.natCast_succ, h_add]
                  exact congrArg₂ _ h h_one

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝ : AddCommMonoid k
f : G ≃ H
a : G
b : k
⊢ equivMapDomain f (single a b) = single (f a) b

Tactic:
apply coeff_injective
  simp_rw [coeff_equivMapDomain, single, Finsupp.equivMapDomain_single]

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

Goal state before:
pp: M : Type u_4
α : Type u_5
inst✝¹ : AddCommMonoid M
f : SkewMonoidAlgebra M α
a a' : α
b : M
inst✝ : DecidableEq α
⊢ (f.update a b).coeff a' = if a' = a then b else f.coeff a'

Tactic:
by
  simp [coeff_update, Function.update_apply]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case refine_1
R : Type uR
inst✝⁵ : Semiring R
S : Type uS
inst✝⁴ : CommSemiring S
T : Type uT
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
r✝ : R → R → Prop
inst✝¹ : Semiring T
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h : x ∈ Ideal.ofRel r
⊢ ∀ x ∈ {x | ∃ a b, r a b ∧ x + b = a}, (mkRingHom r) x = 0

Tactic:
rintro y ⟨a, b, h, su⟩

Goal state after:
case refine_1
R : Type uR
inst✝⁵ : Semiring R
S : Type uS
inst✝⁴ : CommSemiring S
T : Type uT
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
r✝ : R → R → Prop
inst✝¹ : Semiring T
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
h✝ : x ∈ Ideal.ofRel r
y a b : B
h : r a b
su : y + b = a
⊢ (mkRingHom r) y = 0
Module: Mathlib.Algebra.Star.CHSH

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A₀ A₁ B₀ B₁ : R
A₀_inv : A₀ ^ 2 = 1
A₁_inv : A₁ ^ 2 = 1
B₀_inv : B₀ ^ 2 = 1
B₁_inv : B₁ ^ 2 = 1
⊢ (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) =
    4 * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁)

Tactic:
by
  grind

Goal state after:
Module: Mathlib.Algebra.Star.CHSH

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : IsOrderedModule ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (√2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁
w : √2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ = (√2)⁻¹ • (P ^ 2 + Q ^ 2)
⊢ star P = P

Tactic:
simp only [P, star_smul, star_add, star_sub, star_id_of_comm, T.A₀_sa, T.A₁_sa, T.B₀_sa]

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p q : SkewPolynomial R
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
h_add : ∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂
⊢ (p + q).sum f = p.sum f + q.sum f

Tactic:
by
  simp only [sum_def']
  exact SkewMonoidAlgebra.sum_add_index (fun n _ ↦ hf (toAdd n)) (fun n _ ↦ h_add (toAdd n))

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
inst✝⁴ : AddMonoid k
inst✝³ : SMul S₁ S₂
inst✝² : SMulZeroClass S₁ k
inst✝¹ : SMulZeroClass S₂ k
inst✝ : IsScalarTower S₁ S₂ k
x✝² : S₁
x✝¹ : S₂
x✝ : SkewMonoidAlgebra k G
coeff✝ : G →₀ k
⊢ (x✝² • x✝¹) • { coeff := coeff✝ } = x✝² • x✝¹ • { coeff := coeff✝ }

Tactic:
by simp_rw [← ofCoeff_smul, smul_assoc]

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Semiring k
inst✝² : Mul G
inst✝¹ : SMulZeroClass G k
inst✝ : DecidableEq G
f g : SkewMonoidAlgebra k G
x : G
⊢ (f * g).coeff x = f.sum fun a₁ b₁ ↦ g.sum fun a₂ b₂ ↦ if a₁ * a₂ = x then b₁ * a₁ • b₂ else 0

Tactic:
rw [mul_def, coeff_sum]; congr; ext
  rw [coeff_sum]; congr; ext
  exact coeff_single_apply

Goal state after:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a : αˢʸᵐ
⊢ unsym (a * a) = unsym a * unsym a

Tactic:
by
  rw [mul_def, unsym_sym, ← two_mul, invOf_mul_cancel_left]

Goal state after:
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → WithTop R
h : s.Nonempty
⊢ trop (sInf (f '' ↑s)) = ∑ i ∈ s, trop (f i)

Tactic:
← inf'_eq_csInf_image _ h,

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → WithTop R
h : s.Nonempty
⊢ trop (s.inf' h f) = ∑ i ∈ s, trop (f i)
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → Tropical (WithTop R)
h : s.Nonempty
⊢ untrop (∑ i ∈ s, f i) = sInf (untrop ∘ f '' ↑s)

Tactic:
← inf'_eq_csInf_image _ h,

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → Tropical (WithTop R)
h : s.Nonempty
⊢ untrop (∑ i ∈ s, f i) = s.inf' h (untrop ∘ f)
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
⊢ a * b * (a * a) = a * (b * (a * a))

Tactic:
by
    have commute_half_left := fun a : α => by
      have := (Commute.one_left a).add_left (Commute.one_left a)
      rw [one_add_one_eq_two] at this
      exact this.invOf_left.eq
    calc a * b * (a * a)
      _ = sym (⅟2 * ⅟2 * (unsym a * unsym b * unsym (a * a) +
          unsym b * unsym a * unsym (a * a) +
          unsym (a * a) * unsym a * unsym b +
          unsym (a * a) * unsym b * unsym a)) := ?_
      _ = sym (⅟2 * (unsym a *
          unsym (sym (⅟2 * (unsym b * unsym (a * a) + unsym (a * a) * unsym b))) +
          unsym (sym (⅟2 * (unsym b * unsym (a * a) + unsym (a * a) * unsym b))) * unsym a)) := ?_
      _ = a * (b * (a * a)) := ?_
    -- Rearrange LHS
    · rw [mul_def, mul_def a b, unsym_sym, ← mul_assoc, ← commute_half_left (unsym (a * a)),
        mul_assoc, mul_assoc, ← mul_add, ← mul_assoc, add_mul, mul_add (unsym (a * a)),
        ← add_assoc, ← mul_assoc, ← mul_assoc]
    · rw [unsym_sym, sym_inj, ← mul_assoc, ← commute_half_left (unsym a), mul_assoc (⅟2) (unsym a),
        mul_assoc (⅟2) _ (unsym a), ← mul_add, ← mul_assoc]
      conv_rhs => rw [mul_add (unsym a)]
      rw [add_mul, ← add_assoc, ← mul_assoc, ← mul_assoc]
      rw [unsym_mul_self]
      rw [← mul_assoc, ← mul_assoc, ← mul_assoc, ← mul_assoc, ← sub_eq_zero, ← mul_sub]
      convert! mul_zero (⅟(2 : α) * ⅟(2 : α))
      rw [add_sub_add_right_eq_sub, add_assoc, add_assoc, add_sub_add_left_eq_sub, add_comm,
        add_sub_add_right_eq_sub, sub_eq_zero]
    -- Rearrange RHS
    · rw [← mul_def, ← mul_def]

Goal state after:
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ✝ : Type u_1
inst✝¹⁴ : PartialOrder Γ✝
R✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
inst✝¹³ : CommRing R✝
inst✝¹² : AddCommGroup V✝
inst✝¹¹ : Module R✝ V✝
inst✝¹⁰ : AddCommGroup W✝
inst✝⁹ : Module R✝ W✝
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u : U
⊢ ∀ (x : Γ'), ¬A (((of R).symm (B u)).coeff x) = 0 → ¬((of R).symm (B u)).coeff x = 0

Tactic:
intro g' hg' hAB

Goal state after:
Γ✝ : Type u_1
inst✝¹⁴ : PartialOrder Γ✝
R✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
inst✝¹³ : CommRing R✝
inst✝¹² : AddCommGroup V✝
inst✝¹¹ : Module R✝ V✝
inst✝¹⁰ : AddCommGroup W✝
inst✝⁹ : Module R✝ W✝
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u : U
g' : Γ'
hg' : ¬A (((of R).symm (B u)).coeff g') = 0
hAB : ((of R).symm (B u)).coeff g' = 0
⊢ False
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: case w
C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
⊢ g₁.base = g₂.base

Tactic:
have := congr_arg PresheafedSpace.Hom.base eq

Goal state after:
case w
C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this✝ : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
this : (g₁ ≫ X.ofRestrict hf).base = (g₂ ≫ X.ofRestrict hf).base
⊢ g₁.base = g₂.base
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : ↥U → Opens ↑↑X.toPresheafedSpace
iVU : (x : ↥U) → V x ⟶ U
m : ∀ (x : ↥U), ↑x ∈ V x
h_unit : ∀ (x : ↥U), IsUnit ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f)
hcover : U ≤ iSup V
g : (x : ↥U) → ↑(X.presheaf.obj (op (V x)))
hg : ∀ (x : ↥U), (ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f * g x = 1
x y : ↥U
z : ↑↑X.toPresheafedSpace
hzVx : z ∈ ↑(V x)
hzVy : z ∈ ↑(V y)
⊢ (ConcreteCategory.hom (X.presheaf.germ (V x) z hzVx)) ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f) *
      (ConcreteCategory.hom (X.presheaf.germ (V x) z hzVx)) (g x) =
    (ConcreteCategory.hom (X.presheaf.germ (V x) z hzVx)) ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f) *
      (ConcreteCategory.hom (X.presheaf.germ (V y) z hzVy)) (g y)

Tactic:
rw [← map_mul, hg x, germ_res_apply X.presheaf _ _ _ f,
      ← germ_res_apply X.presheaf (iVU y) z hzVy f, ← map_mul, (hg y), map_one, map_one]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
this :
  X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (inv i))) ((ConcreteCategory.hom (X.presheaf.map i)) f)) =
    unop U ⊓ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)
⊢ X.basicOpen f ≤ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)

Tactic:
← CommRingCat.comp_apply,

Goal state after:
case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
this :
  X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i ≫ X.presheaf.map (inv i))) f) =
    unop U ⊓ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)
⊢ X.basicOpen f ≤ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)