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
⊢ StrictMono ↑(f.extendFun hx)

Tactic:
have hx' {c : K} (hc : c ≠ 0) : -c • x ∉ f.val.domain := by
    contrapose hx
    rwa [neg_smul, neg_mem_iff, Submodule.smul_mem_iff _ hc] at hx
  -- only need to prove `0 < f v` for `0 < v = z - y`
  intro y z hyz
  rw [← sub_pos] at hyz
  apply lt_of_sub_pos
  rw [← LinearPMap.map_sub]
  obtain hyzmem := (z - y).prop
  nth_rw 1 [extendFun, LinearPMap.domain_supSpanSingleton] at hyzmem
  -- decompose `v = a + c • x`, reducing this to eval_lt
  obtain ⟨a, ha, b, hb, hab⟩ := Submodule.mem_sup.mp hyzmem
  have : z - y = ⟨a + b, hab.symm ▸ (z - y).prop⟩ := by simp_rw [hab]
  rw [this] at ⊢ hyz
  have habpos : 0 < a + b := by exact hyz
  obtain ⟨c, hc⟩ := Submodule.mem_span_singleton.mp hb
  rw [← hc] at habpos
  simp_rw [← hc, extendFun]
  rw [LinearPMap.supSpanSingleton_apply_mk _ _ _ hx _ ha]
  suffices f.eval (-c • x) < f.val ⟨a, ha⟩ by
    rw [eval_smul, neg_smul] at this
    exact neg_lt_iff_pos_add.mp this
  have hac : -c • x < a := by
    rw [neg_smul]
    exact neg_lt_iff_pos_add.mpr habpos
  by_cases hc : c = 0
  · rw [hc] at ⊢ hac
    suffices f.val 0 < f.val ⟨a, ha⟩ by simpa using! this
    exact f.prop.strictMono (by simpa using! hac)
  · exact f.eval_lt (hx' hc) ⟨a, ha⟩ hac

Goal state after:
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : 0 ≤ mk x
a : ℤ
ha : ↑a < x
b : ℤ
hb : x < ↑b
⊢ ↑b ∈ {r | x < f r}

Tactic:
simpa using hb

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
⊢ P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)

Tactic:
by_cases hdp : P.natDegree = 0

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : P.natDegree = 0
⊢ P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)

case neg
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
⊢ P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Differential A
n : ℕ
x : A
⊢ mapCoeffs ((monomial n) x) = (monomial n) x′

Tactic:
simp [mapCoeffs]

Goal state after:
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: case e'_3.e'_5
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : Differential A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Differential R
inst✝¹ : Algebra A R
inst✝ : DifferentialAlgebra A R
x : R
p : A[X]
⊢ (aeval x) (mapCoeffs p) =
    (PolynomialModule.eval x) ((PolynomialModule.map R (Algebra.linearMap A R)) (deriv.mapCoeffs p))

Tactic:
simp [mapCoeffs]

Goal state after:
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: A : Type u_1
inst✝¹¹ : CommRing A
inst✝¹⁰ : Differential A
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : Differential R
inst✝⁷ : Algebra A R
inst✝⁶ : DifferentialAlgebra A R
R' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : Differential R'
inst✝³ : Algebra A R'
inst✝² : DifferentialAlgebra A R'
inst✝¹ : IsDomain R'
inst✝ : Nontrivial R
f : R →ₐ[A] R'
hf : Function.Injective ⇑f
x : R
h : IsSeparable A x
p : A[X] := minpoly A x
⊢ f x′ = (f x)′

Tactic:
apply mul_left_cancel₀ (a := aeval (f x) (derivative p))

Goal state after:
case ha
A : Type u_1
inst✝¹¹ : CommRing A
inst✝¹⁰ : Differential A
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : Differential R
inst✝⁷ : Algebra A R
inst✝⁶ : DifferentialAlgebra A R
R' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : Differential R'
inst✝³ : Algebra A R'
inst✝² : DifferentialAlgebra A R'
inst✝¹ : IsDomain R'
inst✝ : Nontrivial R
f : R →ₐ[A] R'
hf : Function.Injective ⇑f
x : R
h : IsSeparable A x
p : A[X] := ⋯
⊢ (aeval (f x)) (derivative p) ≠ 0

case h
A : Type u_1
inst✝¹¹ : CommRing A
inst✝¹⁰ : Differential A
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : Differential R
inst✝⁷ : Algebra A R
inst✝⁶ : DifferentialAlgebra A R
R' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : Differential R'
inst✝³ : Algebra A R'
inst✝² : DifferentialAlgebra A R'
inst✝¹ : IsDomain R'
inst✝ : Nontrivial R
f : R →ₐ[A] R'
hf : Function.Injective ⇑f
x : R
h : IsSeparable A x
p : A[X] := ⋯
⊢ (aeval (f x)) (derivative p) * f x′ = (aeval (f x)) (derivative p) * (f x)′
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hq : q.IsMonicOfDegree n
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : p.Monic
this : (p * q).natDegree = m + n
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
rw [h₂.leadingCoeff, hq.leadingCoeff_eq, one_mul]

Goal state after:
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hq : q.IsMonicOfDegree n
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : p.Monic
this : (p * q).natDegree = m + n
⊢ 1 ≠ 0
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a : α
⊢ destutter' R a l <+ a :: l

Tactic:
induction l generalizing a with
  | nil => simp
  | cons b l hl =>
    rw [destutter']
    split_ifs
    · exact Sublist.cons_cons a (hl b)
    · exact (hl a).trans ((l.sublist_cons_self b).cons_cons a)

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case cons
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hb : ∀ {a : α}, IsChain R (a :: l) → destutter' R a l = a :: l
a : α
h✝ : IsChain R (a :: b :: l)
h : R a b
hc : IsChain R (b :: l)
⊢ destutter' R a (b :: l) = a :: b :: l

Tactic:
rw [l.destutter'_cons_pos h, hb hc]

Goal state after:
Module: Mathlib.Data.List.Destutter

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

Tactic:
h.2.destutter_eq_dedup

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : Std.Antisymm r
x y : α
xs : List α
h : (∀ (a' : α), a' ∈ y :: xs → r x a') ∧ Pairwise r (y :: xs)
⊢ (if x ≠ y then x :: (y :: xs).dedup else destutter (fun x1 x2 ↦ x1 ≠ x2) (x :: xs)) = (x :: y :: xs).dedup
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ (trinomial k m n u v w).coeff n = w

Tactic:
by
  rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow,
    if_neg (hkm.trans hmn).ne', if_neg hmn.ne', if_pos rfl, zero_add, zero_add]

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

Goal state before:
pp: case right
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
r : A
p' : A[X]
hp : 0 = (X - C r) ^ (q - 1) * p'
⊢ 0 = (q - 1)! • eval r p'

Tactic:
replace hp := (mul_eq_zero.mp hp.symm).resolve_left ?_

Goal state after:
case right.refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
r : A
p' : A[X]
hp : p' = 0
⊢ 0 = (q - 1)! • eval r p'

case right.refine_1
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
r : A
p' : A[X]
hp : 0 = (X - C r) ^ (q - 1) * p'
⊢ ¬(X - C r) ^ (q - 1) = 0
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
r : R
⊢ (∀ (x : R), x * r = 0 → x = 0) →
    ∀ (x : QuadraticAlgebra R a b), x * (algebraMap R (QuadraticAlgebra R a b)) r = 0 → x = 0

Tactic:
intro h

Goal state after:
case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
r : R
h : ∀ (x : R), x * r = 0 → x = 0
⊢ ∀ (x : QuadraticAlgebra R a b), x * (algebraMap R (QuadraticAlgebra R a b)) r = 0 → x = 0
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case mp
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ (∀ (x : R), x * norm z = 0 → x = 0) → ∀ (x : QuadraticAlgebra R a b), x * z = 0 → x = 0

Tactic:
intro h

Goal state after:
case mp
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
h : ∀ (x : R), x * norm z = 0 → x = 0
⊢ ∀ (x : QuadraticAlgebra R a b), x * z = 0 → x = 0
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: case mp
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃ x = y ◃ y → x = y

Tactic:
intro h

Goal state after:
case mp
R : Type u_1
inst✝ : Rack R
x y : R
h : x ◃ x = y ◃ y
⊢ x = y
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mp
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ : R
⊢ Relation.EqvGen (Rel r) x₁ x₂ → RingConGen.Rel r x₁ x₂

Tactic:
intro h

Goal state after:
case mp
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ : R
h : Relation.EqvGen (Rel r) x₁ x₂
⊢ RingConGen.Rel r x₁ x₂
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mpr
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ : R
⊢ RingConGen.Rel r x₁ x₂ → Relation.EqvGen (Rel r) x₁ x₂

Tactic:
intro h

Goal state after:
case mpr
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ : R
h : RingConGen.Rel r x₁ x₂
⊢ Relation.EqvGen (Rel r) x₁ x₂
Module: Mathlib.Algebra.Star.Free

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
⊢ MulOpposite.unop (((lift R) (MulOpposite.op ∘ ι R)) (MulOpposite.unop (((lift R) (MulOpposite.op ∘ ι R)) x))) = x

Tactic:
let y := lift R (X := X) (MulOpposite.op ∘ ι R)

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
y : FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ := (lift R) (MulOpposite.op ∘ ι R)
⊢ MulOpposite.unop (((lift R) (MulOpposite.op ∘ ι R)) (MulOpposite.unop (((lift R) (MulOpposite.op ∘ ι R)) x))) = x
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : Mul G
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : NonAssocSemiring k
inst✝² : SMul G k
g_hom : Type u_4
inst✝¹ : FunLike g_hom G R
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : SkewMonoidAlgebra k G
h_comm : ∀ {x y : G}, y ∈ a.support → f (y • b.coeff x) * g y = g y * f (b.coeff x)
⊢ (liftNC ↑f ⇑g) (a * b) = (liftNC ↑f ⇑g) (a.sum single) * (liftNC ↑f ⇑g) (b.sum single)

Tactic:
mul_def,

Goal state after:
k : Type u_1
G : Type u_2
inst✝⁵ : Mul G
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : NonAssocSemiring k
inst✝² : SMul G k
g_hom : Type u_4
inst✝¹ : FunLike g_hom G R
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : SkewMonoidAlgebra k G
h_comm : ∀ {x y : G}, y ∈ a.support → f (y • b.coeff x) * g y = g y * f (b.coeff x)
⊢ (liftNC ↑f ⇑g) (a.sum fun a₁ b₁ ↦ b.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) =
    (liftNC ↑f ⇑g) (a.sum single) * (liftNC ↑f ⇑g) (b.sum single)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ single 1 1 * single g a = single g a

Tactic:
mul_def,

Goal state after:
case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ ((single 1 1).sum fun a₁ b₁ ↦ (single g a).sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) = single g a
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ single g a * single 1 1 = single g a

Tactic:
mul_def,

Goal state after:
case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ ((single g a).sum fun a₁ b₁ ↦ (single 1 1).sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) = single g a
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:
mul_def,

Goal state after:
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.sum fun a₁ b₁ ↦ g.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)).coeff x =
    f.sum fun a₁ b₁ ↦ g.sum fun a₂ b₂ ↦ if a₁ * a₂ = x then b₁ * a₁ • b₂ else 0
Module: Mathlib.Algebra.Symmetrized

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

Tactic:
mul_def,

Goal state after:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ sym (⅟2 * (unsym a * unsym (b + c) + unsym (b + c) * unsym a)) = a * b + a * c
Module: Mathlib.Algebra.Symmetrized

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

Tactic:
mul_def,

Goal state after:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ sym (⅟2 * (unsym a * unsym (b + c) + unsym (b + c) * unsym a)) =
    sym (⅟2 * (unsym a * unsym b + unsym b * unsym a)) + a * c
Module: Mathlib.Algebra.Symmetrized

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

Tactic:
mul_def,

Goal state after:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ sym (⅟2 * (unsym a * unsym (b + c) + unsym (b + c) * unsym a)) =
    sym (⅟2 * (unsym a * unsym b + unsym b * unsym a)) + sym (⅟2 * (unsym a * unsym c + unsym c * unsym a))
Module: Mathlib.Algebra.Symmetrized

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

Tactic:
mul_def,

Goal state after:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ sym (⅟2 * (unsym (a + b) * unsym c + unsym c * unsym (a + b))) = a * c + b * c
Module: Mathlib.Algebra.Symmetrized

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

Tactic:
mul_def,

Goal state after:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ sym (⅟2 * (unsym (a + b) * unsym c + unsym c * unsym (a + b))) =
    sym (⅟2 * (unsym a * unsym c + unsym c * unsym a)) + b * c
Module: Mathlib.Algebra.Symmetrized

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

Tactic:
mul_def,

Goal state after:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ sym (⅟2 * (unsym (a + b) * unsym c + unsym c * unsym (a + b))) =
    sym (⅟2 * (unsym a * unsym c + unsym c * unsym a)) + sym (⅟2 * (unsym b * unsym c + unsym c * unsym b))
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
x✝ : αˢʸᵐ
⊢ 0 * x✝ = 0

Tactic:
mul_def,

Goal state after:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
x✝ : αˢʸᵐ
⊢ sym (⅟2 * (unsym 0 * unsym x✝ + unsym x✝ * unsym 0)) = 0
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
x✝ : αˢʸᵐ
⊢ x✝ * 0 = 0

Tactic:
mul_def,

Goal state after:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
x✝ : αˢʸᵐ
⊢ sym (⅟2 * (unsym x✝ * unsym 0 + unsym 0 * unsym x✝)) = 0
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
x✝ : αˢʸᵐ
⊢ 1 * x✝ = x✝

Tactic:
mul_def,

Goal state after:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
x✝ : αˢʸᵐ
⊢ sym (⅟2 * (unsym 1 * unsym x✝ + unsym x✝ * unsym 1)) = x✝
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
x✝ : αˢʸᵐ
⊢ x✝ * 1 = x✝

Tactic:
mul_def,

Goal state after:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
x✝ : αˢʸᵐ
⊢ sym (⅟2 * (unsym x✝ * unsym 1 + unsym 1 * unsym x✝)) = x✝
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:
mul_def,

Goal state after:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a : αˢʸᵐ
⊢ unsym (sym (⅟2 * (unsym a * unsym a + unsym a * unsym a))) = unsym a * unsym a
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝⁴ : Mul α
inst✝³ : AddCommSemigroup α
inst✝² : One α
inst✝¹ : OfNat α 2
inst✝ : Invertible 2
a b : αˢʸᵐ
⊢ a * b = b * a

Tactic:
mul_def,

Goal state after:
α : Type u_1
inst✝⁴ : Mul α
inst✝³ : AddCommSemigroup α
inst✝² : One α
inst✝¹ : OfNat α 2
inst✝ : Invertible 2
a b : αˢʸᵐ
⊢ sym (⅟2 * (unsym a * unsym b + unsym b * unsym a)) = b * a
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝⁴ : Mul α
inst✝³ : AddCommSemigroup α
inst✝² : One α
inst✝¹ : OfNat α 2
inst✝ : Invertible 2
a b : αˢʸᵐ
⊢ sym (⅟2 * (unsym a * unsym b + unsym b * unsym a)) = b * a

Tactic:
mul_def,

Goal state after:
α : Type u_1
inst✝⁴ : Mul α
inst✝³ : AddCommSemigroup α
inst✝² : One α
inst✝¹ : OfNat α 2
inst✝ : Invertible 2
a b : αˢʸᵐ
⊢ sym (⅟2 * (unsym a * unsym b + unsym b * unsym a)) = sym (⅟2 * (unsym b * unsym a + unsym a * unsym b))
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → R
⊢ trop (s.inf f) = ∑ i ∈ s, trop (f i)

Tactic:
by
  convert! Multiset.trop_inf (s.val.map f)
  simp only [Multiset.map_map, Function.comp_apply]
  rfl

Goal state after:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: case calc_1
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ 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))

Tactic:
mul_def,

Goal state after:
case calc_1
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ sym (⅟2 * (unsym (a * b) * unsym (a * a) + unsym (a * a) * unsym (a * b))) =
    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))
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst✝⁶ : Semiring β
inst✝⁵ : Monoid α
inst✝⁴ : Monoid α₂
inst✝³ : FunLike F α α₂
inst✝² : MulSemiringAction α β
inst✝¹ : MulSemiringAction α₂ β
inst✝ : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = f a • x
⊢ (mapDomain ⇑f) (x * y) = (mapDomain ⇑f) x * (mapDomain ⇑f) y

Tactic:
mul_def,

Goal state after:
α : Type u_3
α₂ : Type u_4
β : Type u_5
F : Type u_6
inst✝⁶ : Semiring β
inst✝⁵ : Monoid α
inst✝⁴ : Monoid α₂
inst✝³ : FunLike F α α₂
inst✝² : MulSemiringAction α β
inst✝¹ : MulSemiringAction α₂ β
inst✝ : MulHomClass F α α₂
f : F
x y : SkewMonoidAlgebra β α
hf : ∀ (a : α) (x : β), a • x = f a • x
⊢ (mapDomain ⇑f) (x.sum fun a₁ b₁ ↦ y.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) =
    (mapDomain ⇑f) x * (mapDomain ⇑f) y
Module: Mathlib.Topology.Sheaves.Functors

Goal state before:
pp: case refine_2
C : Type u
inst✝⁸ : Category.{v, u} C
X Y : TopCat
f✝ : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
A : Type u_1
inst✝⁷ : Category.{w, u_1} A
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
FA : A → A → Type u_2
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasColimits A
inst✝³ : HasLimits A
inst✝² : PreservesLimits (CategoryTheory.forget A)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget A)
inst✝ : (CategoryTheory.forget A).ReflectsIsomorphisms
X✝ Y✝ : TopCat.Sheaf A Y
u : X✝ ⟶ Y✝
⊢ sheafifyLift (Opens.grothendieckTopology ↑X) (⋯.pullbackIso.hom.app X✝.obj ≫ ⋯.functor.op.whiskerLeft u.hom) ⋯ =
    sheafifyLift (Opens.grothendieckTopology ↑X) (⋯.pullbackIso.hom.app X✝.obj) ⋯ ≫ hf.functor.op.whiskerLeft u.hom

Tactic:
rw [CategoryTheory.sheafifyLift_comp]

Goal state after:
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
U : Opens ↑X
x : ↑X
hx : x ∈ U
f : (fun X ↦ X) ((subsheafToTypes P).presheaf.obj (op U))
⊢ (ConcreteCategory.hom (stalkToFiber P x)) ((ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ U x hx)) f) =
    ↑f ⟨x, hx⟩

Tactic:
dsimp [stalkToFiber, Presheaf.germ]
  exact colimit.ι_desc_apply _ _ _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
g : ↥X → ↥Y
h : ⇑f = g
x : ↥X
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      ({ base := ofHom { toFun := g, continuous_toFun := ⋯ },
            c := f.c ≫ (Presheaf.pushforwardEq ⋯ X.presheaf).hom }.stalkMap
        x))

Tactic:
by
    subst h
    convert! f.prop x using 4
    cat_disch

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
hg : IsOpenImmersion g
x : ↥X
y : ↥Y
h : f x = g y
a : ↑(pullback f.base g.base)
ha : (ConcreteCategory.hom (pullback.fst f.base g.base)) a = x
⊢ ∃ a,
    (ConcreteCategory.hom
          ((PreservesPullback.iso forgetToTop f g).hom ≫ pullback.fst (forgetToTop.map f) (forgetToTop.map g)))
        a =
      x

Tactic:
use (PreservesPullback.iso Scheme.forgetToTop f g).inv a

Goal state after:
case h
P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
hg : IsOpenImmersion g
x : ↥X
y : ↥Y
h : f x = g y
a : ↑(pullback f.base g.base)
ha : (ConcreteCategory.hom (pullback.fst f.base g.base)) a = x
⊢ (ConcreteCategory.hom
        ((PreservesPullback.iso forgetToTop f g).hom ≫ pullback.fst (forgetToTop.map f) (forgetToTop.map g)))
      ((ConcreteCategory.hom (PreservesPullback.iso forgetToTop f g).inv) a) =
    x
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
H : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ lift f g H ≫ f = g

Tactic:
by
  simp [AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift,
    CategoryTheory.Limits.pullback.condition]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: K : Precoverage Scheme
X✝ Y Z : Scheme
𝒰 : Cover K X✝
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
P Q : MorphismProperty Scheme
X : Scheme
R : Presieve X
x✝ : R ∈ (precoverage P).coverings X
x : ↥X
hR : R ∈ jointlySurjectivePrecoverage.coverings X
right✝ : R ∈ P.precoverage.coverings X
⊢ ∃ Y g, R g ∧ x ∈ Set.range ⇑g

Tactic:
by
    rw [jointlySurjectivePrecoverage, Presieve.mem_comap_jointlySurjectivePrecoverage_iff] at hR
    obtain ⟨Y, g, hg, heq⟩ := hR x
    use Y, g, hg
    exact heq

Goal state after: