mathlib-initiative/mathlib-tactics huggingface dataset:
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

Goal state after:
case re
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 }).re =
    (c₂ • { re := 0, imI := 0, imJ := 1, imK := 0 } - { re := 0, imI := 0, imJ := 0, imK := 1 }).re

case imI
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 }).imI =
    (c₂ • { re := 0, imI := 0, imJ := 1, imK := 0 } - { re := 0, imI := 0, imJ := 0, imK := 1 }).imI

case imJ
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 }).imJ =
    (c₂ • { re := 0, imI := 0, imJ := 1, imK := 0 } - { re := 0, imI := 0, imJ := 0, imK := 1 }).imJ

case imK
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 }).imK =
    (c₂ • { re := 0, imI := 0, imJ := 1, imK := 0 } - { re := 0, imI := 0, imJ := 0, imK := 1 }).imK
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
a₁✝ a₂✝ : NonAssocSemiring R
a✝ : a₁✝.toNonUnitalNonAssocSemiring = a₂✝.toNonUnitalNonAssocSemiring
⊢ a₁✝ = a₂✝

Tactic:
ext

Goal state after:
case h_add
R : Type u
a₁✝ a₂✝ : NonAssocSemiring R
a✝ : a₁✝.toNonUnitalNonAssocSemiring = a₂✝.toNonUnitalNonAssocSemiring
x✝¹ x✝ : R
⊢ x✝¹ + x✝ = x✝¹ + x✝

case h_mul
R : Type u
a₁✝ a₂✝ : NonAssocSemiring R
a✝ : a₁✝.toNonUnitalNonAssocSemiring = a₂✝.toNonUnitalNonAssocSemiring
x✝¹ x✝ : R
⊢ x✝¹ * x✝ = x✝¹ * x✝
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
q : Basis A c₁ c₂ c₃
⊢ (Basis.self R).compHom q.liftHom = q

Tactic:
ext

Goal state after:
case hi
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
q : Basis A c₁ c₂ c₃
⊢ ((Basis.self R).compHom q.liftHom).i = q.i

case hj
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
q : Basis A c₁ c₂ c₃
⊢ ((Basis.self R).compHom q.liftHom).j = q.j
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
F : ℍ[R,c₁,c₂,c₃] →ₐ[R] A
⊢ ((Basis.self R).compHom F).liftHom = F

Tactic:
ext

Goal state after:
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
F : ℍ[R,c₁,c₂,c₃] →ₐ[R] A
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ ((Basis.self R).compHom F).liftHom x✝ = F x✝
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
a₁✝ a₂✝ : NonUnitalRing R
a✝ : a₁✝.toNonUnitalNonAssocRing = a₂✝.toNonUnitalNonAssocRing
⊢ a₁✝ = a₂✝

Tactic:
ext

Goal state after:
case h_add
R : Type u
a₁✝ a₂✝ : NonUnitalRing R
a✝ : a₁✝.toNonUnitalNonAssocRing = a₂✝.toNonUnitalNonAssocRing
x✝¹ x✝ : R
⊢ x✝¹ + x✝ = x✝¹ + x✝

case h_mul
R : Type u
a₁✝ a₂✝ : NonUnitalRing R
a✝ : a₁✝.toNonUnitalNonAssocRing = a₂✝.toNonUnitalNonAssocRing
x✝¹ x✝ : R
⊢ x✝¹ * x✝ = x✝¹ * x✝
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
a₁✝ a₂✝ : NonAssocRing R
a✝ : a₁✝.toNonUnitalNonAssocRing = a₂✝.toNonUnitalNonAssocRing
⊢ a₁✝ = a₂✝

Tactic:
ext

Goal state after:
case h_add
R : Type u
a₁✝ a₂✝ : NonAssocRing R
a✝ : a₁✝.toNonUnitalNonAssocRing = a₂✝.toNonUnitalNonAssocRing
x✝¹ x✝ : R
⊢ x✝¹ + x✝ = x✝¹ + x✝

case h_mul
R : Type u
a₁✝ a₂✝ : NonAssocRing R
a✝ : a₁✝.toNonUnitalNonAssocRing = a₂✝.toNonUnitalNonAssocRing
x✝¹ x✝ : R
⊢ x✝¹ * x✝ = x✝¹ * x✝
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₁ inst₂ : Semiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ inst₁ = inst₂

Tactic:
have h₀ : inst₁.toAddCommMonoid = inst₂.toAddCommMonoid := by
    ext : 1 <;> assumption
  have h₁ : inst₁.toNonUnitalSemiring = inst₂.toNonUnitalSemiring := by
    ext : 1 <;> assumption
  have h₂ : inst₁.toNonAssocSemiring = inst₂.toNonAssocSemiring := by
    ext : 1 <;> assumption
  have h₃ : (inst₁.toMonoidWithZero).toMonoid = (inst₂.toMonoidWithZero).toMonoid := by
    ext : 1; exact h_mul
  -- Split into fields and prove they are equal using the above.
  cases inst₁; cases inst₂
  congr <;> solve | injection h₁ | injection h₂

Goal state after:
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✝¹⁶ : NonUnitalNonAssocSemiring α
inst✝¹⁵ : Monoid M
inst✝¹⁴ : Monoid N
inst✝¹³ : Semiring R✝
inst✝¹² : DistribMulAction M α
inst✝¹¹ : SMulCommClass M α α
inst✝¹⁰ : IsScalarTower M α α
inst✝⁹ : DistribMulAction N α
inst✝⁸ : SMulCommClass N α α
inst✝⁷ : IsScalarTower N α α
inst✝⁶ : Module R✝ α
inst✝⁵ : SMulCommClass R✝ α α
inst✝⁴ : IsScalarTower R✝ α α
R : Type u_6
inst✝³ : CommSemiring «R»
inst✝² : Module «R» α
inst✝¹ : SMulCommClass «R» α α
inst✝ : IsScalarTower «R» α α
z : ↥(NonUnitalSubsemiring.center α)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by
        rw [Subsemiring.mem_center_iff]
        intro g
        ext a
        exact map_mul_left g (↑z) a

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

Goal state before:
pp: α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
⊢ a ∈ NonUnitalSubsemiring.center α ↔ R a = L a ∧ L a ∈ (toEndRingHom α).rangeS

Tactic:
constructor

Goal state after:
case mp
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
⊢ a ∈ NonUnitalSubsemiring.center α → R a = L a ∧ L a ∈ (toEndRingHom α).rangeS

case mpr
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
⊢ R a = L a ∧ L a ∈ (toEndRingHom α).rangeS → a ∈ NonUnitalSubsemiring.center α
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: case mpr
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
hc : R a = L a
T : CentroidHom α
hT : (toEndRingHom α) T = L a
e1 : ∀ (d : α), T d = a * d
e2 : ∀ (d : α), T d = d * a
⊢ a ∈ NonUnitalSubsemiring.center α

Tactic:
constructor

Goal state after:
case mpr.comm
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
hc : R a = L a
T : CentroidHom α
hT : (toEndRingHom α) T = L a
e1 : ∀ (d : α), T d = a * d
e2 : ∀ (d : α), T d = d * a
⊢ ∀ (a_1 : α), Commute a a_1

case left_assoc
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
hc : R a = L a
T : CentroidHom α
hT : (toEndRingHom α) T = L a
e1 : ∀ (d : α), T d = a * d
e2 : ∀ (d : α), T d = d * a
⊢ ∀ (b c : α), a * (b * c) = a * b * c

case mpr.right_assoc
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
a : α
hc : R a = L a
T : CentroidHom α
hT : (toEndRingHom α) T = L a
e1 : ∀ (d : α), T d = a * d
e2 : ∀ (d : α), T d = d * a
⊢ ∀ (a_1 b : α), a_1 * b * a = a_1 * (b * a)
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 α
⊢ T 1 ∈ Subsemiring.center α

Tactic:
constructor

Goal state after:
case comm
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonAssocSemiring α
T : CentroidHom α
⊢ ∀ (a : α), Commute (T 1) a

case left_assoc
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonAssocSemiring α
T : CentroidHom α
⊢ ∀ (b c : α), T 1 * (b * c) = T 1 * b * c

case right_assoc
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonAssocSemiring α
T : CentroidHom α
⊢ ∀ (a b : α), a * b * T 1 = a * (b * T 1)
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✝ : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
f g : CentroidHom α
⊢ f * g = g * f

Tactic:
ext

Goal state after:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
f g : CentroidHom α
a✝ : α
⊢ (f * g) a✝ = (g * f) a✝
Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁸ : CommSemiring k
inst✝⁷ : Monoid G
inst✝⁶ : Monoid H
A : Type u_4
B : Type u_5
inst✝⁵ : Semiring A
inst✝⁴ : Algebra k A
inst✝³ : Semiring B
inst✝² : Algebra k B
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
f : G →* A
⊢ (fun f ↦ (↑f).comp (of k G)) ((fun F ↦ liftNCAlgHom (Algebra.ofId k A) F ⋯) f) = f

Tactic:
ext

Goal state after:
k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁸ : CommSemiring k
inst✝⁷ : Monoid G
inst✝⁶ : Monoid H
A : Type u_4
B : Type u_5
inst✝⁵ : Semiring A
inst✝⁴ : Algebra k A
inst✝³ : Semiring B
inst✝² : Algebra k B
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
f : G →* A
x✝ : G
⊢ ((fun f ↦ (↑f).comp (of k G)) ((fun F ↦ liftNCAlgHom (Algebra.ofId k A) F ⋯) 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
inst✝⁸ : CommSemiring k
inst✝⁷ : Monoid G
inst✝⁶ : Monoid H
A : Type u_4
B : Type u_5
inst✝⁵ : Semiring A
inst✝⁴ : Algebra k A
inst✝³ : Semiring B
inst✝² : Algebra k B
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
F : SkewMonoidAlgebra k G →ₐ[k] A
⊢ (fun F ↦ liftNCAlgHom (Algebra.ofId k A) F ⋯) ((fun f ↦ (↑f).comp (of k G)) F) = F

Tactic:
ext

Goal state after:
k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁸ : CommSemiring k
inst✝⁷ : Monoid G
inst✝⁶ : Monoid H
A : Type u_4
B : Type u_5
inst✝⁵ : Semiring A
inst✝⁴ : Algebra k A
inst✝³ : Semiring B
inst✝² : Algebra k B
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
F : SkewMonoidAlgebra k G →ₐ[k] A
x✝ : G
⊢ ((↑((fun F ↦ liftNCAlgHom (Algebra.ofId k A) F ⋯) ((fun f ↦ (↑f).comp (of k G)) F))).comp (of k G)) x✝ =
    ((↑F).comp (of k G)) x✝
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

Goal state before:
pp: M : Type u_4
α : Type u_5
inst✝¹ : AddCommMonoid M
a : α
f : SkewMonoidAlgebra M α
inst✝ : DecidableEq α
⊢ ((erase a) f).support = f.support.erase a

Tactic:
ext

Goal state after:
M : Type u_4
α : Type u_5
inst✝¹ : AddCommMonoid M
a : α
f : SkewMonoidAlgebra M α
inst✝ : DecidableEq α
a✝ : α
⊢ a✝ ∈ ((erase a) f).support ↔ a✝ ∈ f.support.erase a
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

Goal state before:
pp: M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
a : α
f : SkewMonoidAlgebra M α
⊢ single a (f.coeff a) + (erase a) f = f

Tactic:
ext

Goal state after:
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
a : α
f : SkewMonoidAlgebra M α
a✝ : α
⊢ (single a (f.coeff a) + (erase a) f).coeff a✝ = f.coeff a✝
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case rel
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✝ : R
hab : Rel r x✝ y✝
c d : R
hcd : Relation.EqvGen (Rel r) c d
⊢ Relation.EqvGen (Rel r) (y✝ + c) (y✝ + d)

Tactic:
induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.add_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case refl
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✝ c d : R
hcd : Relation.EqvGen (Rel r) c d
⊢ Relation.EqvGen (Rel r) (x✝ + c) (x✝ + d)

Tactic:
induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.add_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: 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:
constructor

Goal state after:
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₂

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₂
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

Goal state before:
pp: M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
⊢ f.update a (f.coeff a) = f

Tactic:
ext

Goal state after:
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
f : SkewMonoidAlgebra M α
a a✝ : α
⊢ (f.update a (f.coeff a)).coeff a✝ = f.coeff a✝
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✝ } = { toQuot := Quot.mk (Rel r) a✝ }

Tactic:
simp [add_quot, ← zero_quot, zero_add]

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 : α
⊢ f.update a 0 = (erase a) f

Tactic:
ext

Goal state after:
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
f : SkewMonoidAlgebra M α
a a✝ : α
⊢ (f.update a 0).coeff a✝ = ((erase a) f).coeff a✝
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: 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
⊢ ∀ (n : ℕ) (x : RingQuot r), (n + 1) • x = n • x + x

Tactic:
rintro n ⟨⟨⟩⟩
    simp only [smul_quot, nsmul_eq_mul, Nat.cast_add, Nat.cast_one, add_mul, one_mul,
               add_comm, add_quot]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: 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 : { f // ∀ ⦃x y : R⦄, r x y → f x = f y }
⊢ (fun F ↦ ⟨F.comp (mkRingHom r), ⋯⟩) ((fun f ↦ preLift ⋯) f) = f

Tactic:
ext

Goal state after:
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 : { f // ∀ ⦃x y : R⦄, r x y → f x = f y }
x✝ : R
⊢ ↑((fun F ↦ ⟨F.comp (mkRingHom r), ⋯⟩) ((fun f ↦ preLift ⋯) f)) x✝ = ↑f x✝
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: 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 : RingQuot r →+* T
⊢ { toFun := fun x ↦ Quot.lift ⇑(F.comp (mkRingHom r)) ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
      map_add' := ⋯ } =
    F

Tactic:
ext

Goal state after:
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 : RingQuot r →+* T
x✝ : R
⊢ ({ toFun := fun x ↦ Quot.lift ⇑(F.comp (mkRingHom r)) ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
            map_add' := ⋯ }.comp
        (mkRingHom r))
      x✝ =
    (F.comp (mkRingHom r)) x✝
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝¹ : Semiring R
T : Type uT
inst✝ : Semiring T
f : R →+* T
r : R → R → Prop
w : ∀ ⦃x y : R⦄, r x y → f x = f y
g : RingQuot r →+* T
h : g.comp (mkRingHom r) = f
⊢ g = lift ⟨f, w⟩

Tactic:
ext

Goal state after:
R : Type uR
inst✝¹ : Semiring R
T : Type uT
inst✝ : Semiring T
f : R →+* T
r : R → R → Prop
w : ∀ ⦃x y : R⦄, r x y → f x = f y
g : RingQuot r →+* T
h : g.comp (mkRingHom r) = f
x✝ : R
⊢ (g.comp (mkRingHom r)) x✝ = ((lift ⟨f, w⟩).comp (mkRingHom r)) x✝
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: S : Type uS
inst✝² : CommSemiring S
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
s : A → A → Prop
this : Function.Surjective fun x ↦ { toQuot := Quot.mk (Rel s) x }
⊢ Function.Surjective ⇑(mkAlgHom S s)

Tactic:
by
    simpa [mkAlgHom_def, mkRingHom_def]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: 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 u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
f : A →ₐ[S] B
h : ∀ ⦃x y : A⦄, s x y → f x = f y
x : RingQuot s
⊢ ∀ (a b : A), Rel s a b → f a = f b

Tactic:
by
              rintro _ _ r
              induction r with
              | of r => exact h r
              | add_left _ r' => simp only [map_add, r']
              | mul_left _ r' => simp only [map_mul, r']
              | mul_right _ r' => simp only [map_mul, r']

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: 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 u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
f : { f // ∀ ⦃x y : A⦄, s x y → f x = f y }
⊢ (fun F ↦ ⟨F.comp (mkAlgHom S s), ⋯⟩) ((fun f' ↦ preLiftAlgHom S ⋯) f) = f

Tactic:
ext

Goal state after:
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 u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
f : { f // ∀ ⦃x y : A⦄, s x y → f x = f y }
x✝ : A
⊢ ↑((fun F ↦ ⟨F.comp (mkAlgHom S s), ⋯⟩) ((fun f' ↦ preLiftAlgHom S ⋯) f)) x✝ = ↑f x✝
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: 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 u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
F : RingQuot s →ₐ[S] B
⊢ (fun f' ↦ preLiftAlgHom S ⋯) ((fun F ↦ ⟨F.comp (mkAlgHom S s), ⋯⟩) F) = F

Tactic:
ext

Goal state after:
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 u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
F : RingQuot s →ₐ[S] B
x✝ : A
⊢ (((fun f' ↦ preLiftAlgHom S ⋯) ((fun F ↦ ⟨F.comp (mkAlgHom S s), ⋯⟩) F)).comp (mkAlgHom S s)) x✝ =
    (F.comp (mkAlgHom S s)) x✝
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: S : Type uS
inst✝⁴ : CommSemiring S
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
f : A →ₐ[S] B
s : A → A → Prop
w : ∀ ⦃x y : A⦄, s x y → f x = f y
g : RingQuot s →ₐ[S] B
h : g.comp (mkAlgHom S s) = f
⊢ g = (liftAlgHom S) ⟨f, w⟩

Tactic:
ext

Goal state after:
S : Type uS
inst✝⁴ : CommSemiring S
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
f : A →ₐ[S] B
s : A → A → Prop
w : ∀ ⦃x y : A⦄, s x y → f x = f y
g : RingQuot s →ₐ[S] B
h : g.comp (mkAlgHom S s) = f
x✝ : A
⊢ (g.comp (mkAlgHom S s)) x✝ = (((liftAlgHom S) ⟨f, w⟩).comp (mkAlgHom S s)) x✝
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
R' : Type u_5
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Semiring R'
f : SkewPolynomial R
g : ℕ → R → SkewPolynomial R'
h : ℕ → R' → P
h_zero : ∀ (a : ℕ), h a 0 = 0
h_add : ∀ (a : ℕ) (b₁ b₂ : R'), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ (f.sum g).sum h = f.sum fun a b ↦ (g a b).sum h

Tactic:
simp only [sum_def', SkewMonoidAlgebra.sum_sum_index (fun a ↦ h_zero (toAdd a))
    (fun a ↦ h_add (toAdd a))]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
f g : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ f * g = f.sum fun a₁ b₁ ↦ g.sum fun a₂ b₂ ↦ (monomial (a₁ + a₂)) (b₁ * (⇑φ)^[a₁] b₂)

Tactic:
ext

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
f g : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
a✝ : Multiplicative ℕ
⊢ (f * g).coeff a✝ = (f.sum fun a₁ b₁ ↦ g.sum fun a₂ b₂ ↦ (monomial (a₁ + a₂)) (b₁ * (⇑φ)^[a₁] b₂)).coeff a✝
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
T : CentroidHom α
⊢ T 1 ∈ StarSubsemiring.center α

Tactic:
constructor

Goal state after:
case comm
α : Type u_1
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
T : CentroidHom α
⊢ ∀ (a : α), Commute (T 1) a

case left_assoc
α : Type u_1
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
T : CentroidHom α
⊢ ∀ (b c : α), T 1 * (b * c) = T 1 * b * c

case right_assoc
α : Type u_1
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
T : CentroidHom α
⊢ ∀ (a b : α), a * b * T 1 = a * (b * T 1)
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : SkewPolynomial R
n : ℕ
a : R
⊢ (p.update n a).coeff = Function.update p.coeff n a

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : SkewPolynomial R
n : ℕ
a : R
x✝ : ℕ
⊢ (p.update n a).coeff x✝ = Function.update p.coeff n a x✝
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : SkewPolynomial R
n : ℕ
⊢ p.update n 0 = erase n p

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : SkewPolynomial R
n n✝ : ℕ
⊢ (p.update n 0).coeff n✝ = (erase n p).coeff n✝
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
p : SkewMonoidAlgebra k G → Prop
f : SkewMonoidAlgebra k G
zero : p 0
single : ∀ (g : G) (a : k), p (SkewMonoidAlgebra.single g a)
add : ∀ (f g : SkewMonoidAlgebra k G), p f → p g → p (f + g)
⊢ p (∑ a ∈ f.support, SkewMonoidAlgebra.single a (f.coeff a))

Tactic:
exact Finset.sum_induction _ _ add zero (by simp_all)

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

Goal state before:
pp: S : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
inst✝² : SMul S R
inst✝¹ : IsScalarTower S R R
inst✝ : SMulCommClass S R R
⊢ (let __RingEquiv := (MulSemiringAction.toRingEquiv (ConjAct Rˣ) R) (ConjAct.toConjAct (toUnits 1));
    { toRingEquiv := __RingEquiv, map_star' := ⋯, map_smul' := ⋯ }) =
    1

Tactic:
ext

Goal state after:
S : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
inst✝² : SMul S R
inst✝¹ : IsScalarTower S R R
inst✝ : SMulCommClass S R R
a✝ : R
⊢ (let __RingEquiv := (MulSemiringAction.toRingEquiv (ConjAct Rˣ) R) (ConjAct.toConjAct (toUnits 1));
      { toRingEquiv := __RingEquiv, map_star' := ⋯, map_smul' := ⋯ })
      a✝ =
    1 a✝