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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
⊢ inl 0⁻¹ = inl 0

Tactic:
inv_zero

Goal state after:
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
⊢ inl 0 = inl 0
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ ↑(TensorProduct.assoc R (A × B) (A × B) (A × B)) ∘ₗ
      rTensor (A × B)
          ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
            (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
        (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
          (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul) =
    lTensor (A × B)
        ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
          (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
      (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)

Tactic:
ext x : 2 <;> dsimp only [comp_apply, LinearEquiv.coe_coe, coe_inl, coe_inr, coprod_apply]

Goal state after:
case hl
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x : A
⊢ (TensorProduct.assoc R (A × B) (A × B) (A × B))
      ((rTensor (A × B)
          ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
            (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)))
        ((TensorProduct.map (inl R A B) (inl R A B)) (comul x) +
          (TensorProduct.map (inr R A B) (inr R A B)) (comul 0))) =
    (lTensor (A × B)
        ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
          (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)))
      ((TensorProduct.map (inl R A B) (inl R A B)) (comul x) + (TensorProduct.map (inr R A B) (inr R A B)) (comul 0))

case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x : B
⊢ (TensorProduct.assoc R (A × B) (A × B) (A × B))
      ((rTensor (A × B)
          ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
            (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)))
        ((TensorProduct.map (inl R A B) (inl R A B)) (comul 0) +
          (TensorProduct.map (inr R A B) (inr R A B)) (comul x))) =
    (lTensor (A × B)
        ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
          (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)))
      ((TensorProduct.map (inl R A B) (inl R A B)) (comul 0) + (TensorProduct.map (inr R A B) (inr R A B)) (comul x))
Module: Mathlib.RingTheory.Coalgebra.Hom

Goal state before:
pp: R : Type u
A : Type v
B : Type w
ι : Type u_1
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : Coalgebra R A
inst✝² : Coalgebra R B
a : A
repr : Repr R a ι
F : Type u_2
inst✝¹ : FunLike F A B
inst✝ : CoalgHomClass F R A B
φ : F
⊢ (map ↑φ ↑φ ∘ₗ comul) a = ∑ i ∈ repr.index, (⇑φ ∘ repr.left) i ⊗ₜ[R] (⇑φ ∘ repr.right) i

Tactic:
rw [LinearMap.comp_apply, ← repr.eq, map_sum]

Goal state after:
R : Type u
A : Type v
B : Type w
ι : Type u_1
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : Coalgebra R A
inst✝² : Coalgebra R B
a : A
repr : Repr R a ι
F : Type u_2
inst✝¹ : FunLike F A B
inst✝ : CoalgHomClass F R A B
φ : F
⊢ ∑ x ∈ repr.index, (map ↑φ ↑φ) (repr.left x ⊗ₜ[R] repr.right x) =
    ∑ i ∈ repr.index, (⇑φ ∘ repr.left) i ⊗ₜ[R] (⇑φ ∘ repr.right) i
Module: Mathlib.RingTheory.Coalgebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : Coalgebra R A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : CoalgebraStruct R B
f : A ≃ₗc[R] B
⊢ LinearMap.rTensor B counit ∘ₗ comul = (TensorProduct.mk R R B) 1

Tactic:
(f.toLinearEquiv.eq_comp_toLinearMap_symm _ _).2 f.counit_comp,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : Coalgebra R A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : CoalgebraStruct R B
f : A ≃ₗc[R] B
⊢ LinearMap.rTensor B (counit ∘ₗ ↑f.toLinearEquiv.symm) ∘ₗ comul = (TensorProduct.mk R R B) 1
Module: Mathlib.RingTheory.Coalgebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : Coalgebra R A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : CoalgebraStruct R B
f : A ≃ₗc[R] B
⊢ LinearMap.lTensor B counit ∘ₗ comul = (TensorProduct.mk R B R).flip 1

Tactic:
(f.toLinearEquiv.eq_comp_toLinearMap_symm _ _).2 f.counit_comp,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : Coalgebra R A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : CoalgebraStruct R B
f : A ≃ₗc[R] B
⊢ LinearMap.lTensor B (counit ∘ₗ ↑f.toLinearEquiv.symm) ∘ₗ comul = (TensorProduct.mk R B R).flip 1
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : AddCommMonoid A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Algebra R S
inst✝⁷ : Module R A
inst✝⁶ : Module S A
inst✝⁵ : Module R B
inst✝⁴ : IsScalarTower R S A
inst✝³ : Coalgebra R B
inst✝² : Coalgebra S A
inst✝¹ : IsCocomm S A
inst✝ : IsCocomm R B
x : A
y : B
| (AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B) (comul x ⊗ₜ[R] comul y)

Tactic:
rw [← comm_comul _ x, ← comm_comul _ y]

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : AddCommMonoid A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Algebra R S
inst✝⁷ : Module R A
inst✝⁶ : Module S A
inst✝⁵ : Module R B
inst✝⁴ : IsScalarTower R S A
inst✝³ : Coalgebra R B
inst✝² : Coalgebra S A
inst✝¹ : IsCocomm S A
inst✝ : IsCocomm R B
x : A
y : B
| (AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B)
    ((TensorProduct.comm S A A) (comul x) ⊗ₜ[R] (TensorProduct.comm R B B) (comul y))
Module: Mathlib.CategoryTheory.Category.Pointed

Goal state before:
pp: case none
X : Type ?u.36
Y : Pointed
f : typeToPointed.obj X ⟶ Y
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.point ⇑(ConcreteCategory.hom f), map_point := ⋯ })
          ((fun f ↦ ↾(f.toFun ∘ some)) f)).toFun
      none =
    f.toFun none

pp: case some
X : Type ?u.36
Y : Pointed
f : typeToPointed.obj X ⟶ Y
val✝ : X
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.point ⇑(ConcreteCategory.hom f), map_point := ⋯ })
          ((fun f ↦ ↾(f.toFun ∘ some)) f)).toFun
      (some val✝) =
    f.toFun (some val✝)

Tactic:
· exact f.map_point.symm

Goal state after:
case some
X : Type ?u.36
Y : Pointed
f : typeToPointed.obj X ⟶ Y
val✝ : X
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.point ⇑(ConcreteCategory.hom f), map_point := ⋯ })
          ((fun f ↦ ↾(f.toFun ∘ some)) f)).toFun
      (some val✝) =
    f.toFun (some val✝)
Module: Mathlib.Order.Category.PartOrd

Goal state before:
pp: X : Preord
x : ↑{ carrier := Antisymmetrization ↑X fun x1 x2 ↦ x1 ≤ x2, str := instPartialOrderAntisymmetrization }
⊢ (PartOrd.Hom.hom (PartOrd.ofHom (Preord.Hom.hom (𝟙 X)).antisymmetrization)) x =
    (PartOrd.Hom.hom
        (𝟙 { carrier := Antisymmetrization ↑X fun x1 x2 ↦ x1 ≤ x2, str := instPartialOrderAntisymmetrization }))
      x

Tactic:
induction x using Quotient.inductionOn'

Goal state after:
case h
X : Preord
a✝ : ↑X
⊢ (PartOrd.Hom.hom (PartOrd.ofHom (Preord.Hom.hom (𝟙 X)).antisymmetrization)) (Quotient.mk'' a✝) =
    (PartOrd.Hom.hom
        (𝟙 { carrier := Antisymmetrization ↑X fun x1 x2 ↦ x1 ≤ x2, str := instPartialOrderAntisymmetrization }))
      (Quotient.mk'' a✝)
Module: Mathlib.Order.Category.PartOrd

Goal state before:
pp: X✝ Y✝ Z✝ : Preord
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x : ↑{ carrier := Antisymmetrization ↑X✝ fun x1 x2 ↦ x1 ≤ x2, str := instPartialOrderAntisymmetrization }
⊢ (PartOrd.Hom.hom (PartOrd.ofHom (Preord.Hom.hom (f ≫ g)).antisymmetrization)) x =
    (PartOrd.Hom.hom
        (PartOrd.ofHom (Preord.Hom.hom f).antisymmetrization ≫ PartOrd.ofHom (Preord.Hom.hom g).antisymmetrization))
      x

Tactic:
induction x using Quotient.inductionOn'

Goal state after:
case h
X✝ Y✝ Z✝ : Preord
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
a✝ : ↑X✝
⊢ (PartOrd.Hom.hom (PartOrd.ofHom (Preord.Hom.hom (f ≫ g)).antisymmetrization)) (Quotient.mk'' a✝) =
    (PartOrd.Hom.hom
        (PartOrd.ofHom (Preord.Hom.hom f).antisymmetrization ≫ PartOrd.ofHom (Preord.Hom.hom g).antisymmetrization))
      (Quotient.mk'' a✝)
Module: Mathlib.GroupTheory.MonoidLocalization.Away

Goal state before:
pp: M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
A : Type u_4
inst✝² : AddCommMonoid A
x : A
B : Type u_5
inst✝¹ : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst✝ : AddCommMonoid C
g : A →+ C
hg : IsAddUnit (g x)
y : ↥(multiples x)
n : ℕ
hn : (fun i ↦ i • x) n = ↑y
⊢ IsAddUnit (g (n • x))

Tactic:
g.map_nsmul

Goal state after:
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
A : Type u_4
inst✝² : AddCommMonoid A
x : A
B : Type u_5
inst✝¹ : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst✝ : AddCommMonoid C
g : A →+ C
hg : IsAddUnit (g x)
y : ↥(multiples x)
n : ℕ
hn : (fun i ↦ i • x) n = ↑y
⊢ IsAddUnit (n • g x)
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case mp
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
⊢ I.radical = I.jacobson → ⊥.radical = ⊥.jacobson

pp: case mpr
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
⊢ ⊥.radical = ⊥.jacobson → I.radical = I.jacobson

Tactic:
· intro h
    have := congr_arg (map (Ideal.Quotient.mk I)) h
    rw [map_radical_of_surjective hf (le_of_eq mk_ker),
      map_jacobson_of_surjective hf (le_of_eq mk_ker)] at this
    simpa using this

Goal state after:
case mpr
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
⊢ ⊥.radical = ⊥.jacobson → I.radical = I.jacobson
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    (((Functor.const J).obj (F.1 i)).map f ≫
        if h : Y = i then eqToHom ⋯ else (H Y h).from (((Functor.const J).obj (F.1 i)).obj Y)) =
      (if h : X = i then eqToHom ⋯ else (H X h).from (((Functor.const J).obj (F.1 i)).obj X)) ≫ F.map f

Tactic:
intro j k f

Goal state after:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j k : J
f : j ⟶ k
⊢ (((Functor.const J).obj (F.1 i)).map f ≫
      if h : k = i then eqToHom ⋯ else (H k h).from (((Functor.const J).obj (F.1 i)).obj k)) =
    (if h : j = i then eqToHom ⋯ else (H j h).from (((Functor.const J).obj (F.1 i)).obj j)) ≫ F.map f
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
⊢ selfZPow x B 0 = 1

Tactic:
by
  simp [selfZPow_of_nonneg _ _ le_rfl]

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
inst✝⁶ : BraidedCategory C
X Y Z W : C
inst✝⁵ : MonObj X
inst✝⁴ : MonObj Y
inst✝³ : MonObj Z
inst✝² : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst✝¹ : IsMonHom f
inst✝ : IsMonHom g
⊢ μ ≫ (f ⊗ₘ g) = ((f ⊗ₘ g) ⊗ₘ f ⊗ₘ g) ≫ μ

Tactic:
dsimp [tensorObj.mul_def]

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
inst✝⁶ : BraidedCategory C
X Y Z W : C
inst✝⁵ : MonObj X
inst✝⁴ : MonObj Y
inst✝³ : MonObj Z
inst✝² : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst✝¹ : IsMonHom f
inst✝ : IsMonHom g
⊢ (tensorμ X Z X Z ≫ (μ ⊗ₘ μ)) ≫ (f ⊗ₘ g) = ((f ⊗ₘ g) ⊗ₘ f ⊗ₘ g) ≫ tensorμ Y W Y W ≫ (μ ⊗ₘ μ)
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
⊢ μ ≫ (β_ X Y).hom = ((β_ X Y).hom ⊗ₘ (β_ X Y).hom) ≫ μ

Tactic:
dsimp [tensorObj.mul_def]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
⊢ (tensorμ X Y X Y ≫ (μ ⊗ₘ μ)) ≫ (β_ X Y).hom = ((β_ X Y).hom ⊗ₘ (β_ X Y).hom) ≫ tensorμ Y X Y X ≫ (μ ⊗ₘ μ)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case mk
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
a : A
s : ↥S
⊢ Quot.mk ⇑(OreLocalization.oreEqv S A) (a, s) * 1 = Quot.mk ⇑(OreLocalization.oreEqv S A) (a, s)

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

Goal state after:
Module: Mathlib.Logic.Equiv.Functor

Goal state before:
pp: α : Type u
f : Type u → Type v
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
x : f α
⊢ (mapEquiv f (Equiv.refl α)) x = (Equiv.refl (f α)) x

Tactic:
simp only [mapEquiv_apply, refl_apply]

Goal state after:
α : Type u
f : Type u → Type v
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
x : f α
⊢ ⇑(Equiv.refl α) <$> x = x
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'
s : ↥S
x y : LocalizedModule S M
⊢ ∀ (m m' : M) (s_1 s' : ↥S),
    (mk m s_1 + mk m' s').liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯ =
      (mk m s_1).liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯ + (mk m' s').liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯

Tactic:
intro m₁ m₂ t₁ t₂

Goal state after:
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'
s : ↥S
x y : LocalizedModule S M
m₁ m₂ : M
t₁ t₂ : ↥S
⊢ (mk m₁ t₁ + mk m₂ t₂).liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯ =
    (mk m₁ t₁).liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯ + (mk m₂ t₂).liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x y : LocalizedModule S M
⊢ ∀ (m m' : M) (s s' : ↥S),
    fromLocalizedModule' S f (LocalizedModule.mk m s + LocalizedModule.mk m' s') =
      fromLocalizedModule' S f (LocalizedModule.mk m s) + fromLocalizedModule' S f (LocalizedModule.mk m' s')

Tactic:
by
      intro a a' b b'
      simp only [LocalizedModule.mk_add_mk, fromLocalizedModule'_mk]
      rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, smul_add, ← map_smul, ← map_smul,
        ← map_smul, map_add]
      congr 1
      all_goals rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff']
      · simp [mul_smul, Submonoid.smul_def]
      · rw [Submonoid.coe_mul, LinearMap.map_smul_of_tower, mul_comm, mul_smul, Submonoid.smul_def]

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst✝⁴ : NonUnitalNonAssocSemiring M
inst✝³ : Semiring M'
inst✝² : Module R M
inst✝¹ : Algebra R M'
f : M →ₗ[R] M'
hf : ∀ (m₁ m₂ : M), f (m₁ * m₂) = f m₁ * f m₂
inst✝ : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ f (m₁ • m₂) = mk' f (↑s₁ • m₁) s₁ • ↑s₂ • mk' f m₂ s₂

Tactic:
← mk'_smul

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst✝⁴ : NonUnitalNonAssocSemiring M
inst✝³ : Semiring M'
inst✝² : Module R M
inst✝¹ : Algebra R M'
f : M →ₗ[R] M'
hf : ∀ (m₁ m₂ : M), f (m₁ * m₂) = f m₁ * f m₂
inst✝ : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ f (m₁ • m₂) = mk' f (↑s₁ • m₁) s₁ • mk' f (↑s₂ • m₂) s₂
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁸ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : AddCommMonoid M'
inst✝¹⁵ : AddCommMonoid M''
A : Type u_5
inst✝¹⁴ : CommSemiring A
inst✝¹³ : Algebra R A
inst✝¹² : Module A M'
inst✝¹¹ : IsLocalization S A
inst✝¹⁰ : Module R M
inst✝⁹ : Module R M'
inst✝⁸ : Module R M''
inst✝⁷ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝⁶ : IsLocalizedModule S f
M₁ : Type u_6
M₂ : Type u_7
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
S₁ S₂ : Submonoid R
h : S₁ ≤ S₂
f₁ : M →ₗ[R] M₁
f₂ : M →ₗ[R] M₂
inst✝¹ : IsLocalizedModule S₁ f₁
inst✝ : IsLocalizedModule S₂ f₂
x₁ x₂ : M × ↥S₁
c : ↥S₂
e : ↑c • ↑x₁.2 • x₂.1 = ↑c • ↑x₂.2 • x₁.1
⊢ ↑1 • ↑x₁.2 • ↑c • x₂.1 = ↑1 • ↑x₂.2 • ↑c • x₁.1

Tactic:
by simpa [← smul_comm c.1]

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

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
A : Type u_3
N : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : CommRing A
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module A N
inst✝⁵ : Algebra R A
inst✝⁴ : Module R N
inst✝³ : IsScalarTower R A N
f : M →ₗ[R] N
S : Submonoid R
hS : ∀ s ∈ S, s ≠ 0 → IsRegular s
inst✝² : IsTorsionFree R M
inst✝¹ : IsLocalization S A
inst✝ : IsLocalizedModule S f
c : A
hc : IsRegular c
x y : N
hxy : (fun x ↦ c • x) x = (fun x ↦ c • x) y
hS₀ : 0 ∈ S
⊢ x = y

Tactic:
have : Subsingleton N := (IsLocalizedModule.subsingleton_iff S f).2 fun _ ↦ ⟨0, hS₀, by simp⟩
      exact Subsingleton.elim ..

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ c✝ : B
f✝ f'✝ : a✝ ⟶ b✝
η : f✝ ⟶ f'✝
g : b✝ ⟶ c✝
⊢ G.map₂ (F.mapComp f✝ g) ≫ G.mapComp (F.map f✝) (F.map g) ≫ G.map₂ (F.map₂ η) ▷ G.map (F.map g) =
    (G.map₂ (F.mapComp f✝ g) ≫ G.mapComp (F.map f✝) (F.map g)) ≫ G.map₂ (F.map₂ η) ▷ G.map (F.map g)

Tactic:
assoc

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ c✝ : B
f✝ f'✝ : a✝ ⟶ b✝
η : f✝ ⟶ f'✝
g : b✝ ⟶ c✝
⊢ G.map₂ (F.mapComp f✝ g) ≫ G.mapComp (F.map f✝) (F.map g) ≫ G.map₂ (F.map₂ η) ▷ G.map (F.map g) =
    G.map₂ (F.mapComp f✝ g) ≫ G.mapComp (F.map f✝) (F.map g) ≫ G.map₂ (F.map₂ η) ▷ G.map (F.map g)
Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ c✝ : B
η : a✝ ⟶ b✝
g✝ g'✝ : b✝ ⟶ c✝
η✝ : g✝ ⟶ g'✝
⊢ G.map₂ (F.mapComp η g✝) ≫ G.mapComp (F.map η) (F.map g✝) ≫ G.map (F.map η) ◁ G.map₂ (F.map₂ η✝) =
    (G.map₂ (F.mapComp η g✝) ≫ G.mapComp (F.map η) (F.map g✝)) ≫ G.map (F.map η) ◁ G.map₂ (F.map₂ η✝)

Tactic:
assoc

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ c✝ : B
η : a✝ ⟶ b✝
g✝ g'✝ : b✝ ⟶ c✝
η✝ : g✝ ⟶ g'✝
⊢ G.map₂ (F.mapComp η g✝) ≫ G.mapComp (F.map η) (F.map g✝) ≫ G.map (F.map η) ◁ G.map₂ (F.map₂ η✝) =
    G.map₂ (F.mapComp η g✝) ≫ G.mapComp (F.map η) (F.map g✝) ≫ G.map (F.map η) ◁ G.map₂ (F.map₂ η✝)
Module: Mathlib.RingTheory.Finiteness.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
n : ℕ
hI : I.FG
⊢ (I ^ Nat.zero).FG

Tactic:
rw [I.pow_zero, one_eq_top]

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
n : ℕ
hI : I.FG
⊢ ⊤.FG
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case refine_2
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := fun x ↦ MvPolynomial.C ↑x - (MvPolynomial.map (algebraMap R A)) (t' x)
⊢ Ideal.span ↑(Finset.image (⇑(MvPolynomial.map (algebraMap R A))) s ∪ Finset.image g t.attach) =
    RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)).toRingHom

Tactic:
rw [Finset.coe_union, Finset.coe_image, Finset.coe_image, Finset.attach_eq_univ,
      Finset.coe_univ, Set.image_univ]

Goal state after:
case refine_2
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := fun x ↦ MvPolynomial.C ↑x - (MvPolynomial.map (algebraMap R A)) (t' x)
⊢ Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) =
    RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)).toRingHom
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X Y : F.Elements
f : X ⟶ Y
⊢ (StructuredArrow.mk (↾fun x ↦ X.snd)).hom ≫ F.map ↑f = (StructuredArrow.mk (↾fun x ↦ Y.snd)).hom

Tactic:
ext; simp [f.2]

Goal state after: