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

Goal state before:
pp: case cons.refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) ∧ ∀ b ∈ ↑s, i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
a b : ι → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
⊢ ∀ i_1 ∈ Finset.cons i s hi,
    (Function.update (fun j ↦ r j * a j %ₘ g j) i ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) i_1).degree < (g i_1).degree

Tactic:
rw [Finset.forall_mem_cons, Function.update_self]
      refine ⟨degree_modByMonic_lt _ hg.1, fun j hj => ?_⟩
      rw [Function.update_of_ne (hjs hj).symm]
      exact degree_modByMonic_lt _ (hg.2 j hj)

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ fold max 0 (natDegree ∘ fun i ↦ C ((i + k).choose k • p.coeff (i + k)) * X ^ i) ((⇑derivative)^[k] p).support ≤
    p.natDegree - k

Tactic:
fold_max_le

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ 0 ≤ p.natDegree - k ∧
    ∀ x ∈ ((⇑derivative)^[k] p).support,
      (natDegree ∘ fun i ↦ C ((i + k).choose k • p.coeff (i + k)) * X ^ i) x ≤ p.natDegree - k
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: hp : IsUnitTrinomial 0
⊢ False

Tactic:
simpa using hp.card_support_eq_three

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

Goal state before:
pp: p q : ℤ[X]
h : p * p.mirror = q * q.mirror
⊢ p.IsUnitTrinomial ↔ q.IsUnitTrinomial

Tactic:
isUnitTrinomial_iff',

Goal state after:
p q : ℤ[X]
h : p * p.mirror = q * q.mirror
⊢ (p * p.mirror).coeff (((p * p.mirror).natDegree + (p * p.mirror).natTrailingDegree) / 2) = 3 ↔ q.IsUnitTrinomial
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: p q : ℤ[X]
h : p * p.mirror = q * q.mirror
⊢ (p * p.mirror).coeff (((p * p.mirror).natDegree + (p * p.mirror).natTrailingDegree) / 2) = 3 ↔ q.IsUnitTrinomial

Tactic:
isUnitTrinomial_iff',

Goal state after:
p q : ℤ[X]
h : p * p.mirror = q * q.mirror
⊢ (p * p.mirror).coeff (((p * p.mirror).natDegree + (p * p.mirror).natTrailingDegree) / 2) = 3 ↔
    (q * q.mirror).coeff (((q * q.mirror).natDegree + (q * q.mirror).natTrailingDegree) / 2) = 3
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
c : ℕ → R[X]
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - q
hc : ∀ (k : ℕ) (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
⊢ fold max 0 (natDegree ∘ c) (range (p.natDegree + 1)) ≤ p.natDegree - q

Tactic:
fold_max_le

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
c : ℕ → R[X]
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - q
hc : ∀ (k : ℕ) (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
⊢ 0 ≤ p.natDegree - q ∧ ∀ x ∈ range (p.natDegree + 1), (natDegree ∘ c) x ≤ p.natDegree - q
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case inr.refine_1
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
⊢ fold max 0 (natDegree ∘ c) (Ico q (p.natDegree + 1)) ≤ p.natDegree - q

Tactic:
fold_max_le

Goal state after:
case inr.refine_1
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
⊢ 0 ≤ p.natDegree - q ∧ ∀ x ∈ Ico q (p.natDegree + 1), (natDegree ∘ c) x ≤ p.natDegree - q
Module: Mathlib.Algebra.PresentedMonoid.Basic

Goal state before:
pp: case h.mul
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
x y : FreeMonoid α
hx : (mk rels) x ∈ closure (range (of rels))
hy : (mk rels) y ∈ closure (range (of rels))
⊢ (mk rels) (x * y) ∈ closure (range (of rels))

Tactic:
| mul x y hx hy =>

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

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ norm z = 1 ↔ z * star z = 1

Tactic:
← algebraMap_norm_eq_mul_star

Goal state after:
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ norm z = 1 ↔ (algebraMap R (QuadraticAlgebra R a b)) (norm z) = 1
Module: Mathlib.Algebra.Polynomial.PartialFractions

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

Tactic:
nontriviality R
  simp only [← Finset.sum_mul] at hf
  have hrd {r : (i : ι) → Fin (n i) → R[X]} (hr : ∀ i ∈ s, ∀ j, (r i j).degree < (g i).degree)
      (i : ι) (hi : i ∈ s) : (∑ j, r i j * g i ^ j.1).degree < (g i ^ n i).degree := by
    refine (degree_sum_le _ _).trans_lt ((Finset.sup_lt_iff ?_).2 fun j _ => ?_)
    · rw [bot_lt_iff_ne_bot, degree_ne_bot]
      exact ((hg i hi).pow (n i)).ne_zero
    · refine (degree_mul_le _ _).trans_lt ?_
      rw [degree_eq_natDegree ((hg i hi).pow j.1).ne_zero, (hg i hi).natDegree_pow,
        degree_eq_natDegree ((hg i hi).pow (n i)).ne_zero, (hg i hi).natDegree_pow]
      conv_rhs => rw [← Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.2 j.neZero.ne)]
      rw [Nat.add_one_mul, Nat.add_comm, Nat.cast_add, ← degree_eq_natDegree (hg i hi).ne_zero]
      refine WithBot.add_lt_add_of_lt_of_le (WithBot.natCast_ne_bot _) (hr i hi j) ?_
      exact Nat.cast_le.2 (Nat.mul_le_mul_right _ (Nat.le_sub_one_of_lt j.isLt))
  obtain ⟨hq, hr⟩ := quo_mul_prod_add_sum_rem_mul_prod_unique
    (fun i hi => (hg i hi).pow (n i)) (hgg.imp fun i j hij => hij.pow) (hrd hr₁) (hrd hr₂) hf
  refine ⟨hq, fun i hi => ?_⟩
  exact (quo_mul_pow_add_sum_rem_mul_pow_unique (hg i hi) (hr₁ i hi) (hr₂ i hi)
    (congrArg (0 * g i ^ n i + ·) (hr i hi))).2

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
f : R →◃ Quandle.Conj G
a b c : PreEnvelGroup R
⊢ mapAux f ((a.mul b).mul c) = mapAux f (a.mul (b.mul c))

Tactic:
by apply mul_assoc

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

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

Tactic:
mul_assoc (algebraMap R[X] K (r i j.rev))

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

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

Tactic:
cases b

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

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

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

Tactic:
cases b

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

case coe.zero.coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a✝¹ a✝ : α
⊢ (0 + ↑a✝) * ↑a✝¹ = 0 * ↑a✝¹ + ↑a✝ * ↑a✝¹
Module: Mathlib.Algebra.Ring.WithZero

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

Tactic:
cases b

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

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.SkewMonoidAlgebra.Lift

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝ : AddCommMonoid k
f : G ≃ H
l : SkewMonoidAlgebra k G
x : H
⊢ (equivMapDomain f l).coeff x = ((mapDomain ⇑f) l).coeff x

Tactic:
coeff_equivMapDomain,

Goal state after:
k : Type u_1
G : Type u_2
H : Type u_3
inst✝ : AddCommMonoid k
f : G ≃ H
l : SkewMonoidAlgebra k G
x : H
⊢ (Finsupp.equivMapDomain f l.coeff) x = ((mapDomain ⇑f) l).coeff x
Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝ : AddCommMonoid k
f : G ≃ H
a : G
b : k
⊢ (equivMapDomain f (single a b)).coeff = (single (f a) b).coeff

Tactic:
coeff_equivMapDomain,

Goal state after:
k : Type u_1
G : Type u_2
H : Type u_3
inst✝ : AddCommMonoid k
f : G ≃ H
a : G
b : k
⊢ Finsupp.equivMapDomain f (single a b).coeff = (single (f a) b).coeff
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

Goal state before:
pp: 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 α
f : SkewMonoidAlgebra M α
hf : f.support = ∅
⊢ p f

Tactic:
rwa [support_eq_empty.1 hf]

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✝³ : CommSemiring T
inst✝² : Algebra S R
inst✝¹ : Algebra T R
inst✝ : SMulCommClass S T R
s : S
t : T
x✝ : RingQuot r
a : Quot (Rel r)
a' : R
⊢ s • t • { toQuot := Quot.mk (Rel r) a' } = t • s • { toQuot := Quot.mk (Rel r) a' }

Tactic:
simp only [RingQuot.smul_quot, smul_comm s t]

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

Goal state before:
pp: A : Type v
B : Type w
C : Type w'
R : Type v
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
S : NonUnitalStarSubsemiring R
s : Set R
hs : s = ↑S
x : R
hx : x ∈ s
⊢ star x ∈ (S.copy s hs).carrier

Tactic:
change star x ∈ s
      rw [hs] at hx ⊢
      exact S.star_mem' hx

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

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
f g : ↥(Subsemiring.center (CentroidHom α))
a : α
⊢ star (g (f (star a))) = star (g (star (star (f (star a)))))

Tactic:
simp only [star_star]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
ih : ∀ {p : SkewPolynomial R}, X ^ n * p = (p.sum fun a b ↦ (monomial a) ((⇑φ)^[n] b)) * X ^ n
p : SkewPolynomial R
⊢ (X ^ n * p.sum fun a b ↦ (monomial a) (φ b)) * X = (p.sum fun a b ↦ (monomial a) ((⇑φ)^[n + 1] b)) * X ^ (n + 1)

Tactic:
ih,

Goal state after:
case succ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
ih : ∀ {p : SkewPolynomial R}, X ^ n * p = (p.sum fun a b ↦ (monomial a) ((⇑φ)^[n] b)) * X ^ n
p : SkewPolynomial R
⊢ ((p.sum fun a b ↦ (monomial a) (φ b)).sum fun a b ↦ (monomial a) ((⇑φ)^[n] b)) * X ^ n * X =
    (p.sum fun a b ↦ (monomial a) ((⇑φ)^[n + 1] b)) * X ^ (n + 1)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddMonoid k
a a' : G
b : k
h : b ≠ 0
⊢ single a b = single a' b ↔ a = a'

Tactic:
rw [← coeff_inj]

Goal state after:
k : Type u_1
G : Type u_2
inst✝ : AddMonoid k
a a' : G
b : k
h : b ≠ 0
⊢ (single a b).coeff = (single a' b).coeff ↔ a = a'
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 f

Tactic:
rw [← sum_single f, sum_def']

Goal state after:
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))
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : StarMul R
inst✝⁶ : CommRing S
inst✝⁵ : StarMul S
inst✝⁴ : Algebra S R
inst✝³ : StarModule S R
inst✝² : Algebra.IsCentral S R
inst✝¹ : IsCancelMulZero S
inst✝ : Module.IsTorsionFree S R
u v : ↥(unitary R)
x✝ : ∃ y, y • 1 = star ↑v * ↑u
y : S
h : y • 1 = star ↑v * ↑u
huv : ↑u = y • ↑v
hvu : ↑v = star y • ↑u
this : star y * y = 1
⊢ ↑u = ↑(⟨y, ⋯⟩ • v)

Tactic:
exact huv

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Ideal

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
r : R
m : M
hrm : (r, m) = inr (snd (r, m))
⊢ r = 0

Tactic:
by rw [← fst_mk r m, hrm, fst_inr]

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

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

Tactic:
rwa [add_eq_left hx]

Goal state after:
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
F : J ⥤ PresheafedSpace C
inst✝ : HasColimit F
U : Opens ↑↑(colimit F)
j k : Jᵒᵖ
f : j ⟶ k
⊢ (Opens.map (F.map f.unop).base).op.obj (op ((Opens.map (colimit.ι F (unop j)).base).obj U)) =
    op ((Opens.map (colimit.ι F (unop k)).base).obj U)

Tactic:
rw [← colimit.w F f.unop, comp_base]

Goal state after:
J : Type u'
inst✝² : Category.{v', u'} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ PresheafedSpace C
inst✝ : HasColimit F
U : Opens ↑↑(colimit F)
j k : Jᵒᵖ
f : j ⟶ k
⊢ (Opens.map (F.map f.unop).base).op.obj (op ((Opens.map (colimit.ι F (unop j)).base).obj U)) =
    op ((Opens.map ((F.map f.unop).base ≫ (colimit.ι F (unop j)).base)).obj U)
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
⊢ (opEquiv (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf))
        (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf)))
      ((pushforward C (colimit.ι (F ⋙ forget C) j)).map (F.map (𝟙 j)).c ≫
          (Pushforward.comp ((F ⋙ forget C).map (𝟙 j)) (colimit.ι (F ⋙ forget C) j) (F.obj j).presheaf).inv ≫
            (pushforwardEq ⋯ (F.obj j).presheaf).hom).op =
    (opEquiv (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf))
        (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf)))
      (𝟙 (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf)))

Tactic:
refine NatTrans.ext (funext fun U => ?_)

Goal state after:
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
U : (Opens ↑(colimit (F ⋙ forget C)))ᵒᵖ
⊢ ((opEquiv (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf))
            (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf)))
          ((pushforward C (colimit.ι (F ⋙ forget C) j)).map (F.map (𝟙 j)).c ≫
              (Pushforward.comp ((F ⋙ forget C).map (𝟙 j)) (colimit.ι (F ⋙ forget C) j) (F.obj j).presheaf).inv ≫
                (pushforwardEq ⋯ (F.obj j).presheaf).hom).op).app
      U =
    ((opEquiv (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf))
            (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf)))
          (𝟙 (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf)))).app
      U
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₃
⊢ (opEquiv (op ((pushforward C (colimit.ι (F ⋙ forget C) j₁)).obj (F.obj j₁).presheaf))
        (op ((pushforward C (colimit.ι (F ⋙ forget C) j₃)).obj (F.obj j₃).presheaf)))
      ((pushforward C (colimit.ι (F ⋙ forget C) j₃)).map (F.map (f ≫ g)).c ≫
          (Pushforward.comp ((F ⋙ forget C).map (f ≫ g)) (colimit.ι (F ⋙ forget C) j₃) (F.obj j₁).presheaf).inv ≫
            (pushforwardEq ⋯ (F.obj j₁).presheaf).hom).op =
    (opEquiv (op ((pushforward C (colimit.ι (F ⋙ forget C) j₁)).obj (F.obj j₁).presheaf))
        (op ((pushforward C (colimit.ι (F ⋙ forget C) j₃)).obj (F.obj j₃).presheaf)))
      (((pushforward C (colimit.ι (F ⋙ forget C) j₂)).map (F.map f).c ≫
            (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j₂) (F.obj j₁).presheaf).inv ≫
              (pushforwardEq ⋯ (F.obj j₁).presheaf).hom).op ≫
        ((pushforward C (colimit.ι (F ⋙ forget C) j₃)).map (F.map g).c ≫
            (Pushforward.comp ((F ⋙ forget C).map g) (colimit.ι (F ⋙ forget C) j₃) (F.obj j₂).presheaf).inv ≫
              (pushforwardEq ⋯ (F.obj j₂).presheaf).hom).op)

Tactic:
refine NatTrans.ext (funext fun U => ?_)

Goal state after:
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)))ᵒᵖ
⊢ ((opEquiv (op ((pushforward C (colimit.ι (F ⋙ forget C) j₁)).obj (F.obj j₁).presheaf))
            (op ((pushforward C (colimit.ι (F ⋙ forget C) j₃)).obj (F.obj j₃).presheaf)))
          ((pushforward C (colimit.ι (F ⋙ forget C) j₃)).map (F.map (f ≫ g)).c ≫
              (Pushforward.comp ((F ⋙ forget C).map (f ≫ g)) (colimit.ι (F ⋙ forget C) j₃) (F.obj j₁).presheaf).inv ≫
                (pushforwardEq ⋯ (F.obj j₁).presheaf).hom).op).app
      U =
    ((opEquiv (op ((pushforward C (colimit.ι (F ⋙ forget C) j₁)).obj (F.obj j₁).presheaf))
            (op ((pushforward C (colimit.ι (F ⋙ forget C) j₃)).obj (F.obj j₃).presheaf)))
          (((pushforward C (colimit.ι (F ⋙ forget C) j₂)).map (F.map f).c ≫
                (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j₂) (F.obj j₁).presheaf).inv ≫
                  (pushforwardEq ⋯ (F.obj j₁).presheaf).hom).op ≫
            ((pushforward C (colimit.ι (F ⋙ forget C) j₃)).map (F.map g).c ≫
                (Pushforward.comp ((F ⋙ forget C).map g) (colimit.ι (F ⋙ forget C) j₃) (F.obj j₂).presheaf).inv ≫
                  (pushforwardEq ⋯ (F.obj j₂).presheaf).hom).op)).app
      U
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
h : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
⊢ ∃ V i, ∃ (_ : x ∈ V), IsUnit ((ConcreteCategory.hom (X.presheaf.map i.op)) f)

Tactic:
obtain ⟨g', heq⟩ := h.exists_right_inv

Goal state after:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
h : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
g' : ↑(X.presheaf.stalk x)
heq : (ConcreteCategory.hom (X.presheaf.germ U x hx)) f * g' = 1
⊢ ∃ V i, ∃ (_ : x ∈ V), IsUnit ((ConcreteCategory.hom (X.presheaf.map i.op)) f)