mathlib-initiative/mathlib-tactics huggingface dataset:
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
a : S
⊢ ∃ b, IsInteger R (↑b • a)

Tactic:
by
  simp_rw [Algebra.smul_def, mul_comm _ a]
  apply exists_integer_multiple'

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 : C
inst✝¹ : MonObj M
inst✝ : MonObj N
⊢ (λ_ (𝟙_ C)).inv ▷ (M ⊗ N) ≫ tensorμ (𝟙_ C) (𝟙_ C) M N ≫ ((λ_ M).hom ⊗ₘ (λ_ N).hom) = (λ_ (M ⊗ N)).hom

Tactic:
symm

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
⊢ (λ_ (M ⊗ N)).hom = (λ_ (𝟙_ C)).inv ▷ (M ⊗ N) ≫ tensorμ (𝟙_ C) (𝟙_ C) M N ≫ ((λ_ M).hom ⊗ₘ (λ_ N).hom)
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 : C
inst✝¹ : MonObj M
inst✝ : MonObj N
⊢ (M ⊗ N) ◁ (λ_ (𝟙_ C)).inv ≫ tensorμ M N (𝟙_ C) (𝟙_ C) ≫ ((ρ_ M).hom ⊗ₘ (ρ_ N).hom) = (ρ_ (M ⊗ N)).hom

Tactic:
symm

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
⊢ (ρ_ (M ⊗ N)).hom = (M ⊗ N) ◁ (λ_ (𝟙_ C)).inv ≫ tensorμ M N (𝟙_ C) (𝟙_ C) ≫ ((ρ_ M).hom ⊗ₘ (ρ_ N).hom)
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : MonObj M
| μ ▷ 𝟙_ C ≫ (ρ_ M).hom

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : MonObj M
| tensorμ M (𝟙_ C) M (𝟙_ C)

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : MonObj M
| (M ⊗ M) ◁ (λ_ (𝟙_ C)).hom

Tactic:
rw [rightUnitor_naturality]

Goal state after:
case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : MonObj M
| (ρ_ (M ⊗ M)).hom ≫ μ

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : MonObj M
| tensorμ M (𝟙_ C) M (𝟙_ C)

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : MonObj M
| (M ⊗ M) ◁ (λ_ (𝟙_ C)).hom
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 : ∀ (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
t : Finset ι
g g' : ι → R
eq : ∑ i ∈ t, g i • (sec (v i)).1 = ∑ i ∈ t, g' i • (sec (v i)).1
i : ι
⊢ i ∈ t → g i = g' i

Tactic:
hit

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
t : Finset ι
g g' : ι → R
eq : ∑ i ∈ t, g i • (sec (v i)).1 = ∑ i ∈ t, g' i • (sec (v i)).1
i : ι
hit : i ∈ t
⊢ g i = g' i
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O X : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
A : Mon C
f : trivial C ⟶ A
⊢ 𝟙 (𝟙_ C) ≫ f.hom = η

Tactic:
rw [← trivial_mon_one, IsMonHom.one_hom]

Goal state after:
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

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

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
⊢ t₁.snd ≫ i₂ ≫ g₂ = t₁.snd ≫ t₂.snd ≫ i₃

Tactic:
← t₂.condition,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
⊢ t₁.snd ≫ i₂ ≫ g₂ = t₁.snd ≫ t₂.fst ≫ g₂
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
D : WalkingSpan ⥤ C
c : Cocone D
hc : IsColimit c
⊢ D.map WalkingSpan.Hom.fst ≫ c.ι.app WalkingSpan.left = D.map WalkingSpan.Hom.snd ≫ c.ι.app WalkingSpan.right

Tactic:
Cocone.w

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

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

Tactic:
← t₂.condition,

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone i₂ f₂
hi₂ : i₂ = t₁.inr
⊢ f₁ ≫ t₁.inr ≫ t₂.inl = f₁ ≫ f₂ ≫ t₂.inr

Tactic:
← t₂.condition,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone i₂ f₂
hi₂ : i₂ = t₁.inr
⊢ f₁ ≫ t₁.inr ≫ t₂.inl = f₁ ≫ i₂ ≫ t₂.inl
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: M : Type u_7
N : Type u_8
inst✝³ : Monoid M
inst✝² : Monoid N
F : Type u_9
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
⊢ map f (IsUnit.submonoid M) ≤ IsUnit.submonoid N

Tactic:
rintro x ⟨y, hy, rfl⟩

Goal state after:
M : Type u_7
N : Type u_8
inst✝³ : Monoid M
inst✝² : Monoid N
F : Type u_9
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
y : M
hy : y ∈ ↑(IsUnit.submonoid M)
⊢ f y ∈ IsUnit.submonoid N
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_7
S : Type u_8
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
⊢ algebraMapSubmonoid S (IsUnit.submonoid R) ≤ IsUnit.submonoid S

Tactic:
rintro x ⟨y, hy, rfl⟩

Goal state after:
R : Type u_7
S : Type u_8
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
y : R
hy : y ∈ ↑(IsUnit.submonoid R)
⊢ (algebraMap R S) y ∈ IsUnit.submonoid S
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
S : Submonoid A
N : Type u_7
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
g : M →ₗ[A] M'
h : IsLocalizedModule S g
⊢ IsLocalizedModule S ((AlgebraTensorModule.rTensor R N) g)

Tactic:
let Aₚ := Localization S

Goal state after:
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
S : Submonoid A
N : Type u_7
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
g : M →ₗ[A] M'
h : IsLocalizedModule S g
Aₚ : Type u_2 := Localization S
⊢ IsLocalizedModule S ((AlgebraTensorModule.rTensor R N) g)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case uniq.h₀
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
⊢ s.ι = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.fst

Tactic:
symm

Goal state after:
case uniq.h₀
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
⊢ H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.fst = s.ι
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case uniq.h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
⊢ s.ι = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.snd

Tactic:
symm

Goal state after:
case uniq.h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
⊢ H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.snd = s.ι
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

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

Tactic:
symm

Goal state after:
case uniq.h₀
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g ⋯).pt ⟶ s.pt
e : (Cofork.ofπ g ⋯).π ≫ m = s.π
⊢ H.cocone.inl ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯) = s.π
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

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

Tactic:
symm

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

Goal state before:
pp: F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α : Type u₀
⊢ ∀ {α_1 β : Type u₁}, mapConst = map ∘ Function.const β

Tactic:
simp [mapConst, Functor.map]

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case refine_2
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
⊢ ∃ n, (lift fun a ↦ if a ∈ s then 0 else X) (-1) = ↑n

Tactic:
use -1

Goal state after:
case h
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
⊢ (lift fun a ↦ if a ∈ s then 0 else X) (-1) = ↑(-1)
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case neg_one
α : Type u
⊢ ∃ a, ↑a = -1

Tactic:
use -1

Goal state after:
case h
α : Type u
⊢ ↑(-1) = -1
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✝ g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
m✝ : LocalizedModule S M
x✝² x✝¹ : M × ↥S
m : M
s : ↥S
m' : M
s' : ↥S
x✝ : (m, s) ≈ (m', s')
c : ↥S
eq1 : ↑c • ↑s' • m = ↑c • ↑s • m'
this : c • s • g m' = c • s' • g m
⊢ ↑(m, s).2 • g m' = ↑(m', s').2 • g m

Tactic:
have : Function.Injective (h c).unit.inv := ((Module.End.isUnit_iff _).1 (by simp)).1

Goal state after:
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✝ g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
m✝ : LocalizedModule S M
x✝² x✝¹ : M × ↥S
m : M
s : ↥S
m' : M
s' : ↥S
x✝ : (m, s) ≈ (m', s')
c : ↥S
eq1 : ↑c • ↑s' • m = ↑c • ↑s • m'
this✝ : c • s • g m' = c • s' • g m
this : Function.Injective ⇑⋯.unit.inv
⊢ ↑(m, s).2 • g m' = ↑(m', s').2 • g m
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✝ g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
m✝ : LocalizedModule S M
x✝² x✝¹ : M × ↥S
m : M
s : ↥S
m' : M
s' : ↥S
x✝ : (m, s) ≈ (m', s')
c : ↥S
eq1 : ↑c • ↑s' • m = ↑c • ↑s • m'
this✝ : c • s • g m' = c • s' • g m
this : Function.Injective ⇑⋯.unit.inv
⊢ ↑(m, s).2 • g m' = ↑⋯.unit⁻¹ (↑c • ↑(m', s').2 • g m)

Tactic:
symm

Goal state after:
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✝ g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
m✝ : LocalizedModule S M
x✝² x✝¹ : M × ↥S
m : M
s : ↥S
m' : M
s' : ↥S
x✝ : (m, s) ≈ (m', s')
c : ↥S
eq1 : ↑c • ↑s' • m = ↑c • ↑s • m'
this✝ : c • s • g m' = c • s' • g m
this : Function.Injective ⇑⋯.unit.inv
⊢ ↑⋯.unit⁻¹ (↑c • ↑(m', s').2 • g m) = ↑(m, s).2 • g m'
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case e_a
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ g (b' • a) = ↑⋯.unit⁻¹ (g (↑(b * b') • a))

Tactic:
symm

Goal state after:
case e_a
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ ↑⋯.unit⁻¹ (g (↑(b * b') • a)) = g (b' • a)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case e_a
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ g (b • a') = ↑⋯.unit⁻¹ (↑(b * b') • g a')

Tactic:
symm

Goal state after:
case e_a
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ ↑⋯.unit⁻¹ (↑(b * b') • g a') = g (b • a')
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
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M'
⊢ (iso S f).symm m = LocalizedModule.mk ⋯.choose.1 ⋯.choose.2

Tactic:
apply_fun iso S f using LinearEquiv.injective (iso S 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
m : M'
⊢ (iso S f) ((iso S f).symm m) = (iso S f) (LocalizedModule.mk ⋯.choose.1 ⋯.choose.2)
Module: Mathlib.Algebra.Category.Ring.Constructions

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

Tactic:
by
  algebraize [f, fₘ, fₘ.comp (algebraMap R Rₘ)]
  have : IsScalarTower R S Sₘ := .of_algebraMap_eq' H
  have : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ := ‹_›
  exact CommRingCat.isPushout_iff_isPushout.mpr (Algebra.isPushout_of_isLocalization M _ _ _)

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_6
M' : Type u_7
inst✝⁴ : NonUnitalNonAssocSemiring M
inst✝³ : Semiring M'
inst✝² : Module R M
inst✝¹ : Algebra R M'
f : M →ₗ[R] M'
hf : ∀ (m₁ m₂ : M), f (m₁ * m₂) = f m₁ * f m₂
inst✝ : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ mk' f m₁ s₁ * mk' f m₂ s₂ = mk' f (m₁ * m₂) (s₁ * s₂)

Tactic:
symm

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst✝⁴ : NonUnitalNonAssocSemiring M
inst✝³ : Semiring M'
inst✝² : Module R M
inst✝¹ : Algebra R M'
f : M →ₗ[R] M'
hf : ∀ (m₁ m₂ : M), f (m₁ * m₂) = f m₁ * f m₂
inst✝ : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ mk' f (m₁ * m₂) (s₁ * s₂) = mk' f m₁ s₁ * mk' f m₂ s₂
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case refine_2
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
x : ↑X
e : 0 = 1
⊢ (Hom.hom (ofHom { toMonoidHom := 1, map_zero' := ⋯, map_add' := ⋯ } ≫ f)) x = (Hom.hom (𝟙 X)) x

Tactic:
replace e : 0 * x = 1 * x := congr_arg (· * x) e

Goal state after:
case refine_2
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
x : ↑X
e : 0 * x = 1 * x
⊢ (Hom.hom (ofHom { toMonoidHom := 1, map_zero' := ⋯, map_add' := ⋯ } ≫ f)) x = (Hom.hom (𝟙 X)) x
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case property.right
A B : CommRingCat
f g : A ⟶ B
s : Fork f g
⊢ ∀ {m : s.pt ⟶ (equalizerFork f g).pt},
    m ≫ (equalizerFork f g).ι = s.ι → m = ofHom ((Hom.hom s.ι).codRestrict ((Hom.hom f).eqLocus (Hom.hom g)) ⋯)

Tactic:
intro m hm

Goal state after:
case property.right
A B : CommRingCat
f g : A ⟶ B
s : Fork f g
m : s.pt ⟶ (equalizerFork f g).pt
hm : m ≫ (equalizerFork f g).ι = s.ι
⊢ m = ofHom ((Hom.hom s.ι).codRestrict ((Hom.hom f).eqLocus (Hom.hom g)) ⋯)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_6
M : Type u_8
M' : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
S : Submonoid R
g : M →ₗ[R] M'
inst✝ : IsLocalizedModule S g
m : M
⊢ m ∈ g.ker ↔ ∃ r ∈ S, r • m = 0

Tactic:
simpa using IsLocalizedModule.eq_zero_iff S g

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case refine_1
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
⊢ adjoin A (⇑f '' Set.range MvPolynomial.X) = ⊤

Tactic:
eq_top_iff,

Goal state after:
case refine_1
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
⊢ ∀ (x : B), x ∈ adjoin A (⇑f '' Set.range MvPolynomial.X)
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: T : Type u_1
inst✝² : Category.{v_1, u_1} T
P Q W : MorphismProperty T
inst✝¹ : Q.IsMultiplicative
inst✝ : W.IsMultiplicative
A B : P.Arrow Q W
f g : A ⟶ B
hl : f.left = g.left
hr : f.right = g.right
⊢ f = g

Tactic:
ext
  · exact hl
  · exact hr

Goal state after: