mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : Ring S
f : R →+* S
J : Type u_3
inst✝¹ : Category.{v_1, u_3} J
F : J ⥤ ModuleCat S
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat S) AddCommGrpCat)
⊢ PreservesColimit F (restrictScalars f)

Tactic:
have : HasColimit ((F ⋙ restrictScalars f) ⋙ forget₂ (ModuleCat R) AddCommGrpCat) :=
    inferInstanceAs (HasColimit (F ⋙ forget₂ _ AddCommGrpCat))
  apply preservesColimit_of_preserves_colimit_cocone (HasColimit.isColimitColimitCocone F)
  apply isColimitOfReflects (forget₂ (ModuleCat.{v} R) AddCommGrpCat)
  apply isColimitOfPreserves (forget₂ (ModuleCat.{v} S) AddCommGrpCat.{v})
  exact HasColimit.isColimitColimitCocone F

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
⊢ (extendScalarsComp (RingHom.id R₁) f₁₂).hom ≫
      Functor.whiskerRight (extendScalarsId R₁).hom (extendScalars f₁₂) ≫ (extendScalars f₁₂).leftUnitor.hom =
    𝟙 (extendScalars (f₁₂.comp (RingHom.id R₁)))

Tactic:
by
  ext M m
  dsimp
  erw [extendScalarsComp_hom_app_one_tmul (RingHom.id R₁) f₁₂ M m]
  rw [ExtendScalars.map_tmul]
  erw [extendScalarsId_hom_app_one_tmul]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Category.Pointed

Goal state before:
pp: X'✝ X✝ : Type ?u.36
Y✝ : Pointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget Pointed).obj Y✝
x : (typeToPointed.obj X'✝).X
⊢ ({ toFun := fun f ↦ ↾(f.toFun ∘ some),
              invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.point ⇑(ConcreteCategory.hom f), map_point := ⋯ },
              left_inv := ⋯, right_inv := ⋯ }.symm
          (f ≫ g)).toFun
      x =
    (typeToPointed.map f ≫
          { toFun := fun f ↦ ↾(f.toFun ∘ some),
                invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.point ⇑(ConcreteCategory.hom f), map_point := ⋯ },
                left_inv := ⋯, right_inv := ⋯ }.symm
            g).toFun
      x

Tactic:
cases x <;> rfl

Goal state after:
Module: Mathlib.CategoryTheory.Category.Bipointed

Goal state before:
pp: X : Pointed
Y : Bipointed
f : pointedToBipointedFst.obj X ⟶ Y
⊢ (fun f ↦ { toFun := fun o ↦ Option.elim o Y.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ })
      ((fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ }) f) =
    f

Tactic:
apply Bipointed.Hom.ext

Goal state after:
X : Pointed
Y : Bipointed
f : pointedToBipointedFst.obj X ⟶ Y
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ })
        ((fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ }) f)).toFun =
    f.toFun
Module: Mathlib.CategoryTheory.Category.Bipointed

Goal state before:
pp: X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedFst.obj Y✝
⊢ { toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
          invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ },
          left_inv := ⋯, right_inv := ⋯ }.symm
      (f ≫ g) =
    pointedToBipointedFst.map f ≫
      { toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
            invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ },
            left_inv := ⋯, right_inv := ⋯ }.symm
        g

Tactic:
apply Bipointed.Hom.ext

Goal state after:
X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedFst.obj Y✝
⊢ ({ toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
            invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ },
            left_inv := ⋯, right_inv := ⋯ }.symm
        (f ≫ g)).toFun =
    (pointedToBipointedFst.map f ≫
        { toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
              invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ },
              left_inv := ⋯, right_inv := ⋯ }.symm
          g).toFun
Module: Mathlib.CategoryTheory.Category.Bipointed

Goal state before:
pp: X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedFst.obj Y✝
x : (pointedToBipointedFst.obj X'✝).X
⊢ ({ toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
              invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ },
              left_inv := ⋯, right_inv := ⋯ }.symm
          (f ≫ g)).toFun
      x =
    (pointedToBipointedFst.map f ≫
          { toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
                invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ },
                left_inv := ⋯, right_inv := ⋯ }.symm
            g).toFun
      x

Tactic:
cases x <;> rfl

Goal state after:
Module: Mathlib.CategoryTheory.Category.Bipointed

Goal state before:
pp: X : Pointed
Y : Bipointed
f : pointedToBipointedSnd.obj X ⟶ Y
⊢ (fun f ↦ { toFun := fun o ↦ Option.elim o Y.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ })
      ((fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ }) f) =
    f

Tactic:
apply Bipointed.Hom.ext

Goal state after:
X : Pointed
Y : Bipointed
f : pointedToBipointedSnd.obj X ⟶ Y
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ })
        ((fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ }) f)).toFun =
    f.toFun
Module: Mathlib.CategoryTheory.Category.Bipointed

Goal state before:
pp: X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedSnd.obj Y✝
⊢ { toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
          invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ },
          left_inv := ⋯, right_inv := ⋯ }.symm
      (f ≫ g) =
    pointedToBipointedSnd.map f ≫
      { toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
            invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ },
            left_inv := ⋯, right_inv := ⋯ }.symm
        g

Tactic:
apply Bipointed.Hom.ext

Goal state after:
X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedSnd.obj Y✝
⊢ ({ toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
            invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ },
            left_inv := ⋯, right_inv := ⋯ }.symm
        (f ≫ g)).toFun =
    (pointedToBipointedSnd.map f ≫
        { toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
              invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ },
              left_inv := ⋯, right_inv := ⋯ }.symm
          g).toFun
Module: Mathlib.CategoryTheory.Category.Bipointed

Goal state before:
pp: X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedSnd.obj Y✝
x : (pointedToBipointedSnd.obj X'✝).X
⊢ ({ toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
              invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ },
              left_inv := ⋯, right_inv := ⋯ }.symm
          (f ≫ g)).toFun
      x =
    (pointedToBipointedSnd.map f ≫
          { toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
                invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ },
                left_inv := ⋯, right_inv := ⋯ }.symm
            g).toFun
      x

Tactic:
cases x <;> rfl

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
f g : HeytingHom α β
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f; obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g; congr

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f g : CoheytingHom α β
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f; obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g; congr

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
f g : BiheytingHom α β
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f; obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g; congr

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M : C
inst✝ : ComonObj M
Z : C
f : M ⟶ Z
⊢ Δ ≫ (f ⊗ₘ ε) = f ≫ (ρ_ Z).inv

Tactic:
rw [rightUnitor_inv_naturality, tensorHom_def', comul_counit_assoc]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case inl
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
x : R
n : ℕ
hnorm : normalize 0 = 0
hle : 0 ^ n ∣ x
hlt : ¬0 ^ (n + 1) ∣ x
⊢ count 0 (normalizedFactors x) = n

Tactic:
cases n
    · exact count_eq_zero.2 (zero_notMem_normalizedFactors _)
    · rw [zero_pow (Nat.succ_ne_zero _)] at hle hlt
      exact absurd hle hlt

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
P : Type u_3
inst✝⁶ : CommSemiring P
Q : Type u_4
inst✝⁵ : CommSemiring Q
inst✝⁴ : Algebra P Q
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
⊢ (∀ (a : S), (map S Q f r) a = 0 → a = 0) ↔ ∀ (a : R), f a = 0 → ∃ n, r ^ n * a = 0

Tactic:
trans ∀ a n, f r ^ n * f a = 0 → ∃ m, r ^ m * a = 0

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
P : Type u_3
inst✝⁶ : CommSemiring P
Q : Type u_4
inst✝⁵ : CommSemiring Q
inst✝⁴ : Algebra P Q
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
⊢ (∀ (a : S), (map S Q f r) a = 0 → a = 0) ↔ ∀ (a : R) (n : ℕ), f r ^ n * f a = 0 → ∃ m, r ^ m * a = 0

R : Type u_1
inst✝⁷ : CommSemiring R
P : Type u_3
inst✝⁶ : CommSemiring P
Q : Type u_4
inst✝⁵ : CommSemiring Q
inst✝⁴ : Algebra P Q
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
⊢ (∀ (a : R) (n : ℕ), f r ^ n * f a = 0 → ∃ m, r ^ m * a = 0) ↔ ∀ (a : R), f a = 0 → ∃ n, r ^ n * a = 0
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)
eq2 : ∀ (a b : ↑↑s), r a * ↑b ^ N = r b * ↑a ^ N
c : ↑↑s → R
eq1 : ∑ i, c i • ↑i ^ N = 1
a : ↑↑s
⊢ (algebraMap R (Away ↑a)) (r a * ∑ i, c i * ↑i ^ N) = (algebraMap R (Away ↑a)) (r a)

Tactic:
← smul_eq_mul (a := c _),

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)
eq2 : ∀ (a b : ↑↑s), r a * ↑b ^ N = r b * ↑a ^ N
c : ↑↑s → R
eq1 : ∑ i, c i • ↑i ^ N = 1
a : ↑↑s
⊢ (algebraMap R (Away ↑a)) (r a * ∑ x, c x • ↑x ^ N) = (algebraMap R (Away ↑a)) (r a)
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : n < 0
hm : m < 0
⊢ mk' B 1 (Submonoid.pow x (n.natAbs + m.natAbs)) =
    mk' B 1 (Submonoid.pow x n.natAbs) * mk' B 1 (Submonoid.pow x m.natAbs)

Tactic:
← mk'_mul,

Goal state after:
case inr.inr
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : n < 0
hm : m < 0
⊢ mk' B 1 (Submonoid.pow x (n.natAbs + m.natAbs)) = mk' B (1 * 1) (Submonoid.pow x n.natAbs * Submonoid.pow x m.natAbs)
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M X Y : C
inst✝ : MonObj M
e : M ≅ X
⊢ X ◁ (η ≫ e.hom) ≫ (e.inv ⊗ₘ e.inv) ≫ μ ≫ e.hom = (ρ_ X).hom

Tactic:
← cancel_epi (ρ_ X).inv

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M X Y : C
inst✝ : MonObj M
e : M ≅ X
⊢ (ρ_ X).inv ≫ X ◁ (η ≫ e.hom) ≫ (e.inv ⊗ₘ e.inv) ≫ μ ≫ e.hom = (ρ_ X).inv ≫ (ρ_ X).hom
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: case mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : C
one✝¹ : 𝟙_ C ⟶ X
mul✝¹ : X ⊗ X ⟶ X
one_mul✝¹ : one✝¹ ▷ X ≫ mul✝¹ = (λ_ X).hom
mul_one✝¹ : X ◁ one✝¹ ≫ mul✝¹ = (ρ_ X).hom
mul_assoc✝¹ : mul✝¹ ▷ X ≫ mul✝¹ = (α_ X X X).hom ≫ X ◁ mul✝¹ ≫ mul✝¹
one✝ : 𝟙_ C ⟶ X
mul✝ : X ⊗ X ⟶ X
one_mul✝ : one✝ ▷ X ≫ mul✝ = (λ_ X).hom
mul_one✝ : X ◁ one✝ ≫ mul✝ = (ρ_ X).hom
mul_assoc✝ : mul✝ ▷ X ≫ mul✝ = (α_ X X X).hom ≫ X ◁ mul✝ ≫ mul✝
H : μ = μ
this : η = η
⊢ { one := one✝¹, mul := mul✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹, mul_assoc := mul_assoc✝¹ } =
    { one := one✝, mul := mul✝, one_mul := one_mul✝, mul_one := mul_one✝, mul_assoc := mul_assoc✝ }

Tactic:
subst H this

Goal state after:
case mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : C
one✝ : 𝟙_ C ⟶ X
mul✝ : X ⊗ X ⟶ X
one_mul✝¹ : one✝ ▷ X ≫ mul✝ = (λ_ X).hom
mul_one✝¹ : X ◁ one✝ ≫ mul✝ = (ρ_ X).hom
mul_assoc✝¹ : mul✝ ▷ X ≫ mul✝ = (α_ X X X).hom ≫ X ◁ mul✝ ≫ mul✝
mul_assoc✝ : μ ▷ X ≫ μ = (α_ X X X).hom ≫ X ◁ μ ≫ μ
one_mul✝ : η ▷ X ≫ μ = (λ_ X).hom
mul_one✝ : X ◁ η ≫ μ = (ρ_ X).hom
⊢ { one := one✝, mul := mul✝, one_mul := one_mul✝¹, mul_one := mul_one✝¹, mul_assoc := mul_assoc✝¹ } =
    { one := η, mul := μ, one_mul := one_mul✝, mul_one := mul_one✝, mul_assoc := mul_assoc✝ }
Module: Mathlib.RingTheory.Localization.Integer

Goal state before:
pp: case refine_2.e_a
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
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ ∏ x ∈ insert i (s.erase i), ↑(sec M (f x)).2 = ∏ x ∈ s, M.subtype (sec M (f x)).2

Tactic:
Finset.insert_erase hi

Goal state after:
case refine_2.e_a
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
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ ∏ x ∈ s, ↑(sec M (f x)).2 = ∏ x ∈ s, M.subtype (sec M (f x)).2
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : MonObj M
⊢ (tensorμ M (𝟙_ C) M (𝟙_ C) ≫ (M ⊗ M) ◁ (λ_ (𝟙_ C)).hom ≫ μ ▷ 𝟙_ C) ≫ (ρ_ M).hom =
    ((ρ_ M).hom ⊗ₘ (ρ_ M).hom) ≫ 𝟙 (M ⊗ M) ≫ μ

Tactic:
slice_lhs 3 4 => rw [rightUnitor_naturality]

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

Tactic:
by simp [Functor.map, functor_norm]

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₀
⊢ ∀ {α_1 β γ : Type u₁} (g : α_1 → β) (h : β → γ) (x : F α α_1), (h ∘ g) <$> x = h <$> g <$> x

Tactic:
by simp [Functor.map, functor_norm]

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case refine_4
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
⊢ ∀ {x y : FreeCommRing α},
    (∃ n, (lift fun a ↦ if a ∈ s then 0 else X) x = ↑n) →
      (∃ n, (lift fun a ↦ if a ∈ s then 0 else X) y = ↑n) → ∃ n, (lift fun a ↦ if a ∈ s then 0 else X) (x + y) = ↑n

Tactic:
· rintro x y ⟨q, hq⟩ ⟨r, hr⟩
      refine ⟨q + r, ?_⟩
      rw [map_add, hq, hr]
      norm_cast

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

Goal state before:
pp: case h
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
m : M
s : ↥S
⊢ 0 • mk m s = 0

Tactic:
show (0 : T) = IsLocalization.mk' T (0 : R) (1 : S) by rw [IsLocalization.mk'_zero],

Goal state after:
case h
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
m : M
s : ↥S
⊢ IsLocalization.mk' T 0 1 • mk m s = 0
Module: Mathlib.Algebra.Group.Submonoid.Units

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
x : Gˣ
⊢ ↑x ∈ H ∧ ↑x⁻¹ ∈ H ↔ ↑x ∈ H

Tactic:
val_inv_eq_inv_val,

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup G
x : Gˣ
⊢ ↑x ∈ H ∧ (↑x)⁻¹ ∈ H ↔ ↑x ∈ H
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : AddCommMonoid M''
A : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Module A M'
inst✝⁴ : IsLocalization S A
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
inst✝ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
x₁✝ x₂✝ : M
h : (↑e ∘ₗ f) x₁✝ = (↑e ∘ₗ f) x₂✝
⊢ ∃ c, c • x₁✝ = c • x₂✝

Tactic:
simp_rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
      EmbeddingLike.apply_eq_iff_eq] at h

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 : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
x₁✝ x₂✝ : M
h : f x₁✝ = f x₂✝
⊢ ∃ c, c • x₁✝ = c • x₂✝
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: A B : CommRingCat
s : Cone (pair A B)
m : s.pt ⟶ (A.prodFan B).pt
h : ∀ (j : Discrete WalkingPair), m ≫ (A.prodFan B).π.app j = s.π.app j
x : ↑s.pt
eq1 : (ConcreteCategory.hom (m ≫ (A.prodFan B).fst)) x = (ConcreteCategory.hom (BinaryFan.fst s)) x
eq2 : (ConcreteCategory.hom (m ≫ (A.prodFan B).snd)) x = (ConcreteCategory.hom (BinaryFan.snd s)) x
⊢ (ConcreteCategory.hom m) x =
    ((ConcreteCategory.hom (m ≫ (A.prodFan B).fst)) x, (ConcreteCategory.hom (m ≫ (A.prodFan B).snd)) x)

Tactic:
simp [prodFan]

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

Goal state before:
pp: J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
j k : J
f : j ⟶ k
h : (ConcreteCategory.hom (c.π.app k)) r * (ConcreteCategory.hom (F.map f)) (inv j) = 1
this : (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (c.π.app j)) r) = (ConcreteCategory.hom (c.π.app k)) r
⊢ (ConcreteCategory.hom (F.map f)) (inv j) * (ConcreteCategory.hom (c.π.app k)) r * inv k = inv k

Tactic:
nth_rw 2 [mul_comm]

Goal state after:
J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
j k : J
f : j ⟶ k
h : (ConcreteCategory.hom (c.π.app k)) r * (ConcreteCategory.hom (F.map f)) (inv j) = 1
this : (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (c.π.app j)) r) = (ConcreteCategory.hom (c.π.app k)) r
⊢ (ConcreteCategory.hom (c.π.app k)) r * (ConcreteCategory.hom (F.map f)) (inv j) * inv k = inv k
Module: Mathlib.RingTheory.Finiteness.Ideal

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
⊢ ∀ (J : Ideal R), J.FG → J ≤ I.radical → ∃ n, J ^ n ≤ I

Tactic:
intro J hJ hJK

Goal state after:
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J : Ideal R
hJ : J.FG
hJK : J ≤ I.radical
⊢ ∃ n, J ^ n ≤ I
Module: Mathlib.RingTheory.Finiteness.Ideal

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J : Ideal R
x : R
hJK : R ∙ x ≤ I.radical
n : ℕ
hn : x ^ n ∈ I
⊢ (R ∙ x) ^ n ≤ I

Tactic:
by rwa [← span, span_singleton_pow, span_le, Set.singleton_subset_iff]

Goal state after:
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
⊢ (eval₂Hom (algebraMap R B) (⇑(algebraMap A B) ∘ x)) p = (algebraMap A B) ((eval₂Hom (algebraMap R A) x) p)

Tactic:
map_eval₂Hom,

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
⊢ (eval₂Hom (algebraMap R B) (⇑(algebraMap A B) ∘ x)) p =
    (eval₂Hom ((algebraMap A B).comp (algebraMap R A)) fun i ↦ (algebraMap A B) (x i)) p
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
P Q : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{w, v, u} P
inst✝ : ObjectProperty.Small.{w, v, u} Q
⊢ Function.Surjective fun x ↦
    match x with
    | Sum.inl x => ⟨↑x, ⋯⟩
    | Sum.inr x => ⟨↑x, ⋯⟩

Tactic:
by rintro ⟨x, hx | hx⟩ <;> aesop

Goal state after: