mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case cons
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddCommMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
xs : List (tsze R M)
ih :
  xs.prod.snd =
    (List.map (fun x ↦ (List.take x.2 (List.map fst xs)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod)
        xs.zipIdx).sum
⊢ (List.map (fun x_1 ↦ x.fst •> x_1)
          (List.map
            (fun x ↦ (List.take x.2 (List.map fst xs)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod)
            xs.zipIdx)).sum +
      x.snd <• (List.map fst xs).prod =
    x.snd <• (List.map fst xs).prod +
      (List.map
          (fun x_1 ↦
            x.fst •> (List.take x_1.2 (List.map fst xs)).prod •> x_1.1.snd <•
              (List.drop (x_1.2 + 1) (List.map fst xs)).prod)
          xs.zipIdx).sum

Tactic:
List.map_map,

Goal state after:
case cons
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddCommMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
xs : List (tsze R M)
ih :
  xs.prod.snd =
    (List.map (fun x ↦ (List.take x.2 (List.map fst xs)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod)
        xs.zipIdx).sum
⊢ (List.map
          ((fun x_1 ↦ x.fst •> x_1) ∘ fun x ↦
            (List.take x.2 (List.map fst xs)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod)
          xs.zipIdx).sum +
      x.snd <• (List.map fst xs).prod =
    x.snd <• (List.map fst xs).prod +
      (List.map
          (fun x_1 ↦
            x.fst •> (List.take x_1.2 (List.map fst xs)).prod •> x_1.1.snd <•
              (List.drop (x_1.2 + 1) (List.map fst xs)).prod)
          xs.zipIdx).sum
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h1
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
x : tsze R M
h : r * x.fst = 1
⊢ (r + 0) * x.fst = 1

Tactic:
rw [add_zero, h]

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

Goal state before:
pp: case h1
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
r : R
h : x.fst * r = 1
⊢ x.fst * (r + 0) = 1

Tactic:
rw [add_zero, h]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
inst✝ : Category.{v₄, u₄} D
L₀₁ : A ⥤ B
R₁₀ : B ⥤ A
L₁₂ : B ⥤ C
R₂₁ : C ⥤ B
L₂₃ : C ⥤ D
R₃₂ : D ⥤ C
adj₀₁ : L₀₁ ⊣ R₁₀
adj₁₂ : L₁₂ ⊣ R₂₁
adj₂₃ : L₂₃ ⊣ R₃₂
⊢ (conjugateEquiv (adj₀₁.comp (adj₁₂.comp adj₂₃)) ((adj₀₁.comp adj₁₂).comp adj₂₃)) (L₀₁.associator L₁₂ L₂₃).hom =
    (R₃₂.associator R₂₁ R₁₀).hom

Tactic:
ext X
  simp only [comp_obj, conjugateEquiv_apply_app, Adjunction.comp_unit_app,
    Functor.comp_map, Category.assoc, ← map_comp, associator_hom_app, map_id,
    Adjunction.comp_counit_app, Category.id_comp]
  simp

Goal state after:
Module: Mathlib.Algebra.Category.BialgCat.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y : BialgCat R
f : X ⟶ Y
x✝ : IsIso ((forget (BialgCat R)).map f)
i : (forget (BialgCat R)).obj X ≅ (forget (BialgCat R)).obj Y := asIso ((forget (BialgCat R)).map f)
⊢ IsIso f

Tactic:
let e : X ≃ₐc[R] Y := { f.toBialgHom, i.toEquiv with }

Goal state after:
R : Type u
inst✝ : CommRing R
X Y : BialgCat R
f : X ⟶ Y
x✝ : IsIso ((forget (BialgCat R)).map f)
i : (forget (BialgCat R)).obj X ≅ (forget (BialgCat R)).obj Y := asIso ((forget (BialgCat R)).map f)
e : X.carrier ≃ₐc[R] Y.carrier :=
  let __src := Hom.toBialgHom f;
  let __src_1 := i.toEquiv;
  { toCoalgHom := __src.toCoalgHom, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
⊢ IsIso f
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
this : Algebra R S := f.toAlgebra
s : S
m : ↑M
⊢ (ConcreteCategory.hom α) (s ⊗ₜ[R] m) = (ConcreteCategory.hom β) (s ⊗ₜ[R] m)

Tactic:
have : s ⊗ₜ[R] (m : M) = s • (1 : S) ⊗ₜ[R] m := by
    rw [ExtendScalars.smul_tmul, mul_one]

Goal state after:
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
this✝ : Algebra R S := f.toAlgebra
s : S
m : ↑M
this : s ⊗ₜ[R] m = s • 1 ⊗ₜ[R] m
⊢ (ConcreteCategory.hom α) (s ⊗ₜ[R] m) = (ConcreteCategory.hom β) (s ⊗ₜ[R] m)
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
Y : ModuleCat S
s : S
z : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑((restrictScalars f).obj Y)
⊢ (lift { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
      (s • z) =
    (RingHom.id S) s •
      (lift
          { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
        z

Tactic:
by
      let m1 : Module R S := Module.compHom S f
      let m2 : Module R Y := Module.compHom Y f
      induction z using TensorProduct.induction_on with
      | zero => rw [smul_zero, map_zero, smul_zero]
      | tmul s' y => simp [mul_smul]
      | add _ _ ih1 ih2 => rw [smul_add, map_add, map_add, ih1, ih2, smul_add]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R₁ R₂ R₃ R₄ : Type u₁
inst✝³ : CommRing R₁
inst✝² : CommRing R₂
inst✝¹ : CommRing R₃
inst✝ : CommRing R₄
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
f₃₄ : R₃ →+* R₄
M : ModuleCat R₁
m : ↑M
h₁ : (ConcreteCategory.hom ((extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₃] (1 ⊗ₜ[R₁] m)
h₂ : (ConcreteCategory.hom ((extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₂] (1 ⊗ₜ[R₁] m)
h₃ :
  ∀ (M : ModuleCat R₂) (m : ↑M),
    (ConcreteCategory.hom ((extendScalarsComp f₂₃ f₃₄).hom.app M)) (1 ⊗ₜ[R₂] m) = 1 ⊗ₜ[R₃] (1 ⊗ₜ[R₂] m)
h₄ : (ConcreteCategory.hom ((extendScalarsComp f₁₂ f₂₃).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₂] (1 ⊗ₜ[R₁] m)
⊢ (Hom.hom ((extendScalars f₃₄).map ((extendScalarsComp f₁₂ f₂₃).hom.app M))) (1 ⊗ₜ[R₃] (1 ⊗ₜ[R₁] m)) =
    (Hom.hom ((extendScalarsComp f₂₃ f₃₄).hom.app ((extendScalars f₁₂).obj M)))
      ((Hom.hom ((extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom.app M)) (1 ⊗ₜ[R₁] m))

Tactic:
h₂

Goal state after:
R₁ R₂ R₃ R₄ : Type u₁
inst✝³ : CommRing R₁
inst✝² : CommRing R₂
inst✝¹ : CommRing R₃
inst✝ : CommRing R₄
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
f₃₄ : R₃ →+* R₄
M : ModuleCat R₁
m : ↑M
h₁ : (ConcreteCategory.hom ((extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₃] (1 ⊗ₜ[R₁] m)
h₂ : (ConcreteCategory.hom ((extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₂] (1 ⊗ₜ[R₁] m)
h₃ :
  ∀ (M : ModuleCat R₂) (m : ↑M),
    (ConcreteCategory.hom ((extendScalarsComp f₂₃ f₃₄).hom.app M)) (1 ⊗ₜ[R₂] m) = 1 ⊗ₜ[R₃] (1 ⊗ₜ[R₂] m)
h₄ : (ConcreteCategory.hom ((extendScalarsComp f₁₂ f₂₃).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₂] (1 ⊗ₜ[R₁] m)
⊢ (Hom.hom ((extendScalars f₃₄).map ((extendScalarsComp f₁₂ f₂₃).hom.app M))) (1 ⊗ₜ[R₃] (1 ⊗ₜ[R₁] m)) =
    (Hom.hom ((extendScalarsComp f₂₃ f₃₄).hom.app ((extendScalars f₁₂).obj M))) (1 ⊗ₜ[R₂] (1 ⊗ₜ[R₁] m))
Module: Mathlib.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: case ha
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
a : A
⊢ (Algebra.TensorProduct.map ↑(Algebra.TensorProduct.comm R A B) ↑(Algebra.TensorProduct.comm R A B))
      ((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A B B) (comul a ⊗ₜ[R] comul 1)) =
    (TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R B B A A) (comul 1 ⊗ₜ[R] comul a)

Tactic:
rw [← (ℛ R a).eq]

Goal state after:
case ha
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
a : A
⊢ (Algebra.TensorProduct.map ↑(Algebra.TensorProduct.comm R A B) ↑(Algebra.TensorProduct.comm R A B))
      ((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A B B)
        ((∑ i ∈ (ℛ R a).index, (ℛ R a).left i ⊗ₜ[R] (ℛ R a).right i) ⊗ₜ[R] comul 1)) =
    (TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R B B A A)
      (comul 1 ⊗ₜ[R] ∑ i ∈ (ℛ R a).index, (ℛ R a).left i ⊗ₜ[R] (ℛ R a).right i)
Module: Mathlib.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: case hb
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
a : B
⊢ (Algebra.TensorProduct.map ↑(Algebra.TensorProduct.comm R A B) ↑(Algebra.TensorProduct.comm R A B))
      ((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A B B) (comul 1 ⊗ₜ[R] comul a)) =
    (TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R B B A A) (comul a ⊗ₜ[R] comul 1)

Tactic:
rw [← (ℛ R a).eq]

Goal state after:
case hb
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
a : B
⊢ (Algebra.TensorProduct.map ↑(Algebra.TensorProduct.comm R A B) ↑(Algebra.TensorProduct.comm R A B))
      ((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A B B)
        (comul 1 ⊗ₜ[R] ∑ i ∈ (ℛ R a).index, (ℛ R a).left i ⊗ₜ[R] (ℛ R a).right i)) =
    (TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R B B A A)
      ((∑ i ∈ (ℛ R a).index, (ℛ R a).left i ⊗ₜ[R] (ℛ R a).right i) ⊗ₜ[R] comul 1)
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Mon Cᵒᵖ
⊢ (η ▷ A.X ≫ μ).unop = (λ_ (unop A.X)).inv

Tactic:
MonObj.one_mul

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Mon Cᵒᵖ
⊢ (λ_ A.X).hom.unop = (λ_ (unop A.X)).inv
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝⁹ : CommRing R
M N P : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Coalgebra R M
inst✝¹ : Coalgebra R N
inst✝ : Coalgebra R P
⊢ CoalgebraStruct.comul = CoalgebraStruct.comul

Tactic:
by
  rw [ofComonObjCoalgebraStruct_comul]
  simp only [Comon.monoidal_tensorObj_comon_comul]
  simp [tensorμ_eq_tensorTensorTensorComm, TensorProduct.comul_def,
    AlgebraTensorModule.tensorTensorTensorComm_eq]
  rfl

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
P : Type u_3
inst✝⁵ : CommSemiring P
x : R
inst✝⁴ : Away x S
g : R →+* P
Q : Type u_4
inst✝³ : CommSemiring Q
inst✝² : Algebra P Q
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
⊢ Submonoid.powers r ≤ Submonoid.comap f (Submonoid.powers (f r))

Tactic:
rintro x ⟨n, rfl⟩

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
P : Type u_3
inst✝⁵ : CommSemiring P
x : R
inst✝⁴ : Away x S
g : R →+* P
Q : Type u_4
inst✝³ : CommSemiring Q
inst✝² : Algebra P Q
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
n : ℕ
⊢ (fun x ↦ r ^ x) n ∈ Submonoid.comap f (Submonoid.powers (f r))
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
fg : N.FG
le : N ≤ Ring.jacobson R • N
⊢ N = ⊥

Tactic:
contrapose! le; exact (jacobson_smul_lt le fg).not_ge

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommSemiring R
s : Set R
f : (a : ↑s) → Away ↑a
h : ∀ (a b : ↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem✝ : 1 ∈ Ideal.span s
this :
  ∀ (s : Set R) (f : (a : ↑s) → Away ↑a),
    (∀ (a b : ↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)) →
      1 ∈ Ideal.span s → (∃ t, ↑t = s) → ∃! r, ∀ (a : ↑s), (algebraMap R (Away ↑a)) r = f a
finset_eq : ¬∃ t, ↑t = s
t : Finset R
hts✝ : ↑t ⊆ s
mem : 1 ∈ Submodule.span R ↑t
r : R
eq : (fun r ↦ ∀ (a : ↑↑t), (algebraMap R (Away ↑a)) r = f ⟨↑a, ⋯⟩) r
uniq : ∀ (y : R), (fun r ↦ ∀ (a : ↑↑t), (algebraMap R (Away ↑a)) r = f ⟨↑a, ⋯⟩) y → y = r
a : ↑s
hts : insert ↑a ↑t ⊆ s
⊢ (algebraMap R (Away ↑a)) r = f a

Tactic:
have ⟨r', eq, _⟩ := this ({a.1} ∪ t) (fun a ↦ f ⟨a, hts a.2⟩) (fun a b ↦
      h ⟨a, hts a.2⟩ ⟨b, hts b.2⟩) (Ideal.span_mono (fun _ ↦ .inr) mem) ⟨{a.1} ∪ t, by simp⟩
    exact (congr_arg _ (uniq _ fun b ↦ eq ⟨b, .inr b.2⟩).symm).trans (eq ⟨a, .inl rfl⟩)

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : C
h₁ h₂ : MonObj X
H : μ = μ
⊢ h₁ = h₂

Tactic:
suffices h₁.one = h₂.one by cases h₁; cases h₂; subst H this; rfl

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : C
h₁ h₂ : MonObj X
H : μ = μ
⊢ η = η
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
b : Basis ι R M
m : M
i✝ i : ι
⊢ (↑R ↑(ofIsLocalizedModule Rₛ S f b).repr ∘ₗ f) (b i) =
    (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ) ∘ₗ ↑b.repr) (b i)

Tactic:
rw [LinearMap.coe_comp, Function.comp_apply, LinearMap.coe_restrictScalars,
    LinearEquiv.coe_coe, ← b.ofIsLocalizedModule_apply Rₛ S f, repr_self, LinearMap.coe_comp,
    Function.comp_apply, LinearEquiv.coe_coe, repr_self, Finsupp.mapRange.linearMap_apply,
    Finsupp.mapRange_single, Algebra.linearMap_apply, map_one]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝¹⁴ : Category.{v₁, u₁} C
inst✝¹³ : MonoidalCategory C
M N O X✝ : C
inst✝¹² : MonObj M
inst✝¹¹ : MonObj N
inst✝¹⁰ : MonObj O
D : Type u₂
inst✝⁹ : Category.{v₂, u₂} D
inst✝⁸ : MonoidalCategory D
E : Type u₃
inst✝⁷ : Category.{v₃, u₃} E
inst✝⁶ : MonoidalCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝⁵ : F.LaxMonoidal
inst✝⁴ : F'.LaxMonoidal
inst✝³ : G.LaxMonoidal
X Y : C
inst✝² : MonObj X
inst✝¹ : MonObj Y
f : X ⟶ Y
inst✝ : IsMonHom f
⊢ «μ» F X X ▷ F.obj X ≫ «μ» F (X ⊗ X) X ≫ F.map (μ ▷ X) ≫ F.map μ =
    (α_ (F.obj X) (F.obj X) (F.obj X)).hom ≫ F.obj X ◁ «μ» F X X ≫ F.obj X ◁ F.map μ ≫ «μ» F X X ≫ F.map μ

Tactic:
μ_natural_right_assoc

Goal state after:
C : Type u₁
inst✝¹⁴ : Category.{v₁, u₁} C
inst✝¹³ : MonoidalCategory C
M N O X✝ : C
inst✝¹² : MonObj M
inst✝¹¹ : MonObj N
inst✝¹⁰ : MonObj O
D : Type u₂
inst✝⁹ : Category.{v₂, u₂} D
inst✝⁸ : MonoidalCategory D
E : Type u₃
inst✝⁷ : Category.{v₃, u₃} E
inst✝⁶ : MonoidalCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝⁵ : F.LaxMonoidal
inst✝⁴ : F'.LaxMonoidal
inst✝³ : G.LaxMonoidal
X Y : C
inst✝² : MonObj X
inst✝¹ : MonObj Y
f : X ⟶ Y
inst✝ : IsMonHom f
⊢ «μ» F X X ▷ F.obj X ≫ «μ» F (X ⊗ X) X ≫ F.map (μ ▷ X) ≫ F.map μ =
    (α_ (F.obj X) (F.obj X) (F.obj X)).hom ≫ F.obj X ◁ «μ» F X X ≫ «μ» F X (X ⊗ X) ≫ F.map (X ◁ μ) ≫ F.map μ
Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts

Goal state before:
pp: case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal Z
H₂ : IsLimit (BinaryFan.mk h k)
s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk h k ⋯).pt
h₁ : m ≫ (PullbackCone.mk h k ⋯).fst = s.fst
⊢ m ≫ (PullbackCone.mk h k ⋯).snd = s.snd → m = BinaryFan.IsLimit.lift H₂ s.fst s.snd

Tactic:
h₂

Goal state after:
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal Z
H₂ : IsLimit (BinaryFan.mk h k)
s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk h k ⋯).pt
h₁ : m ≫ (PullbackCone.mk h k ⋯).fst = s.fst
h₂ : m ≫ (PullbackCone.mk h k ⋯).snd = s.snd
⊢ m = BinaryFan.IsLimit.lift H₂ s.fst s.snd
Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts

Goal state before:
pp: case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
m : (PushoutCocone.mk f g ⋯).pt ⟶ s.pt
h₁ : (PushoutCocone.mk f g ⋯).inl ≫ m = s.inl
⊢ (PushoutCocone.mk f g ⋯).inr ≫ m = s.inr → m = BinaryCofan.IsColimit.desc H₂ s.inl s.inr

Tactic:
h₂

Goal state after:
case right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
m : (PushoutCocone.mk f g ⋯).pt ⟶ s.pt
h₁ : (PushoutCocone.mk f g ⋯).inl ≫ m = s.inl
h₂ : (PushoutCocone.mk f g ⋯).inr ≫ m = s.inr
⊢ m = BinaryCofan.IsColimit.desc H₂ s.inl s.inr
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
P' : C
fst' : P' ⟶ X
snd' : P' ⟶ Y
h : IsPullback fst snd f g
h' : IsPullback fst' snd' f g
⊢ (isoIsPullback X Y h h').inv ≫ snd = snd'

Tactic:
by
  simp only [Iso.inv_comp_eq, isoIsPullback_hom_snd]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryProduct A X
inst✝ : HasBinaryProduct B X
s : PullbackCone f prod.fst
m : s.pt ⟶ (PullbackCone.mk prod.fst (prod.map f (𝟙 X)) ⋯).pt
h₁ : m ≫ (PullbackCone.mk prod.fst (prod.map f (𝟙 X)) ⋯).fst = s.fst
⊢ m ≫ (PullbackCone.mk prod.fst (prod.map f (𝟙 X)) ⋯).snd = s.snd → m = prod.lift s.fst (s.snd ≫ prod.snd)

Tactic:
h₂

Goal state after:
case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryProduct A X
inst✝ : HasBinaryProduct B X
s : PullbackCone f prod.fst
m : s.pt ⟶ (PullbackCone.mk prod.fst (prod.map f (𝟙 X)) ⋯).pt
h₁ : m ≫ (PullbackCone.mk prod.fst (prod.map f (𝟙 X)) ⋯).fst = s.fst
h₂ : m ≫ (PullbackCone.mk prod.fst (prod.map f (𝟙 X)) ⋯).snd = s.snd
⊢ m = prod.lift s.fst (s.snd ≫ prod.snd)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : M × ↥S
u : ↥S
v : R
h₁ : u • b.1 = v • a.1
h₂ : ↑u * ↑b.2 = v * ↑a.2
⊢ (v * ↑a.2) • a.1 = (↑u * ↑a.2) • b.1

Tactic:
rw [mul_comm, mul_smul, ← h₁, mul_comm, mul_smul, Submonoid.smul_def]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryCoproduct A X
inst✝ : HasBinaryCoproduct B X
s : PushoutCocone coprod.inl f
m : (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).pt ⟶ s.pt
h₁ : (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inl ≫ m = s.inl
⊢ (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inr ≫ m = s.inr → m = coprod.desc s.inr (coprod.inr ≫ s.inl)

Tactic:
h₂

Goal state after:
case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryCoproduct A X
inst✝ : HasBinaryCoproduct B X
s : PushoutCocone coprod.inl f
m : (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).pt ⟶ s.pt
h₁ : (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inl ≫ m = s.inl
h₂ : (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inr ≫ m = s.inr
⊢ m = coprod.desc s.inr (coprod.inr ≫ s.inl)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝¹⁰ : CommSemiring R
S✝ : Submonoid R
M : Type v
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
T : Type u_1
inst✝⁷ : CommSemiring T
inst✝⁶ : Algebra R T
inst✝⁵ : IsLocalization S✝ T
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
⊢ ∀ (a : LocalizedModule S A), 1 * a = a

Tactic:
by
      rintro ⟨a, s⟩
      with_unfolding_all exact mk_eq.mpr ⟨1, by simp only [one_mul, mul_one, one_smul]⟩

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Submonoid R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
s₁ s₂ : ↥S
⊢ mk a₁ s₁ * mk a₂ s₂ = mk (a₁ * a₂) (s₁ * s₂)

Tactic:
mk_mul_mk',

Goal state after:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
s₁ s₂ : ↥S
⊢ mk (a₁ * a₂) (s₂ * s₁) = mk (a₁ * a₂) (s₁ * s₂)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case zero
R : Type u
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
a : A
s : ↥S
⊢ 1 = mk 1 1

Tactic:
OreLocalization.one_def

Goal state after:
case zero
R : Type u
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
a : A
s : ↥S
⊢ 1 /ₒ 1 = mk 1 1
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
g' : Z ⟶ W
inst✝¹ : HasPushout f g
inst✝ : HasPushout (pushout.inr f g) g'
⊢ pushout.inl f g ≫ pushout.inl (pushout.inr f g) g' ≫ (pushoutLeftPushoutInrIso f g g').hom = pushout.inl f (g ≫ g')

Tactic:
by
  rw [← Category.assoc]
  apply IsColimit.comp_coconePointUniqueUpToIso_hom (pasteHorizIsPushout _ _ _) _ WalkingSpan.left

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
H :
  ∀ ⦃X Y Z : C⦄ (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g],
    ∃ P fst snd, IsPullback fst snd f g ∧ IsPullback (F.map fst) (F.map snd) (F.map f) (F.map g)
⊢ PreservesLimitsOfShape WalkingCospan F

Tactic:
by
  suffices h : ∀ {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z), PreservesLimit (cospan f g) F from
    ⟨fun {K} ↦ preservesLimit_of_iso_diagram _ (Limits.diagramIsoCospan K).symm⟩
  intro X Y Z f g
  refine .mk' fun h ↦ ?_
  obtain ⟨P, fst, snd, h, h'⟩ := H f g
  rwa [h.preservesLimit_cospan_iff]

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case refine_3
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hxs : x.IsSupported s
p : α
hps : p ∈ s
n : FreeCommRing α
ih : (map Subtype.val) ((restriction s) n) = n
⊢ (map Subtype.val) (of ⟨p, hps⟩) * (map Subtype.val) ((restriction s) n) = of p * n

Tactic:
map_of,

Goal state after:
case refine_3
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hxs : x.IsSupported s
p : α
hps : p ∈ s
n : FreeCommRing α
ih : (map Subtype.val) ((restriction s) n) = n
⊢ of ↑⟨p, hps⟩ * (map Subtype.val) ((restriction s) n) = of p * n