mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
inst✝¹¹ : MonoidalCategory C
D : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} D
inst✝⁹ : MonoidalCategory D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
inst✝⁷ : MonoidalCategory E
C' : Type u₁'
inst✝⁶ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝⁵ : F.OplaxMonoidal
inst✝⁴ : G.LaxMonoidal
inst✝³ : adj.IsMonoidal
F' : D ⥤ E
G' : E ⥤ D
adj' : F' ⊣ G'
inst✝² : F'.OplaxMonoidal
inst✝¹ : G'.LaxMonoidal
inst✝ : adj'.IsMonoidal
⊢ ε (G' ⋙ G) = (adj.comp adj').unit.app (𝟙_ C) ≫ (G' ⋙ G).map (η (F ⋙ F'))

Tactic:
by
    simp [IsMonoidal.leftAdjoint_ε (adj := adj'), IsMonoidal.leftAdjoint_ε (adj := adj),
      ← map_comp, ← adj'.unit_naturality_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
⊢ (forget C).PreservesMonomorphisms → MorphismProperty.injective C = monomorphisms C

Tactic:
· intro
    apply le_antisymm (injective_le_monomorphisms C)
    intro _ _ f hf
    have : Mono f := hf
    change Function.Injective ((forget C).map f)
    rw [← mono_iff_injective]
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
⊢ (α_ (F.obj X✝) (F.obj Y✝) (F.obj Z✝)).hom ≫
      F.obj X✝ ◁ μ F Y✝ Z✝ ≫ μ F X✝ (Y✝ ⊗ Z✝) ≫ F.map (β X✝ (Y✝ ⊗ Z✝)).hom ≫ F.map (α_ Y✝ Z✝ X✝).hom =
    (β_ (F.obj X✝) (F.obj Y✝)).hom ▷ F.obj Z✝ ≫
      (α_ (F.obj Y✝) (F.obj X✝) (F.obj Z✝)).hom ≫
        F.obj Y✝ ◁ μ F X✝ Z✝ ≫ F.obj Y✝ ◁ F.map (β X✝ Z✝).hom ≫ μ F Y✝ (Z✝ ⊗ X✝)

Tactic:
←
      whiskerLeft_comp_assoc,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
⊢ (α_ (F.obj X✝) (F.obj Y✝) (F.obj Z✝)).hom ≫
      F.obj X✝ ◁ μ F Y✝ Z✝ ≫ μ F X✝ (Y✝ ⊗ Z✝) ≫ F.map (β X✝ (Y✝ ⊗ Z✝)).hom ≫ F.map (α_ Y✝ Z✝ X✝).hom =
    (β_ (F.obj X✝) (F.obj Y✝)).hom ▷ F.obj Z✝ ≫
      (α_ (F.obj Y✝) (F.obj X✝) (F.obj Z✝)).hom ≫ F.obj Y✝ ◁ (μ F X✝ Z✝ ≫ F.map (β X✝ Z✝).hom) ≫ μ F Y✝ (Z✝ ⊗ X✝)
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ : RingCon M
f : M →+* P
c d : RingCon M
h : c ≤ d
x y : (ker (c.map d h)).Quotient
w z : c.Quotient
a b : M
⊢ (c.quotientQuotientEquivQuotient d.toSetoid h).toFun (↑↑a * ↑↑b) = d.mk' a * d.mk' b

Tactic:
rw [← d.mk'.map_mul]

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ : RingCon M
f : M →+* P
c d : RingCon M
h : c ≤ d
x y : (ker (c.map d h)).Quotient
w z : c.Quotient
a b : M
⊢ (c.quotientQuotientEquivQuotient d.toSetoid h).toFun (↑↑a * ↑↑b) = d.mk' (a * b)
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
R : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Semiring N
inst✝² : Algebra R N
inst✝¹ : Semiring P
inst✝ : Algebra R P
c✝ d✝ : RingCon M
f : M →ₐ[R] P
c d : RingCon M
h : c ≤ d
x✝ : R
⊢ (c.quotientQuotientEquivQuotient d h).toFun ((algebraMap R (ker ↑(factorₐ R h)).Quotient) x✝) =
    (algebraMap R d.Quotient) x✝

Tactic:
by rfl

Goal state after:
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : TensorAlgebra R M → Prop
algebraMap : ∀ (r : R), C ((Algebra.algebraMap R (TensorAlgebra R M)) r)
ι : ∀ (x : M), C ((TensorAlgebra.ι R) x)
mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
s : Subalgebra R (TensorAlgebra R M) :=
  { carrier := {a | C a}, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯,
    algebraMap_mem' := algebraMap }
of : M →ₗ[R] ↥s := LinearMap.codRestrict (Subalgebra.toSubmodule s) (TensorAlgebra.ι R) ι
of_apply : ∀ {x : M}, ↑(of x) = (TensorAlgebra.ι R) x
of_id : AlgHom.id R (TensorAlgebra R M) = s.val.comp ((lift R) of)
⊢ C ((s.val.comp ((lift R) of)) a)

Tactic:
exact Subtype.prop (lift R of a)

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

Goal state before:
pp: R : Type u₁
inst✝ : Ring R
f : R →+* R
hf : f = RingHom.id R
M : ModuleCat R
⊢ ↑((restrictScalars f).obj M) ≃+ ↑M

Tactic:
by rfl

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

Goal state before:
pp: R₁ : Type u₁
R₂ : Type u₂
R₃ : Type u₃
inst✝² : Ring R₁
inst✝¹ : Ring R₂
inst✝ : Ring R₃
f : R₁ →+* R₂
g : R₂ →+* R₃
gf : R₁ →+* R₃
hgf : gf = g.comp f
M : ModuleCat R₃
⊢ ↑((restrictScalars gf).obj M) ≃+ ↑((restrictScalars f).obj ((restrictScalars g).obj M))

Tactic:
by rfl

Goal state after:
Module: Mathlib.Order.Category.BddLat

Goal state before:
pp: X : Lat
x✝ : BddLat
f : latToBddLat.obj X ⟶ x✝
a b : ↑X
⊢ (some ∘ some) (a ⊔ b) = (some ∘ some) a ⊔ (some ∘ some) b

Tactic:
by rfl

Goal state after:
Module: Mathlib.Order.Category.BddLat

Goal state before:
pp: X : Lat
x✝ : BddLat
f : latToBddLat.obj X ⟶ x✝
a b : ↑X
⊢ (some ∘ some) (a ⊓ b) = (some ∘ some) a ⊓ (some ∘ some) b

Tactic:
by rfl

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Comon C
⊢ Δ.op ▷ op A.X ≫ Δ.op = (α_ (op A.X) (op A.X) (op A.X)).hom ≫ op A.X ◁ Δ.op ≫ Δ.op

Tactic:
rw [← op_inv_associator, ← op_whiskerRight, ← op_comp, ← op_whiskerLeft, ← op_comp,
      comul_assoc_flip, op_comp, op_comp_assoc]
    rfl

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X✝ Y✝ : CoalgCat R
x✝ : X✝ ⟶ Y✝
⊢ (𝟭 (CoalgCat R)).map x✝ ≫ (Iso.refl ((𝟭 (CoalgCat R)).obj Y✝)).hom =
    (Iso.refl ((𝟭 (CoalgCat R)).obj X✝)).hom ≫ (toComon R ⋙ ofComon R).map x✝

Tactic:
by rfl

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X✝ Y✝ : Comon (ModuleCat R)
x✝ : X✝ ⟶ Y✝
⊢ (ofComon R ⋙ toComon R).map x✝ ≫ (Iso.refl ((ofComon R ⋙ toComon R).obj Y✝)).hom =
    (Iso.refl ((ofComon R ⋙ toComon R).obj X✝)).hom ≫ (𝟭 (Comon (ModuleCat R))).map x✝

Tactic:
by rfl

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
x : R
inst✝ : Away x S
⊢ (algebraMap R S) x * invSelf x = 1

Tactic:
by
  convert! IsLocalization.mk'_mul_mk'_eq_one (M := Submonoid.powers x) (S := S) _ 1
  symm
  apply IsLocalization.mk'_one

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
P : Type u_3
inst✝⁴ : CommSemiring P
Q : Type u_4
inst✝³ : CommSemiring Q
inst✝² : Algebra P Q
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
H : ∀ (a : P), ∃ b m, f b = f r ^ m * a
a : P
n : ℕ
b : R
m : ℕ
e : f b = f r ^ m * a
⊢ f (r ^ (0 + n) * b) = f r ^ (0 + (n + m)) * a

Tactic:
simp [e, pow_add]; ring_nf

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsLocalRing R
a b : R
h : IsUnit (a + b)
⊢ IsUnit a ∨ IsUnit b

Tactic:
by
  rcases h with ⟨u, hu⟩
  rw [← Units.inv_mul_eq_one, mul_add] at hu
  apply Or.imp _ _ (isUnit_or_isUnit_of_add_one hu) <;> exact (u⁻¹.isUnit_units_mul _).mp

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
K : Type u_3
inst✝ : Field K
a : K
h : a = 0
⊢ IsUnit (1 - a)

Tactic:
rw [h, sub_zero]; exact isUnit_one

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case mp
R : Type u
inst✝ : Ring R
I : Ideal R
h : I.jacobson = I
x : R
hx : ∃ I_1 ∈ {J | I ≤ J ∧ J.IsMaximal}, x ∉ I_1
⊢ ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M

Tactic:
exact hx

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)
a b : ↑↑s
⊢ (algebraMap R (Away (↑a * ↑b))) (r a * ↑b ^ N) = (algebraMap R (Away (↑a * ↑b))) (r b * ↑a ^ N)

Tactic:
simp_rw [map_mul, ← Away.awayToAwayRight_eq (S := Away a.1) a.1 b (r a),
        ← Away.awayToAwayLeft_eq (S := Away b.1) b.1 a (r b), ← eq, map_mul,
        Away.awayToAwayRight_eq, Away.awayToAwayLeft_eq, h, mul_assoc, ← map_mul, mul_comm]

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
M N P : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj P
⊢ tensorμ (M ⊗ N) P (M ⊗ N) P ≫ (tensorμ M N M N ⊗ₘ 𝟙 (P ⊗ P)) ≫ (α_ (M ⊗ M) (N ⊗ N) (P ⊗ P)).hom ≫ (μ ⊗ₘ μ ⊗ₘ μ) =
    ((α_ M N P).hom ⊗ₘ (α_ M N P).hom) ≫ tensorμ M (N ⊗ P) M (N ⊗ P) ≫ (μ ⊗ₘ tensorμ N P N P ≫ (μ ⊗ₘ μ))

Tactic:
slice_rhs 3 4 => rw [← Category.id_comp μ, ← tensorHom_comp_tensorHom]

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
M N P : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj P
⊢ tensorμ (M ⊗ N) P (M ⊗ N) P ≫ (tensorμ M N M N ⊗ₘ 𝟙 (P ⊗ P)) ≫ (α_ (M ⊗ M) (N ⊗ N) (P ⊗ P)).hom ≫ (μ ⊗ₘ μ ⊗ₘ μ) =
    ((α_ M N P).hom ⊗ₘ (α_ M N P).hom) ≫ tensorμ M (N ⊗ P) M (N ⊗ P) ≫ (𝟙 (M ⊗ M) ⊗ₘ tensorμ N P N P) ≫ (μ ⊗ₘ μ ⊗ₘ μ)
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 : Cocone F
X : C
hX : IsInitial X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc : IsColimit (PushoutCocone.mk (c.ι.app { as := WalkingPair.left }) (c.ι.app { as := WalkingPair.right }) ⋯)
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), c.ι.app j ≫ m = s.ι.app j
⊢ m = hc.desc (PushoutCocone.mk (s.ι.app { as := WalkingPair.left }) (s.ι.app { as := WalkingPair.right }) ⋯)

Tactic:
let c' :=
      PushoutCocone.mk (c.ι.app ⟨WalkingPair.left⟩ ≫ m) (c.ι.app ⟨WalkingPair.right⟩ ≫ m)
        (hX.hom_ext (f ≫ _) (g ≫ _))

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cocone F
X : C
hX : IsInitial X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc : IsColimit (PushoutCocone.mk (c.ι.app { as := WalkingPair.left }) (c.ι.app { as := WalkingPair.right }) ⋯)
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), c.ι.app j ≫ m = s.ι.app j
c' : PushoutCocone f g :=
  PushoutCocone.mk (c.ι.app { as := WalkingPair.left } ≫ m) (c.ι.app { as := WalkingPair.right } ≫ m) ⋯
⊢ m = hc.desc (PushoutCocone.mk (s.ι.app { as := WalkingPair.left }) (s.ι.app { as := WalkingPair.right }) ⋯)
Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts

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

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

Tactic:
· exact h₁.trans (H₂.fac (BinaryCofan.mk s.inl s.inr) ⟨WalkingPair.left⟩).symm

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
i : Z ⟶ S
Pfg : C
fstfg : Pfg ⟶ X
sndfg : Pfg ⟶ Y
hfg : IsPullback fstfg sndfg f g
Pfi : C
fstfi : Pfi ⟶ X
sndfi : Pfi ⟶ Z
hfi : IsPullback fstfi sndfi f i
R : C
rY : R ⟶ Y
rZ : R ⟶ Z
hrw : rY ≫ g = rZ ≫ i
Psndfgr : C
fstsndfgr : Psndfgr ⟶ Pfg
sndsndfgr : Psndfgr ⟶ R
hsndfgr : IsPullback fstsndfgr sndsndfgr sndfg rY
t : Psndfgr ⟶ Pfi
ht₁ : t ≫ fstfi = fstsndfgr ≫ fstfg
ht₂ : t ≫ sndfi = sndsndfgr ≫ rZ
⊢ IsPullback t sndsndfgr sndfi rZ

Tactic:
refine .of_right ?_ ht₂ hfi
  rw [← hrw, ht₁]
  exact .paste_horiz hsndfgr hfg

Goal state after:
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 : IsIso g
⊢ IsIso inl

Tactic:
have := h.hasPushout

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 : IsIso g
this : HasPushout f g
⊢ IsIso inl
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

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

Tactic:
rw [← Category.assoc]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
g' : Z ⟶ W
inst✝¹ : HasPushout f g
inst✝ : HasPushout (pushout.inr f g) g'
⊢ (pushout.inl f g ≫ pushout.inl (pushout.inr f g) g') ≫ (pushoutLeftPushoutInrIso f g g').hom = pushout.inl f (g ≫ g')
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

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

Tactic:
rw [← Category.assoc]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
f' : Y ⟶ W
inst✝¹ : HasPushout f g
inst✝ : HasPushout f' (pushout.inl f g)
⊢ (pushout.inr f g ≫ pushout.inr f' (pushout.inl f g)) ≫ (pushoutRightPushoutInlIso f g f').hom = pushout.inr (f ≫ f') g
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hxs : x.IsSupported s
⊢ (map Subtype.val) ((restriction s) x) = x

Tactic:
refine Subring.InClosure.recOn hxs ?_ ?_ ?_ ?_

Goal state after:
case refine_1
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hxs : x.IsSupported s
⊢ (map Subtype.val) ((restriction s) 1) = 1

case refine_2
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hxs : x.IsSupported s
⊢ (map Subtype.val) ((restriction s) (-1)) = -1

case refine_3
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hxs : x.IsSupported s
⊢ ∀ z ∈ of '' s,
    ∀ (n : FreeCommRing α),
      (map Subtype.val) ((restriction s) n) = n → (map Subtype.val) ((restriction s) (z * n)) = z * n

case refine_4
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hxs : x.IsSupported s
⊢ ∀ {x y : FreeCommRing α},
    (map Subtype.val) ((restriction s) x) = x →
      (map Subtype.val) ((restriction s) y) = y → (map Subtype.val) ((restriction s) (x + y)) = x + y
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
r : R
hr : r ∈ S
y : LocalizedModule S M
m : M
s : ↥S
⊢ r • mk m s = y ↔ mk m s = Localization.mk 1 ⟨r, hr⟩ • y

Tactic:
| h m s =>

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Under.Basic

Goal state before:
pp: R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f : A ⟶ B
⊢ Under.Hom.right
      ((tensorProdObjIsoPushoutObj S A).inv ≫ (R.tensorProd S).map f ≫ (tensorProdObjIsoPushoutObj S B).hom) =
    Under.Hom.right
      ((tensorProdObjIsoPushoutObj S A).inv ≫
        (tensorProdObjIsoPushoutObj S A).hom ≫
          Under.homMk
            (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap ↑R ↑S)))
              (pushout.inr B.hom (ofHom (algebraMap ↑R ↑S))) ⋯)
            ⋯)

Tactic:
apply pushout.hom_ext

Goal state after:
case h₀
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f : A ⟶ B
⊢ pushout.inl A.hom (ofHom (algebraMap ↑R ↑S)) ≫
      Under.Hom.right
        ((tensorProdObjIsoPushoutObj S A).inv ≫ (R.tensorProd S).map f ≫ (tensorProdObjIsoPushoutObj S B).hom) =
    pushout.inl A.hom (ofHom (algebraMap ↑R ↑S)) ≫
      Under.Hom.right
        ((tensorProdObjIsoPushoutObj S A).inv ≫
          (tensorProdObjIsoPushoutObj S A).hom ≫
            Under.homMk
              (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap ↑R ↑S)))
                (pushout.inr B.hom (ofHom (algebraMap ↑R ↑S))) ⋯)
              ⋯)

case h₁
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f : A ⟶ B
⊢ pushout.inr A.hom (ofHom (algebraMap ↑R ↑S)) ≫
      Under.Hom.right
        ((tensorProdObjIsoPushoutObj S A).inv ≫ (R.tensorProd S).map f ≫ (tensorProdObjIsoPushoutObj S B).hom) =
    pushout.inr A.hom (ofHom (algebraMap ↑R ↑S)) ≫
      Under.Hom.right
        ((tensorProdObjIsoPushoutObj S A).inv ≫
          (tensorProdObjIsoPushoutObj S A).hom ≫
            Under.homMk
              (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap ↑R ↑S)))
                (pushout.inr B.hom (ofHom (algebraMap ↑R ↑S))) ⋯)
              ⋯)
Module: Mathlib.CategoryTheory.Limits.Comma

Goal state before:
pp: case h₁
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 : J ⥤ Comma L R
inst✝ : PreservesLimit (F ⋙ snd L R) R
c₁ : Cone (F ⋙ fst L R)
c₂ : Cone (F ⋙ snd L R)
t₂ : IsLimit c₂
j₁ j₂ : J
t : j₁ ⟶ j₂
⊢ (((const J).obj
              { left := c₁.pt, right := c₂.pt, hom := (isLimitOfPreserves R t₂).lift (limitAuxiliaryCone F c₁) }).map
          t ≫
        { left := c₁.π.app j₂, right := c₂.π.app j₂, w := ⋯ }).left =
    ({ left := c₁.π.app j₁, right := c₂.π.app j₁, w := ⋯ } ≫ F.map t).left

pp: case h₂
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 : J ⥤ Comma L R
inst✝ : PreservesLimit (F ⋙ snd L R) R
c₁ : Cone (F ⋙ fst L R)
c₂ : Cone (F ⋙ snd L R)
t₂ : IsLimit c₂
j₁ j₂ : J
t : j₁ ⟶ j₂
⊢ (((const J).obj
              { left := c₁.pt, right := c₂.pt, hom := (isLimitOfPreserves R t₂).lift (limitAuxiliaryCone F c₁) }).map
          t ≫
        { left := c₁.π.app j₂, right := c₂.π.app j₂, w := ⋯ }).right =
    ({ left := c₁.π.app j₁, right := c₂.π.app j₁, w := ⋯ } ≫ F.map t).right

Tactic:
· simp [← c₁.w t]

Goal state after:
case h₂
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 : J ⥤ Comma L R
inst✝ : PreservesLimit (F ⋙ snd L R) R
c₁ : Cone (F ⋙ fst L R)
c₂ : Cone (F ⋙ snd L R)
t₂ : IsLimit c₂
j₁ j₂ : J
t : j₁ ⟶ j₂
⊢ (((const J).obj
              { left := c₁.pt, right := c₂.pt, hom := (isLimitOfPreserves R t₂).lift (limitAuxiliaryCone F c₁) }).map
          t ≫
        { left := c₁.π.app j₂, right := c₂.π.app j₂, w := ⋯ }).right =
    ({ left := c₁.π.app j₁, right := c₂.π.app j₁, w := ⋯ } ≫ F.map t).right
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: A B : CommRingCat
s : BinaryCofan A B
m : ↑A ⊗[ℤ] ↑B →+* ↑s.pt
hm : ∀ (j : Discrete WalkingPair), (A.coproductCocone B).ι.app j ≫ { hom' := m } = s.ι.app j
⊢ { hom' := m }.hom.toIntAlgHom =
    (Hom.hom
        (ofHom
          (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯).toRingHom)).toIntAlgHom

Tactic:
apply Algebra.TensorProduct.liftEquiv.symm.injective

Goal state after:
A B : CommRingCat
s : BinaryCofan A B
m : ↑A ⊗[ℤ] ↑B →+* ↑s.pt
hm : ∀ (j : Discrete WalkingPair), (A.coproductCocone B).ι.app j ≫ { hom' := m } = s.ι.app j
⊢ Algebra.TensorProduct.liftEquiv.symm { hom' := m }.hom.toIntAlgHom =
    Algebra.TensorProduct.liftEquiv.symm
      (Hom.hom
          (ofHom
            (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom
                ⋯).toRingHom)).toIntAlgHom