mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x✝ y✝ : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
x y : S
⊢ QuadraticAlgebra.C ((algebraMap S R) (x * y)) =
    QuadraticAlgebra.C ((algebraMap S R) x) * QuadraticAlgebra.C ((algebraMap S R) y)

Tactic:
ext <;> simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
⊢ QuadraticAlgebra.C ((algebraMap S R) 0) = 0

Tactic:
ext <;> simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x✝ y✝ : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
x y : S
⊢ QuadraticAlgebra.C ((algebraMap S R) (x + y)) =
    QuadraticAlgebra.C ((algebraMap S R) x) + QuadraticAlgebra.C ((algebraMap S R) y)

Tactic:
ext <;> simp

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

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ z - star z = z.im • (ω - star ω)

Tactic:
ext <;> simp

Goal state after:
case re
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ b * z.im = z.im * b

case im
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ z.im + z.im = z.im * (1 + 1)
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : CommRing R
n : ℤ
x y : R
⊢ ↑n * { re := x, im := y } = { re := ↑n * x, im := ↑n * y }

Tactic:
ext <;> simp

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

Goal state before:
pp: case neg
K : Type u_1
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
hz : z.re ^ 2 = a * z.im * z.im - b * z.re * z.im
h : ¬z.im = 0
⊢ False

Tactic:
apply Hab.out (-z.re / z.im)

Goal state after:
case neg
K : Type u_1
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
hz : z.re ^ 2 = a * z.im * z.im - b * z.re * z.im
h : ¬z.im = 0
⊢ (-z.re / z.im) ^ 2 = a + b * (-z.re / z.im)
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)
⊢ 0⁻¹ = 0

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝ : Rack R
x y : R
⊢ (x ◃ x) ◃ y = x ◃ y

Tactic:
by rw [← right_inv x y, ← self_distrib]

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
⊢ { re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 } =
    c₁ • 1 + c₂ • { re := 0, imI := 1, imJ := 0, imK := 0 }

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: case refl
R : Type u_1
inst✝ : Rack R
⊢ ∀ (x : PreEnvelGroup R), PreEnvelGroupRel R x x

Tactic:
apply PreEnvelGroupRel.refl

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
⊢ { re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 } = c₃ • 1

Tactic:
ext <;> simp

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
hc : ∀ x ∈ s, (algebraMap R[X] K) (g x ^ n x) * gi x ^ n x = 1
i : ι
hi : i ∈ s
j : Fin (n i)
⊢ ↑j + 1 ≤ n i

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
⊢ { re := 0, imI := 1, imJ := 0, imK := 0 } * { re := 0, imI := 0, imJ := 1, imK := 0 } =
    { re := 0, imI := 0, imJ := 0, imK := 1 }

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ c₃ : R
⊢ { re := 0, imI := 0, imJ := 1, imK := 0 } * { re := 0, imI := 1, imJ := 0, imK := 0 } =
    c₂ • { re := 0, imI := 0, imJ := 1, imK := 0 } - { re := 0, imI := 0, imJ := 0, imK := 1 }

Tactic:
ext <;> simp

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
⊢ ∃ q r,
    (∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree) ∧
      (algebraMap R[X] K) f * ∏ i ∈ s, gi i ^ n i =
        (algebraMap R[X] K) q + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r i j) * gi i ^ (↑j + 1)

Tactic:
classical
  obtain ⟨q, r, hr, hf⟩ := eq_quo_mul_prod_pow_add_sum_rem_mul_prod_pow f hg hgg n
  refine ⟨q, fun i j => r i j.rev, fun i hi j => hr i hi j.rev, ?_⟩
  rw [hf, map_add, map_mul, map_prod, add_mul, mul_assoc, ← Finset.prod_mul_distrib]
  have hc (x : ι) (hx : x ∈ s) : (algebraMap R[X] K) (g x ^ n x) * gi x ^ n x = 1 := by
    rw [map_pow, ← mul_pow, mul_comm, hgi x hx, one_pow]
  rw [Finset.prod_congr rfl hc, Finset.prod_const_one,
    mul_one, add_right_inj, map_sum, Finset.sum_mul]
  refine Finset.sum_congr rfl fun i hi => ?_
  rw [map_sum, Finset.sum_mul, ← Equiv.sum_comp Fin.revPerm]
  refine Fintype.sum_congr _ _ fun j => ?_
  rw [Fin.revPerm_apply, map_mul, map_prod, ← Finset.prod_erase_mul s _ hi,
    ← mul_rotate', mul_assoc, ← Finset.prod_mul_distrib,
    Finset.prod_congr rfl fun x hx => hc x (Finset.mem_of_mem_erase hx),
    Finset.prod_const_one, mul_one, map_mul, map_pow, mul_left_comm]
  refine congrArg (_ * ·) ?_
  rw [← mul_one (gi i ^ (j.1 + 1)), ← @one_pow K _ j.rev, ← hgi i hi,
    mul_pow, ← mul_assoc, ← pow_add, Fin.val_rev, Nat.add_sub_cancel' (by lia)]

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
ι : Type u_3
s : Finset ι
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
hf :
  (algebraMap R[X] K) q₁ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₁ i j) * gi i ^ (↑j + 1) =
    (algebraMap R[X] K) q₂ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₂ i j) * gi i ^ (↑j + 1)
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
i : ι
hi : i ∈ s
j : Fin (n i)
⊢ ↑j + 1 ≤ n i

Tactic:
lia

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
g₁ g₂ : R[X]
hg₁ : g₁.Monic
hg₂ : g₂.Monic
hcoprime✝ : IsCoprime g₁ g₂
q₁ q₂ r₁₁ r₁₂ r₂₁ r₂₂ : R[X]
hr₁₁ : r₁₁.degree < g₁.degree
hr₁₂ : r₁₂.degree < g₁.degree
hr₂₁ : r₂₁.degree < g₂.degree
hr₂₂ : r₂₂.degree < g₂.degree
hf : ↑q₁ + ↑r₁₁ / ↑g₁ + ↑r₂₁ / ↑g₂ = ↑q₂ + ↑r₁₂ / ↑g₁ + ↑r₂₂ / ↑g₂
g : Bool → R[X] := fun t ↦ Bool.rec g₂ g₁ t
r₁ : Bool → R[X] := fun t ↦ Bool.rec r₂₁ r₁₁ t
r₂ : Bool → R[X] := fun t ↦ Bool.rec r₂₂ r₁₂ t
hg : ∀ i ∈ Finset.univ, (g i).Monic
hcoprime : (↑Finset.univ).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : ∀ i ∈ Finset.univ, (r₁ i).degree < (g i).degree
⊢ q₁ = q₂ ∧ r₁₁ = r₁₂ ∧ r₂₁ = r₂₂

Tactic:
have hr₂ (i : Bool) (_ : i ∈ Finset.univ) : (r₂ i).degree < (g i).degree := Bool.rec hr₂₂ hr₁₂ i

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
g₁ g₂ : R[X]
hg₁ : g₁.Monic
hg₂ : g₂.Monic
hcoprime✝ : IsCoprime g₁ g₂
q₁ q₂ r₁₁ r₁₂ r₂₁ r₂₂ : R[X]
hr₁₁ : r₁₁.degree < g₁.degree
hr₁₂ : r₁₂.degree < g₁.degree
hr₂₁ : r₂₁.degree < g₂.degree
hr₂₂ : r₂₂.degree < g₂.degree
hf : ↑q₁ + ↑r₁₁ / ↑g₁ + ↑r₂₁ / ↑g₂ = ↑q₂ + ↑r₁₂ / ↑g₁ + ↑r₂₂ / ↑g₂
g : Bool → R[X] := fun t ↦ Bool.rec g₂ g₁ t
r₁ : Bool → R[X] := fun t ↦ Bool.rec r₂₁ r₁₁ t
r₂ : Bool → R[X] := fun t ↦ Bool.rec r₂₂ r₁₂ t
hg : ∀ i ∈ Finset.univ, (g i).Monic
hcoprime : (↑Finset.univ).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : ∀ i ∈ Finset.univ, (r₁ i).degree < (g i).degree
hr₂ : ∀ i ∈ Finset.univ, (r₂ i).degree < (g i).degree
⊢ q₁ = q₂ ∧ r₁₁ = r₁₂ ∧ r₂₁ = r₂₂
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsFormallyReal R
⊢ 1 < 2

Tactic:
lia

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

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
a b c : WithZero α
⊢ a * (b + c) = a * b + a * c

Tactic:
by
    cases a; · rfl
    cases b <;> cases c <;> try rfl
    exact congr_arg some (left_distrib _ _ _)

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
A : Type u_4
inst✝³ : Semiring A
inst✝² : Algebra k A
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
F : G →* A
x : G
⊢ ((lift k G A).symm ((lift k G A) F)) x = F x

Tactic:
Equiv.symm_apply_apply

Goal state after:
k : Type u_1
G : Type u_2
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
A : Type u_4
inst✝³ : Semiring A
inst✝² : Algebra k A
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
F : G →* A
x : G
⊢ F x = F x
Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
A : Type u_4
inst✝ : AddCommMonoid A
e : G ≃ H
v : SkewMonoidAlgebra A G
⊢ equivMapDomain e.symm (equivMapDomain e v) = v

Tactic:
simp [← equivMapDomain_trans]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
A : Type u_4
inst✝ : AddCommMonoid A
e : G ≃ H
v : SkewMonoidAlgebra A H
⊢ equivMapDomain e (equivMapDomain e.symm v) = v

Tactic:
simp [← equivMapDomain_trans]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case trans
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
a b x y z : R
a✝¹ : Relation.EqvGen (Rel r) x y
a✝ : Relation.EqvGen (Rel r) y z
h : ∀ {c d : R}, Relation.EqvGen (Rel r) c d → Relation.EqvGen (Rel r) (x * c) (y * d)
h' : ∀ {c d : R}, Relation.EqvGen (Rel r) c d → Relation.EqvGen (Rel r) (y * c) (z * d)
c d : R
hcd : Relation.EqvGen (Rel r) c d
⊢ Relation.EqvGen (Rel r) (x * c) (z * d)

Tactic:
| trans x y z _ _ h h' =>

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case trans
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
a b x y z : R
a✝¹ : Relation.EqvGen (Rel r) x y
a✝ : Relation.EqvGen (Rel r) y z
h : ∀ {c d : R}, Relation.EqvGen (Rel r) c d → Relation.EqvGen (Rel r) (x + c) (y + d)
h' : ∀ {c d : R}, Relation.EqvGen (Rel r) c d → Relation.EqvGen (Rel r) (y + c) (z + d)
c d : R
hcd : Relation.EqvGen (Rel r) c d
⊢ Relation.EqvGen (Rel r) (x + c) (z + d)

Tactic:
| trans x y z _ _ h h' =>

Goal state after:
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✝ → Prop
R : Type uR
inst✝ : Ring R
r : R → R → Prop
n : ℕ
toQuot✝ : Quot (Rel r)
a✝ : R
⊢ ↑n.succ • { toQuot := Quot.mk (Rel r) a✝ } = ↑n • { toQuot := Quot.mk (Rel r) a✝ } + { toQuot := Quot.mk (Rel r) a✝ }

Tactic:
simp [smul_quot, add_quot, add_mul, add_comm]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case add_left
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
r : R → R → Prop
f : R →+* T
h : ∀ ⦃x y : R⦄, r x y → f x = f y
x : RingQuot r
a✝² b✝¹ a✝¹ b✝ c✝ : R
a✝ : Rel r a✝¹ b✝
r' : f a✝¹ = f b✝
⊢ f a✝¹ + f c✝ = f b✝ + f c✝

Tactic:
r'

Goal state after:
case add_left
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
r : R → R → Prop
f : R →+* T
h : ∀ ⦃x y : R⦄, r x y → f x = f y
x : RingQuot r
a✝² b✝¹ a✝¹ b✝ c✝ : R
a✝ : Rel r a✝¹ b✝
r' : f a✝¹ = f b✝
⊢ f b✝ + f c✝ = f b✝ + f c✝
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mul_left
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
r : R → R → Prop
f : R →+* T
h : ∀ ⦃x y : R⦄, r x y → f x = f y
x : RingQuot r
a✝² b✝¹ a✝¹ b✝ c✝ : R
a✝ : Rel r a✝¹ b✝
r' : f a✝¹ = f b✝
⊢ f a✝¹ * f c✝ = f b✝ * f c✝

Tactic:
r'

Goal state after:
case mul_left
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
r : R → R → Prop
f : R →+* T
h : ∀ ⦃x y : R⦄, r x y → f x = f y
x : RingQuot r
a✝² b✝¹ a✝¹ b✝ c✝ : R
a✝ : Rel r a✝¹ b✝
r' : f a✝¹ = f b✝
⊢ f b✝ * f c✝ = f b✝ * f c✝
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mul_right
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
r : R → R → Prop
f : R →+* T
h : ∀ ⦃x y : R⦄, r x y → f x = f y
x : RingQuot r
a✝² b✝¹ a✝¹ b✝ c✝ : R
a✝ : Rel r b✝ c✝
r' : f b✝ = f c✝
⊢ f a✝¹ * f b✝ = f a✝¹ * f c✝

Tactic:
r'

Goal state after:
case mul_right
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
r : R → R → Prop
f : R →+* T
h : ∀ ⦃x y : R⦄, r x y → f x = f y
x : RingQuot r
a✝² b✝¹ a✝¹ b✝ c✝ : R
a✝ : Rel r b✝ c✝
r' : f b✝ = f c✝
⊢ f a✝¹ * f c✝ = f a✝¹ * f c✝
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
y a b : B
h : r a b
su : y + b = a
⊢ (mkRingHom r) y = 0

Tactic:
symm at 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 : a = y + b
⊢ (mkRingHom r) y = 0
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : SkewPolynomial R
n i : ℕ
h : i ≠ n
⊢ (erase n p).coeff i = p.coeff i

Tactic:
by
  simp [coeff_erase, h]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
S : Type u_3
inst✝ : NonUnitalNonAssocSemiring S
b : S
s : SkewMonoidAlgebra k G
f : G → k → S
⊢ s.sum f * b = s.sum fun a c ↦ f a c * b

Tactic:
simp only [sum, Finsupp.sum, Finset.sum_mul]

Goal state after:
Module: Mathlib.Algebra.Symmetrized

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

Tactic:
zero_mul,

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

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

Tactic:
zero_mul,

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : AddCommMonoid R
s : Finset S
f : S → Tropical R
⊢ untrop (∏ i ∈ s, f i) = ∑ i ∈ s, untrop (f i)

Tactic:
by
  convert! Multiset.untrop_prod (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_2
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ 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))

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

Tactic:
· 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]

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

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
A : VertexOperator R V
n : ℤ
x : V
h : n < ((HahnModule.of R).symm (A x)).order
⊢ -(-n - 1) - 1 < ((HahnModule.of R).symm (A x)).order

Tactic:
lia

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : (Presheaf.pushforward C H.hom).obj X.presheaf ≅ Y.presheaf
⊢ { base := H.hom, c := α.inv } ≫ { base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom } = 𝟙 X

Tactic:
ext <;> simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
U : Opens ↑↑Y
⊢ (Presheaf.pushforwardToOfIso ((forget C).mapIso H).symm H.inv.c).app (op U) ≫ H.hom.c.app (op U) =
    (𝟙 ((Presheaf.pushforward C H.hom.base).obj X.presheaf)).app (op U)

Tactic:
rw [NatTrans.id_app]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
U : Opens ↑↑Y
⊢ (Presheaf.pushforwardToOfIso ((forget C).mapIso H).symm H.inv.c).app (op U) ≫ H.hom.c.app (op U) =
    𝟙 (((Presheaf.pushforward C H.hom.base).obj X.presheaf).obj (op U))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: case refine_2
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
U : (Opens ↑↑s.pt)ᵒᵖ
j j' : Jᵒᵖ
f : j ⟶ j'
⊢ 𝟙 (s.pt.presheaf.obj U) ≫
      ((F.map f.unop ≫ s.ι.app (unop j)).c.app U ≫ (F.obj (unop j')).presheaf.map (eqToHom ⋯)) ≫
        (F.obj (unop j')).presheaf.map (eqToHom ⋯) =
    ((s.ι.app (unop j)).c.app U ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯)) ≫
      (F.map f.unop).c.app
          (op
            ((Opens.map (colimit.ι (F ⋙ forget C) (unop j))).obj
              ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))) ≫
        𝟙
            ((F.obj (unop j')).presheaf.obj
              (op
                ((Opens.map (F.map f.unop).base).obj
                  ((Opens.map (colimit.ι (F ⋙ forget C) (unop j))).obj
                    ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))))) ≫
          (pushforwardEq ⋯ (F.obj (unop j')).presheaf).hom.app
            (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))

Tactic:
have w :=
      Functor.congr_obj
        (congr_arg Opens.map (colimit.ι_desc ((PresheafedSpace.forget C).mapCocone s) (unop j)))
        (unop U)

Goal state after:
case refine_2
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
U : (Opens ↑↑s.pt)ᵒᵖ
j j' : Jᵒᵖ
f : j ⟶ j'
w :
  (Opens.map (colimit.ι (F ⋙ forget C) (unop j) ≫ colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U) =
    (Opens.map (((forget C).mapCocone s).ι.app (unop j))).obj (unop U)
⊢ 𝟙 (s.pt.presheaf.obj U) ≫
      ((F.map f.unop ≫ s.ι.app (unop j)).c.app U ≫ (F.obj (unop j')).presheaf.map (eqToHom ⋯)) ≫
        (F.obj (unop j')).presheaf.map (eqToHom ⋯) =
    ((s.ι.app (unop j)).c.app U ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯)) ≫
      (F.map f.unop).c.app
          (op
            ((Opens.map (colimit.ι (F ⋙ forget C) (unop j))).obj
              ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))) ≫
        𝟙
            ((F.obj (unop j')).presheaf.obj
              (op
                ((Opens.map (F.map f.unop).base).obj
                  ((Opens.map (colimit.ι (F ⋙ forget C) (unop j))).obj
                    ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))))) ≫
          (pushforwardEq ⋯ (F.obj (unop j')).presheaf).hom.app
            (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: case inr
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
n : ℕ
hn : f ^ n = 0
h : n > 0
⊢ X.toRingedSpace.basicOpen f = ⊥

Tactic:
rw [← X.toRingedSpace.basicOpen_pow f n h, hn]

Goal state after:
case inr
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
n : ℕ
hn : f ^ n = 0
h : n > 0
⊢ X.toRingedSpace.basicOpen 0 = ⊥
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
⊢ f ≫ toSpecΓ S = toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op

Tactic:
ext : 2
  refine Subtype.ext <| funext fun x' => ?_; symm
  erw [comap_apply]
  apply Localization.localRingHom_to_map

Goal state after: