mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case cons
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
hf :
  q₁ * (g i * ∏ x ∈ s, g x) +
      (r₁ i * ∏ k ∈ (Finset.cons i s hi).erase i, g k + ∑ x ∈ s, r₁ x * ∏ k ∈ (Finset.cons i s hi).erase x, g k) =
    q₂ * (g i * ∏ x ∈ s, g x) +
      (r₂ i * ∏ k ∈ (Finset.cons i s hi).erase i, g k + ∑ x ∈ s, r₂ x * ∏ k ∈ (Finset.cons i s hi).erase x, g k)
cop : IsCoprime (g i) (∏ i ∈ s, g i)
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1

Tactic:
Finset.erase_cons

Goal state after:
case cons
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
hf :
  q₁ * (g i * ∏ x ∈ s, g x) + (r₁ i * ∏ k ∈ s, g k + ∑ x ∈ s, r₁ x * ∏ k ∈ (Finset.cons i s hi).erase x, g k) =
    q₂ * (g i * ∏ x ∈ s, g x) + (r₂ i * ∏ k ∈ s, g k + ∑ x ∈ s, r₂ x * ∏ k ∈ (Finset.cons i s hi).erase x, g k)
cop : IsCoprime (g i) (∏ i ∈ s, g i)
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case cons
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hf :
  (r₁ i - r₂ i) * ∏ x ∈ s, g x +
      (g i * (q₁ * ∏ x ∈ s, g x + ∑ i ∈ s, r₁ i * ∏ x ∈ s.erase i, g x) -
        g i * (q₂ * ∏ x ∈ s, g x + ∑ i ∈ s, r₂ i * ∏ x ∈ s.erase i, g x)) =
    0
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1

Tactic:
← mul_sub,

Goal state after:
case cons
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hf :
  (r₁ i - r₂ i) * ∏ x ∈ s, g x +
      g i *
        (q₁ * ∏ x ∈ s, g x + ∑ i ∈ s, r₁ i * ∏ x ∈ s.erase i, g x -
          (q₂ * ∏ x ∈ s, g x + ∑ i ∈ s, r₂ i * ∏ x ∈ s.erase i, g x)) =
    0
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
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
⊢ (algebraMap R[X] K) q * ∏ x ∈ s, (algebraMap R[X] K) (g x ^ n x) * gi x ^ n x +
      (algebraMap R[X] K) (∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k) * ∏ i ∈ s, gi i ^ n i =
    (algebraMap R[X] K) q + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) ((fun i j ↦ r i j.rev) i j) * gi i ^ (↑j + 1)

Tactic:
rw [Finset.prod_congr rfl hc, Finset.prod_const_one,
    mul_one, add_right_inj, map_sum, Finset.sum_mul]

Goal state after:
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 ∈ s, (algebraMap R[X] K) (∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k) * ∏ i ∈ s, gi i ^ n i =
    ∑ i ∈ s, ∑ j, (algebraMap R[X] K) ((fun i j ↦ r i j.rev) i j) * gi i ^ (↑j + 1)
Module: Mathlib.Algebra.Quandle

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

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

Tactic:
· rintro rfl; rfl

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

Goal state before:
pp: case succ
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : inst₁.toAddMonoid = inst₂.toAddMonoid
h_zero' : inst₁.toZero = inst₂.toZero
h_one' : inst₁.toOne = inst₂.toOne
n : ℕ
h : ↑n = ↑n
⊢ ↑n + 1 = ↑(n + 1)

Tactic:
inst₂.natCast_succ,

Goal state after:
case succ
R : Type u
inst₁ inst₂ : AddMonoidWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
h_monoid : inst₁.toAddMonoid = inst₂.toAddMonoid
h_zero' : inst₁.toZero = inst₂.toZero
h_one' : inst₁.toOne = inst₂.toOne
n : ℕ
h : ↑n = ↑n
⊢ ↑n + 1 = ↑n + 1
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: case sq_add.inl
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
s✝ s : R
hs✝ : IsSumSq s
ih : s ≠ 0 → IsSumNonzeroSq s
hs : 0 * 0 + s ≠ 0
⊢ IsSumNonzeroSq (0 * 0 + s)

pp: case sq_add.inr
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
s✝ a s : R
hs✝ : IsSumSq s
ih : s ≠ 0 → IsSumNonzeroSq s
hs : a * a + s ≠ 0
ne_a : a ≠ 0
⊢ IsSumNonzeroSq (a * a + s)

Tactic:
· simp_all

Goal state after:
case sq_add.inr
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
s✝ a s : R
hs✝ : IsSumSq s
ih : s ≠ 0 → IsSumNonzeroSq s
hs : a * a + s ≠ 0
ne_a : a ≠ 0
⊢ IsSumNonzeroSq (a * a + s)
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
⊢ a ∈ NonUnitalSubsemiring.center α

Tactic:
have e2 (d : α) : T d = d * a := congr($(hT.trans hc.symm) d)

Goal state after:
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 α
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 α
z : ↥(Subsemiring.center α)
⊢ ↑((fun T ↦ ⟨T 1, ⋯⟩) (centerToCentroid.toFun z)) = ↑z

Tactic:
by simp only [MulHom.toFun_eq_coe,
      NonUnitalRingHom.coe_toMulHom, centerToCentroid_apply, mul_one]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Monoid G
inst✝² : Semiring k
inst✝¹ : MulSemiringAction G k
f : SkewMonoidAlgebra k G
inst✝ : DecidableEq G
r : k
x : G
rx : IsRightRegular x
hrx : ∀ (g : G) (y : k), y * g • r = 0 ↔ y = 0
⊢ (f * single x r).support = image (fun x_1 ↦ x_1 * x) f.support

Tactic:
by
  refine subset_antisymm (support_mul_single_subset f _ _) fun y hy ↦ ?_
  obtain ⟨y, yf, rfl⟩ : ∃ a : G, a ∈ f.support ∧ a * x = y := by
    simpa only [Finset.mem_image, exists_prop] using hy
  simp [coeff_mul, mem_support_iff.mp yf, hrx, mem_support_iff, sum_single_index, mul_zero,
    ite_self, rx.eq_iff]

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

Goal state before:
pp: case a
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f✝ : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ (Finset.cons a s has).erase a = s

Tactic:
Finset.erase_cons

Goal state after:
case a
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f✝ : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ s = s
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
⊢ ∀ (a : RingQuot r), 0 + a = a

Tactic:
rintro ⟨⟨⟩⟩

Goal state after:
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✝ }
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
⊢ ∀ (a : RingQuot r), a + 0 = a

Tactic:
rintro ⟨⟨⟩⟩

Goal state after:
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
⊢ { toQuot := Quot.mk (Rel r) a✝ } + 0 = { toQuot := Quot.mk (Rel r) 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
⊢ ∀ (x : RingQuot r), 0 • x = 0

Tactic:
rintro ⟨⟨⟩⟩

Goal state after:
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✝ } = 0
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
⊢ ∀ (a : RingQuot r), 1 * a = a

Tactic:
rintro ⟨⟨⟩⟩

Goal state after:
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
⊢ 1 * { toQuot := Quot.mk (Rel r) a✝ } = { toQuot := Quot.mk (Rel r) 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
⊢ ∀ (a : RingQuot r), a * 1 = a

Tactic:
rintro ⟨⟨⟩⟩

Goal state after:
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
⊢ { toQuot := Quot.mk (Rel r) a✝ } * 1 = { toQuot := Quot.mk (Rel r) 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
⊢ ∀ (x : RingQuot r), x ^ 0 = 1

Tactic:
rintro ⟨⟨⟩⟩

Goal state after:
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
⊢ { toQuot := Quot.mk (Rel r) a✝ } ^ 0 = 1
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
⊢ ∀ (a : RingQuot r), 0 * a = 0

Tactic:
rintro ⟨⟨⟩⟩

Goal state after:
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✝ } = 0
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
⊢ ∀ (a : RingQuot r), a * 0 = 0

Tactic:
rintro ⟨⟨⟩⟩

Goal state after:
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
⊢ { toQuot := Quot.mk (Rel r) a✝ } * 0 = 0
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
R : Type uR
inst✝ : Ring R
r : R → R → Prop
⊢ ∀ (a : RingQuot r), 0 • a = 0

Tactic:
rintro ⟨⟨⟩⟩

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

Tactic:
rintro ⟨⟨⟩⟩

Goal state after:
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
toQuot✝ : Quot (Rel r)
a✝ : R
⊢ -{ toQuot := Quot.mk (Rel r) a✝ } + { toQuot := Quot.mk (Rel r) a✝ } = 0
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝ : Semiring R
r : R → R → Prop
⊢ Function.Surjective fun x ↦ { toQuot := Quot.mk (Rel r) x }

Tactic:
rintro ⟨⟨⟩⟩

Goal state after:
case mk
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
toQuot✝ : Quot (Rel r)
a✝ : R
⊢ ∃ a, (fun x ↦ { toQuot := Quot.mk (Rel r) x }) a = { toQuot := Quot.mk (Rel r) a✝ }
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
z : ↥(NonUnitalStarSubsemiring.center α)
a : α
⊢ a * ↑(star z) = ↑(star z) * a

Tactic:
rw [(star z).property.comm]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a : R
⊢ C a = 0 ↔ C a = C 0

Tactic:
C_0

Goal state after:
R : Type u_1
inst✝ : Semiring R
a : R
⊢ C a = 0 ↔ C a = 0
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
a : R
n : ℕ
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ (monomial n) (a * 1) = (monomial n) (a • 1)

Tactic:
simp [mul_one, smul_eq_mul]

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

Goal state before:
pp: R✝ : Type u
inst✝³ : Semiring R✝
r✝ : R✝ → R✝ → Prop
inst✝² : StarRing R✝
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
r : R → R → Prop
hr : ∀ (a b : R), r a b → r (star a) (star b)
⊢ Function.Involutive (star' r hr)

Tactic:
rintro ⟨⟨⟩⟩

Goal state after:
case mk
R✝ : Type u
inst✝³ : Semiring R✝
r✝ : R✝ → R✝ → Prop
inst✝² : StarRing R✝
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
r : R → R → Prop
hr : ∀ (a b : R), r a b → r (star a) (star b)
toQuot✝ : Quot (Rel r)
a✝ : R
⊢ star' r hr (star' r hr { toQuot := Quot.mk (Rel r) a✝ }) = { toQuot := Quot.mk (Rel r) a✝ }
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : One G
inst✝ : AddMonoidWithOne k
n : ℕ
⊢ ↑n = single 1 ↑n

Tactic:
induction n <;> simp_all

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

Goal state before:
pp: case inr
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
⊢ x + y ≤ x + z

Tactic:
rw [add_eq_right hy]

Goal state after:
case inr
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
⊢ y ≤ x + z
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_5
E : Type u_6
F : Type u_7
G : Type u_8
H : Type u_9
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : AddCommMonoid E
inst✝¹⁴ : StarAddMonoid E
inst✝¹³ : Module R E
inst✝¹² : StarModule R E
inst✝¹¹ : AddCommMonoid F
inst✝¹⁰ : StarAddMonoid F
inst✝⁹ : Module R F
inst✝⁸ : StarModule R F
inst✝⁷ : AddCommMonoid G
inst✝⁶ : StarAddMonoid G
inst✝⁵ : Module R G
inst✝⁴ : StarModule R G
inst✝³ : AddCommMonoid H
inst✝² : StarAddMonoid H
inst✝¹ : Module R H
inst✝ : StarModule R H
f : WithConv (E →ₗ[R] F)
g : WithConv (G →ₗ[R] H)
x : TensorProduct R E G
⊢ star ((TensorProduct.map f.ofConv g.ofConv) x) = (TensorProduct.map (star f).ofConv (star g).ofConv) (star x)

Tactic:
by
  simpa using congr($(TensorProduct.intrinsicStar_map f g) (star x))

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
ic : IsCompatible (sheaf X).obj V g
gl : ↑(X.presheaf.obj (op U))
gl_spec : ∀ (i : ↥U), (ConcreteCategory.hom ((sheaf X).obj.map (iVU i).op)) gl = g i
i : ↥U
⊢ (ConcreteCategory.hom ((sheaf X).obj.map (iVU i).op)) (f * gl) =
    (ConcreteCategory.hom ((sheaf X).obj.map (iVU i).op)) 1

Tactic:
change ((sheaf X).obj.map (iVU i).op).hom (f * gl) = ((sheaf X).obj.map (iVU i).op) 1

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
ic : IsCompatible (sheaf X).obj V g
gl : ↑(X.presheaf.obj (op U))
gl_spec : ∀ (i : ↥U), (ConcreteCategory.hom ((sheaf X).obj.map (iVU i).op)) gl = g i
i : ↥U
⊢ (CommRingCat.Hom.hom ((sheaf X).obj.map (iVU i).op)) (f * gl) =
    (ConcreteCategory.hom ((sheaf X).obj.map (iVU i).op)) 1
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X : Scheme
x : ↥X
U : X.Opens
hxU : x ∈ U
V : TopologicalSpace.Opens ↑X.toTopCat
hxV : x ∈ V
R : CommRingCat
e : X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)
this : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ (Opens.map (e.inv.base ≫ V.inclusion')).obj U
r : ↑R
hr : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ ↑(PrimeSpectrum.basicOpen r)
hr' : ↑(PrimeSpectrum.basicOpen r) ⊆ ↑((Opens.map (e.inv.base ≫ V.inclusion')).obj U)
f : Spec (CommRingCat.of (Localization.Away r)) ⟶ X :=
  Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) ≫ { toLRSHom' := e.inv ≫ X.ofRestrict ⋯ }
⊢ x ∈
      ⇑{ toLRSHom' := e.inv ≫ X.ofRestrict ⋯ } ''
        Set.range ⇑(Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r)))) ∧
    ⇑{ toLRSHom' := e.inv ≫ X.ofRestrict ⋯ } ''
        Set.range ⇑(Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r)))) ⊆
      ↑U

Tactic:
PrimeSpectrum.localization_away_comap_range (Localization.Away r) r

Goal state after:
X : Scheme
x : ↥X
U : X.Opens
hxU : x ∈ U
V : TopologicalSpace.Opens ↑X.toTopCat
hxV : x ∈ V
R : CommRingCat
e : X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)
this : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ (Opens.map (e.inv.base ≫ V.inclusion')).obj U
r : ↑R
hr : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ ↑(PrimeSpectrum.basicOpen r)
hr' : ↑(PrimeSpectrum.basicOpen r) ⊆ ↑((Opens.map (e.inv.base ≫ V.inclusion')).obj U)
f : Spec (CommRingCat.of (Localization.Away r)) ⟶ X :=
  Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) ≫ { toLRSHom' := e.inv ≫ X.ofRestrict ⋯ }
⊢ x ∈ ⇑{ toLRSHom' := e.inv ≫ X.ofRestrict ⋯ } '' ↑(PrimeSpectrum.basicOpen r) ∧
    ⇑{ toLRSHom' := e.inv ≫ X.ofRestrict ⋯ } '' ↑(PrimeSpectrum.basicOpen r) ⊆ ↑U
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsIso f ↔ IsIso f.base ∧ ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)

Tactic:
isIso_iff_isOpenImmersion_and_epi_base,

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ IsOpenImmersion f ∧ Epi f.base ↔ IsIso f.base ∧ ∀ (x : ↥X), IsIso (Scheme.Hom.stalkMap f x)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
O : (↑U).Opens
W : (↑V).Opens
e' : W ≤ resLE f U V e ⁻¹ᵁ O
⊢ appLE (resLE f U V e) O W e' = appLE f (U.ι ''ᵁ O) (V.ι ''ᵁ W) ⋯

Tactic:
by
  dsimp [appLE, resLE]
  simp only [morphismRestrict_app', appLE, homOfLE_leOfHom, homOfLE_app, Category.assoc]
  rw [← X.presheaf.map_comp, ← X.presheaf.map_comp]
  rfl

Goal state after: