mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Order.Group

Goal state before:
pp: G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a b ε : G
hε : ε > 1
hε_min : ∀ a < ε, a ≤ 1
this : ∀ (x : G), ∀ᶠ (y : G) in 𝓝 x, y = x
⊢ ∀ (a_1 : G × G), a_1.1 = a ∧ a_1.2 = b → |a_1.1 * a_1.2 / (a * b)|ₘ < ε

Tactic:
simp [hε]

Goal state after:
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: case neg
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
ha : ¬IsTop a
⊢ 𝓝[>] a = ⊥ ↔ ∃ b, a ⋖ b

Tactic:
rw [isTop_iff_isMax, not_isMax_iff] at ha

Goal state after:
case neg
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
ha : ∃ b, a < b
⊢ 𝓝[>] a = ⊥ ↔ ∃ b, a ⋖ b
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁵ : Semifield 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
inst✝ : ContinuousMul 𝕜
⊢ (∀ a' < 1, ∀ᶠ (b : 𝕜) in 𝓝 1, a' < b⁻¹) ∧ ∀ a' > 1, ∀ᶠ (b : 𝕜) in 𝓝 1, b⁻¹ < a'

Tactic:
by
  refine ⟨fun x hx => ?_, fun x hx => ?_⟩
  · obtain ⟨x', h₀, hxx', h₁⟩ : ∃ x', 0 < x' ∧ x ≤ x' ∧ x' < 1 :=
      ⟨max x (1 / 2), one_half_pos.trans_le (le_max_right _ _), le_max_left _ _,
        max_lt hx one_half_lt_one⟩
    filter_upwards [Ioo_mem_nhds one_pos ((one_lt_inv₀ h₀).2 h₁)] with y hy
    exact hxx'.trans_lt <| lt_inv_of_lt_inv₀ hy.1 hy.2
  · filter_upwards [Ioi_mem_nhds (inv_lt_one_of_one_lt₀ hx)] with y hy
    exact inv_lt_of_inv_lt₀ (by positivity) hy

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
hs : Disjoint e.source e'.source
ht : Disjoint e.target e'.target
⊢ ↑e '' (e.source ∩ e'.source) = e.target ∩ e'.target

Tactic:
rw [hs.inter_eq, ht.inter_eq, image_empty]

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : α
⊢ x ∈ e.source

Tactic:
rw [s]

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : α
⊢ x ∈ univ
Module: Mathlib.Algebra.Category.Grp.Images

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
⊢ ∀ (x y : ↥(Hom.hom f).range),
    (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(x + y)) ⋯) =
      (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯) +
        (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑y) ⋯)

Tactic:
by
      intro x y
      have := F'.m_mono
      apply injective_of_mono F'.m
      rw [map_add]
      change (F'.e ≫ F'.m) _ = (F'.e ≫ F'.m) _ + (F'.e ≫ F'.m) _
      rw [F'.fac]
      rw [(Classical.indefiniteDescription (fun z => f z = _) _).2]
      rw [(Classical.indefiniteDescription (fun z => f z = _) _).2]
      rw [(Classical.indefiniteDescription (fun z => f z = _) _).2]
      rfl

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ toIcoDiv hp a =ᶠ[𝓝[≥] x] fun x_1 ↦ toIcoDiv hp a x

Tactic:
by
  simp only [Filter.EventuallyEq, toIcoDiv_eq_iff, sub_mem_Ico_iff_left]
  apply Ico_mem_nhdsGE_of_mem
  rw [← sub_mem_Ico_iff_left, ← toIcoDiv_eq_iff]

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝[>] x, toIocDiv hp a x_1 = toIocDiv hp a x

Tactic:
convert! (eventuallyEq_toIocDiv_nhdsGT hp a x).eventually using 3

Goal state after:
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
x✝ : 𝕜
⊢ toIocDiv hp a x = toIcoDiv hp a x
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
inst✝ : SecondCountableTopology α
t : Set β
f : β → α
a✝ : Nontrivial β
this : Nonempty α
s : Set β := ⋯
z : β → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
⊢ StrictMonoOn f s

Tactic:
intro x hx y hy hxy

Goal state after:
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
inst✝ : SecondCountableTopology α
t : Set β
f : β → α
a✝ : Nontrivial β
this : Nonempty α
s : Set β := {x | x ∈ t ∧ ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
z : β → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
x : β
hx : x ∈ s
y : β
hy : y ∈ s
hxy : x < y
⊢ f x < f y
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : Field 𝕜
p q r : 𝕜
m : ℕ
⊢ ↑(↑m / q * r) = m • ↑(r / q)

Tactic:
by
  rw [mul_comm_div, ← nsmul_eq_mul, coe_nsmul]

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

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 F' : C ⥤ D
G : D ⥤ E
inst✝² : F.LaxBraided
inst✝¹ : F'.LaxBraided
inst✝ : G.LaxBraided
A : CommMon C
⊢ (β_ (F.mapMon.obj A.toMon).X (F.mapMon.obj A.toMon).X).hom ≫ μ = μ

Tactic:
dsimp
            rw [← Functor.LaxBraided.braided_assoc, ← Functor.map_comp, IsCommMonObj.mul_comm]

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
⊢ Nat.card { u // addOrderOf u = n } = n.totient

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn)

Goal state after:
case inl
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
⊢ Nat.card { u // addOrderOf u = 0 } = Nat.totient 0

case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : n > 0
⊢ Nat.card { u // addOrderOf u = n } = n.totient
Module: Mathlib.Algebra.Category.ModuleCat.Subobject

Goal state before:
pp: case i
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ underlying.obj S ≅ of R ↥((fun S ↦ (Hom.hom S.arrow).range) S)

Tactic:
apply LinearEquiv.toModuleIso
          apply LinearEquiv.ofBijective (LinearMap.codRestrict
            (LinearMap.range S.arrow.hom) S.arrow.hom _)
          constructor
          · simp [← LinearMap.ker_eq_bot, ker_eq_bot_of_mono]
          · rw [← LinearMap.range_eq_top, LinearMap.range_codRestrict,
              Submodule.comap_subtype_self]
            exact LinearMap.mem_range_self _

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

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : CartesianMonoidalCategory C
inst✝⁹ : BraidedCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : CartesianMonoidalCategory D
inst✝⁶ : BraidedCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : CartesianMonoidalCategory E
inst✝³ : BraidedCategory E
F F' : C ⥤ D
inst✝² : F.Braided
inst✝¹ : F'.Braided
G : D ⥤ E
inst✝ : G.Braided
A : CommGrp C
⊢ (β_ (F.mapGrp.obj A.toGrp).X (F.mapGrp.obj A.toGrp).X).hom ≫ μ = μ

Tactic:
dsimp
            rw [← Functor.LaxBraided.braided_assoc, ← Functor.map_comp, IsCommMonObj.mul_comm]

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
hS : S.Exact
⊢ S.δlast.Exact

Tactic:
exact_iff_δlast

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
hS : S.δlast.Exact ∧ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
⊢ S.δlast.Exact
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h₁ : S.δlast.Exact
h₂ : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
⊢ S.Exact

Tactic:
exact_iff_δlast

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h₁ : S.δlast.Exact
h₂ : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
⊢ S.δlast.Exact ∧ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: case right.right.id
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
x : { x // ∀ (i : J.R), (hom (I.fst i)) (x (J.fst i)) = (hom (I.snd i)) (x (J.snd i)) }
b : J.R
⊢ (hom ((I.multicospan ⋙ forget C).map (WalkingMulticospan.Hom.id (WalkingMulticospan.right b))))
      ((fun j ↦
          match j with
          | WalkingMulticospan.left a => ↑x a
          | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)))
        (WalkingMulticospan.right b)) =
    (fun j ↦
        match j with
        | WalkingMulticospan.left a => ↑x a
        | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)))
      (WalkingMulticospan.right b)

Tactic:
· simp only [WalkingMulticospan.Hom.id_eq_id, Functor.map_id]; rfl

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
B : C
α : Type v
inst✝² : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
x : ToType (widePushout B X f)
⊢ ∃ i y, (hom (ι f i)) y = x

Tactic:
rcases Concrete.widePushout_exists_rep f x with (⟨y, rfl⟩ | ⟨i, y, rfl⟩)

Goal state after:
case inl
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
B : C
α : Type v
inst✝² : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : ToType B
⊢ ∃ i y_1, (hom (ι f i)) y_1 = (hom (head f)) y

case inr
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
B : C
α : Type v
inst✝² : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
i : α
y : ToType (X i)
⊢ ∃ i_1 y_1, (hom (ι f i_1)) y_1 = (hom (ι f i)) y
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: J : MultispanShape
⊢ Function.LeftInverse
    (Sum.elim (fun X ↦ Arrow.mk (𝟙 X)) (Sum.elim (fun a ↦ Arrow.mk (Hom.fst a)) fun a ↦ Arrow.mk (Hom.snd a))) fun f ↦
    match f.right, f.left, f.hom with
    | x, .(x), Hom.id .(x) => Sum.inl x
    | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
    | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a)

Tactic:
rintro ⟨_, _, (_ | _ | _)⟩

Goal state after:
case id
J : MultispanShape
left✝ : WalkingMultispan J
⊢ Sum.elim (fun X ↦ Arrow.mk (𝟙 X)) (Sum.elim (fun a ↦ Arrow.mk (Hom.fst a)) fun a ↦ Arrow.mk (Hom.snd a))
      ((fun f ↦
          match f.right, f.left, f.hom with
          | x, .(x), Hom.id .(x) => Sum.inl x
          | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
          | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a))
        { left := left✝, right := left✝, hom := Hom.id ((𝟭 (WalkingMultispan J)).obj left✝) }) =
    { left := left✝, right := left✝, hom := Hom.id ((𝟭 (WalkingMultispan J)).obj left✝) }

case fst
J : MultispanShape
a✝ : J.L
⊢ Sum.elim (fun X ↦ Arrow.mk (𝟙 X)) (Sum.elim (fun a ↦ Arrow.mk (Hom.fst a)) fun a ↦ Arrow.mk (Hom.snd a))
      ((fun f ↦
          match f.right, f.left, f.hom with
          | x, .(x), Hom.id .(x) => Sum.inl x
          | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
          | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a))
        { left := left a✝, right := right (J.fst a✝), hom := Hom.fst a✝ }) =
    { left := left a✝, right := right (J.fst a✝), hom := Hom.fst a✝ }

case snd
J : MultispanShape
a✝ : J.L
⊢ Sum.elim (fun X ↦ Arrow.mk (𝟙 X)) (Sum.elim (fun a ↦ Arrow.mk (Hom.fst a)) fun a ↦ Arrow.mk (Hom.snd a))
      ((fun f ↦
          match f.right, f.left, f.hom with
          | x, .(x), Hom.id .(x) => Sum.inl x
          | .(right (J.fst a)), .(left a), Hom.fst a => Sum.inr (Sum.inl a)
          | .(right (J.snd a)), .(left a), Hom.snd a => Sum.inr (Sum.inr a))
        { left := left a✝, right := right (J.snd a✝), hom := Hom.snd a✝ }) =
    { left := left a✝, right := right (J.snd a✝), hom := Hom.snd a✝ }
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : D
⊢ R.map (h.counit.app (L.obj (R.obj X))) ≫ R.map (h.counit.app X) =
    R.map (L.map (R.map (h.counit.app X))) ≫ R.map (h.counit.app X)

Tactic:
← R.map_comp,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : D
⊢ R.map (h.counit.app (L.obj (R.obj X)) ≫ h.counit.app X) =
    R.map (L.map (R.map (h.counit.app X))) ≫ R.map (h.counit.app X)
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ R.map (L.map (R.map f)) ≫ R.map (h.counit.app Y✝) = R.map (h.counit.app X✝) ≫ R.map f

Tactic:
← R.map_comp,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ R.map (L.map (R.map f) ≫ h.counit.app Y✝) = R.map (h.counit.app X✝) ≫ R.map f
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ : ComposableArrows C n
F G : ComposableArrows C (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ ≫ app' β.hom 0 ⋯ = α.hom ≫ G.map' 0 1 homMk₁._proof_4 ⋯
⊢ G.map' 0 1 homMk₁._proof_4 ⋯ ≫ app' β.inv 0 ⋯ = α.inv ≫ F.map' 0 1 homMk₁._proof_4 ⋯

Tactic:
← cancel_epi α.hom,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ : ComposableArrows C n
F G : ComposableArrows C (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ ≫ app' β.hom 0 ⋯ = α.hom ≫ G.map' 0 1 homMk₁._proof_4 ⋯
⊢ α.hom ≫ G.map' 0 1 homMk₁._proof_4 ⋯ ≫ app' β.inv 0 ⋯ = α.hom ≫ α.inv ≫ F.map' 0 1 homMk₁._proof_4 ⋯
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.ReflectsIsomorphisms
inst✝¹ : HasEqualizerOfIsCosplitPair F
inst✝ : PreservesLimitOfIsCosplitPair F
⊢ ComonadicLeftAdjoint F

Tactic:
by
  have : ReflectsLimitOfIsCosplitPair F := ⟨fun f g _ => by
    have := HasEqualizerOfIsCosplitPair.out F f g
    apply reflectsLimit_of_reflectsIsomorphisms⟩
  apply comonadicOfHasPreservesReflectsFSplitEqualizers adj

Goal state after:
Module: Mathlib.RingTheory.IsPrimary

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
x✝ : S ≠ ⊤
a✝¹ : R
a✝ : M
⊢ (a✝¹ • a✝ ∈ S → a✝ ∈ S ∨ ∃ n, a✝¹ ^ n • ⊤ ≤ S) ↔ a✝¹ • a✝ ∈ S → a✝ ∈ S ∨ ∃ n, a✝¹ ^ n • map S.mkQ ⊤ ≤ ⊥

Tactic:
← map_pointwise_smul,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
x✝ : S ≠ ⊤
a✝¹ : R
a✝ : M
⊢ (a✝¹ • a✝ ∈ S → a✝ ∈ S ∨ ∃ n, a✝¹ ^ n • ⊤ ≤ S) ↔ a✝¹ • a✝ ∈ S → a✝ ∈ S ∨ ∃ n, map S.mkQ (a✝¹ ^ n • ⊤) ≤ ⊥
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
N' : Submodule S N
n : N
hn : n ∈ N'
⊢ n ∈ localized' S p f (comap f (restrictScalars R N'))

Tactic:
obtain ⟨⟨m, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective p f n

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
N' : Submodule S N
m : M
s : ↥p
hn : Function.uncurry (IsLocalizedModule.mk' f) (m, s) ∈ N'
⊢ Function.uncurry (IsLocalizedModule.mk' f) (m, s) ∈ localized' S p f (comap f (restrictScalars R N'))
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
⊢ (toFunLinear R A) ((a₁ * a₂) ⊗ₜ[R] (p₁ * p₂)) = (toFunLinear R A) (a₁ ⊗ₜ[R] p₁) * (toFunLinear R A) (a₂ ⊗ₜ[R] p₂)

Tactic:
classical
    simp only [toFunLinear_tmul_apply, toFunBilinear_apply_eq_sum]
    ext k
    simp_rw [coeff_sum, coeff_monomial, sum_def, Finset.sum_ite_eq', mem_support_iff, Ne]
    conv_rhs => rw [coeff_mul]
    simp_rw [finsetSum_coeff, coeff_monomial, Finset.sum_ite_eq', mem_support_iff, Ne, mul_ite,
      mul_zero, ite_mul, zero_mul]
    simp_rw [← ite_zero_mul (¬coeff p₁ _ = 0) (a₁ * (algebraMap R A) (coeff p₁ _))]
    simp_rw [← mul_ite_zero (¬coeff p₂ _ = 0) _ (_ * _)]
    simp_rw [toFunLinear_mul_tmul_mul_aux_1, toFunLinear_mul_tmul_mul_aux_2]

Goal state after:
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
⊢ ∀ (n : ℕ) (a : A), (toFunAlgHom R A) (invFun R A ((monomial n) a)) = (monomial n) a

Tactic:
intro n a
    rw [invFun_monomial, Algebra.TensorProduct.tmul_pow,
        one_pow, Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul, toFunAlgHom_apply_tmul,
        X_pow_eq_monomial, sum_monomial_index] <;>
      simp

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
⊢ IsFractionRing S T

Tactic:
by
  have := isLocalization_of_submonoid_le S T M (nonZeroDivisors R) hM
  refine @isLocalization_of_is_exists_mul_mem _ _ _ _ _ _ _ this ?_ ?_
  · exact map_nonZeroDivisors_le M S
  · rintro ⟨x, -, hx⟩
    obtain ⟨⟨y, s⟩, e⟩ := IsLocalization.surj M x
    use algebraMap R S s
    rw [mul_comm, Subtype.coe_mk, e]
    refine Set.mem_image_of_mem (algebraMap R S) (mem_nonZeroDivisors_iff_right.mpr ?_)
    intro z hz
    apply IsLocalization.injective S hM
    rw [map_zero]
    apply hx
    rw [← (map_units S s).mul_left_inj, mul_assoc, e, ← map_mul, hz, map_zero,
      zero_mul]

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
x y : ↥(adjoin R ↑σ)
e : (algebraMap (↥(adjoin R ↑σ)) S) x = (algebraMap (↥(adjoin R ↑σ)) S) y
⊢ ↑1 * x = ↑1 * y

Tactic:
by simpa using Subtype.ext e

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: case tmul
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra R B
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module B N
inst✝ : IsScalarTower R B N
n : Submodule B N
m : A
x : M
y : N
⊢ (TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n)) (m • x ⊗ₜ[R] Submodule.Quotient.mk y) =
    (RingHom.id A) m •
      (TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n)) (x ⊗ₜ[R] Submodule.Quotient.mk y)

Tactic:
smul_tmul'

Goal state after:
case tmul
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra R B
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module B N
inst✝ : IsScalarTower R B N
n : Submodule B N
m : A
x : M
y : N
⊢ (TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n)) ((m • x) ⊗ₜ[R] Submodule.Quotient.mk y) =
    (RingHom.id A) m •
      (TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n)) (x ⊗ₜ[R] Submodule.Quotient.mk y)
Module: Mathlib.RingTheory.Localization.Submodule

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Set R
⊢ coeSubmodule S (Ideal.span s) = Submodule.span R (⇑(algebraMap R S) '' s)

Tactic:
IsLocalization.coeSubmodule,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Set R
⊢ Submodule.map (Algebra.linearMap R S) (Ideal.span s) = Submodule.span R (⇑(algebraMap R S) '' s)
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
p : Ideal R
inst✝⁵ : p.IsPrime
Rₚ : Type u_4
inst✝⁴ : CommSemiring Rₚ
inst✝³ : Algebra R Rₚ
inst✝² : IsLocalization.AtPrime Rₚ p
inst✝¹ : IsLocalRing Rₚ
inst✝ : p.IsMaximal
n : ℕ
x✝ : R
⊢ (∃ m ∈ p.primeCompl, m * x✝ ∈ p ^ n) ↔ x✝ ∈ p ^ n

Tactic:
refine ⟨fun ⟨m, hm, h⟩ ↦ ?_, fun h ↦ ⟨1, by simp, by simp [h]⟩⟩

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
p : Ideal R
inst✝⁵ : p.IsPrime
Rₚ : Type u_4
inst✝⁴ : CommSemiring Rₚ
inst✝³ : Algebra R Rₚ
inst✝² : IsLocalization.AtPrime Rₚ p
inst✝¹ : IsLocalRing Rₚ
inst✝ : p.IsMaximal
n : ℕ
x✝¹ : R
x✝ : ∃ m ∈ p.primeCompl, m * x✝¹ ∈ p ^ n
m : R
hm : m ∈ p.primeCompl
h : m * x✝¹ ∈ p ^ n
⊢ x✝¹ ∈ p ^ n
Module: Mathlib.LinearAlgebra.Matrix.Polynomial

Goal state before:
pp: n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ ∀ (a : Equiv.Perm n), (sign a • ∏ i, (X • A.map ⇑C + B.map ⇑C) (a i) i).natDegree ≤ Fintype.card n

Tactic:
intro g

Goal state after:
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ (sign g • ∏ i, (X • A.map ⇑C + B.map ⇑C) (g i) i).natDegree ≤ Fintype.card n