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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ F₁₂' : C₁ ⥤ C₂ ⥤ C₁₂
φ : F₁₂ ⟶ F₁₂'
G : C₁₂ ⥤ C₃ ⥤ C₄
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
X₃ : C₃
⊢ (G.map ((F₁₂.obj X₁).map f)).app X₃ ≫ (G.map ((φ.app X₁).app Y₂)).app X₃ =
    (G.map ((φ.app X₁).app X₂)).app X₃ ≫ (G.map ((F₁₂'.obj X₁).map f)).app X₃

Tactic:
simp only [← NatTrans.comp_app, NatTrans.naturality, ← G.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ F₁₂' : C₁ ⥤ C₂ ⥤ C₁₂
φ : F₁₂ ⟶ F₁₂'
G : C₁₂ ⥤ C₃ ⥤ C₄
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
X₂ : C₂
X₃ : C₃
⊢ (G.map ((F₁₂.map f).app X₂)).app X₃ ≫ (G.map ((φ.app Y₁).app X₂)).app X₃ =
    (G.map ((φ.app X₁).app X₂)).app X₃ ≫ (G.map ((F₁₂'.map f).app X₂)).app X₃

Tactic:
simp only [← NatTrans.comp_app, NatTrans.naturality, ← G.map_comp]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : C), IsSplitEpi (h.unit.app X)
X Y : C
f : L.obj X ⟶ L.obj Y
⊢ ∃ a, L.map a = f

Tactic:
by
    use ((h.homEquiv X (L.obj Y)) f ≫ section_ (h.unit.app Y))
    suffices L.map (section_ (h.unit.app Y)) = h.counit.app (L.obj Y) by simp [this]
    rw [← comp_id (L.map (section_ (h.unit.app Y)))]
    simp only [Functor.id_obj, ← h.left_triangle_components Y,
      ← assoc, ← Functor.map_comp, IsSplitEpi.id, Functor.map_id, id_comp]

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

Goal state before:
pp: case e'_3
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
E : Type u_1
inst✝² : Category.{v_1, u_1} E
T : C ⥤ E
S : E ⥤ D
X : C
adj2 : T ⊣ S ⋙ R
inst✝¹ : R.Faithful
inst✝ : R.Full
FF : R.FullyFaithful := FullyFaithful.ofFullyFaithful R
Y : E
e_1✝ : (T.obj ((L ⋙ R).obj X) ⟶ Y) = (T.obj (R.obj (L.obj X)) ⟶ Y)
e_2✝ : (T.obj ((𝟭 C).obj X) ⟶ Y) = (T.obj X ⟶ Y)
x : T.obj ((L ⋙ R).obj X) ⟶ Y
⊢ T.map (h.unit.app X) ≫ x =
    ((adj2.homEquiv (R.obj (L.obj X)) Y).trans
        (FF.homEquiv.symm.trans ((h.homEquiv X (S.obj Y)).trans (adj2.homEquiv X Y).symm)))
      x

Tactic:
have := adj2.counit_naturality x

Goal state after:
case e'_3
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
E : Type u_1
inst✝² : Category.{v_1, u_1} E
T : C ⥤ E
S : E ⥤ D
X : C
adj2 : T ⊣ S ⋙ R
inst✝¹ : R.Faithful
inst✝ : R.Full
FF : R.FullyFaithful := FullyFaithful.ofFullyFaithful R
Y : E
e_1✝ : (T.obj ((L ⋙ R).obj X) ⟶ Y) = (T.obj (R.obj (L.obj X)) ⟶ Y)
e_2✝ : (T.obj ((𝟭 C).obj X) ⟶ Y) = (T.obj X ⟶ Y)
x : T.obj ((L ⋙ R).obj X) ⟶ Y
this : T.map ((S ⋙ R).map x) ≫ adj2.counit.app Y = adj2.counit.app (T.obj ((L ⋙ R).obj X)) ≫ x
⊢ T.map (h.unit.app X) ≫ x =
    ((adj2.homEquiv (R.obj (L.obj X)) Y).trans
        (FF.homEquiv.symm.trans ((h.homEquiv X (S.obj Y)).trans (adj2.homEquiv X Y).symm)))
      x
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

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
F G : LaxMonoidalFunctor C D
α β : F ⟶ G
h : α.hom = β.hom
⊢ α = β

Tactic:
cases α

Goal state after:
case mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G : LaxMonoidalFunctor C D
β : F ⟶ G
hom✝ : F.toFunctor ⟶ G.toFunctor
isMonoidal✝ : NatTrans.IsMonoidal hom✝
h : { hom := hom✝, isMonoidal := isMonoidal✝ }.hom = β.hom
⊢ { hom := hom✝, isMonoidal := isMonoidal✝ } = β
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

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
E' : Type u₄
inst✝⁴ : Category.{v₄, u₄} E'
inst✝³ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝² : F₁.LaxMonoidal
inst✝¹ : F₂.LaxMonoidal
inst✝ : F₃.LaxMonoidal
F G : LaxMonoidalFunctor C D
e : (X : C) → F.obj X ≅ G.obj X
naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (e Y).hom = (e X).hom ≫ G.map f
unit : ε F.toFunctor ≫ (e (𝟙_ C)).hom = ε G.toFunctor
tensor : ∀ (X Y : C), μ F.toFunctor X Y ≫ (e (X ⊗ Y)).hom = ((e X).hom ⊗ₘ (e Y).hom) ≫ μ G.toFunctor X Y
⊢ NatTrans.IsMonoidal (NatIso.ofComponents e ⋯).hom

Tactic:
by constructor <;> assumption

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M N : SemimoduleCat R
f : M ⟶ N
⊢ tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom = (rightUnitor M).hom ≫ f

Tactic:
ext : 1
  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): broken ext
  apply TensorProduct.ext
  ext
  simp [tensorHom, tensorObj, rightUnitor]

Goal state after:
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
F : C ⥤ D
inst✝ : F.Monoidal
X Y Z : C
⊢ 𝟙 (F.obj ((X ⊗ Y) ⊗ Z)) =
    δ F (X ⊗ Y) Z ≫
      δ F X Y ▷ F.obj Z ≫
        (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫
          F.obj X ◁ μ F Y Z ≫
            μ F X (Y ⊗ Z) ≫
              δ F X (Y ⊗ Z) ≫
                F.obj X ◁ δ F Y Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv ≫ μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z

Tactic:
OplaxMonoidal.associativity_inv_assoc,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
X Y Z : C
⊢ 𝟙 (F.obj ((X ⊗ Y) ⊗ Z)) =
    δ F (X ⊗ Y) Z ≫
      δ F X Y ▷ F.obj Z ≫
        (α_ (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).inv ≫ δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z ≫ μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z
Module: Mathlib.CategoryTheory.MorphismProperty.Concrete

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : C
⊢ Bijective ⇑(ConcreteCategory.hom (𝟙 X))

Tactic:
convert! bijective_id

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : C
⊢ ⇑(ConcreteCategory.hom (𝟙 X)) = id
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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.OplaxMonoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
⊢ F.map (ε G) ≫ adj.counit.app (𝟙_ D) = η F

Tactic:
simp [IsMonoidal.leftAdjoint_ε (adj := adj)]

Goal state after:
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✝ : G.LaxMonoidal
X Y Z : C
| (X ⊗ Y) ◁ adj.unit.app Z ≫
    adj.unit.app (X ⊗ Y) ▷ G.obj (F.obj Z) ≫
      (G.map (F.map (adj.unit.app X ⊗ₘ adj.unit.app Y)) ≫
            G.map (F.map (μ G (F.obj X) (F.obj Y))) ≫ G.map (adj.counit.app (F.obj X ⊗ F.obj Y))) ▷
          G.obj (F.obj Z) ≫
        μ G (F.obj X ⊗ F.obj Y) (F.obj Z) ≫ G.map (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom

Tactic:
← comp_whiskerRight_assoc

Goal state after:
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✝ : G.LaxMonoidal
X Y Z : C
| (X ⊗ Y) ◁ adj.unit.app Z ≫
    (adj.unit.app (X ⊗ Y) ≫
          G.map (F.map (adj.unit.app X ⊗ₘ adj.unit.app Y)) ≫
            G.map (F.map (μ G (F.obj X) (F.obj Y))) ≫ G.map (adj.counit.app (F.obj X ⊗ F.obj Y))) ▷
        G.obj (F.obj Z) ≫
      μ G (F.obj X ⊗ F.obj Y) (F.obj Z) ≫ G.map (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom
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✝ : G.LaxMonoidal
X Y Z : C
| (X ⊗ Y) ◁ adj.unit.app Z ≫
    (adj.unit.app X ⊗ₘ adj.unit.app Y) ▷ G.obj (F.obj Z) ≫
      μ G (F.obj X) (F.obj Y) ▷ G.obj (F.obj Z) ≫
        μ G (F.obj X ⊗ F.obj Y) (F.obj Z) ≫ G.map (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom

Tactic:
← comp_whiskerRight_assoc

Goal state after:
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✝ : G.LaxMonoidal
X Y Z : C
| (X ⊗ Y) ◁ adj.unit.app Z ≫
    ((adj.unit.app X ⊗ₘ adj.unit.app Y) ≫ μ G (F.obj X) (F.obj Y)) ▷ G.obj (F.obj Z) ≫
      μ G (F.obj X ⊗ F.obj Y) (F.obj Z) ≫ G.map (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝¹ : DecidableEq J
A : Type w
inst✝ : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
x : Quot F
⊢ (ConcreteCategory.hom (hc.desc (toCocone F f))) ((desc F c) x) = f x

Tactic:
by
  conv_rhs => rw [← Quot.desc_toCocone_desc F c f hc]
  dsimp

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
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : TensorAlgebra R M →ₐ[R] A
w : f.toLinearMap ∘ₗ ι R = g.toLinearMap ∘ₗ ι R
⊢ f = g

Tactic:
rw [← lift_symm_apply, ← lift_symm_apply] at w
  exact (lift R).symm.injective w

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
⊢ Algebra.adjoin R (Set.range ⇑(ι R)) = ⊤

Tactic:
refine top_unique fun x hx => ?_

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : TensorAlgebra R M
hx : x ∈ ⊤
⊢ x ∈ Algebra.adjoin R (Set.range ⇑(ι R))
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
X : Type u₇
Y : Type u₈
Z : Type u₉
inst✝⁸ : Category.{v₁, u₁} A
inst✝⁷ : Category.{v₂, u₂} B
inst✝⁶ : Category.{v₃, u₃} C
inst✝⁵ : Category.{v₄, u₄} D
inst✝⁴ : Category.{v₅, u₅} E
inst✝³ : Category.{v₆, u₆} F
inst✝² : Category.{v₇, u₇} X
inst✝¹ : Category.{v₈, u₈} Y
inst✝ : Category.{v₉, u₉} Z
G₁ : A ⥤ D
H₁ : B ⥤ E
K₁ : C ⥤ F
G₂ : D ⥤ X
H₂ : E ⥤ Y
K₂ : F ⥤ Z
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : B ⥤ C
R₂ : C ⥤ B
L₃ : D ⥤ E
R₃ : E ⥤ D
L₄ : E ⥤ F
R₄ : F ⥤ E
L₅ : X ⥤ Y
R₅ : Y ⥤ X
L₆ : Y ⥤ Z
R₆ : Z ⥤ Y
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
adj₄ : L₄ ⊣ R₄
adj₅ : L₅ ⊣ R₅
adj₆ : L₆ ⊣ R₆
α : TwoSquare G₁ L₁ L₃ H₁
β : TwoSquare H₁ L₂ L₄ K₁
γ : TwoSquare G₂ L₃ L₅ H₂
δ : TwoSquare H₂ L₄ L₆ K₂
⊢ (mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆)) ((α ≫ᵥ β) ≫ₕ γ ≫ᵥ δ) =
    ((mateEquiv adj₂ adj₄) β ≫ₕ (mateEquiv adj₁ adj₃) α) ≫ᵥ (mateEquiv adj₄ adj₆) δ ≫ₕ (mateEquiv adj₃ adj₅) γ

Tactic:
have vcomp :=
    mateEquiv_vcomp (adj₁.comp adj₂) (adj₃.comp adj₄) (adj₅.comp adj₆) (α ≫ᵥ β) (γ ≫ᵥ δ)
  simp only [mateEquiv_hcomp] at vcomp
  assumption

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

Goal state before:
pp: case h2
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
⊢ -((b.fst⁻¹ * a.fst⁻¹) •> a.fst •> b.snd <• (b.fst⁻¹ * a.fst⁻¹) +
        (b.fst⁻¹ * a.fst⁻¹) •> (a.snd <• b.fst) <• (b.fst⁻¹ * a.fst⁻¹)) =
    -(b.fst⁻¹ •> (a.fst⁻¹ •> a.snd <• a.fst⁻¹)) + -(b.fst⁻¹ •> b.snd <• b.fst⁻¹ <• a.fst⁻¹)

Tactic:
smul_comm (_ : R),

Goal state after:
case h2
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
⊢ -((b.fst⁻¹ * a.fst⁻¹) •> a.fst •> b.snd <• (b.fst⁻¹ * a.fst⁻¹) +
        (b.fst⁻¹ * a.fst⁻¹) •> a.snd <• b.fst <• (b.fst⁻¹ * a.fst⁻¹)) =
    -(b.fst⁻¹ •> a.fst⁻¹ •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• b.fst⁻¹ <• a.fst⁻¹)
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: S : Type u_1
R : Type u
M : Type v
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Algebra S R
inst✝⁵ : Module S M
inst✝⁴ : Module R M
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : SMulCommClass R Rᵐᵒᵖ M
inst✝¹ : IsScalarTower S R M
inst✝ : IsScalarTower S Rᵐᵒᵖ M
⊢ (inlAlgHom S R M).range ⊔ Algebra.adjoin S (Set.range inr) = ⊤

Tactic:
refine top_unique fun x hx => ?_

Goal state after:
S : Type u_1
R : Type u
M : Type v
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Algebra S R
inst✝⁵ : Module S M
inst✝⁴ : Module R M
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : SMulCommClass R Rᵐᵒᵖ M
inst✝¹ : IsScalarTower S R M
inst✝ : IsScalarTower S Rᵐᵒᵖ M
x : tsze R M
hx : x ∈ ⊤
⊢ x ∈ (inlAlgHom S R M).range ⊔ Algebra.adjoin S (Set.range inr)
Module: Mathlib.RingTheory.Bialgebra.Basic

Goal state before:
pp: R✝ : Type u
A✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Bialgebra R✝ A✝
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
C : Coalgebra R A
counit_one : counit 1 = 1
counit_mul : ∀ {a b : A}, counit (a * b) = counit a * counit b
comul_one : comul 1 = 1
comul_mul : ∀ {a b : A}, comul (a * b) = comul a * comul b
⊢ (LinearMap.mul R A).compr₂ comul = (LinearMap.mul R (A ⊗[R] A)).compl₁₂ comul comul

Tactic:
by ext; exact comul_mul

Goal state after:
Module: Mathlib.Algebra.Ring.BooleanRing

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

Tactic:
dsimp only [(· ⊓ ·)]

Goal state after:
α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a * b = b * a
Module: Mathlib.Algebra.Ring.BooleanRing

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

Tactic:
dsimp only [(· ⊓ ·)]

Goal state after:
α : Type u_1
inst✝ : BooleanRing α
a b c : α
⊢ a * b * c = a * (b * c)
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: R : CommRingCat
S T : Under R
f : S ⟶ T
⊢ Hom.hom
      (Under.Hom.right
        (((Under.forget R ⋙ forget₂ CommRingCat CommMonCat) ⋙ R.monoidAlgebra).map f ≫
          Under.homMk
            (ofHom
              (MonoidAlgebra.liftNCRingHom (Hom.hom T.hom)
                (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj T)) ⋯))
            ⋯)) =
    Hom.hom
      (Under.Hom.right
        (Under.homMk
            (ofHom
              (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
            ⋯ ≫
          (𝟭 (Under R)).map f))

Tactic:
apply MonoidAlgebra.ringHom_ext <;>
        intro <;> simp [MonoidAlgebra.liftNCRingHom, ← Under.w f, -Under.w]

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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
e : R
he : IsIdempotentElem e
H : RingHom.ker (algebraMap R S) = Ideal.span {1 - e}
H' : Function.Surjective ⇑(algebraMap R S)
x y : R
⊢ x • e = y • e ↔ e * x = e * y

Tactic:
simp_rw [mul_comm e, smul_eq_mul]

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
z : R
⊢ z ∈ span s ↔ z ∈ span (univ * s * univ)

pp: R : Type u_1
inst✝ : Ring R
s : Set R
z : R
⊢ z ∈ span (univ * s * univ) ↔ z ∈ AddSubgroup.closure (univ * s * univ)

Tactic:
· refine ⟨(span_mono (fun x hx ↦ ?_) ·), fun hz ↦ ?_⟩
    · exact ⟨1 * x, ⟨1, mem_univ _, x, hx, rfl⟩, 1, mem_univ _, by simp⟩
    · exact mem_span_iff.mp hz (span s) <| subset_mul_set (set_mul_subset subset_span _) _

Goal state after:
R : Type u_1
inst✝ : Ring R
s : Set R
z : R
⊢ z ∈ span (univ * s * univ) ↔ z ∈ AddSubgroup.closure (univ * s * univ)
Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
x : R
⊢ x ∉ maximalIdeal R ↔ IsUnit x

Tactic:
by
  simp only [mem_maximalIdeal, mem_nonunits_iff, not_not]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasStrictInitialObjects C
I X : C
inst✝ : HasBinaryProduct X I
hI : IsInitial I
⊢ X ⨯ I ≅ I

Tactic:
have := hI.isIso_to (prod.snd : X ⨯ I ⟶ I)
  exact asIso prod.snd

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

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
⊢ Function.LeftInverse (↑R) (extendScalarsOfIsLocalization S A)

Tactic:
by intro _; ext; simp

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

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
⊢ Function.RightInverse (↑R) (extendScalarsOfIsLocalization S A)

Tactic:
by intro _; ext; simp

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

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
P' : C
fst' : P' ⟶ X
snd' : P' ⟶ Y
h : IsPullback fst snd f g
h' : IsPullback fst' snd' f g
⊢ (isoIsPullback X Y h h').inv ≫ snd = snd'

Tactic:
simp only [Iso.inv_comp_eq, isoIsPullback_hom_snd]

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

Goal state before:
pp: case hc
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
inst✝³ : HasInitial C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : PreservesColimitsOfShape WalkingSpan F
K : Discrete WalkingPair ⥤ C
⊢ IsColimit
    (PushoutCocone.mk ((F.mapCocone (colimitCoconeOfInitialAndPushouts K).cocone).ι.app { as := WalkingPair.left })
      ((F.mapCocone (colimitCoconeOfInitialAndPushouts K).cocone).ι.app { as := WalkingPair.right }) ⋯)

pp: case f
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
inst✝³ : HasInitial C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : PreservesColimitsOfShape WalkingSpan F
K : Discrete WalkingPair ⥤ C
⊢ F.obj (⊥_ C) ⟶ (K ⋙ F).obj { as := WalkingPair.left }

pp: case g
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
inst✝³ : HasInitial C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : PreservesColimitsOfShape WalkingSpan F
K : Discrete WalkingPair ⥤ C
⊢ F.obj (⊥_ C) ⟶ (K ⋙ F).obj { as := WalkingPair.right }

Tactic:
apply isColimitOfHasPushoutOfPreservesColimit

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
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
⊢ e₁.hom ≫ fst' ≫ f' = e₁.hom ≫ snd' ≫ g'

Tactic:
← reassoc_of% commfst,

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
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
⊢ fst ≫ e₂.hom ≫ f' = e₁.hom ≫ snd' ≫ g'
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_1
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
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
⊢ fst = e₁.hom ≫ fst' ≫ e₂.inv

Tactic:
← reassoc_of% commfst,

Goal state after:
case refine_1
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
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
⊢ fst = fst ≫ e₂.hom ≫ e₂.inv
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'
T : Type u_5
B : Type u_6
inst✝⁸ : CommSemiring T
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra T B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R T B
inst✝¹ : IsScalarTower R A B
α : Type u_7
inst✝ : IsLocalizedModule S f
e : Localization S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LocalizedModule.equivTensorProduct S M).symm ≪≫ₗ IsLocalizedModule.iso S f
e' : Localization S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ M' :=
  finsuppRight R R (Localization S) M α ≪≫ₗ Finsupp.mapRange.linearEquiv e
this : IsLocalizedModule S (↑e'.symm ∘ₗ Finsupp.mapRange.linearMap f)
⊢ IsLocalizedModule S (Finsupp.mapRange.linearMap f)

Tactic:
by
    convert! this.of_linearEquiv (e := e')
    ext
    simp

Goal state after:
Module: Mathlib.Control.Bifunctor

Goal state before:
pp: F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α₀ α₁ : Type u₀
β₀ β₁ : Type u₁
f : α₀ → α₁
f' : β₀ → β₁
x : F α₀ β₀
⊢ snd f' (fst f x) = bimap f f' x

Tactic:
by simp [snd, bimap_bimap]

Goal state after: