mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
F : Type u_3
inst✝¹ : FunLike F R S
f : F
inst✝ : NonUnitalRingHomClass F R S
I : TwoSidedIdeal S
⊢ ∀ ⦃b : TwoSidedIdeal S⦄,
    I ≤ b → (fun I ↦ { ringCon := I.ringCon.comap f }) I ≤ (fun I ↦ { ringCon := I.ringCon.comap f }) b

Tactic:
J

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
F : Type u_3
inst✝¹ : FunLike F R S
f : F
inst✝ : NonUnitalRingHomClass F R S
I J : TwoSidedIdeal S
⊢ I ≤ J → (fun I ↦ { ringCon := I.ringCon.comap f }) I ≤ (fun I ↦ { ringCon := I.ringCon.comap f }) J
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z : R
⊢ ∀ (y x : R), y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ → y * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
rintro y x (((hy | ⟨y, hy, r, -, rfl⟩) | ⟨r, -, y, hy, rfl⟩) |
        ⟨-, ⟨r', -, y, hy, rfl⟩, r, -, rfl⟩)

Goal state after:
case refine_2.inl.inl.inl
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z y x : R
hy : y ∈ s
⊢ y * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

case refine_2.inl.inl.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x y : R
hy : y ∈ s
r : R
⊢ (fun x1 x2 ↦ x1 * x2) y r * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

case refine_2.inl.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r y : R
hy : y ∈ s
⊢ (fun x1 x2 ↦ x1 * x2) r y * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

case refine_2.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
⊢ (fun x1 x2 ↦ x1 * x2) ((fun x1 x2 ↦ x1 * x2) r' y) r * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_3
inst✝⁵ : CommRing R
x : R
B : Type u_4
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : IsLocalization.Away x B
inst✝¹ : IsDomain R
inst✝ : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
d : ℕ
hy : x ^ d = ↑y
this : IsDomain B
H : b * (algebraMap R B) x ^ d = (algebraMap R B) a₀
⊢ a₀ ≠ 0

Tactic:
apply ((injective_iff_map_eq_zero' (algebraMap R B)).mp _ a₀).mpr.mt

Goal state after:
R : Type u_3
inst✝⁵ : CommRing R
x : R
B : Type u_4
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : IsLocalization.Away x B
inst✝¹ : IsDomain R
inst✝ : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
d : ℕ
hy : x ^ d = ↑y
this : IsDomain B
H : b * (algebraMap R B) x ^ d = (algebraMap R B) a₀
⊢ ¬(algebraMap R B) a₀ = 0

R : Type u_3
inst✝⁵ : CommRing R
x : R
B : Type u_4
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : IsLocalization.Away x B
inst✝¹ : IsDomain R
inst✝ : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
d : ℕ
hy : x ^ d = ↑y
this : IsDomain B
H : b * (algebraMap R B) x ^ d = (algebraMap R B) a₀
⊢ Function.Injective ⇑(algebraMap R B)
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| (M ◁ η ⊗ₘ N ◁ η) ≫ (μ ⊗ₘ μ)

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| (M ⊗ N) ◁ (λ_ (𝟙_ C)).inv

pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| tensorμ M N (𝟙_ C) (𝟙_ C)

Tactic:
rw [tensorHom_comp_tensorHom, mul_one, mul_one]

Goal state after:
case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| (ρ_ M).hom ⊗ₘ (ρ_ N).hom

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| (M ⊗ N) ◁ (λ_ (𝟙_ C)).inv

case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| tensorμ M N (𝟙_ C) (𝟙_ C)
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
v : ι → M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
t : Finset ι
g₁ g₂ : ι → Rₛ
eq : ∑ i ∈ t, g₁ i • (⇑f ∘ v) i = ∑ i ∈ t, g₂ i • (⇑f ∘ v) i
i : ι
hi : i ∈ t
a : ↥S
fg : ι ⊕ ι → R
hfg :
  (∀ (a_1 : ι), Sum.inl a_1 ∈ t.disjSum t → (algebraMap R Rₛ) (fg (Sum.inl a_1)) = ↑a • Sum.elim g₁ g₂ (Sum.inl a_1)) ∧
    ∀ (b : ι), Sum.inr b ∈ t.disjSum t → (algebraMap R Rₛ) (fg (Sum.inr b)) = ↑a • Sum.elim g₁ g₂ (Sum.inr b)
⊢ g₁ i = g₂ i

Tactic:
Finset.inl_mem_disjSum,

Goal state after:
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
v : ι → M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
t : Finset ι
g₁ g₂ : ι → Rₛ
eq : ∑ i ∈ t, g₁ i • (⇑f ∘ v) i = ∑ i ∈ t, g₂ i • (⇑f ∘ v) i
i : ι
hi : i ∈ t
a : ↥S
fg : ι ⊕ ι → R
hfg :
  (∀ a_1 ∈ t, (algebraMap R Rₛ) (fg (Sum.inl a_1)) = ↑a • Sum.elim g₁ g₂ (Sum.inl a_1)) ∧
    ∀ (b : ι), Sum.inr b ∈ t.disjSum t → (algebraMap R Rₛ) (fg (Sum.inr b)) = ↑a • Sum.elim g₁ g₂ (Sum.inr b)
⊢ g₁ i = g₂ i
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
A✝ B✝ : Mon C
f : A✝ ⟶ B✝
e : IsIso ((forget C).map f)
⊢ f ≫ Hom.mk' (inv f.hom) ⋯ ⋯ = 𝟙 A✝ ∧ Hom.mk' (inv f.hom) ⋯ ⋯ ≫ f = 𝟙 B✝

Tactic:
cat_disch

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

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
inst✝¹ : IsIso fst
inst✝ : Mono g
sq : CommSq fst snd f g
⊢ ∀ (s : PullbackCone f g) (m : s.pt ⟶ P), m ≫ fst = s.fst → m ≫ snd = s.snd → m = s.fst ≫ inv fst

Tactic:
cat_disch

Goal state after:
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
inst✝⁶ : IsLocalization S A
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_4
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
inst✝¹ : Module A M'
inst✝ : IsScalarTower R A M'
f : M →ₗ[R] M'
h : IsBaseChange A f
this✝ : Module A (LocalizedModule S M) := LocalizedModule.moduleOfIsLocalization
this : IsBaseChange A (LocalizedModule.mkLinearMap S M)
e : LocalizedModule S M ≃ₗ[R] M' := LinearEquiv.restrictScalars R (this.equiv.symm ≪≫ₗ h.equiv)
x✝ : M
⊢ f x✝ = (↑e ∘ₗ LocalizedModule.mkLinearMap S M) x✝

Tactic:
rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
    LinearEquiv.restrictScalars_apply, LinearEquiv.trans_apply, IsBaseChange.equiv_symm_apply,
    IsBaseChange.equiv_tmul, one_smul]

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

Goal state before:
pp: case h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
c : BinaryFan X Y
hc : IsLimit c
T : C
hT : IsTerminal T
s :
  PullbackCone (hT.from ((pair X Y).obj { as := WalkingPair.left }))
    (hT.from ((pair X Y).obj { as := WalkingPair.right }))
m : s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
h₁ : m ≫ c.fst = s.fst
h₂ : m ≫ c.snd = s.snd
⊢ m ≫ c.fst = BinaryFan.IsLimit.lift hc s.fst s.snd ≫ c.fst

Tactic:
cat_disch

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

Goal state before:
pp: case h₂
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
c : BinaryFan X Y
hc : IsLimit c
T : C
hT : IsTerminal T
s :
  PullbackCone (hT.from ((pair X Y).obj { as := WalkingPair.left }))
    (hT.from ((pair X Y).obj { as := WalkingPair.right }))
m : s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
h₁ : m ≫ c.fst = s.fst
h₂ : m ≫ c.snd = s.snd
⊢ m ≫ c.snd = BinaryFan.IsLimit.lift hc s.fst s.snd ≫ c.snd

Tactic:
cat_disch

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

Goal state before:
pp: case h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
I : C
hI : IsInitial I
s :
  PushoutCocone (hI.to ((pair X Y).obj { as := WalkingPair.right })) (hI.to ((pair X Y).obj { as := WalkingPair.left }))
m : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.right } ⟶ s.pt
h₁ : c.inr ≫ m = s.inl
h₂ : c.inl ≫ m = s.inr
⊢ c.inl ≫ m = c.inl ≫ BinaryCofan.IsColimit.desc hc s.inr s.inl

Tactic:
cat_disch

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

Goal state before:
pp: case h₂
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
I : C
hI : IsInitial I
s :
  PushoutCocone (hI.to ((pair X Y).obj { as := WalkingPair.right })) (hI.to ((pair X Y).obj { as := WalkingPair.left }))
m : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.right } ⟶ s.pt
h₁ : c.inr ≫ m = s.inl
h₂ : c.inl ≫ m = s.inr
⊢ c.inr ≫ m = c.inr ≫ BinaryCofan.IsColimit.desc hc s.inr s.inl

Tactic:
cat_disch

Goal state after:
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_7
S : Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
A : Type u_9
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
s : S
x : R
y : ↥M
⊢ s ⊗ₜ[R] (algebraMap R A) x = (RingHom.id S) ((algebraMap R S) x * s) ⊗ₜ[R] 1

Tactic:
RingHom.id_apply,

Goal state after:
R : Type u_7
S : Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
A : Type u_9
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
s : S
x : R
y : ↥M
⊢ s ⊗ₜ[R] (algebraMap R A) x = ((algebraMap R S) x * s) ⊗ₜ[R] 1
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_7
S : Type u_8
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
A : Type u_9
inst✝¹¹ : CommSemiring A
inst✝¹⁰ : Algebra R A
M : Submonoid A
B : Type u_10
inst✝⁹ : CommSemiring B
inst✝⁸ : Algebra R B
inst✝⁷ : Algebra A B
inst✝⁶ : IsScalarTower R A B
inst✝⁵ : IsLocalization M B
C : Type u_11
inst✝⁴ : CommSemiring C
inst✝³ : Algebra S C
inst✝² : Algebra (S ⊗[R] A) C
inst✝¹ : IsScalarTower S (S ⊗[R] A) C
inst✝ : IsLocalization (Submonoid.map Algebra.TensorProduct.includeRight M) C
x : S
a : A
this : Algebra (S ⊗[R] A) (S ⊗[R] B) :=
  (Algebra.TensorProduct.map (AlgHom.id R S) (IsScalarTower.toAlgHom R A B)).toAlgebra
⊢ (tensorProductEquivOfMapIncludeRight R S M B C) (x ⊗ₜ[R] (algebraMap A B) a) = (algebraMap (S ⊗[R] A) C) (x ⊗ₜ[R] a)

Tactic:
have heq : x ⊗ₜ[R] (algebraMap A B) a = algebraMap _ _ (x ⊗ₜ[R] a) := rfl

Goal state after:
R : Type u_7
S : Type u_8
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
A : Type u_9
inst✝¹¹ : CommSemiring A
inst✝¹⁰ : Algebra R A
M : Submonoid A
B : Type u_10
inst✝⁹ : CommSemiring B
inst✝⁸ : Algebra R B
inst✝⁷ : Algebra A B
inst✝⁶ : IsScalarTower R A B
inst✝⁵ : IsLocalization M B
C : Type u_11
inst✝⁴ : CommSemiring C
inst✝³ : Algebra S C
inst✝² : Algebra (S ⊗[R] A) C
inst✝¹ : IsScalarTower S (S ⊗[R] A) C
inst✝ : IsLocalization (Submonoid.map Algebra.TensorProduct.includeRight M) C
x : S
a : A
this : Algebra (S ⊗[R] A) (S ⊗[R] B) :=
  (Algebra.TensorProduct.map (AlgHom.id R S) (IsScalarTower.toAlgHom R A B)).toAlgebra
heq : x ⊗ₜ[R] (algebraMap A B) a = (algebraMap (S ⊗[R] A) (S ⊗[R] B)) (x ⊗ₜ[R] a)
⊢ (tensorProductEquivOfMapIncludeRight R S M B C) (x ⊗ₜ[R] (algebraMap A B) a) = (algebraMap (S ⊗[R] A) C) (x ⊗ₜ[R] a)
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
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x y : T
m : M
s : ↥S
⊢ (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 *
        IsLocalization.mk' T (IsLocalization.sec S y).1 (IsLocalization.sec S y).2) •
      mk m s =
    IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 •
      IsLocalization.mk' T (IsLocalization.sec S y).1 (IsLocalization.sec S y).2 • mk m s

Tactic:
simp_rw [← IsLocalization.mk'_mul, mk'_smul_mk, ← mul_smul, mul_assoc]

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_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''
e : M'' ≃ₗ[R] M
hf : IsLocalizedModule S f
x₁✝ x₂✝ : M''
h : f (e x₁✝) = f (e x₂✝)
c : ↥S
hc : c • e x₁✝ = c • e x₂✝
⊢ c • x₁✝ = c • x₂✝

Tactic:
simpa only [Submonoid.smul_def, map_smul, e.symm_apply_apply]
      using congr(e.symm $hc)

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Algebra

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
A B : T.Algebra
f : A ⟶ B
inst✝ : IsIso f.f
⊢ f ≫ { f := inv f.f, h := ⋯ } = 𝟙 A ∧ { f := inv f.f, h := ⋯ } ≫ f = 𝟙 B

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Algebra

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : Comonad C
A B : G.Coalgebra
f : A ⟶ B
inst✝ : IsIso f.f
⊢ f ≫ { f := inv f.f, h := ⋯ } = 𝟙 A ∧ { f := inv f.f, h := ⋯ } ≫ f = 𝟙 B

Tactic:
cat_disch

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

Goal state before:
pp: case e_a
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ g (↑(b * b') • a) = ↑b • g (b' • a)

Tactic:
simp only [Submonoid.coe_mul, LinearMap.map_smul_of_tower]

Goal state after:
case e_a
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ (↑b * ↑b') • g a = ↑b • b' • g a
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_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
l : LocalizedModule S M →ₗ[R] M''
hl : l ∘ₗ mkLinearMap S M = g
⊢ lift S g h = l

Tactic:
by
  ext x; induction x with | _ m s
  rw [LocalizedModule.lift_mk]
  rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← hl, LinearMap.coe_comp,
    Function.comp_apply, LocalizedModule.mkLinearMap_apply, ← l.map_smul, LocalizedModule.smul'_mk]
  congr 1; rw [LocalizedModule.mk_eq]
  refine ⟨1, ?_⟩; simp only [one_smul, Submonoid.smul_def]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Pullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst✝ : HasPullbacksAlong f
x : Over X
y : Over Y
⊢ Function.LeftInverse (fun v ↦ homMk (Hom.left v ≫ pullback.fst y.hom f) ⋯) fun u ↦
    homMk (pullback.lift (Hom.left u) x.hom ⋯) ⋯

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Pullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst✝ : HasPushoutsAlong f
x : Under X
y : Under Y
⊢ Function.RightInverse (fun v ↦ homMk (pushout.desc (Hom.right v) y.hom ⋯) ⋯) fun u ↦
    homMk (pushout.inl x.hom f ≫ Hom.right u) ⋯

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
g : (⊥_ StructuredArrow A G).right ⟶ B
B' : StructuredArrow A G := StructuredArrow.mk ((⊥_ StructuredArrow A G).hom ≫ G.map g)
g' : ⊥_ StructuredArrow A G ⟶ B' := StructuredArrow.homMk g ⋯
⊢ initial.to B' = g'

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B : D
A : C
⊢ Function.LeftInverse (fun g ↦ G.map g ≫ (⊤_ CostructuredArrow G A).hom) fun g ↦
    (terminal.from (CostructuredArrow.mk g)).left

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B : D
A : C
g : B ⟶ (⊤_ CostructuredArrow G A).left
B' : CostructuredArrow G A := CostructuredArrow.mk (G.map g ≫ (⊤_ CostructuredArrow G A).hom)
g' : B' ⟶ ⊤_ CostructuredArrow G A := CostructuredArrow.homMk g ⋯
⊢ terminal.from B' = g'

Tactic:
cat_disch

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_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
m : M
s : ↥S
⊢ (fromLocalizedModule S f) (LocalizedModule.mk (s • m) s) = f m

Tactic:
LocalizedModule.mk_cancel,

Goal state after:
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
m : M
s : ↥S
⊢ (fromLocalizedModule S f) (LocalizedModule.mk m 1) = f m
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : ↥S
m : M
⊢ (LocalizedModule.mkLinearMap S M) m = LocalizedModule.mk (s • m) s

Tactic:
LocalizedModule.mk_cancel,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : ↥S
m : M
⊢ (LocalizedModule.mkLinearMap S M) m = LocalizedModule.mk m 1
Module: Mathlib.CategoryTheory.Limits.Comma

Goal state before:
pp: J : Type w
inst✝³ : Category.{w', w} J
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
G : A ⥤ T
X : T
F : J ⥤ CostructuredArrow G X
i₁ : HasColimit (F ⋙ proj G X)
i₂ : PreservesColimit (F ⋙ proj G X) G
⊢ HasColimit F

Tactic:
have : HasColimit (F ⋙ Comma.fst G (Functor.fromPUnit X)) := i₁

Goal state after:
J : Type w
inst✝³ : Category.{w', w} J
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
G : A ⥤ T
X : T
F : J ⥤ CostructuredArrow G X
i₁ : HasColimit (F ⋙ proj G X)
i₂ : PreservesColimit (F ⋙ proj G X) G
this : HasColimit (F ⋙ Comma.fst G (fromPUnit X))
⊢ HasColimit F
Module: Mathlib.CategoryTheory.Limits.ConeCategory

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : Cone F
⊢ Function.LeftInverse (fun h s ↦ { default := h.from s, uniq := ⋯ }) fun x ↦ IsTerminal.ofUnique c

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConeCategory

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : Cone F
⊢ Function.RightInverse (fun h s ↦ { default := h.from s, uniq := ⋯ }) fun x ↦ IsTerminal.ofUnique c

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConeCategory

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : Cocone F
⊢ Function.LeftInverse (fun h s ↦ { default := h.to s, uniq := ⋯ }) fun x ↦ IsInitial.ofUnique c

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConeCategory

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : Cocone F
⊢ Function.RightInverse (fun h s ↦ { default := h.to s, uniq := ⋯ }) fun x ↦ IsInitial.ofUnique c

Tactic:
cat_disch

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 : B ⥤ᵒᵖᴸ C
b : B
f : b ⟶ b
hf : f = 𝟙 b
⊢ f = 𝟙 b

Tactic:
rw [hf]

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

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᴸ C
b : B
f : b ⟶ b
hf : f = 𝟙 b
⊢ 𝟙 b = f

Tactic:
rw [hf]

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

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
a b✝ b : B
f : b ⟶ b
hf : f = 𝟙 b
⊢ f = 𝟙 b

Tactic:
rw [hf]

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Opposite

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
X : P.op.FullSubcategory
⊢ ((P.lift P.op.ι.leftOp ⋯).rightOp.map ((Iso.refl (𝟭 P.op.FullSubcategory)).hom.app X) ≫
        (Iso.refl (P.op.lift P.ι.op ⋯ ⋙ (P.lift P.op.ι.leftOp ⋯).rightOp)).hom.app
          ((P.lift P.op.ι.leftOp ⋯).rightOp.obj X)).unop =
    (𝟙 ((P.lift P.op.ι.leftOp ⋯).rightOp.obj X)).unop

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Cone

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
X : C
K : J ⥤ Over X
F : C ⥤ D
t t₁ t₂ : Cone K
f : t₁ ⟶ t₂
⊢ Over.Hom.left f.hom ≫
      { pt := t₂.pt.left,
              π :=
                {
                  app := fun x ↦
                    match x with
                    | of a => Over.Hom.left (t₂.π.app a)
                    | star => t₂.pt.hom,
                  naturality := ⋯ } }.π.app
        star =
    { pt := t₁.pt.left,
            π :=
              {
                app := fun x ↦
                  match x with
                  | of a => Over.Hom.left (t₁.π.app a)
                  | star => t₁.pt.hom,
                naturality := ⋯ } }.π.app
      star

Tactic:
cat_disch

Goal state after: