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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝⁴ : CommRing α
inst✝³ : FunLike F α R
inst✝² : ZeroHomClass F α R
inst✝¹ : NonnegHomClass F α R
inst✝ : SubmultiplicativeHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a b : α
⊢ ∃ m < n + 1, f ((a + b) ^ n) ≤ f (a ^ m) * f (b ^ (n - m))

Tactic:
obtain ⟨m, hm_lt, hM⟩ := finset_image_add (by aesop) (by aesop) hna
    (fun m => a ^ m * b ^ (n - m) * ↑(n.choose m)) (Finset.range (n + 1))
  simp only [Finset.nonempty_range_iff, ne_eq, Nat.succ_ne_zero, not_false_iff, Finset.mem_range,
    forall_true_left] at hm_lt
  refine ⟨m, hm_lt, ?_⟩
  simp only [← add_pow] at hM
  rw [mul_comm] at hM
  exact le_trans hM (le_trans (nmul_le hna) (map_mul_le_mul _ _ _))

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
⊢ (x * y).coeff (x.order + y.order) = x.leadingCoeff * y.leadingCoeff

Tactic:
simp only [← of_symm_smul_of_eq_mul]

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
⊢ ((HahnModule.of R).symm (x • (HahnModule.of R) y)).coeff (x.order + y.order) = x.leadingCoeff * y.leadingCoeff
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
⊢ (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff

Tactic:
simp only [leadingCoeff_eq, order_mul_of_ne_zero h, coeff_mul_order_add_order]

Goal state after:
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
k : K
x : M
hk : ¬k = 0
c : FiniteArchimedeanClass M
this : f.evalCoeff (k • x) c = k • f.evalCoeff x c
⊢ { coeff := f.evalCoeff (k • x), isPWO_support' := ⋯ }.coeff c =
    (k • { coeff := f.evalCoeff x, isPWO_support' := ⋯ }).coeff c

Tactic:
simpa using this

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case mpr
K : Type u
inst✝² : Field K
Γ₁ : Type u_2
Γ₂ : Type u_3
inst✝¹ : LinearOrderedCommGroupWithZero Γ₁
inst✝ : LinearOrderedCommGroupWithZero Γ₂
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
h : v₁.valuationSubring = v₂.valuationSubring
x : K
this : x ∈ v₁.valuationSubring ↔ x ∈ v₂.valuationSubring
⊢ v₁ x ≤ 1 ↔ v₂ x ≤ 1

Tactic:
simpa using this

Goal state after:
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a : G
s : Set G
ha : a ∈ s
b : G
hb : b ∈ ↑(stabilizer G s)
⊢ b <• a ∈ b •> s

Tactic:
exact smul_mem_smul_set ha

Goal state after:
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Finset α
⊢ s ⊆ a • s ↔ ↑s ⊆ ↑(a • s)

Tactic:
Finset.coe_subset

Goal state after:
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Finset α
⊢ s ⊆ a • s ↔ s ⊆ a • s
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Finset α
⊢ a • s ⊆ s ↔ ↑(a • s) ⊆ ↑s

Tactic:
Finset.coe_subset

Goal state after:
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Finset α
⊢ a • s ⊆ s ↔ a • s ⊆ s
Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree

Goal state before:
pp: case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
this : DecidableEq Fq := Classical.decEq Fq
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : ¬p + q = 0
⊢ (if p + q = 0 then 0 else ↑(Fintype.card Fq) ^ (p + q).natDegree) ≤
    (if p = 0 then 0 else ↑(Fintype.card Fq) ^ p.natDegree) + if q = 0 then 0 else ↑(Fintype.card Fq) ^ q.natDegree

Tactic:
simp only [hpq, hp, hq, if_false]

Goal state after:
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
this : DecidableEq Fq := Classical.decEq Fq
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : ¬p + q = 0
⊢ ↑(Fintype.card Fq) ^ (p + q).natDegree ≤ ↑(Fintype.card Fq) ^ p.natDegree + ↑(Fintype.card Fq) ^ q.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
f : R[X]
⊢ f.IsMonicOfDegree 2 ↔ ∃ a b, f = X ^ 2 - C a * X + C b

Tactic:
by
  refine ⟨fun H ↦ ?_, fun ⟨a, b, h⟩ ↦ h ▸ isMonicOfDegree_sub_add_two a b⟩
  simp only [sub_eq_add_neg, ← neg_mul, ← map_neg]
  obtain ⟨a, b, h⟩ := isMonicOfDegree_two_iff.mp H
  exact ⟨-a, b, (neg_neg a).symm ▸ h⟩

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree

pp: case neg
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree

Tactic:
· rw [hp, zero_mul, natTrailingDegree_zero, mul_zero]

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : Std.Antisymm r
x y : α
xs : List α
hxy : x ≠ y
h : (r x y ∧ ∀ (a : α), a ∈ xs → r x a) ∧ (∀ (a' : α), a' ∈ xs → r y a') ∧ Pairwise r xs
this : ¬x ∈ xs
⊢ (if x ≠ y then x :: (y :: xs).dedup else destutter (fun x1 x2 ↦ x1 ≠ x2) (x :: xs)) = (x :: y :: xs).dedup

Tactic:
if_pos hxy,

Goal state after:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : Std.Antisymm r
x y : α
xs : List α
hxy : x ≠ y
h : (r x y ∧ ∀ (a : α), a ∈ xs → r x a) ∧ (∀ (a' : α), a' ∈ xs → r y a') ∧ Pairwise r xs
this : ¬x ∈ xs
⊢ x :: (y :: xs).dedup = (x :: y :: xs).dedup
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
n : ℕ
⊢ (X ^ (n + 1) * p).smeval x = x ^ (n + 1) * p.smeval x

Tactic:
rw [add_comm, npow_add, mul_assoc, npow_one, smeval_X_mul, smeval_X_pow_mul n, npow_add,
      smeval_X_pow_assoc, npow_one]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
h : ∀ (a : R), ¬X - C a ∣ p
q : R[X]
hq : q.Monic
hq1 : q.natDegree = 1
⊢ ¬X - -C (q.coeff 0) ∣ p

Tactic:
← C_neg

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
h : ∀ (a : R), ¬X - C a ∣ p
q : R[X]
hq : q.Monic
hq1 : q.natDegree = 1
⊢ ¬X - C (-q.coeff 0) ∣ p
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree < n
⊢ sumIDeriv p = ∑ i ∈ range n, (⇑derivative)^[i] p

Tactic:
by
  dsimp [sumIDeriv]
  exact Finsupp.sum_of_support_subset _ (by simp [hn]) _ (by simp)

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
⊢ sumIDeriv p = ∑ i ∈ range (n + 1), (⇑derivative)^[i] p

Tactic:
by
  dsimp [sumIDeriv]
  exact Finsupp.sum_of_support_subset _ (by simp [hn]) _ (by simp)

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

Goal state before:
pp: case e'_2.e'_5
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
h : ∀ (x : ℕ), 1 ≤ x → x ≤ q → (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1)
⊢ ∑ i ∈ range q,
      eval r
        ((q.choose (i + 1) * q.descFactorial (q - (i + 1))) • (X - C r) ^ (q - (q - (i + 1))) *
          (⇑derivative)^[i + 1] p') =
    0

Tactic:
apply sum_eq_zero

Goal state after:
case e'_2.e'_5
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
h : ∀ (x : ℕ), 1 ≤ x → x ≤ q → (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1)
⊢ ∀ x ∈ range q,
    eval r
        ((q.choose (x + 1) * q.descFactorial (q - (x + 1))) • (X - C r) ^ (q - (q - (x + 1))) *
          (⇑derivative)^[x + 1] p') =
      0
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case refine_1
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ ↑u ^ 2 + (↑v ^ 2 + ↑w ^ 2) = 3

Tactic:
← Units.val_pow_eq_pow_val,

Goal state after:
case refine_1
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ ↑(u ^ 2) + (↑(v ^ 2) + ↑(w ^ 2)) = 3
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 : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
⊢ (aeval r) ((⇑derivative)^[q] p) = q ! • eval r p'

Tactic:
by
  have h (x) (h : 1 ≤ x) (h' : x ≤ q) :
      (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1) := by
    rw [← pow_add, add_tsub_cancel_of_le]
    rwa [tsub_tsub_cancel_of_le h']
  rw [aeval_def, eval₂_eq_eval_map, ← iterate_derivative_map]
  simp_rw [hp, iterate_derivative_mul, iterate_derivative_X_sub_pow, ← smul_mul_assoc, smul_smul]
  rw [sum_range_succ', Nat.choose_zero_right, one_mul, tsub_zero, Nat.descFactorial_self, tsub_self,
    pow_zero, smul_mul_assoc, one_mul, Function.iterate_zero_apply, eval_add, eval_smul]
  convert! zero_add _
  rw [eval_finsetSum]
  apply sum_eq_zero
  intro x hx
  rw [h (x + 1) le_add_self (Nat.add_one_le_iff.mpr (mem_range.mp hx)), pow_one,
    eval_mul, eval_smul, eval_mul, eval_sub, eval_X, eval_C, sub_self, zero_mul,
    smul_zero, zero_mul]

Goal state after:
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]
r : A
⊢ eval₂ (algebraMap R A) r (sumIDeriv p) = eval₂ (RingHom.id A) r (map (algebraMap R A) (sumIDeriv p))

Tactic:
eval₂_map,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
r : A
⊢ eval₂ (algebraMap R A) r (sumIDeriv p) = eval₂ ((RingHom.id A).comp (algebraMap R A)) r (sumIDeriv p)
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case inr.refine_2.e_a.e_a
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this✝ : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
⊢ ∑ x ∈ range (q - 1), (aeval r) ((⇑derivative)^[x] p) = 0

Tactic:
apply sum_eq_zero

Goal state after:
case inr.refine_2.e_a.e_a
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := ⋯
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this✝ : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
⊢ ∀ x ∈ range (q - 1), (aeval r) ((⇑derivative)^[x] p) = 0
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

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

Tactic:
← C_neg

Goal state after:
case inr
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : -p = C (-↑u) * X ^ k + C (-↑v) * X ^ m + C (-↑w) * X ^ n
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x) (-↑v) ↑z
h1 : ↑y = -↑v
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
x : QuadraticAlgebra R a b
⊢ norm (star x) = norm x

Tactic:
simp only [norm, MonoidHom.coe_mk, OneHom.coe_mk, re_star, im_star, mul_neg, neg_mul, neg_neg,
    sub_left_inj]
  ring

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

Goal state before:
pp: K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
hz : ¬norm z = 0
⊢ (algebraMap K (QuadraticAlgebra K a b)) ((norm z)⁻¹ * norm z) = 1

Tactic:
inv_mul_cancel₀ hz,

Goal state after:
K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
hz : ¬norm z = 0
⊢ (algebraMap K (QuadraticAlgebra K a b)) 1 = 1
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
ih : ∀ (P : R[X]), Multiset.countP (fun x ↦ 0 < x) P.roots = n✝ → n✝ ≤ P.signVariations
P : R[X]
h : Multiset.countP (fun x ↦ 0 < x) P.roots = n✝ + 1
hp : P ≠ 0
⊢ ∃ x ∈ P.roots, 0 < x

Tactic:
grind [Multiset.countP_pos]

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
x y z : Conj G
⊢ x * (y * z * y⁻¹) * x⁻¹ = x * y * x⁻¹ * (x * z * x⁻¹) * (x * y * x⁻¹)⁻¹

Tactic:
simp [mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
x y : Conj G
⊢ (MulEquiv.symm (MulAut.conj x)) ((MulAut.conj x) y) = y

Tactic:
simp [mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: Q : Type u_1
inst✝¹ : Quandle Q
G : Type u_2
inst✝ : Group G
x y : Conj G
⊢ (MulAut.conj x) ((MulEquiv.symm (MulAut.conj x)) y) = y

Tactic:
simp [mul_assoc]

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.i * (q.j * q.j) = c₃ • q.i

Tactic:
j_mul_j,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.i * c₃ • 1 = c₃ • q.i
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ c₂ • (q.j * q.j) - q.k * q.j = (c₂ * c₃) • 1 - c₃ • q.i

Tactic:
j_mul_j,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ c₂ • c₃ • 1 - q.k * q.j = (c₂ * c₃) • 1 - c₃ • q.i
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ c₂ • (q.i * (q.j * q.j)) - (c₁ • q.j + c₂ • (q.i * q.j)) * q.j = -((c₁ * c₃) • 1)

Tactic:
j_mul_j,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ c₂ • (q.i * c₃ • 1) - (c₁ • q.j + c₂ • (q.i * q.j)) * q.j = -((c₁ * c₃) • 1)
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ c₂ • (q.i * c₃ • 1) - (c₁ • (q.j * q.j) + c₂ • (q.i * q.j) * q.j) = -((c₁ * c₃) • 1)

Tactic:
j_mul_j,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ c₂ • (q.i * c₃ • 1) - (c₁ • c₃ • 1 + c₂ • (q.i * q.j) * q.j) = -((c₁ * c₃) • 1)
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case ofNat
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne
this : inst₁.toNatCast = inst₂.toNatCast
toAddMonoid_eq✝ : inst₁.toAddMonoid = inst₂.toAddMonoid
toNeg_eq✝ : inst₁.toNeg = inst₂.toNeg
toSub_eq✝ : inst₁.toSub = inst₂.toSub
toZSMul_eq✝ : inst₁.toZSMul = inst₂.toZSMul
n : ℕ
⊢ IntCast.intCast (Int.ofNat n) = IntCast.intCast (Int.ofNat n)

Tactic:
rewrite [Int.ofNat_eq_natCast, inst₁.intCast_ofNat, inst₂.intCast_ofNat]; congr

Goal state after:
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
⊢ closure {x | ∃ x_1, x_1 ≠ 0 ∧ x_1 * x_1 = x} = sumNonzeroSq R

Tactic:
refine closure_eq_of_le (fun x hx ↦ by aesop) (fun x hx ↦ ?_)

Goal state after:
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
x : R
hx : x ∈ sumNonzeroSq R
⊢ x ∈ closure {x | ∃ x_1, x_1 ≠ 0 ∧ x_1 * x_1 = x}
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: case refine_1
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
⊢ T ∈ (toEndRingHom α).rangeS → T ∈ Subsemiring.centralizer (Set.range ⇑L ∪ Set.range ⇑R)

Tactic:
rintro ⟨f, rfl⟩ S (⟨a, rfl⟩ | ⟨b, rfl⟩)

Goal state after:
case refine_1.inl
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
a : α
⊢ L a * (toEndRingHom α) f = (toEndRingHom α) f * L a

case refine_1.inr
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
b : α
⊢ R b * (toEndRingHom α) f = (toEndRingHom α) f * R b
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonAssocSemiring α
T : CentroidHom α
x✝ : α
⊢ (centerToCentroid ((fun T ↦ ⟨T 1, ⋯⟩) T)) x✝ = T x✝

Tactic:
centerToCentroid_apply,

Goal state after:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonAssocSemiring α
T : CentroidHom α
x✝ : α
⊢ ↑((fun T ↦ ⟨T 1, ⋯⟩) T) * x✝ = T x✝
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mk
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 → R → Prop
toQuot✝ : Quot (Rel r)
a✝ : R
⊢ 0 * { toQuot := Quot.mk (Rel r) a✝ } = 0

Tactic:
simp only [mul_quot, ← zero_quot, zero_mul]

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

Goal state before:
pp: R : Type u
inst✝ : LinearOrderedAddCommMonoidWithTop R
x✝ : Tropical R
⊢ untrop (0 * x✝) = untrop 0

Tactic:
simp [top_add]

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

Goal state before:
pp: X✝ X : LocallyRingedSpace
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
⊢ ↑(X.presheaf.1 U) →+* PUnit.{u + 1}

Tactic:
refine ⟨⟨⟨0, ?_⟩, ?_⟩, ?_, ?_⟩ <;> intros

Goal state after:
case refine_1
X✝ X : LocallyRingedSpace
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
⊢ 0 1 = 1

case refine_2
X✝ X : LocallyRingedSpace
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
x✝ y✝ : ↑(X.presheaf.1 U)
⊢ { toFun := 0, map_one' := ?refine_1 }.toFun (x✝ * y✝) =
    { toFun := 0, map_one' := ?refine_1 }.toFun x✝ * { toFun := 0, map_one' := ?refine_1 }.toFun y✝

case refine_3
X✝ X : LocallyRingedSpace
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
⊢ (↑{ toFun := 0, map_one' := ?refine_1, map_mul' := ⋯ }).toFun 0 = 0

case refine_4
X✝ X : LocallyRingedSpace
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
x✝ y✝ : ↑(X.presheaf.1 U)
⊢ (↑{ toFun := 0, map_one' := ?refine_1, map_mul' := ⋯ }).toFun (x✝ + y✝) =
    (↑{ toFun := 0, map_one' := ?refine_1, map_mul' := ⋯ }).toFun x✝ +
      (↑{ toFun := 0, map_one' := ?refine_1, map_mul' := ⋯ }).toFun y✝
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
⊢ (X.ofRestrict ⋯).c = eqToHom ⋯

Tactic:
ext
  dsimp [ofRestrict]
  erw [eqToHom_map, eqToHom_app]
  simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X : Scheme
x : ↥X
U : X.Opens
hxU : x ∈ U
V : TopologicalSpace.Opens ↑X.toTopCat
hxV : x ∈ V
R : CommRingCat
e : X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)
this : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ (Opens.map (e.inv.base ≫ V.inclusion')).obj U
r : ↑R
hr : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ ↑(PrimeSpectrum.basicOpen r)
hr' : ↑(PrimeSpectrum.basicOpen r) ⊆ ↑((Opens.map (e.inv.base ≫ V.inclusion')).obj U)
f : Spec (CommRingCat.of (Localization.Away r)) ⟶ X :=
  Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) ≫ { toLRSHom' := e.inv ≫ X.ofRestrict ⋯ }
⊢ x ∈ ⇑{ toLRSHom' := e.inv ≫ X.ofRestrict ⋯ } '' ↑(PrimeSpectrum.basicOpen r) ∧
    ⇑{ toLRSHom' := e.inv ≫ X.ofRestrict ⋯ } '' ↑(PrimeSpectrum.basicOpen r) ⊆ ↑U

Tactic:
exact ⟨⟨_, hr, congr(($(e.hom_inv_id).base ⟨x, hxV⟩).1)⟩, Set.image_subset_iff.mpr hr'⟩

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
inst✝ : IsOpenImmersion g
⊢ IsOpenImmersion (limit.π (cospan f g) WalkingCospan.one)

Tactic:
rw [← limit.w (cospan f g) WalkingCospan.Hom.inl, cospan_map_inl]
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: case pos
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↥X
hx : x ∈ Set.range ⇑iU
⊢ x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W) ↔ x ∈ ↑(f ⁻¹ᵁ iV ''ᵁ W)

pp: case neg
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↥X
hx : x ∉ Set.range ⇑iU
⊢ x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W) ↔ x ∈ ↑(f ⁻¹ᵁ iV ''ᵁ W)

Tactic:
· obtain ⟨x, rfl⟩ := hx
    simp only [SetLike.mem_coe, Opens.map_coe, Set.mem_preimage, ← Scheme.Hom.comp_apply, ← H.w]
    simp

Goal state after:
case neg
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↥X
hx : x ∉ Set.range ⇑iU
⊢ x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W) ↔ x ∈ ↑(f ⁻¹ᵁ iV ''ᵁ W)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst✝ : IsOpenImmersion g
⊢ IsOpenImmersion (limit.π (cospan f g) WalkingCospan.one)

Tactic:
rw [← limit.w (cospan f g) WalkingCospan.Hom.inl, cospan_map_inl]
  infer_instance

Goal state after: