mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Finset R
f : (a : ↑↑s) → Away ↑a
h : ∀ (a b : ↑↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span ↑s
span_eq : Ideal.span ↑s = ⊤
n : ↑↑s → ℕ
r✝¹ : ↑↑s → R
eq✝¹ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) ↑a ^ n a = (algebraMap R (Away ↑a)) (r✝¹ a)
N✝ : ℕ := s.attach.sup n
r✝ : ↑↑s → R := fun a ↦ ↑a ^ (N✝ - n a) * r✝¹ a
eq✝ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N✝) = (algebraMap R (Away ↑a)) (r✝ a)
N'✝ : ↑↑s → ↑↑s → ℕ
hN' : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N'✝ a b * (r✝ a * ↑b ^ N✝) = (↑a * ↑b) ^ N'✝ a b * (r✝ b * ↑a ^ N✝)
N' : ℕ := (s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩
eq2 : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N' * (r✝ a * ↑b ^ N✝) = (↑a * ↑b) ^ N' * (r✝ b * ↑a ^ N✝)
N : ℕ := N' + N✝
r : ↑↑s → R := fun a ↦ ↑a ^ N' * r✝ a
eq : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N) = (algebraMap R (Away ↑a)) (r a)
a b : ↑↑s
⊢ (↑a * ↑b) ^ N' * (r✝ b * ↑a ^ N✝) = r b * ↑a ^ N

Tactic:
mul_comm a.1,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Finset R
f : (a : ↑↑s) → Away ↑a
h : ∀ (a b : ↑↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span ↑s
span_eq : Ideal.span ↑s = ⊤
n : ↑↑s → ℕ
r✝¹ : ↑↑s → R
eq✝¹ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) ↑a ^ n a = (algebraMap R (Away ↑a)) (r✝¹ a)
N✝ : ℕ := s.attach.sup n
r✝ : ↑↑s → R := fun a ↦ ↑a ^ (N✝ - n a) * r✝¹ a
eq✝ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N✝) = (algebraMap R (Away ↑a)) (r✝ a)
N'✝ : ↑↑s → ↑↑s → ℕ
hN' : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N'✝ a b * (r✝ a * ↑b ^ N✝) = (↑a * ↑b) ^ N'✝ a b * (r✝ b * ↑a ^ N✝)
N' : ℕ := (s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩
eq2 : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N' * (r✝ a * ↑b ^ N✝) = (↑a * ↑b) ^ N' * (r✝ b * ↑a ^ N✝)
N : ℕ := N' + N✝
r : ↑↑s → R := fun a ↦ ↑a ^ N' * r✝ a
eq : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N) = (algebraMap R (Away ↑a)) (r a)
a b : ↑↑s
⊢ (↑b * ↑a) ^ N' * (r✝ b * ↑a ^ N✝) = r b * ↑a ^ N
Module: Mathlib.RingTheory.LocalRing.RingHom.Basic

Goal state before:
pp: R✝ : Type u_1
S : Type u_2
T : Type u_3
K : Type u_4
R : Type u_5
inst✝² : DivisionRing K
inst✝¹ : CommRing R
inst✝ : Nontrivial R
f : K →+* R
r : K
hr : IsUnit (f r)
⊢ IsUnit r

Tactic:
simpa only [isUnit_iff_ne_zero, ne_eq, map_eq_zero] using hr.ne_zero

Goal state after:
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 N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| (M ⊗ N) ◁ (η ⊗ₘ η) ≫ tensorμ M N M N

pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| μ ⊗ₘ μ

pp: case a
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

Tactic:
tensorμ_natural_right

Goal state after:
case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| tensorμ M N (𝟙_ C) (𝟙_ C) ≫ (M ◁ η ⊗ₘ N ◁ η)

case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| μ ⊗ₘ μ

case a
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
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
hv : LinearIndependent R v
h : ∀ (s : ↥S), IsRegular ↑s
⊢ Set.InjOn ⇑f ↑(span R (Set.range v))

Tactic:
by
    rw [← Finsupp.range_linearCombination]
    rintro _ ⟨_, r, rfl⟩ _ ⟨_, r', rfl⟩ eq
    congr; ext i
    have ⟨s, eq⟩ := IsLocalizedModule.exists_of_eq (S := S) eq
    simp_rw [Submonoid.smul_def, ← map_smul] at eq
    exact (h s).1 (DFunLike.congr_fun (hv eq) i)

Goal state after:
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₁ : Y₁ ⟶ X₁
t₁ : PullbackCone i₁ f₁
i₂ : t₁.pt ⟶ X₂
t₂ : PullbackCone «i₂» f₂
hi₂ : «i₂» = t₁.snd
H₁ : IsLimit t₁
H₂ : IsLimit t₂
⊢ IsLimit (t₁.pasteVert t₂ hi₂)

Tactic:
by
  apply PullbackCone.isLimitOfFlip <| IsLimit.ofIsoLimit _ (t₁.pasteVertFlip t₂ hi₂).symm
  exact pasteHorizIsPullback hi₂ (PullbackCone.flipIsLimit H₁) (PullbackCone.flipIsLimit H₂)

Goal state after:
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✝
R : Type u_7
S : Type u_8
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
r : R
A : Type u_9
inst✝¹¹ : CommSemiring A
inst✝¹⁰ : Algebra R A
M : Submonoid A
B : Type u_10
inst✝⁹ : CommSemiring B
inst✝⁸ : Algebra R B
inst✝⁷ : Algebra A B
inst✝⁶ : IsScalarTower R A B
inst✝⁵ : IsLocalization M B
C : Type u_11
inst✝⁴ : CommSemiring C
inst✝³ : Algebra S C
inst✝² : Algebra (S ⊗[R] A) C
inst✝¹ : IsScalarTower S (S ⊗[R] A) C
inst✝ : IsLocalization (Submonoid.map Algebra.TensorProduct.includeRight M) C
M' : Submonoid (S ⊗[R] A) := Submonoid.map Algebra.TensorProduct.includeRight M
this✝ : Algebra (S ⊗[R] A) (S ⊗[R] B) :=
  (Algebra.TensorProduct.map (AlgHom.id R S) (IsScalarTower.toAlgHom R A B)).toAlgebra
this : IsScalarTower S (S ⊗[R] A) (S ⊗[R] B)
⊢ (algebraMap (S ⊗[R] A) (S ⊗[R] B)).comp Algebra.TensorProduct.includeRight.toRingHom =
    Algebra.TensorProduct.includeRight.comp (algebraMap A B)

Tactic:
ext; simp [RingHom.algebraMap_toAlgebra]

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

Goal state before:
pp: 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 : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : ReflectsColimit (span f g) F
e : f ≫ h = g ≫ i
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
⊢ IsPushout f g h i

Tactic:
by
  refine ⟨⟨e⟩, ⟨isColimitOfReflects F <| ?_⟩⟩
  refine
    (IsColimit.equivOfNatIsoOfIso (spanCompIso F f g) _ _ (WalkingSpan.ext ?_ ?_ ?_)).symm
      H.isColimit
  exacts [Iso.refl _, (Category.comp_id _).trans (Category.id_comp _),
    (Category.comp_id _).trans (Category.id_comp _)]

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

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

Tactic:
zero_mul

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
z : α
hzs : z ∈ s
n✝ : FreeCommRing α
a✝ : ∃ n, (lift fun a ↦ if a ∈ s then 0 else X) n✝ = ↑n
⊢ 0 = ↑0
Module: Mathlib.RingTheory.FreeCommRing

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

Tactic:
rintro _ ⟨p, hps, rfl⟩ n ih

Goal state after:
case refine_3
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hxs : x.IsSupported s
p : α
hps : p ∈ s
n : FreeCommRing α
ih : (map Subtype.val) ((restriction s) n) = n
⊢ (map Subtype.val) ((restriction s) (of p * n)) = of p * n
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 m₁ t₁ + mk m₂ t₂).liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯ =
    (mk m₁ t₁).liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯ + (mk m₂ t₂).liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯

Tactic:
simp_rw [mk_add_mk, LocalizedModule.liftOn_mk, mk_add_mk, mul_smul, mul_comm _ s, mul_assoc,
      smul_comm _ s, ← smul_add, mul_left_comm s t₁ t₂, mk_cancel_common_left s]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Basic

Goal state before:
pp: case a.a.a.a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
| T.map (i.hom.app X) ≫ T.map (i.inv.app X)

pp: case a.a.a.a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
| T.μ.app X

pp: case a.a.a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
| i.hom.app X

pp: case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
| T.map (i.inv.app (F.obj X))

pp: case a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
| T.map (T.map (i.inv.app X))

pp: case a.a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
| T.map (T.μ.app X)

Tactic:
← T.map_comp

Goal state after:
case a.a.a.a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
| T.map (i.hom.app X ≫ i.inv.app X)

case a.a.a.a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
| T.μ.app X

case a.a.a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
| i.hom.app X

case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
| T.map (i.inv.app (F.obj X))

case a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
| T.map (T.map (i.inv.app X))

case a.a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
| T.map (T.μ.app X)
Module: Mathlib.CategoryTheory.Monad.Basic

Goal state before:
pp: case a.a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
| T.map (i.inv.app (F.obj X)) ≫ T.map (T.map (i.inv.app X))

pp: case a.a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
| T.map (T.μ.app X)

pp: case a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
| T.μ.app X

pp: case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
| i.hom.app X

Tactic:
← T.map_comp

Goal state after:
case a.a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
| T.map (i.inv.app (F.obj X) ≫ T.map (i.inv.app X))

case a.a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
| T.map (T.μ.app X)

case a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
| T.μ.app X

case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
| i.hom.app X
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case inl
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ of A ⟶ of (A ⊗[R] B)

pp: case inr
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ of B ⟶ of (A ⊗[R] B)

pp: case eq
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ ofHom (algebraMap R A) ≫ ?inl = ofHom (algebraMap R B) ≫ ?inr

Tactic:
· exact ofHom <| Algebra.TensorProduct.includeLeftRingHom (A := A)

Goal state after:
case inr
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ of B ⟶ of (A ⊗[R] B)

case eq
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ ofHom (algebraMap R A) ≫ ofHom Algebra.TensorProduct.includeLeftRingHom = ofHom (algebraMap R B) ≫ ?inr
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: R : CommRingCat
x✝ : of (ULift.{u, 0} ℤ) ⟶ R
⊢ x✝ = default

Tactic:
by
      ext : 1
      rw [← RingHom.cancel_right (f := (ULift.ringEquiv.{0, u} (R := ℤ)).symm.toRingHom)
        (hf := ULift.ringEquiv.symm.surjective)]
      apply RingHom.ext_int

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : PrelaxFunctor B C
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ F.map₂ η.hom ≫ F.map₂ η.inv = 𝟙 (F.map f)

Tactic:
← F.map₂_comp,

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : PrelaxFunctor B C
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ F.map₂ (η.hom ≫ η.inv) = 𝟙 (F.map f)
Module: Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : PrelaxFunctor B C
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ F.map₂ η.inv ≫ F.map₂ η.hom = 𝟙 (F.map g)

Tactic:
← F.map₂_comp,

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : PrelaxFunctor B C
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ F.map₂ (η.inv ≫ η.hom) = 𝟙 (F.map g)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst✝⁹ : AddCommMonoid M₀
inst✝⁸ : AddCommMonoid M₀'
inst✝⁷ : Module R M₀
inst✝⁶ : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst✝⁵ : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_8
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁
inst✝¹ : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst✝ : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
m : M₀
s : ↥S
⊢ ↑s • ((map S f₀ f₁) g ∘ₗ ↑(iso S f₀)) (LocalizedModule.mk m s) =
    ↑s • (↑(iso S f₁) ∘ₗ (map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m s)

Tactic:
← CompatibleSMul.map_smul,

Goal state after:
case h
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst✝⁹ : AddCommMonoid M₀
inst✝⁸ : AddCommMonoid M₀'
inst✝⁷ : Module R M₀
inst✝⁶ : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst✝⁵ : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_8
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁
inst✝¹ : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst✝ : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
m : M₀
s : ↥S
⊢ ((map S f₀ f₁) g ∘ₗ ↑(iso S f₀)) (↑s • LocalizedModule.mk m s) =
    ↑s • (↑(iso S f₁) ∘ₗ (map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m s)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst✝⁹ : AddCommMonoid M₀
inst✝⁸ : AddCommMonoid M₀'
inst✝⁷ : Module R M₀
inst✝⁶ : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst✝⁵ : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_8
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁
inst✝¹ : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst✝ : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
m : M₀
s : ↥S
⊢ ((map S f₀ f₁) g ∘ₗ ↑(iso S f₀)) (↑s • LocalizedModule.mk m s) =
    ↑s • (↑(iso S f₁) ∘ₗ (map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m s)

Tactic:
← CompatibleSMul.map_smul,

Goal state after:
case h
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst✝⁹ : AddCommMonoid M₀
inst✝⁸ : AddCommMonoid M₀'
inst✝⁷ : Module R M₀
inst✝⁶ : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst✝⁵ : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_8
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁
inst✝¹ : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst✝ : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
m : M₀
s : ↥S
⊢ ((map S f₀ f₁) g ∘ₗ ↑(iso S f₀)) (↑s • LocalizedModule.mk m s) =
    (↑(iso S f₁) ∘ₗ (map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (↑s • LocalizedModule.mk m s)
Module: Mathlib.CategoryTheory.Limits.ConeCategory

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X✝ Y✝ : StructuredArrow F (const J)
f : X✝ ⟶ Y✝
j : J
⊢ { pt := X✝.right, ι := X✝.hom }.ι.app j ≫ StructuredArrow.Hom.right f = { pt := Y✝.right, ι := Y✝.hom }.ι.app j

Tactic:
by simp [dsimp% congr_app f.w j]

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

Goal state before:
pp: case exists_of_eq
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
x y : S
⊢ (∃ m, m • x - m • y = 0) → ∃ c, c • x = c • y

Tactic:
sub_eq_zero

Goal state after:
case exists_of_eq
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
x y : S
⊢ (∃ m, m • x = m • y) → ∃ c, c • x = c • y
Module: Mathlib.RingTheory.MvPolynomial.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra R B
inst✝³ : IsScalarTower R A B
inst✝² : IsDomain A
inst✝¹ : Module.IsTorsionFree A B
inst✝ : Nontrivial B
x : σ → A
p : MvPolynomial σ R
⊢ (aeval (⇑(algebraMap A B) ∘ x)) p = 0 ↔ (aeval x) p = 0

Tactic:
aeval_algebraMap_apply,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra R B
inst✝³ : IsScalarTower R A B
inst✝² : IsDomain A
inst✝¹ : Module.IsTorsionFree A B
inst✝ : Nontrivial B
x : σ → A
p : MvPolynomial σ R
⊢ (algebraMap A B) ((aeval x) p) = 0 ↔ (aeval x) p = 0
Module: Mathlib.RingTheory.MvPolynomial.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : σ → A
p : MvPolynomial σ R
h : Function.Injective ⇑(algebraMap A B)
⊢ (aeval (⇑(algebraMap A B) ∘ x)) p = 0 ↔ (aeval x) p = 0

Tactic:
aeval_algebraMap_apply,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : σ → A
p : MvPolynomial σ R
h : Function.Injective ⇑(algebraMap A B)
⊢ (algebraMap A B) ((aeval x) p) = 0 ↔ (aeval x) p = 0
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: 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
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
⊢ adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤

Tactic:
rw [adjoin_union_eq_adjoin_adjoin, ← Subalgebra.restrictScalars_top R (A := AX)
        (S := { x // x ∈ adjoin R ((algebraMap A AX) '' t) })]

Goal state after:
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
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
⊢ Subalgebra.restrictScalars R (adjoin (↥(adjoin R (⇑(algebraMap A AX) '' ↑t))) (Set.range MvPolynomial.X)) =
    Subalgebra.restrictScalars R ⊤