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

Goal state before:
pp: case e_toNatCast
R : Type u
toNonUnitalNonAssocRing✝¹ : NonUnitalNonAssocRing R
toOne✝¹ : One R
one_mul✝¹ : ∀ (a : R), 1 * a = a
mul_one✝¹ : ∀ (a : R), a * 1 = a
toNatCast✝¹ : NatCast R
natCast_zero✝¹ : ↑0 = 0
natCast_succ✝¹ : ∀ (n : ℕ), ↑(n + 1) = ↑n + 1
toIntCast✝¹ : IntCast R
intCast_ofNat✝¹ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝¹ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
toNonUnitalNonAssocRing✝ : NonUnitalNonAssocRing R
toOne✝ : One R
one_mul✝ : ∀ (a : R), 1 * a = a
mul_one✝ : ∀ (a : R), a * 1 = a
toNatCast✝ : NatCast R
natCast_zero✝ : ↑0 = 0
natCast_succ✝ : ∀ (n : ℕ), ↑(n + 1) = ↑n + 1
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₁ :
  { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹,
        toNatCast := toNatCast✝¹, natCast_zero := natCast_zero✝¹, natCast_succ := natCast_succ✝¹,
        toIntCast := toIntCast✝¹, intCast_ofNat := intCast_ofNat✝¹,
        intCast_negSucc := intCast_negSucc✝¹ }.toNonUnitalNonAssocRing =
    { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝,
        toNatCast := toNatCast✝, natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, toIntCast := toIntCast✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toNonUnitalNonAssocRing
h₂ :
  { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹,
        toNatCast := toNatCast✝¹, natCast_zero := natCast_zero✝¹, natCast_succ := natCast_succ✝¹,
        toIntCast := toIntCast✝¹, intCast_ofNat := intCast_ofNat✝¹,
        intCast_negSucc := intCast_negSucc✝¹ }.toNonAssocSemiring =
    { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝,
        toNatCast := toNatCast✝, natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, toIntCast := toIntCast✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toNonAssocSemiring
h₃ :
  { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹,
        toNatCast := toNatCast✝¹, natCast_zero := natCast_zero✝¹, natCast_succ := natCast_succ✝¹,
        toIntCast := toIntCast✝¹, intCast_ofNat := intCast_ofNat✝¹,
        intCast_negSucc := intCast_negSucc✝¹ }.toAddCommGroupWithOne =
    { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝,
        toNatCast := toNatCast✝, natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, toIntCast := toIntCast✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toAddCommGroupWithOne
⊢ toNatCast✝¹ = toNatCast✝

Tactic:
injection h₂

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

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

Tactic:
congr

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

Goal state before:
pp: case h_mul
R : Type u
a₁✝ a₂✝ : NonAssocRing R
a✝ : a₁✝.toNonUnitalNonAssocRing = a₂✝.toNonUnitalNonAssocRing
x✝¹ x✝ : R
⊢ x✝¹ * x✝ = x✝¹ * x✝

Tactic:
congr

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
h : ∀ {s a : R}, IsSumSq s → a * a + s = 0 → a = 0
x a✝ : R
ha : a✝ ≠ 0
hc : a✝ * a✝ = 0
⊢ a✝ * a✝ + 0 = 0

Tactic:
by simpa using hc

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:
injection h₂

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

Goal state before:
pp: R : Type u
toNonUnitalNonAssocSemiring✝¹ : NonUnitalNonAssocSemiring R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toNonUnitalNonAssocSemiring✝ : NonUnitalNonAssocSemiring R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ :
  { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝¹, mul_comm := mul_comm✝¹ }.toNonUnitalNonAssocSemiring =
    { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, mul_comm := mul_comm✝ }.toNonUnitalNonAssocSemiring
⊢ { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝¹, mul_comm := mul_comm✝¹ } =
    { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, mul_comm := mul_comm✝ }

Tactic:
congr

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

Goal state before:
pp: R : Type u
toNonUnitalSemiring✝¹ : NonUnitalSemiring R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toNonUnitalSemiring✝ : NonUnitalSemiring R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ :
  { toNonUnitalSemiring := toNonUnitalSemiring✝¹, mul_comm := mul_comm✝¹ }.toNonUnitalSemiring =
    { toNonUnitalSemiring := toNonUnitalSemiring✝, mul_comm := mul_comm✝ }.toNonUnitalSemiring
⊢ { toNonUnitalSemiring := toNonUnitalSemiring✝¹, mul_comm := mul_comm✝¹ } =
    { toNonUnitalSemiring := toNonUnitalSemiring✝, mul_comm := mul_comm✝ }

Tactic:
congr

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

Goal state before:
pp: R : Type u
toNonUnitalNonAssocRing✝¹ : NonUnitalNonAssocRing R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toNonUnitalNonAssocRing✝ : NonUnitalNonAssocRing R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ :
  { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝¹, mul_comm := mul_comm✝¹ }.toNonUnitalNonAssocRing =
    { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, mul_comm := mul_comm✝ }.toNonUnitalNonAssocRing
⊢ { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝¹, mul_comm := mul_comm✝¹ } =
    { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, mul_comm := mul_comm✝ }

Tactic:
congr

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

Goal state before:
pp: R : Type u
toNonUnitalRing✝¹ : NonUnitalRing R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toNonUnitalRing✝ : NonUnitalRing R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ :
  { toNonUnitalRing := toNonUnitalRing✝¹, mul_comm := mul_comm✝¹ }.toNonUnitalRing =
    { toNonUnitalRing := toNonUnitalRing✝, mul_comm := mul_comm✝ }.toNonUnitalRing
⊢ { toNonUnitalRing := toNonUnitalRing✝¹, mul_comm := mul_comm✝¹ } =
    { toNonUnitalRing := toNonUnitalRing✝, mul_comm := mul_comm✝ }

Tactic:
congr

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

Goal state before:
pp: R : Type u
toSemiring✝¹ : Semiring R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toSemiring✝ : Semiring R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ :
  { toSemiring := toSemiring✝¹, mul_comm := mul_comm✝¹ }.toSemiring =
    { toSemiring := toSemiring✝, mul_comm := mul_comm✝ }.toSemiring
⊢ { toSemiring := toSemiring✝¹, mul_comm := mul_comm✝¹ } = { toSemiring := toSemiring✝, mul_comm := mul_comm✝ }

Tactic:
congr

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

Goal state before:
pp: R : Type u
toRing✝¹ : Ring R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toRing✝ : Ring R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ : { toRing := toRing✝¹, mul_comm := mul_comm✝¹ }.toRing = { toRing := toRing✝, mul_comm := mul_comm✝ }.toRing
⊢ { toRing := toRing✝¹, mul_comm := mul_comm✝¹ } = { toRing := toRing✝, mul_comm := mul_comm✝ }

Tactic:
congr

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

Goal state before:
pp: α : Type u_5
inst✝ : NonUnitalNonAssocCommSemiring α
a : α
⊢ (AddMonoid.End.mulRight a = L a ∧ ∀ g ∈ Set.range ⇑L ∪ Set.range ⇑AddMonoid.End.mulRight, g * L a = L a * g) ↔
    ∀ (b : α), Commute (L b) (L a)

Tactic:
AddMonoid.End.mulRight_eq_mulLeft,

Goal state after:
α : Type u_5
inst✝ : NonUnitalNonAssocCommSemiring α
a : α
⊢ (L a = L a ∧ ∀ g ∈ Set.range ⇑L ∪ Set.range ⇑L, g * L a = L a * g) ↔ ∀ (b : α), Commute (L b) (L a)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

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

Tactic:
by
  classical
  rw [f.coeff_update_apply, if_neg h]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p : SkewPolynomial R
f : ℕ → R → S
⊢ ∑ x ∈ p.coeff.support, f (toAdd x) (p.coeff x) = ∑ n ∈ p.support, f n (p.coeff n)

Tactic:
apply Finset.sum_of_injOn (toAdd) (Injective.injOn fun ⦃a₁ a₂⦄ a ↦ a) (fun _ ↦ ?_) <;>
  simp +contextual [coeff]

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

Goal state before:
pp: case mk.mk
A : Type v
B : Type w
C : Type w'
R : Type v
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : Star R
toNonUnitalSubsemiring✝¹ : NonUnitalSubsemiring R
star_mem'✝¹ : ∀ {a : R}, a ∈ toNonUnitalSubsemiring✝¹.carrier → star a ∈ toNonUnitalSubsemiring✝¹.carrier
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring R
star_mem'✝ : ∀ {a : R}, a ∈ toNonUnitalSubsemiring✝.carrier → star a ∈ toNonUnitalSubsemiring✝.carrier
h : (fun {s} ↦ s.carrier) = fun {s} ↦ s.carrier
⊢ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝¹, star_mem' := star_mem'✝¹ } =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, star_mem' := star_mem'✝ }

Tactic:
congr

Goal state after:
case mk.mk
A : Type v
B : Type w
C : Type w'
R : Type v
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : Star R
toNonUnitalSubsemiring✝¹ : NonUnitalSubsemiring R
star_mem'✝¹ : ∀ {a : R}, a ∈ toNonUnitalSubsemiring✝¹.carrier → star a ∈ toNonUnitalSubsemiring✝¹.carrier
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring R
star_mem'✝ : ∀ {a : R}, a ∈ toNonUnitalSubsemiring✝.carrier → star a ∈ toNonUnitalSubsemiring✝.carrier
h : (fun {s} ↦ s.carrier) = fun {s} ↦ s.carrier
⊢ toNonUnitalSubsemiring✝¹ = toNonUnitalSubsemiring✝
Module: Mathlib.Algebra.Star.Subsemiring

Goal state before:
pp: case mk
R : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : Star R
carrier✝ : Set R
mul_mem'✝ : ∀ {a b : R}, a ∈ carrier✝ → b ∈ carrier✝ → a * b ∈ carrier✝
one_mem'✝ : 1 ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝ }.carrier
add_mem'✝ :
  ∀ {a b : R},
    a ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier →
      b ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier →
        a + b ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier
zero_mem'✝ : 0 ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier
star_mem'✝¹ :
  ∀ {a : R},
    a ∈
        { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, add_mem' := add_mem'✝,
            zero_mem' := zero_mem'✝ }.carrier →
      star a ∈
        { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, add_mem' := add_mem'✝,
            zero_mem' := zero_mem'✝ }.carrier
toSubsemiring✝ : Subsemiring R
star_mem'✝ : ∀ {a : R}, a ∈ toSubsemiring✝.carrier → star a ∈ toSubsemiring✝.carrier
h : (fun {s} ↦ s.carrier) = fun {s} ↦ s.carrier
⊢ { carrier := carrier✝, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, add_mem' := add_mem'✝, zero_mem' := zero_mem'✝,
      star_mem' := star_mem'✝¹ } =
    { toSubsemiring := toSubsemiring✝, star_mem' := star_mem'✝ }

Tactic:
congr

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p q : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
h : p ≠ q
h01 : 0 = 1
⊢ p * 1 = q * 1

Tactic:
← C_1,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
p q : SkewPolynomial R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
h : p ≠ q
h01 : 0 = 1
⊢ p * C 1 = q * C 1
Module: Mathlib.Algebra.Star.TransferInstance

Goal state before:
pp: R : Type u_1
S : Type u_2
e : R ≃ S
inst✝¹ : Mul S
inst✝ : StarMul S
this✝ : Star R := e.star
this : Mul R := e.mul
⊢ StarMul R

Tactic:
apply e.injective.starMul <;> (intros; exact e.apply_symm_apply _)

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

Tactic:
congr

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

Goal state before:
pp: case e_g
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 x✝¹ : G
x✝ : k
⊢ (g.sum fun a₁ b ↦ (single (x✝¹ * a₁) (x✝ * x✝¹ • b)).coeff x) =
    g.sum fun a₂ b₂ ↦ if x✝¹ * a₂ = x then x✝ * x✝¹ • b₂ else 0

Tactic:
congr

Goal state after:
case e_g.e_g
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 x✝¹ : G
x✝ : k
⊢ (fun a₁ b ↦ (single (x✝¹ * a₁) (x✝ * x✝¹ • b)).coeff x) = fun a₂ b₂ ↦ if x✝¹ * a₂ = x then x✝ * x✝¹ • b₂ else 0
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
⊢ (x.sum fun a b ↦ y.sum fun a₂ b₂ ↦ single (f a * f a₂) (b * a • b₂)) =
    x.sum fun a m ↦ ((mapDomain ⇑f) y).sum fun a₂ b₂ ↦ single (f a * a₂) (m * f a • b₂)

Tactic:
congr

Goal state after:
case e_g
α : 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
⊢ (fun a b ↦ y.sum fun a₂ b₂ ↦ single (f a * f a₂) (b * a • b₂)) = fun a m ↦
    ((mapDomain ⇑f) y).sum fun a₂ b₂ ↦ single (f a * a₂) (m * f a • b₂)
Module: Mathlib.Algebra.Tropical.Lattice

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Set (Tropical R)
hs : ¬BddBelow s
this : Set.range untrop = Set.univ
⊢ sInf s = sInf ∅

Tactic:
simp only [sInf, Set.image_empty, trop_inj_iff]

Goal state after:
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Set (Tropical R)
hs : ¬BddBelow s
this : Set.range untrop = Set.univ
⊢ sInf (untrop '' s) = sInf ∅
Module: Mathlib.Geometry.RingedSpace.SheafedSpace

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : ↑X.toPresheafedSpace ⟶ ↑Y.toPresheafedSpace
fc gc : Y.presheaf ⟶ (pushforward C f).obj X.presheaf
h' :
  ∀ (x : ↑↑X.toPresheafedSpace),
    PresheafedSpace.Hom.stalkMap { hom := { base := f, c := fc } }.hom x =
      (Y.presheaf.stalkCongr ⋯).hom ≫ PresheafedSpace.Hom.stalkMap { hom := { base := f, c := gc } }.hom x
⊢ { hom := { base := f, c := fc } } = { hom := { base := f, c := gc } }

Tactic:
congr

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : ↑X.toPresheafedSpace ⟶ ↑Y.toPresheafedSpace
fc gc : Y.presheaf ⟶ (pushforward C f).obj X.presheaf
h' :
  ∀ (x : ↑↑X.toPresheafedSpace),
    PresheafedSpace.Hom.stalkMap { hom := { base := f, c := fc } }.hom x =
      (Y.presheaf.stalkCongr ⋯).hom ≫ PresheafedSpace.Hom.stalkMap { hom := { base := f, c := gc } }.hom x
⊢ fc = gc
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: J : Type u'
inst✝² : Category.{v', u'} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimitsOfShape J TopCat
F : J ⥤ PresheafedSpace C
j₁ j₂ j₃ : J
f : j₁ ⟶ j₂
g : j₂ ⟶ j₃
U : (Opens ↑(colimit (F ⋙ forget C)))ᵒᵖ
⊢ unop (op ((Opens.map ((F.map g).base ≫ colimit.ι (F ⋙ forget C) j₃)).obj (unop U))) =
    unop (op ((Opens.map (colimit.ι (F ⋙ forget C) j₂)).obj (unop U)))

Tactic:
congr

Goal state after:
case e_self
J : Type u'
inst✝² : Category.{v', u'} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimitsOfShape J TopCat
F : J ⥤ PresheafedSpace C
j₁ j₂ j₃ : J
f : j₁ ⟶ j₂
g : j₂ ⟶ j₃
U : (Opens ↑(colimit (F ⋙ forget C)))ᵒᵖ
⊢ (F.map g).base ≫ colimit.ι (F ⋙ forget C) j₃ = colimit.ι (F ⋙ forget C) j₂
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: case mk.mk
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
base✝¹ : ↑X ⟶ ↑Y
c✝¹ : Y.presheaf ⟶ (Presheaf.pushforward C base✝¹).obj X.presheaf
base✝ : ↑X ⟶ ↑Y
c✝ : Y.presheaf ⟶ (Presheaf.pushforward C base✝).obj X.presheaf
w : { base := base✝¹, c := c✝¹ }.base = { base := base✝, c := c✝ }.base
h : { base := base✝¹, c := c✝¹ }.c ≍ { base := base✝, c := c✝ }.c
⊢ { base := base✝¹, c := c✝¹ } = { base := base✝, c := c✝ }

Tactic:
congr

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

Goal state before:
pp: case mk.mk
X Y : LocallyRingedSpace
toHom✝¹ : X.Hom Y.toPresheafedSpace
prop✝¹ : ∀ (x : ↑↑X.toPresheafedSpace), IsLocalHom (CommRingCat.Hom.hom (toHom✝¹.stalkMap x))
toHom✝ : X.Hom Y.toPresheafedSpace
prop✝ : ∀ (x : ↑↑X.toPresheafedSpace), IsLocalHom (CommRingCat.Hom.hom (toHom✝.stalkMap x))
h : { toHom := toHom✝¹, prop := prop✝¹ }.toHom = { toHom := toHom✝, prop := prop✝ }.toHom
⊢ { toHom := toHom✝¹, prop := prop✝¹ } = { toHom := toHom✝, prop := prop✝ }

Tactic:
congr

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

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : ↥U → Opens ↑↑X.toPresheafedSpace
iVU : (x : ↥U) → V x ⟶ U
m : ∀ (x : ↥U), ↑x ∈ V x
h_unit : ∀ (x : ↥U), IsUnit ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f)
hcover : U ≤ iSup V
g : (x : ↥U) → ↑(X.presheaf.obj (op (V x)))
hg : ∀ (x : ↥U), (ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f * g x = 1
x : ↥U
⊢ ∀ (j : ↥U),
    (ConcreteCategory.hom ((sheaf X).obj.map ((V x).infLELeft (V j)).op)) (g x) =
      (ConcreteCategory.hom ((sheaf X).obj.map ((V x).infLERight (V j)).op)) (g j)

Tactic:
y

Goal state after:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : ↥U → Opens ↑↑X.toPresheafedSpace
iVU : (x : ↥U) → V x ⟶ U
m : ∀ (x : ↥U), ↑x ∈ V x
h_unit : ∀ (x : ↥U), IsUnit ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f)
hcover : U ≤ iSup V
g : (x : ↥U) → ↑(X.presheaf.obj (op (V x)))
hg : ∀ (x : ↥U), (ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f * g x = 1
x y : ↥U
⊢ (ConcreteCategory.hom ((sheaf X).obj.map ((V x).infLELeft (V y)).op)) (g x) =
    (ConcreteCategory.hom ((sheaf X).obj.map ((V x).infLERight (V y)).op)) (g y)
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X✝ X Y : LocallyRingedSpace
f : X.toSheafedSpace ≅ Y.toSheafedSpace
⊢ homOfSheafedSpaceHomOfIsIso f.inv ≫ homOfSheafedSpaceHomOfIsIso f.hom = 𝟙 Y

Tactic:
ext : 1
    dsimp
    rw [← InducedCategory.comp_hom, f.inv_hom_id, SheafedSpace.id_hom]

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

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(X.basicOpen (f * g)) ↔ x ∈ ↑(X.basicOpen f ⊓ X.basicOpen g)

Tactic:
by_cases hx : x ∈ U

Goal state after:
case pos
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
⊢ x ∈ ↑(X.basicOpen (f * g)) ↔ x ∈ ↑(X.basicOpen f ⊓ X.basicOpen g)

case neg
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∉ U
⊢ x ∈ ↑(X.basicOpen (f * g)) ↔ x ∈ ↑(X.basicOpen f ⊓ X.basicOpen g)