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

Goal state before:
pp: case e_toNeg
R : Type u
toSemiring✝¹ : Semiring R
toNeg✝¹ : Neg R
toSub✝¹ : Sub R
toZSMul✝¹ : ZSMul R
sub_eq_add_neg✝¹ : ∀ (a b : R), a - b = a + -b
zsmul_zero'✝¹ : ∀ (a : R), 0 • a = 0
zsmul_succ'✝¹ : ∀ (n : ℕ) (a : R), ↑n.succ • a = ↑n • a + a
zsmul_neg'✝¹ : ∀ (n : ℕ) (a : R), Int.negSucc n • a = -(↑n.succ • a)
neg_add_cancel✝¹ : ∀ (a : R), -a + a = 0
toIntCast✝¹ : IntCast R
intCast_ofNat✝¹ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝¹ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
toSemiring✝ : Semiring R
toNeg✝ : Neg R
toSub✝ : Sub R
toZSMul✝ : ZSMul R
sub_eq_add_neg✝ : ∀ (a b : R), a - b = a + -b
zsmul_zero'✝ : ∀ (a : R), 0 • a = 0
zsmul_succ'✝ : ∀ (n : ℕ) (a : R), ↑n.succ • a = ↑n • a + a
zsmul_neg'✝ : ∀ (n : ℕ) (a : R), Int.negSucc n • a = -(↑n.succ • a)
neg_add_cancel✝ : ∀ (a : R), -a + a = 0
toIntCast✝ : IntCast R
intCast_ofNat✝ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ :
  { toSemiring := toSemiring✝¹, toNeg := toNeg✝¹, toSub := toSub✝¹, toZSMul := toZSMul✝¹,
        sub_eq_add_neg := sub_eq_add_neg✝¹, zsmul_zero' := zsmul_zero'✝¹, zsmul_succ' := zsmul_succ'✝¹,
        zsmul_neg' := zsmul_neg'✝¹, neg_add_cancel := neg_add_cancel✝¹, toIntCast := toIntCast✝¹,
        intCast_ofNat := intCast_ofNat✝¹, intCast_negSucc := intCast_negSucc✝¹ }.toSemiring =
    { toSemiring := toSemiring✝, toNeg := toNeg✝, toSub := toSub✝, toZSMul := toZSMul✝,
        sub_eq_add_neg := sub_eq_add_neg✝, zsmul_zero' := zsmul_zero'✝, zsmul_succ' := zsmul_succ'✝,
        zsmul_neg' := zsmul_neg'✝, neg_add_cancel := neg_add_cancel✝, toIntCast := toIntCast✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toSemiring
h₂ : toNonAssocRing = toNonAssocRing
h₃ :
  { toSemiring := toSemiring✝¹, toNeg := toNeg✝¹, toSub := toSub✝¹, toZSMul := toZSMul✝¹,
          sub_eq_add_neg := sub_eq_add_neg✝¹, zsmul_zero' := zsmul_zero'✝¹, zsmul_succ' := zsmul_succ'✝¹,
          zsmul_neg' := zsmul_neg'✝¹, neg_add_cancel := neg_add_cancel✝¹, toIntCast := toIntCast✝¹,
          intCast_ofNat := intCast_ofNat✝¹, intCast_negSucc := intCast_negSucc✝¹ }.toAddCommGroup.toSubNegMonoid =
    { toSemiring := toSemiring✝, toNeg := toNeg✝, toSub := toSub✝, toZSMul := toZSMul✝,
          sub_eq_add_neg := sub_eq_add_neg✝, zsmul_zero' := zsmul_zero'✝, zsmul_succ' := zsmul_succ'✝,
          zsmul_neg' := zsmul_neg'✝, neg_add_cancel := neg_add_cancel✝, toIntCast := toIntCast✝,
          intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toAddCommGroup.toSubNegMonoid
⊢ toNeg✝¹ = toNeg✝

Tactic:
solve | injection h₂ | injection h₃

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

Goal state before:
pp: case e_toSub
R : Type u
toSemiring✝¹ : Semiring R
toNeg✝¹ : Neg R
toSub✝¹ : Sub R
toZSMul✝¹ : ZSMul R
sub_eq_add_neg✝¹ : ∀ (a b : R), a - b = a + -b
zsmul_zero'✝¹ : ∀ (a : R), 0 • a = 0
zsmul_succ'✝¹ : ∀ (n : ℕ) (a : R), ↑n.succ • a = ↑n • a + a
zsmul_neg'✝¹ : ∀ (n : ℕ) (a : R), Int.negSucc n • a = -(↑n.succ • a)
neg_add_cancel✝¹ : ∀ (a : R), -a + a = 0
toIntCast✝¹ : IntCast R
intCast_ofNat✝¹ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝¹ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
toSemiring✝ : Semiring R
toNeg✝ : Neg R
toSub✝ : Sub R
toZSMul✝ : ZSMul R
sub_eq_add_neg✝ : ∀ (a b : R), a - b = a + -b
zsmul_zero'✝ : ∀ (a : R), 0 • a = 0
zsmul_succ'✝ : ∀ (n : ℕ) (a : R), ↑n.succ • a = ↑n • a + a
zsmul_neg'✝ : ∀ (n : ℕ) (a : R), Int.negSucc n • a = -(↑n.succ • a)
neg_add_cancel✝ : ∀ (a : R), -a + a = 0
toIntCast✝ : IntCast R
intCast_ofNat✝ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ :
  { toSemiring := toSemiring✝¹, toNeg := toNeg✝¹, toSub := toSub✝¹, toZSMul := toZSMul✝¹,
        sub_eq_add_neg := sub_eq_add_neg✝¹, zsmul_zero' := zsmul_zero'✝¹, zsmul_succ' := zsmul_succ'✝¹,
        zsmul_neg' := zsmul_neg'✝¹, neg_add_cancel := neg_add_cancel✝¹, toIntCast := toIntCast✝¹,
        intCast_ofNat := intCast_ofNat✝¹, intCast_negSucc := intCast_negSucc✝¹ }.toSemiring =
    { toSemiring := toSemiring✝, toNeg := toNeg✝, toSub := toSub✝, toZSMul := toZSMul✝,
        sub_eq_add_neg := sub_eq_add_neg✝, zsmul_zero' := zsmul_zero'✝, zsmul_succ' := zsmul_succ'✝,
        zsmul_neg' := zsmul_neg'✝, neg_add_cancel := neg_add_cancel✝, toIntCast := toIntCast✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toSemiring
h₂ : toNonAssocRing = toNonAssocRing
h₃ :
  { toSemiring := toSemiring✝¹, toNeg := toNeg✝¹, toSub := toSub✝¹, toZSMul := toZSMul✝¹,
          sub_eq_add_neg := sub_eq_add_neg✝¹, zsmul_zero' := zsmul_zero'✝¹, zsmul_succ' := zsmul_succ'✝¹,
          zsmul_neg' := zsmul_neg'✝¹, neg_add_cancel := neg_add_cancel✝¹, toIntCast := toIntCast✝¹,
          intCast_ofNat := intCast_ofNat✝¹, intCast_negSucc := intCast_negSucc✝¹ }.toAddCommGroup.toSubNegMonoid =
    { toSemiring := toSemiring✝, toNeg := toNeg✝, toSub := toSub✝, toZSMul := toZSMul✝,
          sub_eq_add_neg := sub_eq_add_neg✝, zsmul_zero' := zsmul_zero'✝, zsmul_succ' := zsmul_succ'✝,
          zsmul_neg' := zsmul_neg'✝, neg_add_cancel := neg_add_cancel✝, toIntCast := toIntCast✝,
          intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toAddCommGroup.toSubNegMonoid
⊢ toSub✝¹ = toSub✝

Tactic:
solve | injection h₂ | injection h₃

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

Goal state before:
pp: case mk.mk.e_toZSMul
R : Type u
toSemiring✝¹ : Semiring R
toNeg✝¹ : Neg R
toSub✝¹ : Sub R
toZSMul✝¹ : ZSMul R
sub_eq_add_neg✝¹ : ∀ (a b : R), a - b = a + -b
zsmul_zero'✝¹ : ∀ (a : R), 0 • a = 0
zsmul_succ'✝¹ : ∀ (n : ℕ) (a : R), ↑n.succ • a = ↑n • a + a
zsmul_neg'✝¹ : ∀ (n : ℕ) (a : R), Int.negSucc n • a = -(↑n.succ • a)
neg_add_cancel✝¹ : ∀ (a : R), -a + a = 0
toIntCast✝¹ : IntCast R
intCast_ofNat✝¹ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝¹ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
toSemiring✝ : Semiring R
toNeg✝ : Neg R
toSub✝ : Sub R
toZSMul✝ : ZSMul R
sub_eq_add_neg✝ : ∀ (a b : R), a - b = a + -b
zsmul_zero'✝ : ∀ (a : R), 0 • a = 0
zsmul_succ'✝ : ∀ (n : ℕ) (a : R), ↑n.succ • a = ↑n • a + a
zsmul_neg'✝ : ∀ (n : ℕ) (a : R), Int.negSucc n • a = -(↑n.succ • a)
neg_add_cancel✝ : ∀ (a : R), -a + a = 0
toIntCast✝ : IntCast R
intCast_ofNat✝ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ :
  { toSemiring := toSemiring✝¹, toNeg := toNeg✝¹, toSub := toSub✝¹, toZSMul := toZSMul✝¹,
        sub_eq_add_neg := sub_eq_add_neg✝¹, zsmul_zero' := zsmul_zero'✝¹, zsmul_succ' := zsmul_succ'✝¹,
        zsmul_neg' := zsmul_neg'✝¹, neg_add_cancel := neg_add_cancel✝¹, toIntCast := toIntCast✝¹,
        intCast_ofNat := intCast_ofNat✝¹, intCast_negSucc := intCast_negSucc✝¹ }.toSemiring =
    { toSemiring := toSemiring✝, toNeg := toNeg✝, toSub := toSub✝, toZSMul := toZSMul✝,
        sub_eq_add_neg := sub_eq_add_neg✝, zsmul_zero' := zsmul_zero'✝, zsmul_succ' := zsmul_succ'✝,
        zsmul_neg' := zsmul_neg'✝, neg_add_cancel := neg_add_cancel✝, toIntCast := toIntCast✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toSemiring
h₂ : toNonAssocRing = toNonAssocRing
h₃ :
  { toSemiring := toSemiring✝¹, toNeg := toNeg✝¹, toSub := toSub✝¹, toZSMul := toZSMul✝¹,
          sub_eq_add_neg := sub_eq_add_neg✝¹, zsmul_zero' := zsmul_zero'✝¹, zsmul_succ' := zsmul_succ'✝¹,
          zsmul_neg' := zsmul_neg'✝¹, neg_add_cancel := neg_add_cancel✝¹, toIntCast := toIntCast✝¹,
          intCast_ofNat := intCast_ofNat✝¹, intCast_negSucc := intCast_negSucc✝¹ }.toAddCommGroup.toSubNegMonoid =
    { toSemiring := toSemiring✝, toNeg := toNeg✝, toSub := toSub✝, toZSMul := toZSMul✝,
          sub_eq_add_neg := sub_eq_add_neg✝, zsmul_zero' := zsmul_zero'✝, zsmul_succ' := zsmul_succ'✝,
          zsmul_neg' := zsmul_neg'✝, neg_add_cancel := neg_add_cancel✝, toIntCast := toIntCast✝,
          intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toAddCommGroup.toSubNegMonoid
⊢ toZSMul✝¹ = toZSMul✝

Tactic:
solve | injection h₂ | injection h₃

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

Goal state before:
pp: case e_toIntCast
R : Type u
toSemiring✝¹ : Semiring R
toNeg✝¹ : Neg R
toSub✝¹ : Sub R
toZSMul✝¹ : ZSMul R
sub_eq_add_neg✝¹ : ∀ (a b : R), a - b = a + -b
zsmul_zero'✝¹ : ∀ (a : R), 0 • a = 0
zsmul_succ'✝¹ : ∀ (n : ℕ) (a : R), ↑n.succ • a = ↑n • a + a
zsmul_neg'✝¹ : ∀ (n : ℕ) (a : R), Int.negSucc n • a = -(↑n.succ • a)
neg_add_cancel✝¹ : ∀ (a : R), -a + a = 0
toIntCast✝¹ : IntCast R
intCast_ofNat✝¹ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝¹ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
toSemiring✝ : Semiring R
toNeg✝ : Neg R
toSub✝ : Sub R
toZSMul✝ : ZSMul R
sub_eq_add_neg✝ : ∀ (a b : R), a - b = a + -b
zsmul_zero'✝ : ∀ (a : R), 0 • a = 0
zsmul_succ'✝ : ∀ (n : ℕ) (a : R), ↑n.succ • a = ↑n • a + a
zsmul_neg'✝ : ∀ (n : ℕ) (a : R), Int.negSucc n • a = -(↑n.succ • a)
neg_add_cancel✝ : ∀ (a : R), -a + a = 0
toIntCast✝ : IntCast R
intCast_ofNat✝ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ :
  { toSemiring := toSemiring✝¹, toNeg := toNeg✝¹, toSub := toSub✝¹, toZSMul := toZSMul✝¹,
        sub_eq_add_neg := sub_eq_add_neg✝¹, zsmul_zero' := zsmul_zero'✝¹, zsmul_succ' := zsmul_succ'✝¹,
        zsmul_neg' := zsmul_neg'✝¹, neg_add_cancel := neg_add_cancel✝¹, toIntCast := toIntCast✝¹,
        intCast_ofNat := intCast_ofNat✝¹, intCast_negSucc := intCast_negSucc✝¹ }.toSemiring =
    { toSemiring := toSemiring✝, toNeg := toNeg✝, toSub := toSub✝, toZSMul := toZSMul✝,
        sub_eq_add_neg := sub_eq_add_neg✝, zsmul_zero' := zsmul_zero'✝, zsmul_succ' := zsmul_succ'✝,
        zsmul_neg' := zsmul_neg'✝, neg_add_cancel := neg_add_cancel✝, toIntCast := toIntCast✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toSemiring
h₂ : toNonAssocRing = toNonAssocRing
h₃ :
  { toSemiring := toSemiring✝¹, toNeg := toNeg✝¹, toSub := toSub✝¹, toZSMul := toZSMul✝¹,
          sub_eq_add_neg := sub_eq_add_neg✝¹, zsmul_zero' := zsmul_zero'✝¹, zsmul_succ' := zsmul_succ'✝¹,
          zsmul_neg' := zsmul_neg'✝¹, neg_add_cancel := neg_add_cancel✝¹, toIntCast := toIntCast✝¹,
          intCast_ofNat := intCast_ofNat✝¹, intCast_negSucc := intCast_negSucc✝¹ }.toAddCommGroup.toSubNegMonoid =
    { toSemiring := toSemiring✝, toNeg := toNeg✝, toSub := toSub✝, toZSMul := toZSMul✝,
          sub_eq_add_neg := sub_eq_add_neg✝, zsmul_zero' := zsmul_zero'✝, zsmul_succ' := zsmul_succ'✝,
          zsmul_neg' := zsmul_neg'✝, neg_add_cancel := neg_add_cancel✝, toIntCast := toIntCast✝,
          intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toAddCommGroup.toSubNegMonoid
⊢ toIntCast✝¹ = toIntCast✝

Tactic:
solve | injection h₂ | injection h₃

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

Goal state before:
pp: case coe.zero.zero
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
a✝ : α
⊢ ↑a✝ * (0 + 0) = ↑a✝ * 0 + ↑a✝ * 0

Tactic:
try rfl

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

Goal state before:
pp: case coe.zero.coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
a✝¹ a✝ : α
⊢ ↑a✝¹ * (0 + ↑a✝) = ↑a✝¹ * 0 + ↑a✝¹ * ↑a✝

Tactic:
try rfl

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

Goal state before:
pp: case coe.coe.zero
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
a✝¹ a✝ : α
⊢ ↑a✝¹ * (↑a✝ + 0) = ↑a✝¹ * ↑a✝ + ↑a✝¹ * 0

Tactic:
try rfl

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

Goal state before:
pp: case coe.coe.coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
a✝² a✝¹ a✝ : α
⊢ ↑a✝² * (↑a✝¹ + ↑a✝) = ↑a✝² * ↑a✝¹ + ↑a✝² * ↑a✝

Tactic:
try rfl

Goal state after:
case coe.coe.coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LeftDistribClass α
a✝² a✝¹ a✝ : α
⊢ ↑a✝² * (↑a✝¹ + ↑a✝) = ↑a✝² * ↑a✝¹ + ↑a✝² * ↑a✝
Module: Mathlib.Algebra.Ring.WithZero

Goal state before:
pp: case coe.zero.zero
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a✝ : α
⊢ (0 + 0) * ↑a✝ = 0 * ↑a✝ + 0 * ↑a✝

Tactic:
try rfl

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

Goal state before:
pp: case coe.zero.coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a✝¹ a✝ : α
⊢ (0 + ↑a✝) * ↑a✝¹ = 0 * ↑a✝¹ + ↑a✝ * ↑a✝¹

Tactic:
try rfl

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

Goal state before:
pp: case coe.coe.zero
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a✝¹ a✝ : α
⊢ (↑a✝ + 0) * ↑a✝¹ = ↑a✝ * ↑a✝¹ + 0 * ↑a✝¹

Tactic:
try rfl

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

Goal state before:
pp: case coe.coe.coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a✝² a✝¹ a✝ : α
⊢ (↑a✝¹ + ↑a✝) * ↑a✝² = ↑a✝¹ * ↑a✝² + ↑a✝ * ↑a✝²

Tactic:
try rfl

Goal state after:
case coe.coe.coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a✝² a✝¹ a✝ : α
⊢ (↑a✝¹ + ↑a✝) * ↑a✝² = ↑a✝¹ * ↑a✝² + ↑a✝ * ↑a✝²
Module: Mathlib.Algebra.Ring.CentroidHom

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

Tactic:
exact fun ha ↦ ⟨AddMonoidHom.ext <| fun _ => (IsMulCentral.comm ha _).symm,
      ⟨centerToCentroid ⟨a, ha⟩, rfl⟩⟩

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
  · exact fun ha ↦ ⟨AddMonoidHom.ext <| fun _ => (IsMulCentral.comm ha _).symm,
      ⟨centerToCentroid ⟨a, ha⟩, rfl⟩⟩
  · rintro ⟨hc, ⟨T, hT⟩⟩
    have e1 (d : α) : T d = a * d := congr($hT d)
    have e2 (d : α) : T d = d * a := congr($(hT.trans hc.symm) d)
    constructor
    case comm => exact (congr($hc.symm ·))
    case left_assoc => simpa [e1] using (map_mul_right T · ·)
    case right_assoc => simpa [e2] using (map_mul_left T · ·)

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

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Semiring k
inst✝⁵ : Monoid G
inst✝⁴ : MulSemiringAction G k
V : Type u_4
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : Module (SkewMonoidAlgebra k G) V
inst✝ : IsScalarTower k (SkewMonoidAlgebra k G) V
W : Submodule k V
h : ∀ (g : G), ∀ v ∈ W, (of k G) g • v ∈ W
f : SkewMonoidAlgebra k G
v : V
⊢ v ∈ ↑W → f • v ∈ ↑W

Tactic:
hv

Goal state after:
k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Semiring k
inst✝⁵ : Monoid G
inst✝⁴ : MulSemiringAction G k
V : Type u_4
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : Module (SkewMonoidAlgebra k G) V
inst✝ : IsScalarTower k (SkewMonoidAlgebra k G) V
W : Submodule k V
h : ∀ (g : G), ∀ v ∈ W, (of k G) g • v ∈ W
f : SkewMonoidAlgebra k G
v : V
hv : v ∈ ↑W
⊢ f • v ∈ ↑W
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

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

Tactic:
aesop (add norm [update, Finsupp.support_update_ne_zero])

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
H : 1 = 0
⊢ ((monomial 1) 0).support = ∅

Tactic:
monomial_zero_right,

Goal state after:
R : Type u_1
inst✝ : Semiring R
H : 1 = 0
⊢ support 0 = ∅
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : AddMonoid k
S : Type u_3
inst✝¹ : Monoid S
inst✝ : DistribMulAction S k
a : S
ha : IsSMulRegular k a
coeff✝¹ coeff✝ : G →₀ k
h : (fun x ↦ a • x) { coeff := coeff✝¹ } = (fun x ↦ a • x) { coeff := coeff✝ }
⊢ { coeff := coeff✝¹ } = { coeff := coeff✝ }

Tactic:
by
    exact congr_arg _ <| ha.finsupp (ofCoeff.inj h)

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
f : SkewMonoidAlgebra k G
⊢ f * 1 = f

Tactic:
induction f with
    | single g a => rw [one_def, mul_def, sum_single_index, sum_single_index] <;> simp
    | add f g _ _ => simp_all [add_mul]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
inst✝³ : AddMonoid k
inst✝² : SMulZeroClass S k
inst✝¹ : FaithfulSMul S k
inst✝ : Nonempty G
_s₁ _s₂ : S
h : ∀ (a : SkewMonoidAlgebra k G), _s₁ • a = _s₂ • a
⊢ _s₁ = _s₂

Tactic:
apply eq_of_smul_eq_smul fun a : G →₀ k ↦ congr_arg coeff _
    intro a
    simp_rw [ofCoeff_smul, h]

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

Goal state before:

Tactic:
(f * g).coeff x = ∑ a₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂) := coeff_mul f g x
    _ = ∑ p ∈ f.support ×ˢ g.support, F p := by rw [Finset.sum_product]
    _ = ∑ p ∈ (f.support ×ˢ g.support).filter fun p : G × G ↦ p.1 * p.2 = x,
      f.coeff p.1 * p.1 • g.coeff p.2 := (Finset.sum_filter _ _).symm
    _ = ∑ p ∈ s.filter fun p : G × G ↦ p.1 ∈ f.support ∧ p.2 ∈ g.support,
      f.coeff p.1 * p.1 • g.coeff p.2 := by
        apply Finset.sum_congr_of_eq_on_inter <;> aesop
    _ = ∑ p ∈ s, f.coeff p.1 * p.1 • g.coeff p.2 :=
      Finset.sum_subset (Finset.filter_subset _ _) fun p hps hp ↦ by
        simp only [Finset.mem_filter, mem_support_iff, not_and, Classical.not_not] at hp ⊢
        by_cases h1 : f.coeff p.1 = 0 <;> simp_all

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

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

Tactic:
X.basicOpen_res i f

Goal state after:
case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
⊢ unop V ⊓ X.basicOpen f ≤ X.basicOpen f
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ f.toPshHom.c.app (op ((PresheafedSpace.IsOpenImmersion.opensFunctor f.toPshHom).obj U)) ≫ X.presheaf.map (eqToHom ⋯) =
    app f (f ''ᵁ U) ≫ X.presheaf.map (eqToHom ⋯).op

Tactic:
rw [eqToHom_op]; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: X Y : Type u
f : X ⟶ Y
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
x : Y
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom f)

Tactic:
by simp [hf.range_eq]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PreservesLimit (cospan ((cospan f g ⋙ forget).map Hom.inl) ((cospan f g ⋙ forget).map Hom.inr))
    LocallyRingedSpace.forgetToTop

Tactic:
dsimp [LocallyRingedSpace.forgetToTop]

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PreservesLimit (cospan (Scheme.Hom.toLRSHom f) (Scheme.Hom.toLRSHom g))
    (LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat)
Module: Mathlib.Topology.Category.TopCommRingCat

Goal state before:
pp: X Y : TopCommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget₂ TopCommRingCat TopCat).map f)
i_Top : (forget₂ TopCommRingCat TopCat).obj X ≅ (forget₂ TopCommRingCat TopCat).obj Y :=
  asIso ((forget₂ TopCommRingCat TopCat).map f)
e_Ring : X.α ≃+* Y.α :=
  let __src := ↑f;
  let __src_1 := ((forget TopCat).mapIso i_Top).toEquiv;
  { toFun := (↑↑__src).toFun, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
⊢ ⟨↑e_Ring.symm, ⋯⟩ ≫ f = 𝟙 Y

Tactic:
ext x
            exact e_Ring.right_inv x

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
f g₁ g₂ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : U ≤ basicOpen g₁
hu₂ : U ≤ basicOpen g₂
⊢ const g₁ g₂ U hu₂ * const f g₁ U hu₁ = const f g₂ U hu₂

Tactic:
by
  rw [mul_comm, const_mul_cancel]

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

Goal state before:
pp: X✝ : TopCat
R✝ : TopCommRingCat
X : TopCatᵒᵖ
R S : TopCommRingCat
φ : R ⟶ S
x✝² x✝¹ : unop X ⟶ (forget₂ TopCommRingCat TopCat).obj R
x✝ : ↑(unop X)
⊢ (ConcreteCategory.hom ((x✝² + x✝¹) ≫ (forget₂ TopCommRingCat TopCat).map φ)) x✝ =
    (ConcreteCategory.hom (x✝² ≫ (forget₂ TopCommRingCat TopCat).map φ + x✝¹ ≫ (forget₂ TopCommRingCat TopCat).map φ))
      x✝

Tactic:
exact φ.1.map_add _ _

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
s : (structureSheafInType R M).obj.obj (op (basicOpen f))
ι : Type u
w✝ : Fintype ι
a : ι → M
b : ι → R
ibU : ∀ (i : ι), basicOpen (b i) ≤ basicOpen f
iU : basicOpen f ≤ ⨆ i, basicOpen (b i)
hab : ∀ (i j : ι), b j • a i = b i • a j
H :
  ∀ (i : ι),
    (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s = const (a i) (b i) (basicOpen (b i)) ⋯
⊢ PrimeSpectrum.zeroLocus (Set.range b) ⊆ PrimeSpectrum.zeroLocus {f}

Tactic:
simpa [← SetLike.coe_subset_coe, ← Set.compl_iInter,
        ← PrimeSpectrum.zeroLocus_iUnion, PrimeSpectrum.Top] using iU

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝ : P.IsLocalAtSource K
X Y : C
f : X ⟶ Y
𝒰 : K.ZeroHypercover X
h : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
U : C
g : U ⟶ X
⊢ 𝒰.presieve₀ g → P (g ≫ f)

Tactic:
rintro ⟨i⟩; exact h _

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : Scheme
⊢ Hom.appTop X.toSpecΓ = (ΓSpecIso Γ(X, ⊤)).hom

Tactic:
have := ΓSpec.adjunction.left_triangle_components X

Goal state after:
X : Scheme
this : Γ.rightOp.map (ΓSpec.adjunction.unit.app X) ≫ ΓSpec.adjunction.counit.app (Γ.rightOp.obj X) = 𝟙 (Γ.rightOp.obj X)
⊢ Hom.appTop X.toSpecΓ = (ΓSpecIso Γ(X, ⊤)).hom
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
inst✝ : IsAffine X
s : Set ↑Γ(X, ⊤)
⊢ ⇑X.isoSpec.hom '' X.zeroLocus s = PrimeSpectrum.zeroLocus s

Tactic:
rw [← X.toSpecΓ_preimage_zeroLocus]
  simp [Scheme.isoSpec, Set.image_preimage_eq (h := (bijective_of_isIso _).surjective)]

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
h : MkCore
i j k : h.J
⊢ h.t' i j k ≫ pullback.snd (h.V j k).inclusion' (h.V j i).inclusion' =
    pullback.fst (h.V i j).inclusion' (h.V i k).inclusion' ≫ h.t i j

Tactic:
delta MkCore.t'

Goal state after:
D : GlueData
h : MkCore
i j k : h.J
⊢ ((pullbackIsoProdSubtype (h.V i j).inclusion' (h.V i k).inclusion').hom ≫
        ofHom
            {
              toFun := fun x ↦
                ⟨(⟨↑((ConcreteCategory.hom (h.t i j)) (↑x).1), ⋯⟩, (ConcreteCategory.hom (h.t i j)) (↑x).1), ⋯⟩,
              continuous_toFun := ⋯ } ≫
          (pullbackIsoProdSubtype (h.V j k).inclusion' (h.V j i).inclusion').inv) ≫
      pullback.snd (h.V j k).inclusion' (h.V j i).inclusion' =
    pullback.fst (h.V i j).inclusion' (h.V i k).inclusion' ≫ h.t i j