mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: 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
⊢ 0 = TensorProduct.map 0 0 ∘ₗ comul

Tactic:
TensorProduct.map_zero_left,

Goal state after:
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
⊢ 0 = 0 ∘ₗ comul
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: 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
⊢ 0 = 0 ∘ₗ comul

Tactic:
zero_comp

Goal state after:
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
⊢ 0 = 0
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: 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
⊢ 0 = TensorProduct.map 0 0 ∘ₗ comul

Tactic:
TensorProduct.map_zero_left,

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
⊢ 0 = 0 ∘ₗ comul
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: 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
⊢ 0 = 0 ∘ₗ comul

Tactic:
zero_comp

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
⊢ 0 = 0
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : CoalgebraStruct R M
⊢ comul ∘ₗ lcoeFun = map lcoeFun lcoeFun ∘ₗ comul

Tactic:
by
  apply LinearMap.ext fun x ↦ ?_
  rw [← Finsupp.univ_sum_single x]
  simp [-univ_sum_single, single_eq_pi_single, map_map]

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A
inst✝¹⁰ : Semiring B
inst✝⁹ : Semiring C
inst✝⁸ : Semiring D
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra R C
inst✝⁴ : Algebra R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
g : A →ₐc[R] B
toCoalgHom✝ : A →ₗc[R] B
map_one'✝ : toCoalgHom✝.toFun 1 = 1
map_mul'✝ : ∀ (x y : A), toCoalgHom✝.toFun (x * y) = toCoalgHom✝.toFun x * toCoalgHom✝.toFun y
h : (fun f ↦ f.toFun) { toCoalgHom := toCoalgHom✝, map_one' := map_one'✝, map_mul' := map_mul'✝ } = (fun f ↦ f.toFun) g
⊢ { toCoalgHom := toCoalgHom✝, map_one' := map_one'✝, map_mul' := map_mul'✝ } = g

Tactic:
rcases g with ⟨_, _⟩

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A
inst✝¹⁰ : Semiring B
inst✝⁹ : Semiring C
inst✝⁸ : Semiring D
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra R C
inst✝⁴ : Algebra R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
toCoalgHom✝¹ : A →ₗc[R] B
map_one'✝¹ : toCoalgHom✝¹.toFun 1 = 1
map_mul'✝¹ : ∀ (x y : A), toCoalgHom✝¹.toFun (x * y) = toCoalgHom✝¹.toFun x * toCoalgHom✝¹.toFun y
toCoalgHom✝ : A →ₗc[R] B
map_one'✝ : toCoalgHom✝.toFun 1 = 1
map_mul'✝ : ∀ (x y : A), toCoalgHom✝.toFun (x * y) = toCoalgHom✝.toFun x * toCoalgHom✝.toFun y
h :
  (fun f ↦ f.toFun) { toCoalgHom := toCoalgHom✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    (fun f ↦ f.toFun) { toCoalgHom := toCoalgHom✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
⊢ { toCoalgHom := toCoalgHom✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    { toCoalgHom := toCoalgHom✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
P : Type u_5
N' : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid N'
inst✝ : Module R N'
f : N →ₗ[R] N'
g : P →ₗ[R] M ⊗[R] N
⊢ α ∘ₗ λ⁻¹ ⊗ₘ f ∘ₗ g = LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f) ∘ₗ λ⁻¹ ∘ₗ g

Tactic:
simp_rw [← LinearMap.comp_assoc, ← assoc_comp_map_lid_symm]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
e : R
he : IsIdempotentElem e
H : ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ e * x = e * y
H' : Function.Surjective ⇑(algebraMap R S)
z : R
⊢ ∃ x, (algebraMap R S) z * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1

Tactic:
exact ⟨⟨z, 1⟩, by simp⟩

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

Goal state before:
pp: case refine_2
S : Type u_4
T : Type u_5
inst✝² : CommRing S
inst✝¹ : CommRing T
inst✝ : Algebra S T
h₁ : Function.Surjective ⇑(algebraMap S T)
r : S
hr : IsUnit ((algebraMap S T) r)
n : ℕ
hn : r ^ n • RingHom.ker (algebraMap S T) ≤ ⊥
x y : S
h : (algebraMap S T) x = (algebraMap S T) y
⊢ r ^ n * x = r ^ n * y

Tactic:
rw [← sub_eq_zero, ← mul_sub]

Goal state after:
case refine_2
S : Type u_4
T : Type u_5
inst✝² : CommRing S
inst✝¹ : CommRing T
inst✝ : Algebra S T
h₁ : Function.Surjective ⇑(algebraMap S T)
r : S
hr : IsUnit ((algebraMap S T) r)
n : ℕ
hn : r ^ n • RingHom.ker (algebraMap S T) ≤ ⊥
x y : S
h : (algebraMap S T) x = (algebraMap S T) y
⊢ r ^ n * (x - y) = 0
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
I✝ I : Ideal R
inst✝ : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribSMul.toLinearMap R R (MulOpposite.op r)) 𝔪
I𝔪₀ : I ≤ 𝔪₀
h : 1 ∈ 𝔪₀
⊢ r ∈ 𝔪

Tactic:
by simpa [𝔪₀] using h

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Finset 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
span_eq : Ideal.span ↑s = ⊤
n : ↑↑s → ℕ
r✝¹ : ↑↑s → R
eq✝¹ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) ↑a ^ n a = (algebraMap R (Away ↑a)) (r✝¹ a)
N✝ : ℕ := s.attach.sup n
r✝ : ↑↑s → R := fun a ↦ ↑a ^ (N✝ - n a) * r✝¹ a
eq✝ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N✝) = (algebraMap R (Away ↑a)) (r✝ a)
N'✝ : ↑↑s → ↑↑s → ℕ
hN' : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N'✝ a b * (r✝ a * ↑b ^ N✝) = (↑a * ↑b) ^ N'✝ a b * (r✝ b * ↑a ^ N✝)
N' : ℕ := (s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩
eq2✝ : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N' * (r✝ a * ↑b ^ N✝) = (↑a * ↑b) ^ N' * (r✝ b * ↑a ^ N✝)
N : ℕ := N' + N✝
r : ↑↑s → R := fun a ↦ ↑a ^ N' * r✝ a
eq : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N) = (algebraMap R (Away ↑a)) (r a)
eq2 : ∀ (a b : ↑↑s), r a * ↑b ^ N = r b * ↑a ^ N
c : ↑↑s → R
eq1 : ∑ i, c i • ↑i ^ N = 1
a : ↑↑s
⊢ (algebraMap R (Away ↑a)) (r a * ∑ x, c x • ↑x ^ N) = (algebraMap R (Away ↑a)) (r a)

Tactic:
eq1,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Finset 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
span_eq : Ideal.span ↑s = ⊤
n : ↑↑s → ℕ
r✝¹ : ↑↑s → R
eq✝¹ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) ↑a ^ n a = (algebraMap R (Away ↑a)) (r✝¹ a)
N✝ : ℕ := s.attach.sup n
r✝ : ↑↑s → R := fun a ↦ ↑a ^ (N✝ - n a) * r✝¹ a
eq✝ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N✝) = (algebraMap R (Away ↑a)) (r✝ a)
N'✝ : ↑↑s → ↑↑s → ℕ
hN' : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N'✝ a b * (r✝ a * ↑b ^ N✝) = (↑a * ↑b) ^ N'✝ a b * (r✝ b * ↑a ^ N✝)
N' : ℕ := (s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩
eq2✝ : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N' * (r✝ a * ↑b ^ N✝) = (↑a * ↑b) ^ N' * (r✝ b * ↑a ^ N✝)
N : ℕ := N' + N✝
r : ↑↑s → R := fun a ↦ ↑a ^ N' * r✝ a
eq : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N) = (algebraMap R (Away ↑a)) (r a)
eq2 : ∀ (a b : ↑↑s), r a * ↑b ^ N = r b * ↑a ^ N
c : ↑↑s → R
eq1 : ∑ i, c i • ↑i ^ N = 1
a : ↑↑s
⊢ (algebraMap R (Away ↑a)) (r a * 1) = (algebraMap R (Away ↑a)) (r a)
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case pos.hn
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
d : ℤ
hd : d ≤ 0
⊢ 0 ≤ -d

Tactic:
apply nonneg_of_neg_nonpos

Goal state after:
case pos.hn
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
d : ℤ
hd : d ≤ 0
⊢ - -d ≤ 0
Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization

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
x : R
s : ↥S
⊢ mk' A x s = IsLocalizedModule.mk' (Algebra.linearMap R A) x s

Tactic:
rw [← IsLocalizedModule.smul_inj (Algebra.linearMap R A) s, IsLocalizedModule.mk'_cancel']
  exact IsLocalization.smul_mk'_self

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cone F
X : C
hX : IsTerminal X
f : F.obj { as := WalkingPair.left } ⟶ X
g : F.obj { as := WalkingPair.right } ⟶ X
hc : IsLimit (PullbackCone.mk (c.π.app { as := WalkingPair.left }) (c.π.app { as := WalkingPair.right }) ⋯)
s : Cone F
m : s.pt ⟶ c.pt
J : ∀ (j : Discrete WalkingPair), m ≫ c.π.app j = s.π.app j
⊢ m = hc.lift (PullbackCone.mk (s.π.app { as := WalkingPair.left }) (s.π.app { as := WalkingPair.right }) ⋯)

Tactic:
let c' :=
      PullbackCone.mk (m ≫ c.π.app ⟨WalkingPair.left⟩) (m ≫ c.π.app ⟨WalkingPair.right⟩ :)
        (hX.hom_ext (_ ≫ f) (_ ≫ g))
    dsimp; rw [← J, ← J]
    apply hc.hom_ext
    rintro (_ | (_ | _)) <;> simp only [PullbackCone.mk_π_app]
    exacts [(Category.assoc _ _ _).symm.trans (hc.fac_assoc c' WalkingCospan.left f).symm,
      (hc.fac c' WalkingCospan.left).symm, (hc.fac c' WalkingCospan.right).symm]

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
h : IsPullback fst snd f g
inst : Mono g
⊢ ∀ {Z : C} (g h : Z ⟶ P), g ≫ fst = h ≫ fst → g = h

Tactic:
intro W

Goal state after:
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
h : IsPullback fst snd f g
inst : Mono g
W : C
⊢ ∀ (g h : W ⟶ P), g ≫ fst = h ≫ fst → g = h
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst : Epi g
⊢ ∀ {Z : C} (g h : P ⟶ Z), inl ≫ g = inl ≫ h → g = h

Tactic:
intro W

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst : Epi g
W : C
⊢ ∀ (g h : P ⟶ W), inl ≫ g = inl ≫ h → g = h
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
a : A
s : ↥S
⊢ 1 • 1 • ((a, s).1 * (0, 1).1) = 1 • ((0, 1).2 * (a, s).2) • 0

Tactic:
simp only [mul_zero, smul_zero]

Goal state after:
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
⊢ (x * y) • mk m s = x • y • mk m s

Tactic:
rw [← IsLocalization.mk'_sec (M := S) T x, ← IsLocalization.mk'_sec (M := S) T y]

Goal state after:
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
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case refine_4
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x✝ : FreeCommRing α
hx : x✝.IsSupported s
x y : FreeCommRing α
q : ℤ
hq : (lift fun a ↦ if a ∈ s then 0 else X) x = ↑q
r : ℤ
hr : (lift fun a ↦ if a ∈ s then 0 else X) y = ↑r
⊢ ∃ n, (lift fun a ↦ if a ∈ s then 0 else X) (x + y) = ↑n

Tactic:
refine ⟨q + r, ?_⟩

Goal state after:
case refine_4
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x✝ : FreeCommRing α
hx : x✝.IsSupported s
x y : FreeCommRing α
q : ℤ
hq : (lift fun a ↦ if a ∈ s then 0 else X) x = ↑q
r : ℤ
hr : (lift fun a ↦ if a ∈ s then 0 else X) y = ↑r
⊢ (lift fun a ↦ if a ∈ s then 0 else X) (x + y) = ↑(q + r)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Quiver.IsThin C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
inst✝¹ : Quiver.IsThin D
F : C ⥤ D
inst✝ : PreservesColimitsOfShape (Discrete WalkingPair) F
⊢ PreservesColimitsOfShape WalkingSpan F

Tactic:
by
  refine preservesColimitsOfShape_walkingCospan_of_forall_isPushout fun X Y Z f g hfg ↦ ?_
  use pushout f g, pushout.inl f g, pushout.inr f g, .of_hasPushout f g
  rw [isPushout_iff_isColimit_binaryCofan_of_isThin]
  refine ⟨(BinaryCofan.mk (pushout.inl f g) (pushout.inr f g)).isColimitMapConeEquiv ?_⟩
  apply isColimitOfPreserves _ (Nonempty.some ?_)
  rw [← CategoryTheory.isPushout_iff_isColimit_binaryCofan_of_isThin (f := f) (g := g)]
  exact .of_hasPushout f g

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

Goal state before:
pp: case h.h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
⊢ r • mk m s = mk n t ↔ mk m s = Localization.mk 1 ⟨r, hr⟩ • mk n t

Tactic:
rw [smul'_mk, mk_smul_mk, one_smul, mk_eq, mk_eq]

Goal state after:
case h.h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
⊢ (∃ u, u • t • r • m = u • s • n) ↔ ∃ u, u • (⟨r, hr⟩ * t) • m = u • s • n
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
p : LocalizedModule S M
x✝² x✝¹ : M × ↥S
a : M
b : ↥S
a' : M
b' : ↥S
x✝ : (a, b) ≈ (a', b')
c : ↥S
eq1 : c • (a', b').2 • (a, b).1 = c • (a, b).2 • (a', b').1
⊢ s • c • (a', b').2 • (a, b).1 = c • (a, b).2 • s • (a', b').1

Tactic:
eq1,

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
p : LocalizedModule S M
x✝² x✝¹ : M × ↥S
a : M
b : ↥S
a' : M
b' : ↥S
x✝ : (a, b) ≈ (a', b')
c : ↥S
eq1 : c • (a', b').2 • (a, b).1 = c • (a, b).2 • (a', b').1
⊢ s • c • (a, b).2 • (a', b').1 = c • (a, b).2 • s • (a', b').1
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
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
⊢ (divBy s) (((algebraMap R (End R (LocalizedModule S M))) ↑s) (mk m t)) = mk m t

Tactic:
Module.algebraMap_end_apply,

Goal state after:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
⊢ (divBy s) (↑s • mk m t) = mk m t
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
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
⊢ ((algebraMap R (End R (LocalizedModule S M))) ↑s) ((mk m t).liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯) = mk m t

Tactic:
Module.algebraMap_end_apply,

Goal state after:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
⊢ ↑s • (mk m t).liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯ = mk m t
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_6
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
S T : Submonoid R
h : S ≤ T
h' : ∀ (x : ↥T), ∃ m, m * ↑x ∈ S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule S f
y : N
⊢ ∃ x, x.2 • y = f x.1

Tactic:
obtain ⟨⟨x, t⟩, e⟩ := IsLocalizedModule.surj S f y
    exact ⟨⟨x, ⟨t, h t.2⟩⟩, e⟩

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''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
⊢ lift S f g h ∘ₗ f = g

Tactic:
by
  dsimp only [IsLocalizedModule.lift]
  rw [LinearMap.comp_assoc, iso_symm_comp, LocalizedModule.lift_comp S g h]

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
⊢ ↑s • mk' f m s = f m

Tactic:
← mk'_smul,

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
⊢ mk' f (↑s • m) s = 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_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₂) = (↑s₁ • mk' f 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₁ • ↑s₂ • mk' f 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
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
m' : M'
⊢ ↑s • mk' f m s = s • m' ↔ f m = s • m'

Tactic:
← mk'_smul,

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
m' : M'
⊢ mk' f (↑s • m) s = s • m' ↔ f m = s • m'
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
L : A ⥤ T
R : B ⥤ T
F✝ F : J ⥤ Comma L R
c : Cocone F
inst✝ : PreservesColimit (F ⋙ fst L R) L
h₁ : IsColimit ((fst L R).mapCocone c)
h₂ : IsColimit ((snd L R).mapCocone c)
s : Cocone F
j : J
⊢ (L.mapCocone ((fst L R).mapCocone c)).ι.app j ≫ L.map (h₁.desc ((fst L R).mapCocone s)) ≫ s.pt.hom =
    (L.mapCocone ((fst L R).mapCocone c)).ι.app j ≫ c.pt.hom ≫ R.map (h₂.desc ((snd L R).mapCocone s))

Tactic:
simp [← Functor.map_comp_assoc, ← Functor.map_comp,
          dsimp% h₁.fac ((fst _ _).mapCocone s) j,
          dsimp% h₂.fac ((snd _ _).mapCocone s) j]

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

Goal state before:
pp: case h
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst✝⁹ : AddCommMonoid M₀
inst✝⁸ : AddCommMonoid M₀'
inst✝⁷ : Module R M₀
inst✝⁶ : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst✝⁵ : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_8
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁
inst✝¹ : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst✝ : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
m : M₀
s : ↥S
⊢ ((algebraMap R (End R M₁')) ↑s) (((map S f₀ f₁) g ∘ₗ ↑(iso S f₀)) (LocalizedModule.mk m s)) =
    ((algebraMap R (End R M₁')) ↑s)
      ((↑(iso S f₁) ∘ₗ (map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m s))

Tactic:
Module.algebraMap_end_apply,

Goal state after:
case h
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst✝⁹ : AddCommMonoid M₀
inst✝⁸ : AddCommMonoid M₀'
inst✝⁷ : Module R M₀
inst✝⁶ : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst✝⁵ : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_8
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁
inst✝¹ : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst✝ : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
m : M₀
s : ↥S
⊢ ↑s • ((map S f₀ f₁) g ∘ₗ ↑(iso S f₀)) (LocalizedModule.mk m s) =
    ((algebraMap R (End R M₁')) ↑s)
      ((↑(iso S f₁) ∘ₗ (map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m s))