mathlib-initiative/mathlib-tactics huggingface dataset:
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)) =
    1 ⊗ₜ[R₃] (1 ⊗ₜ[R₂] (1 ⊗ₜ[R₁] m))

Tactic:
ExtendScalars.map_tmul,

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)
⊢ 1 ⊗ₜ[R₃] (ConcreteCategory.hom ((extendScalarsComp f₁₂ f₂₃).hom.app M)) (1 ⊗ₜ[R₁] m) =
    1 ⊗ₜ[R₃] (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)).comp
            (comulAlgHom R (A ⊗[R] B))).comp
        Algebra.TensorProduct.includeLeft)
      a =
    (((comulAlgHom R (B ⊗[R] A)).comp ↑(Algebra.TensorProduct.comm R A B)).comp Algebra.TensorProduct.includeLeft) a

Tactic:
dsimp
      rw [← (ℛ R a).eq]
      simp [TensorProduct.tmul_sum, TensorProduct.sum_tmul, Algebra.TensorProduct.one_def]

Goal state after:
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
⊢ ((AlgHom.restrictScalars R
            ((Algebra.TensorProduct.map ↑(Algebra.TensorProduct.comm R A B) ↑(Algebra.TensorProduct.comm R A B)).comp
              (comulAlgHom R (A ⊗[R] B)))).comp
        Algebra.TensorProduct.includeRight)
      a =
    ((AlgHom.restrictScalars R ((comulAlgHom R (B ⊗[R] A)).comp ↑(Algebra.TensorProduct.comm R A B))).comp
        Algebra.TensorProduct.includeRight)
      a

Tactic:
dsimp
      rw [← (ℛ R a).eq]
      simp [TensorProduct.tmul_sum, TensorProduct.sum_tmul, Algebra.TensorProduct.one_def]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
M' : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] R
g : N →ₗ[R] M'
⊢ λ ∘ₗ f ⊗ₘ g = g ∘ₗ λ ∘ₗ f ⊗ₘ LinearMap.id

Tactic:
by
  ext; simp

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
M' : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
g : N →ₗ[R] R
⊢ ρ ∘ₗ f ⊗ₘ g = f ∘ₗ ρ ∘ₗ LinearMap.id ⊗ₘ g

Tactic:
by
  ext; simp

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
A : Type u_5
inst✝¹³ : CommSemiring A
inst✝¹² : Algebra R A
B : Type u_6
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : Algebra R B
Aₚ : Type u_7
inst✝⁹ : CommSemiring Aₚ
inst✝⁸ : Algebra A Aₚ
inst✝⁷ : Algebra R Aₚ
inst✝⁶ : IsScalarTower R A Aₚ
Bₚ : Type u_8
inst✝⁵ : CommSemiring Bₚ
inst✝⁴ : Algebra B Bₚ
inst✝³ : Algebra R Bₚ
inst✝² : IsScalarTower R B Bₚ
f : A →ₐ[R] B
a : A
inst✝¹ : Away a Aₚ
inst✝ : Away (f a) Bₚ
r : R
⊢ ↑↑(IsLocalization.map Bₚ ↑f ⋯) ((algebraMap A Aₚ) ((algebraMap R A) r)) = (algebraMap R Bₚ) r

Tactic:
IsScalarTower.algebraMap_eq R B Bₚ

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
A : Type u_5
inst✝¹³ : CommSemiring A
inst✝¹² : Algebra R A
B : Type u_6
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : Algebra R B
Aₚ : Type u_7
inst✝⁹ : CommSemiring Aₚ
inst✝⁸ : Algebra A Aₚ
inst✝⁷ : Algebra R Aₚ
inst✝⁶ : IsScalarTower R A Aₚ
Bₚ : Type u_8
inst✝⁵ : CommSemiring Bₚ
inst✝⁴ : Algebra B Bₚ
inst✝³ : Algebra R Bₚ
inst✝² : IsScalarTower R B Bₚ
f : A →ₐ[R] B
a : A
inst✝¹ : Away a Aₚ
inst✝ : Away (f a) Bₚ
r : R
⊢ ↑↑(IsLocalization.map Bₚ ↑f ⋯) ((algebraMap A Aₚ) ((algebraMap R A) r)) = ((algebraMap B Bₚ).comp (algebraMap R B)) r
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z : R
h : z ∈ span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)
⊢ s ∪ s * univ ∪ univ * s ∪ univ * s * univ ⊆ ↑(span s)

Tactic:
simp only [union_subset_iff, union_assoc]

Goal state after:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z : R
h : z ∈ span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)
⊢ s ⊆ ↑(span s) ∧ s * univ ⊆ ↑(span s) ∧ univ * s ⊆ ↑(span s) ∧ univ * s * univ ⊆ ↑(span s)
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case mpr
R : Type u
inst✝ : Ring R
I : Ideal R
⊢ (∃ M, (∀ J ∈ M, J.IsMaximal ∨ J = ⊤) ∧ I = sInf M) → I.jacobson = I

Tactic:
rintro ⟨M, hM, hInf⟩

Goal state after:
case mpr
R : Type u
inst✝ : Ring R
I : Ideal R
M : Set (Ideal R)
hM : ∀ J ∈ M, J.IsMaximal ∨ J = ⊤
hInf : I = sInf M
⊢ I.jacobson = I
Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
K : Type u_3
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
⊢ (maximalIdeal R).IsMaximal

Tactic:
rw [Ideal.isMaximal_iff]
  constructor
  · intro h
    apply h
    exact isUnit_one
  · intro I x _ hx H
    rw [mem_maximalIdeal, mem_nonunits_iff, Classical.not_not] at hx
    rcases hx with ⟨u, rfl⟩
    simpa using I.mul_mem_left (↑u⁻¹) H

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

Goal state before:
pp: case pos
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
n : ℤ
hn : n ≤ 0
hn0 : n = 0
⊢ selfZPow x B n = mk' B 1 (Submonoid.pow x n.natAbs)

Tactic:
simp [hn0, selfZPow_zero, Submonoid.pow_apply]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
⊢ ((∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R Aₛ)) ↑x)) ∧
      (∀ (y : Aₛ), ∃ x, x.2 • y = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x.1) ∧
        ∀ {x₁ x₂ : A},
          (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x₁ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x₂ →
            ∃ c, c • x₁ = c • x₂) ↔
    (∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit ((algebraMap A Aₛ) ↑y)) ∧
      (∀ (z : Aₛ), ∃ x, z * (algebraMap A Aₛ) ↑x.2 = (algebraMap A Aₛ) x.1) ∧
        ∀ {x y : A}, (algebraMap A Aₛ) x = (algebraMap A Aₛ) y → ∃ c, ↑c * x = ↑c * y

Tactic:
refine and_congr ?_ (and_congr (forall_congr' fun _ ↦ ?_) (forall₂_congr fun _ _ ↦ ?_))

Goal state after:
case refine_1
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
⊢ (∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R Aₛ)) ↑x)) ↔
    ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit ((algebraMap A Aₛ) ↑y)

case refine_2
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
x✝ : Aₛ
⊢ (∃ x, x.2 • x✝ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x.1) ↔
    ∃ x, x✝ * (algebraMap A Aₛ) ↑x.2 = (algebraMap A Aₛ) x.1

case refine_3
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
x✝¹ x✝ : A
⊢ ((IsScalarTower.toAlgHom R A Aₛ).toLinearMap x✝¹ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x✝ →
      ∃ c, c • x✝¹ = c • x✝) ↔
    (algebraMap A Aₛ) x✝¹ = (algebraMap A Aₛ) x✝ → ∃ c, ↑c * x✝¹ = ↑c * x✝
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: case inr
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_3
Mₛ : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid Mₛ
inst✝¹ : Module R Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → Mₛ
hf : LinearIndependent R v
h✝ : Nonempty ι
inj : Function.Injective fun r ↦ r • v (Classical.arbitrary ι)
⊢ ∃ w, LinearIndependent R w

Tactic:
choose sec hsec using surj S f

Goal state after:
case inr
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_3
Mₛ : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid Mₛ
inst✝¹ : Module R Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → Mₛ
hf : LinearIndependent R v
h✝ : Nonempty ι
inj : Function.Injective fun r ↦ r • v (Classical.arbitrary ι)
sec : Mₛ → M × ↥S
hsec : ∀ (y : Mₛ), (sec y).2 • y = f (sec y).1
⊢ ∃ w, LinearIndependent R w
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},
    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:
intro m

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
⊢ 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
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},
    (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:
intro m

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
⊢ (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
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit t₁
s : PullbackCone (g₁ ≫ g₂) i₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
⊢ ∀ {m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt},
    m ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst → m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd → m = l₁

Tactic:
intro m

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit t₁
s : PullbackCone (g₁ ≫ g₂) i₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
⊢ m ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst → m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd → m = l₁
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_2.h₁
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
⊢ (prod.lift s.fst (s.snd ≫ prod.snd) ≫ (PullbackCone.mk prod.fst (prod.map f (𝟙 X)) ⋯).snd) ≫ prod.fst =
    s.snd ≫ prod.fst

Tactic:
simp [PullbackCone.condition]

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},
    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:
intro m

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
⊢ 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)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit (t₂.pasteHoriz t₁ hi₂)
s : PullbackCone g₁ i₂
l : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hl : l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hl' : l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ≫ t₂.snd
⊢ ∀ {m : s.pt ⟶ t₁.pt}, m ≫ t₁.fst = s.fst → m ≫ t₁.snd = s.snd → m = l

Tactic:
intro m

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit (t₂.pasteHoriz t₁ hi₂)
s : PullbackCone g₁ i₂
l : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hl : l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hl' : l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ≫ t₂.snd
m : s.pt ⟶ t₁.pt
⊢ m ≫ t₁.fst = s.fst → m ≫ t₁.snd = s.snd → m = l
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
l₂ : t₂.pt ⟶ s.pt
hl₂ : t₂.inl ≫ l₂ = l₁
hl₂' : t₂.inr ≫ l₂ = s.inr
⊢ ∀ {m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt},
    (t₁.pasteHoriz t₂ hi₂).inl ≫ m = s.inl → (t₁.pasteHoriz t₂ hi₂).inr ≫ m = s.inr → m = l₂

Tactic:
intro m

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
l₂ : t₂.pt ⟶ s.pt
hl₂ : t₂.inl ≫ l₂ = l₁
hl₂' : t₂.inr ≫ l₂ = s.inr
m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
⊢ (t₁.pasteHoriz t₂ hi₂).inl ≫ m = s.inl → (t₁.pasteHoriz t₂ hi₂).inr ≫ m = s.inr → m = l₂
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},
    (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:
intro m

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
⊢ (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)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: 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
⊢ m = BinaryCofan.IsColimit.desc hc s.inr s.inl

Tactic:
by apply BinaryCofan.IsColimit.hom_ext hc <;> cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit (t₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl : (t₁.pasteHoriz t₂ hi₂).inl ≫ l = t₁.inl ≫ s.inl
hl' : (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr
⊢ ∀ {m : t₂.pt ⟶ s.pt}, t₂.inl ≫ m = s.inl → t₂.inr ≫ m = s.inr → m = l

Tactic:
intro m

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit (t₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl : (t₁.pasteHoriz t₂ hi₂).inl ≫ l = t₁.inl ≫ s.inl
hl' : (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr
m : t₂.pt ⟶ s.pt
⊢ t₂.inl ≫ m = s.inl → t₂.inr ≫ m = s.inr → m = l
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case fac
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
⊢ ∀ (s : Cofork f f'), (Cofork.ofπ g ⋯).π ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯) = s.π

pp: case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
⊢ ∀ (s : Cofork f f') (m : (Cofork.ofπ g ⋯).pt ⟶ s.pt),
    (Cofork.ofπ g ⋯).π ≫ m = s.π → m = H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)

Tactic:
· exact fun s => H.isColimit.fac _ WalkingSpan.left

Goal state after:
case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
⊢ ∀ (s : Cofork f f') (m : (Cofork.ofπ g ⋯).pt ⟶ s.pt),
    (Cofork.ofπ g ⋯).π ≫ m = s.π → m = H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)
Module: Mathlib.Logic.Equiv.Functor

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

Tactic:
ext x
  simp only [mapEquiv_apply, refl_apply]
  exact LawfulFunctor.id_map x

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : Z ⟶ X
g : Z ⟶ Y
X' : C
i : X ⟶ X'
inst✝ : IsIso i
h : HasPushout (f ≫ i) g
⊢ HasPushout f g

Tactic:
rw [← Category.comp_id f, ← IsIso.hom_inv_id i, ← Category.assoc]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : Z ⟶ X
g : Z ⟶ Y
X' : C
i : X ⟶ X'
inst✝ : IsIso i
h : HasPushout (f ≫ i) g
⊢ HasPushout ((f ≫ i) ≫ inv i) g
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
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
r : R
a : A
s : ↥S
⊢ r • mk a s = mk ((algebraMap R A) r) 1 * mk a s

Tactic:
rw [mk_mul_mk, smul'_mk, Algebra.smul_def, one_mul]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: R S Rₘ Sₘ : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing Rₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : CommRing S
inst✝³ : CommRing Sₘ
inst✝² : Algebra S Sₘ
f : R →+* S
fₘ : Rₘ →+* Sₘ
H : fₘ.comp (algebraMap R Rₘ) = (algebraMap S Sₘ).comp f
M : Submonoid R
inst✝¹ : IsLocalization M Rₘ
inst✝ : IsLocalization (Submonoid.map f M) Sₘ
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra Rₘ Sₘ := fₘ.toAlgebra
algInst✝ : Algebra R Sₘ := (fₘ.comp (algebraMap R Rₘ)).toAlgebra
scalarTowerInst✝ : IsScalarTower R Rₘ Sₘ := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R Sₘ))
⊢ IsPushout (ofHom f) (ofHom (algebraMap R Rₘ)) (ofHom (algebraMap S Sₘ)) (ofHom fₘ)

Tactic:
have : IsScalarTower R S Sₘ := .of_algebraMap_eq' H

Goal state after:
R S Rₘ Sₘ : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing Rₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : CommRing S
inst✝³ : CommRing Sₘ
inst✝² : Algebra S Sₘ
f : R →+* S
fₘ : Rₘ →+* Sₘ
H : fₘ.comp (algebraMap R Rₘ) = (algebraMap S Sₘ).comp f
M : Submonoid R
inst✝¹ : IsLocalization M Rₘ
inst✝ : IsLocalization (Submonoid.map f M) Sₘ
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra Rₘ Sₘ := fₘ.toAlgebra
algInst✝ : Algebra R Sₘ := (fₘ.comp (algebraMap R Rₘ)).toAlgebra
scalarTowerInst✝ : IsScalarTower R Rₘ Sₘ := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R Sₘ))
this : IsScalarTower R S Sₘ
⊢ IsPushout (ofHom f) (ofHom (algebraMap R Rₘ)) (ofHom (algebraMap S Sₘ)) (ofHom fₘ)