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

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
A : Type u_3
B : Type u_4
inst✝²⁷ : CommSemiring R✝
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : AddCommMonoid A
inst✝²⁴ : AddCommMonoid B
inst✝²³ : Algebra R✝ S✝
inst✝²² : Module R✝ A
inst✝²¹ : Module S✝ A
inst✝²⁰ : Module R✝ B
inst✝¹⁹ : IsScalarTower R✝ S✝ A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : AddCommMonoid P
inst✝¹² : AddCommMonoid Q
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module R P
inst✝⁸ : Module R Q
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower R S M
inst✝⁵ : Coalgebra S M
inst✝⁴ : Module S N
inst✝³ : IsScalarTower R S N
inst✝² : Coalgebra S N
inst✝¹ : Coalgebra R P
inst✝ : Coalgebra R Q
⊢ _root_.TensorProduct.map ↑(AlgebraTensorModule.rid R S M) ↑(AlgebraTensorModule.rid R S M) ∘ₗ comul =
    comul ∘ₗ ↑(AlgebraTensorModule.rid R S M)

Tactic:
ext x

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
A : Type u_3
B : Type u_4
inst✝²⁷ : CommSemiring R✝
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : AddCommMonoid A
inst✝²⁴ : AddCommMonoid B
inst✝²³ : Algebra R✝ S✝
inst✝²² : Module R✝ A
inst✝²¹ : Module S✝ A
inst✝²⁰ : Module R✝ B
inst✝¹⁹ : IsScalarTower R✝ S✝ A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : AddCommMonoid P
inst✝¹² : AddCommMonoid Q
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module R P
inst✝⁸ : Module R Q
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower R S M
inst✝⁵ : Coalgebra S M
inst✝⁴ : Module S N
inst✝³ : IsScalarTower R S N
inst✝² : Coalgebra S N
inst✝¹ : Coalgebra R P
inst✝ : Coalgebra R Q
x : M
⊢ ((AlgebraTensorModule.curry
          (_root_.TensorProduct.map ↑(AlgebraTensorModule.rid R S M) ↑(AlgebraTensorModule.rid R S M) ∘ₗ comul))
        x)
      1 =
    ((AlgebraTensorModule.curry (comul ∘ₗ ↑(AlgebraTensorModule.rid R S M))) x) 1
Module: Mathlib.CategoryTheory.Adjunction.Unique

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
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
⊢ adj1.unit ≫ whiskerRight (adj1.leftAdjointUniq adj2).hom G = adj2.unit

Tactic:
ext x

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
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ (adj1.unit ≫ whiskerRight (adj1.leftAdjointUniq adj2).hom G).app x = adj2.unit.app x
Module: Mathlib.CategoryTheory.Adjunction.Unique

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
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
⊢ G.whiskerLeft (adj1.leftAdjointUniq adj2).hom ≫ adj2.counit = adj1.counit

Tactic:
ext x

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
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ (G.whiskerLeft (adj1.leftAdjointUniq adj2).hom ≫ adj2.counit).app x = adj1.counit.app x
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a ⊔ a ⊓ b = a

Tactic:
by
  dsimp only [(· ⊔ ·), (· ⊓ ·)]
  rw [← mul_assoc, mul_self, add_assoc, add_self, add_zero]

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

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
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
⊢ adj1.unit.app x ≫ adj2.unit.app (G.obj (F.obj x)) ≫ G'.map (adj1.counit.app (F.obj x)) = adj2.unit.app x

Tactic:
rw [← adj2.unit_naturality_assoc, ← G'.map_comp]

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
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
⊢ adj2.unit.app x ≫ G'.map (F.map (adj1.unit.app x) ≫ adj1.counit.app (F.obj x)) = adj2.unit.app x
Module: Mathlib.CategoryTheory.Adjunction.Unique

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
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
⊢ adj1.unit ≫ F.whiskerLeft (adj1.rightAdjointUniq adj2).hom = adj2.unit

Tactic:
ext x

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
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
⊢ (adj1.unit ≫ F.whiskerLeft (adj1.rightAdjointUniq adj2).hom).app x = adj2.unit.app x
Module: Mathlib.CategoryTheory.Category.Pointed

Goal state before:
pp: X Y Z : Pointed
f : X.Hom Y
g : Y.Hom Z
⊢ g.toFun Y.point = Z.point

Tactic:
g.map_point

Goal state after:
X Y Z : Pointed
f : X.Hom Y
g : Y.Hom Z
⊢ Z.point = Z.point
Module: Mathlib.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Bialgebra S A
inst✝² : Algebra R A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
⊢ (TensorProduct.rid R S A).toAlgEquiv = Algebra.TensorProduct.rid R S A

Tactic:
ext x

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Bialgebra S A
inst✝² : Algebra R A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
x : A ⊗[R] R
⊢ (TensorProduct.rid R S A).toAlgEquiv x = (Algebra.TensorProduct.rid R S A) x
Module: Mathlib.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Bialgebra R B
inst✝ : Algebra R A
⊢ (↑(comulAlgHom A (A ⊗[R] B))).comp ↑Algebra.TensorProduct.includeRight =
    (Algebra.TensorProduct.mapRingHom (algebraMap R A) ↑Algebra.TensorProduct.includeRight
          ↑Algebra.TensorProduct.includeRight ⋯ ⋯).comp
      ↑(comulAlgHom R B)

Tactic:
ext x

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Bialgebra R B
inst✝ : Algebra R A
x : B
⊢ ((↑(comulAlgHom A (A ⊗[R] B))).comp ↑Algebra.TensorProduct.includeRight) x =
    ((Algebra.TensorProduct.mapRingHom (algebraMap R A) ↑Algebra.TensorProduct.includeRight
            ↑Algebra.TensorProduct.includeRight ⋯ ⋯).comp
        ↑(comulAlgHom R B))
      x
Module: Mathlib.Order.Category.Preord

Goal state before:
pp: X✝ Y✝ : Preord
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : preordToCat.map a₁✝ = preordToCat.map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
ext x

Goal state after:
X✝ Y✝ : Preord
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : preordToCat.map a₁✝ = preordToCat.map a₂✝
x : ↑X✝
⊢ (Preord.Hom.hom a₁✝) x = (Preord.Hom.hom a₂✝) x
Module: Mathlib.Order.Category.PartOrd

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

Tactic:
ext x

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

Goal state before:
pp: X✝ Y✝ Z✝ : Preord
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ PartOrd.ofHom (Preord.Hom.hom (f ≫ g)).antisymmetrization =
    PartOrd.ofHom (Preord.Hom.hom f).antisymmetrization ≫ PartOrd.ofHom (Preord.Hom.hom g).antisymmetrization

Tactic:
ext x

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

Goal state before:
pp: R : Type u_1
M : Type u_3
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₃ : Type u_16
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : AddCommMonoid N₃
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R N₃
f₃ : M₃ →ₗ[R] N₃
f₁₂ : M →ₗ[R] M₁ ⊗[R] M₂
⊢ α ∘ₗ f₁₂ ⊗ₘ f₃ = LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f₃) ∘ₗ α ∘ₗ f₁₂ ⊗ₘ LinearMap.id

Tactic:
by
  rw [← LinearMap.comp_assoc, map_map_comp_assoc_eq]
  simp only [coassoc_simps]

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

Goal state before:
pp: R : CommRingCat
X✝ Y✝ Z✝ : CommMonCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Hom.hom (Under.Hom.right (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom (f ≫ g)))) ⋯)) =
    Hom.hom
      (Under.Hom.right
        (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom f))) ⋯ ≫
          Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom g))) ⋯))

Tactic:
apply MonoidAlgebra.ringHom_ext <;> intro <;> simp

Goal state after:
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 J : TwoSidedIdeal S
h : I ≤ J
⊢ (fun I ↦ { ringCon := I.ringCon.comap f }) I ≤ (fun I ↦ { ringCon := I.ringCon.comap f }) J

Tactic:
le_iff

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
h : ↑I ⊆ ↑J
⊢ (fun I ↦ { ringCon := I.ringCon.comap f }) I ≤ (fun I ↦ { ringCon := I.ringCon.comap f }) J
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case e'_3
R : Type u_5
inst✝¹³ : CommSemiring R
S₁ : Type u_6
S₂ : Type u_7
T : Type u_8
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
x y : R
inst✝² : Away x S₁
inst✝¹ : Away y S₂
inst✝ : Away ((algebraMap R S₂) x) T
⊢ Submonoid.powers ((algebraMap R S₁) y) = Algebra.algebraMapSubmonoid S₁ (Submonoid.powers y)

Tactic:
ext x

Goal state after:
case e'_3
R : Type u_5
inst✝¹³ : CommSemiring R
S₁ : Type u_6
S₂ : Type u_7
T : Type u_8
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
x✝ y : R
inst✝² : Away x✝ S₁
inst✝¹ : Away y S₂
inst✝ : Away ((algebraMap R S₂) x✝) T
x : S₁
⊢ x ∈ Submonoid.powers ((algebraMap R S₁) y) ↔ x ∈ Algebra.algebraMapSubmonoid S₁ (Submonoid.powers y)
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Ring R
s : Set R
z : R
x✝ : z ∈ span s
x : R
hx : x ∈ s
⊢ x ∈ univ * s * univ

Tactic:
exact ⟨1 * x, ⟨1, mem_univ _, x, hx, rfl⟩, 1, mem_univ _, by simp⟩

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

Goal state before:
pp: 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) ≤ ⊥
⊢ Away r T

Tactic:
refine .mk _ hr (fun t ↦ ?_) fun x y h ↦ ⟨n, ?_⟩

Goal state after:
case refine_1
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) ≤ ⊥
t : T
⊢ ∃ n a, t * (algebraMap S T) r ^ n = (algebraMap S T) a

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
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Ring R
s : Set R
z x r y : R
hy : y ∈ s * univ
⊢ x * (fun x1 x2 ↦ x1 * x2) r y ∈ univ * (s * univ)

Tactic:
exact ⟨x * r, mem_univ _, y, hy, mul_assoc ..⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
le : I ≤ jacobson R
⊢ Function.Surjective ⇑(Ideal.Quotient.mk I).toSemilinearMap

Tactic:
by exact Ideal.Quotient.mk_surjective

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

Goal state before:
pp: case h
R : Type u
inst✝ : Ring R
I : Ideal R
r : R
h : r ∈ I.jacobson
s : R
hs : s * 1 * r + s - 1 ∈ I
⊢ s * r + s - 1 ∈ I

Tactic:
simpa using hs

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
R : Type u_6
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
h₁ : Function.Surjective ⇑(algebraMap S T)
h₂ : Function.Surjective ⇑(algebraMap R S)
r : R
hr : IsUnit ((algebraMap R T) r)
n : ℕ
hn : r ^ n • RingHom.ker (algebraMap R T) ≤ RingHom.ker (algebraMap R S)
⊢ Ideal.map (algebraMap R S) (r ^ n • RingHom.ker (algebraMap R T)) ≤ ⊥

Tactic:
rwa [RingHom.ker_eq_comap_bot (algebraMap R S), ← Ideal.map_le_iff_le_comap] at hn

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Set R
span_eq : Ideal.span s = ⊤
x y : R
eq : (algebraMap R ((a : ↑s) → Away ↑a)) x = (algebraMap R ((a : ↑s) → Away ↑a)) y
ne : ¬Module.eqIdeal R x y = ⊤
⊢ False

Tactic:
have ⟨r, hrs, disj⟩ := Ideal.exists_disjoint_powers_of_span_eq_top s span_eq _ ne

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Set R
span_eq : Ideal.span s = ⊤
x y : R
eq : (algebraMap R ((a : ↑s) → Away ↑a)) x = (algebraMap R ((a : ↑s) → Away ↑a)) y
ne : ¬Module.eqIdeal R x y = ⊤
r : R
hrs : r ∈ s
disj : Disjoint ↑(Module.eqIdeal R x y) ↑(Submonoid.powers r)
⊢ False
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: case neg.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j : J
h_1 : ¬j = i
f : j ⟶ i
this : IsIso (F.map f)
⊢ ((Functor.const J).obj (F.1 i)).map f ≫ eqToHom ⋯ = (H j h_1).from (((Functor.const J).obj (F.1 i)).obj j) ≫ F.map f

Tactic:
rw [← IsIso.comp_inv_eq]

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : 0 ≤ n
hm : m < 0
⊢ n + m = n - -m

Tactic:
sub_neg_eq_add

Goal state after:
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 m : ℤ
hn : 0 ≤ n
hm : m < 0
⊢ n + m = n + m
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
v : Set M
hv : span R v = ⊤
x : Mₛ
x✝ : x ∈ ⊤
m : M
s : ↥S
h : ⋯.unit⁻¹ • f (m, s).1 = x
⊢ (↑R f) (m, s).1 ∈ ↑(map (↑R f) ⊤)

Tactic:
exact mem_map_of_mem mem_top

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))

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 : 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
c' : PullbackCone f g :=
  PullbackCone.mk (m ≫ c.π.app { as := WalkingPair.left }) (m ≫ c.π.app { as := WalkingPair.right }) ⋯
⊢ m = hc.lift (PullbackCone.mk (s.π.app { as := WalkingPair.left }) (s.π.app { as := WalkingPair.right }) ⋯)
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'
M₁ : Type ?u.45
M₂ : Type ?u.47
B : Type ?u.69
C : Type ?u.81
inst✝²¹ : AddCommMonoid M₁
inst✝²⁰ : AddCommMonoid M₂
inst✝¹⁹ : Module R M₁
inst✝¹⁸ : Module R M₂
inst✝¹⁷ : Module A M₁
inst✝¹⁶ : Module A M₂
inst✝¹⁵ : IsScalarTower R A M₁
inst✝¹⁴ : IsScalarTower R A M₂
inst✝¹³ : Semiring B
inst✝¹² : Algebra R B
inst✝¹¹ : Algebra A B
inst✝¹⁰ : IsScalarTower R A B
inst✝⁹ : Semiring C
inst✝⁸ : Algebra R C
inst✝⁷ : Algebra A C
inst✝⁶ : IsScalarTower R A C
N : Type u_5
N' : Type u_6
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N'
g : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S f
inst✝ : IsLocalizedModule S g
⊢ IsLocalizedModule S (TensorProduct.map f g)

Tactic:
by
  let eM := IsLocalizedModule.linearEquiv S f (TensorProduct.mk R (Localization S) M 1)
  let eN := IsLocalizedModule.linearEquiv S g (TensorProduct.mk R (Localization S) N 1)
  convert!
    IsLocalizedModule.of_linearEquiv S (TensorProduct.mk R (Localization S) (M ⊗[R] N) 1) <|
      (AlgebraTensorModule.distribBaseChange R (Localization S) ..).restrictScalars R ≪≫ₗ
        (congr eM eN ≪≫ₗ TensorProduct.equivOfCompatibleSMul ..).symm
  ext; congrm (?_ ⊗ₜ ?_) <;> simp [LinearEquiv.eq_symm_apply, eM, eN]

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

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

Tactic:
ext x

Goal state after:
α : Type u
f : Type u → Type v
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
x : f α
⊢ (mapEquiv f (Equiv.refl α)) x = (Equiv.refl (f α)) x
Module: Mathlib.Logic.Equiv.Functor

Goal state before:
pp: α : Type u
α' : Type v
F : Type u → Type v → Type w
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
⊢ mapEquiv F (Equiv.refl α) (Equiv.refl α') = Equiv.refl (F α α')

Tactic:
ext x

Goal state after:
α : Type u
α' : Type v
F : Type u → Type v → Type w
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
x : F α α'
⊢ (mapEquiv F (Equiv.refl α) (Equiv.refl α')) x = (Equiv.refl (F α α')) x
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
x : T
p✝ : LocalizedModule S M
a : R × ↥S := IsLocalization.sec S x
p p' : M × ↥S
s : ↥S
h : s • p'.2 • p.1 = s • p.2 • p'.1
⊢ a.2 • a.1 • s • p'.2 • p.1 = a.2 • a.1 • s • p.2 • p'.1

Tactic:
by rw [h]

Goal state after:
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
x : T
m : M
s : ↥S
n : M
t : ↥S
⊢ x • mk (t • m + s • n) (s * t) = IsLocalization.mk' T ?m.144 ?m.145 • ?m.147

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

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

Goal state before:
pp: R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
s : ↥S
x y : LocalizedModule S M
m₁ m₂ : M
t₁ t₂ : ↥S
⊢ mk (t₂ • m₁ + t₁ • m₂) (t₁ * (s * t₂)) = mk (s • (t₂ • m₁ + t₁ • m₂)) (s * (t₁ * (s * t₂)))

Tactic:
mk_cancel_common_left s

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Units

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
N : Type u_2
inst✝ : Monoid N
f g : M →* N
r : M
hr : f r = g r
h : IsUnit r
s : M
hs : r * s = 1 ∧ s * r = 1
⊢ ∃ a, r * a = 1 ∧ f a = g a ∧ a * r = 1

Tactic:
refine ⟨s, hs.left, ?_, hs.right⟩

Goal state after:
M : Type u_1
inst✝¹ : Monoid M
N : Type u_2
inst✝ : Monoid N
f g : M →* N
r : M
hr : f r = g r
h : IsUnit r
s : M
hs : r * s = 1 ∧ s * r = 1
⊢ f s = g s
Module: Mathlib.CategoryTheory.Monad.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G M N : Comonad C
f : M.toFunctor ≅ N.toFunctor
f_ε : ∀ (X : C), f.hom.app X ≫ N.ε.app X = M.ε.app X
f_δ : ∀ (X : C), f.hom.app X ≫ N.δ.app X = M.δ.app X ≫ f.hom.app (M.obj X) ≫ N.map (f.hom.app X)
X : C
⊢ f.inv.app X ≫ M.δ.app X = N.δ.app X ≫ f.inv.app (N.obj X) ≫ M.map (f.inv.app X)

Tactic:
by
        rw [← NatIso.cancel_natIso_hom_left f]
        simp only [reassoc_of% (f_δ X), Iso.hom_inv_id_app_assoc, NatTrans.naturality_assoc]
        rw [← Functor.map_comp, Iso.hom_inv_id_app, Functor.map_id]
        apply (comp_id _).symm

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, c • x₁✝ = c • x₂✝

Tactic:
simp_rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply] at h
    obtain ⟨c, hc⟩ := hf.exists_of_eq h
    exact ⟨c, by simpa only [Submonoid.smul_def, map_smul, e.symm_apply_apply]
      using congr(e.symm $hc)⟩

Goal state after: