mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
x✝ : W.ContainsIdentities
X✝ : C
⊢ ∀ ⦃Y : C⦄ (f : X✝ ⟶ Y), identities C f → W f

Tactic:
_

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
x✝ : W.ContainsIdentities
X✝ Y✝ : C
⊢ ∀ (f : X✝ ⟶ Y✝), identities C f → W f
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
x✝ : W.ContainsIdentities
X✝ Y✝ : C
⊢ ∀ (f : X✝ ⟶ Y✝), identities C f → W f

Tactic:
_

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
x✝ : W.ContainsIdentities
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ identities C f✝ → W f✝
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsMultiplicative
X✝ : C
⊢ ∀ ⦃Y : C⦄ (f : X✝ ⟶ Y), W.multiplicativeClosure f → W f

Tactic:
_

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsMultiplicative
X✝ Y✝ : C
⊢ ∀ (f : X✝ ⟶ Y✝), W.multiplicativeClosure f → W f
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsMultiplicative
X✝ Y✝ : C
⊢ ∀ (f : X✝ ⟶ Y✝), W.multiplicativeClosure f → W f

Tactic:
_

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsMultiplicative
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ W.multiplicativeClosure f✝ → W f✝
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W W' : MorphismProperty C
inst✝ : W'.IsMultiplicative
h : W ≤ W'
X✝ : C
⊢ ∀ ⦃Y : C⦄ (f : X✝ ⟶ Y), W.multiplicativeClosure f → W' f

Tactic:
_

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W W' : MorphismProperty C
inst✝ : W'.IsMultiplicative
h : W ≤ W'
X✝ Y✝ : C
⊢ ∀ (f : X✝ ⟶ Y✝), W.multiplicativeClosure f → W' f
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W W' : MorphismProperty C
inst✝ : W'.IsMultiplicative
h : W ≤ W'
X✝ Y✝ : C
⊢ ∀ (f : X✝ ⟶ Y✝), W.multiplicativeClosure f → W' f

Tactic:
_

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W W' : MorphismProperty C
inst✝ : W'.IsMultiplicative
h : W ≤ W'
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ W.multiplicativeClosure f✝ → W' f✝
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
X✝ : D
⊢ ∀ ⦃Y : D⦄ (f : X✝ ⟶ Y), W.multiplicativeClosure.strictMap F f → (W.strictMap F).multiplicativeClosure f

Tactic:
_

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
X✝ Y✝ : D
⊢ ∀ (f : X✝ ⟶ Y✝), W.multiplicativeClosure.strictMap F f → (W.strictMap F).multiplicativeClosure f
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
⊢ W.multiplicativeClosure.strictMap F ≤ (W.strictMap F).multiplicativeClosure

Tactic:
by
  intro _ _ f hf
  induction hf with | map hf
  induction hf with
  | of f hf => exact le_multiplicativeClosure _ _ ⟨hf⟩
  | id x => simpa using .id (F.obj x)
  | comp_of _ _ hf hg h =>
    simpa using multiplicativeClosure.comp_of _ _ h (strictMap.map hg)

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

Goal state before:
pp: case leftAdjoint_μ
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
this : G.LaxMonoidal := adj.rightAdjointLaxMonoidal
X✝ : D
⊢ ∀ (Y : D),
    μ G X✝ Y =
      adj.unit.app (G.obj X✝ ⊗ G.obj Y) ≫ G.map (δ F (G.obj X✝) (G.obj Y) ≫ (adj.counit.app X✝ ⊗ₘ adj.counit.app Y))

Tactic:
_

Goal state after:
case leftAdjoint_μ
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
this : G.LaxMonoidal := adj.rightAdjointLaxMonoidal
X✝ Y✝ : D
⊢ μ G X✝ Y✝ =
    adj.unit.app (G.obj X✝ ⊗ G.obj Y✝) ≫ G.map (δ F (G.obj X✝) (G.obj Y✝) ≫ (adj.counit.app X✝ ⊗ₘ adj.counit.app Y✝))
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
a✝ : (forget C).PreservesEpimorphisms
X✝ : C
⊢ ∀ ⦃Y : C⦄ (f : X✝ ⟶ Y), epimorphisms C f → MorphismProperty.surjective C f

Tactic:
_

Goal state after:
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
a✝ : (forget C).PreservesEpimorphisms
X✝ Y✝ : C
⊢ ∀ (f : X✝ ⟶ Y✝), epimorphisms C f → MorphismProperty.surjective C f
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
a✝ : (forget C).PreservesMonomorphisms
X✝ : C
⊢ ∀ ⦃Y : C⦄ (f : X✝ ⟶ Y), monomorphisms C f → MorphismProperty.injective C f

Tactic:
_

Goal state after:
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
a✝ : (forget C).PreservesMonomorphisms
X✝ Y✝ : C
⊢ ∀ (f : X✝ ⟶ Y✝), monomorphisms C f → MorphismProperty.injective C f
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : BraidedCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : MonoidalCategory D
inst✝⁶ : BraidedCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
inst✝³ : BraidedCategory E
F G : C ⥤ D
i : F ≅ G
inst✝² : F.LaxBraided
inst✝¹ : G.LaxMonoidal
inst✝ : NatTrans.IsMonoidal i.hom
X Y : C
this : ∀ (X Y : C), μ G X Y = (i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (X ⊗ Y)
⊢ ((i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (X ⊗ Y)) ≫ G.map (β_ X Y).hom =
    (β_ (G.obj X) (G.obj Y)).hom ≫ μ G Y X

Tactic:
this Y X,

Goal state after:
C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : BraidedCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : MonoidalCategory D
inst✝⁶ : BraidedCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
inst✝³ : BraidedCategory E
F G : C ⥤ D
i : F ≅ G
inst✝² : F.LaxBraided
inst✝¹ : G.LaxMonoidal
inst✝ : NatTrans.IsMonoidal i.hom
X Y : C
this : ∀ (X Y : C), μ G X Y = (i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (X ⊗ Y)
⊢ ((i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (X ⊗ Y)) ≫ G.map (β_ X Y).hom =
    (β_ (G.obj X) (G.obj Y)).hom ≫ (i.inv.app Y ⊗ₘ i.inv.app X) ≫ μ F Y X ≫ i.hom.app (Y ⊗ X)
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
x : Quot F
j : J
a : ↑(F.obj j)
⊢ ((quotUliftToQuot F).comp (quotToQuotUlift F)) ((Quot.ι F j) a) = (AddMonoidHom.id (Quot F)) ((Quot.ι F j) a)

Tactic:
AddMonoidHom.comp_apply,

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x : Quot F
j : J
a : ↑(F.obj j)
⊢ (quotUliftToQuot F) ((quotToQuotUlift F) ((Quot.ι F j) a)) = (AddMonoidHom.id (Quot F)) ((Quot.ι F j) a)
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
x : Quot (F ⋙ uliftFunctor)
j : J
a : ↑((F ⋙ uliftFunctor).obj j)
⊢ ((quotToQuotUlift F).comp (quotUliftToQuot F)) ((Quot.ι (F ⋙ uliftFunctor) j) a) =
    (AddMonoidHom.id (Quot (F ⋙ uliftFunctor))) ((Quot.ι (F ⋙ uliftFunctor) j) a)

Tactic:
AddMonoidHom.comp_apply,

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x : Quot (F ⋙ uliftFunctor)
j : J
a : ↑((F ⋙ uliftFunctor).obj j)
⊢ (quotToQuotUlift F) ((quotUliftToQuot F) ((Quot.ι (F ⋙ uliftFunctor) j) a)) =
    (AddMonoidHom.id (Quot (F ⋙ uliftFunctor))) ((Quot.ι (F ⋙ uliftFunctor) j) a)
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
j : J
x : ↑(F.obj j)
⊢ ((Hom.hom (hc.desc (toCocone F f))).comp (desc F c)) ((ι F j) x) = f ((ι F j) x)

Tactic:
AddMonoidHom.comp_apply,

Goal state after:
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
j : J
x : ↑(F.obj j)
⊢ (Hom.hom (hc.desc (toCocone F f))) ((desc F c) ((ι F j) x)) = f ((ι F j) x)
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring N
c : RingCon M
f : M →+* N
h : ker f ≤ c
hf : Surjective ⇑f
this : Equivalence (Relation.Map ⇑c.toSetoid ⇑f ⇑f)
i✝ : N
⊢ (mapGen ⇑f) i✝ ≤ Relation.Map (⇑c) (⇑f) (⇑f) i✝

Tactic:
_

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring N
c : RingCon M
f : M →+* N
h : ker f ≤ c
hf : Surjective ⇑f
this : Equivalence (Relation.Map ⇑c.toSetoid ⇑f ⇑f)
i✝¹ i✝ : N
⊢ (mapGen ⇑f) i✝¹ i✝ ≤ Relation.Map (⇑c) (⇑f) (⇑f) i✝¹ i✝
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: case ι
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ (ι R) x ∈ Algebra.adjoin R (Set.range ⇑(ι R))

Tactic:
exact Algebra.subset_adjoin (Set.mem_range_self _)

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.TensorAlgebra

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝ : ModuleCat R
⊢ (tensorAlgebra R).map ({ app := fun M ↦ ModuleCat.ofHom (TensorAlgebra.ι R), naturality := ⋯ }.app x✝) ≫
      { app := fun A ↦ ofHom ((TensorAlgebra.lift R) LinearMap.id), naturality := ⋯ }.app ((tensorAlgebra R).obj x✝) =
    𝟙 ((tensorAlgebra R).obj x✝)

Tactic:
ext : 1
    dsimp
    ext
    simp

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

Goal state before:
pp: 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
x : tsze R M
hx : x.fst ≠ 0
this : Invertible x.fst
⊢ x * x⁻¹ = 1

Tactic:
have := invertibleOfInvertibleFst x

Goal state after:
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
x : tsze R M
hx : x.fst ≠ 0
this✝ : Invertible x.fst
this : Invertible x
⊢ x * x⁻¹ = 1
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: case e'_2
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
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
⊢ ((AlgebraTensorModule.curry (LinearMap.lTensor (A ⊗[R] B) counit ∘ₗ comul)) x) y =
    (TensorProduct.rid S (A ⊗[R] B)).symm
      ((TensorProduct.rid S A) ((LinearMap.lTensor A counit) (comul x)) ⊗ₜ[R]
        (TensorProduct.rid R B) ((LinearMap.lTensor B counit) (comul y)))

Tactic:
dsimp
      hopf_tensor_induction comul (R := S) x with x₁ x₂
      hopf_tensor_induction comul (R := R) y with y₁ y₂
      apply (TensorProduct.rid S _).injective
      dsimp
      rw [tmul_smul, smul_assoc, one_smul, smul_tmul']

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Away

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x : M
F : AwayMap x N
y : M
G : AwayMap (x * y) P
⊢ mk' G (x * y) ⟨x * y, ⋯⟩ = 1

Tactic:
mk'_self

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x : M
F : AwayMap x N
y : M
G : AwayMap (x * y) P
⊢ 1 = 1
Module: Mathlib.GroupTheory.MonoidLocalization.Away

Goal state before:
pp: M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
A : Type u_4
inst✝² : AddCommMonoid A
x : A
B : Type u_5
inst✝¹ : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst✝ : AddCommMonoid C
g : A →+ C
hg : IsAddUnit (g x)
y : ↥(multiples x)
n : ℕ
hn : (fun i ↦ i • x) n = ↑y
⊢ IsAddUnit (g ↑y)

Tactic:
rw [← hn]

Goal state after:
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
A : Type u_4
inst✝² : AddCommMonoid A
x : A
B : Type u_5
inst✝¹ : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst✝ : AddCommMonoid C
g : A →+ C
hg : IsAddUnit (g x)
y : ↥(multiples x)
n : ℕ
hn : (fun i ↦ i • x) n = ↑y
⊢ IsAddUnit (g ((fun i ↦ i • x) n))
Module: Mathlib.GroupTheory.MonoidLocalization.Away

Goal state before:
pp: M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
A : Type u_4
inst✝² : AddCommMonoid A
x : A
B : Type u_5
inst✝¹ : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst✝ : AddCommMonoid C
g : A →+ C
y : A
G : AwayMap (x + y) C
⊢ mk' G (x + y) ⟨x + y, ⋯⟩ = 0

Tactic:
mk'_self

Goal state after:
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
A : Type u_4
inst✝² : AddCommMonoid A
x : A
B : Type u_5
inst✝¹ : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst✝ : AddCommMonoid C
g : A →+ C
y : A
G : AwayMap (x + y) C
⊢ 0 = 0
Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic

Goal state before:
pp: case right
R : Type u_1
S : Type u_2
K : Type u_3
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
I : Ideal R
x : R
⊢ maximalIdeal R ≤ I → x ∉ maximalIdeal R → x ∈ I → 1 ∈ I

Tactic:
_

Goal state after:
case right
R : Type u_1
S : Type u_2
K : Type u_3
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
I : Ideal R
x : R
a✝ : maximalIdeal R ≤ I
⊢ x ∉ maximalIdeal R → x ∈ I → 1 ∈ I
Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization

Goal state before:
pp: 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)

Tactic:
simp_rw [← (Algebra.lmul R Aₛ).commutes, Algebra.lmul_isUnit_iff, Subtype.forall,
      Algebra.algebraMapSubmonoid, ← SetLike.mem_coe, Submonoid.coe_map,
      Set.forall_mem_image, ← IsScalarTower.algebraMap_apply]

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

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
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
⊢ ⇑(algebraMap R S) '' ↑(Finset.image (fun t ↦ integerMultiple M s id t) s.attach) = commonDenomOfFinset M s • ↑s

Tactic:
rw [Finset.coe_image]

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
⊢ ⇑(algebraMap R S) '' (fun t ↦ integerMultiple M s id t) '' ↑s.attach = commonDenomOfFinset M s • ↑s
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
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
⊢ LinearIndependent Rₛ (⇑f ∘ v)

Tactic:
linearIndependent_iff'ₛ

Goal state after:
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
ι : Type u_5
v : ι → M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
⊢ ∀ (s : Finset ι) (f_1 g : ι → Rₛ), ∑ i ∈ s, f_1 i • (⇑f ∘ v) i = ∑ i ∈ s, g i • (⇑f ∘ v) i → ∀ i ∈ s, f_1 i = g i
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: 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
⊢ ∃ w, LinearIndependent R w

Tactic:
cases isEmpty_or_nonempty ι

Goal state after:
case inl
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✝ : IsEmpty ι
⊢ ∃ w, LinearIndependent R w

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 ι
⊢ ∃ w, LinearIndependent R w
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: case h
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
⊢ LinearIndependent R fun i ↦ (sec (v i)).1

Tactic:
linearIndependent_iff'ₛ

Goal state after:
case h
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 : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
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
⊢ ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • (sec (v i)).1 = ∑ i ∈ s, g i • (sec (v i)).1 → ∀ i ∈ s, f i = g i
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: 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
⊢ ∃ w, LinearIndependent R w

Tactic:
cases isEmpty_or_nonempty ι
  · exact ⟨isEmptyElim, linearIndependent_empty_type⟩
  have inj := hf.smul_left_injective (Classical.arbitrary ι)
  choose sec hsec using surj S f
  use fun i ↦ (sec (v i)).1
  rw [linearIndependent_iff'ₛ] at hf ⊢
  intro t g g' eq i hit
  refine (isRegular_of_smul_left_injective f inj (sec (v i)).2).2 <|
    hf t (fun i ↦ _ * (sec (v i)).2) (fun i ↦ _ * (sec (v i)).2) ?_ i hit
  simp_rw [mul_smul, ← Submonoid.smul_def, hsec, ← map_smul, ← map_sum, eq]

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

Goal state before:
pp: R : Type u_1
inst✝¹⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : AddCommMonoid M'
inst✝¹⁴ : Module R M
inst✝¹³ : Module R M'
f : M →ₗ[R] M'
inst✝¹² : IsLocalizedModule S f
N : Type ?u.31
N' : Type ?u.33
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : AddCommMonoid N'
inst✝⁹ : Module R N
inst✝⁸ : Module R N'
g : N →ₗ[R] N'
inst✝⁷ : IsLocalizedModule S g
Rₛ : Type ?u.52
inst✝⁶ : CommSemiring Rₛ
inst✝⁵ : Algebra R Rₛ
inst✝⁴ : Module Rₛ M'
inst✝³ : Module Rₛ N'
inst✝² : IsScalarTower R Rₛ M'
inst✝¹ : IsScalarTower R Rₛ N'
inst✝ : IsLocalization S Rₛ
e : M ≃ₗ[R] N
⊢ ↑R ((mapExtendScalars S g f Rₛ) ↑e.symm ∘ₗ (mapExtendScalars S f g Rₛ) ↑e) = ↑R LinearMap.id

Tactic:
apply IsLocalizedModule.linearMap_ext S f f

Goal state after:
R : Type u_1
inst✝¹⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : AddCommMonoid M'
inst✝¹⁴ : Module R M
inst✝¹³ : Module R M'
f : M →ₗ[R] M'
inst✝¹² : IsLocalizedModule S f
N : Type ?u.31
N' : Type ?u.33
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : AddCommMonoid N'
inst✝⁹ : Module R N
inst✝⁸ : Module R N'
g : N →ₗ[R] N'
inst✝⁷ : IsLocalizedModule S g
Rₛ : Type ?u.52
inst✝⁶ : CommSemiring Rₛ
inst✝⁵ : Algebra R Rₛ
inst✝⁴ : Module Rₛ M'
inst✝³ : Module Rₛ N'
inst✝² : IsScalarTower R Rₛ M'
inst✝¹ : IsScalarTower R Rₛ N'
inst✝ : IsLocalization S Rₛ
e : M ≃ₗ[R] N
⊢ ↑R ((mapExtendScalars S g f Rₛ) ↑e.symm ∘ₗ (mapExtendScalars S f g Rₛ) ↑e) ∘ₗ f = ↑R LinearMap.id ∘ₗ f
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M : C
inst✝² : MonObj M
inst✝¹ : BraidedCategory C
inst✝ : IsCommMonObj M
⊢ (β_ M M).inv ≫ μ = μ

Tactic:
simp [← cancel_epi (β_ M M).hom]

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

Goal state before:
pp: case h₂
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 : B ⨿ X ⟶ s.pt
h₁ : coprod.map f (𝟙 X) ≫ m = s.inl
h₂ : coprod.inl ≫ m = s.inr
⊢ coprod.inr ≫ m = coprod.inr ≫ coprod.desc s.inr (coprod.inr ≫ s.inl)

Tactic:
· simp [← h₁]

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:
simp [snd, bimap_bimap]

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₁
g : β₀ → β₁
g' : β₁ → β₂
x : F α β₀
⊢ snd g' (snd g x) = snd (g' ∘ g) x

Tactic:
simp [snd, bimap_bimap]

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

Goal state before:
pp: case empty
R : Type u
inst✝² : CommSemiring R
ι : Type u_3
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Submonoid R
a : ι → A
s : ι → ↥S
⊢ ∏ i ∈ ∅, mk (a i) (s i) = mk (∏ i ∈ ∅, a i) (∏ i ∈ ∅, s i)

Tactic:
simp [OreLocalization.one_def, *, mk_mul_mk]

Goal state after: