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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
⊢ {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥}.Countable

Tactic:
by
  /- This does not follow from `countable_setOfPred_isolated_right`, which gives the result when `s`
  is the whole space, as one cannot use it inside the subspace since it doesn't have the order
  topology. Instead, we follow the main steps of its proof. -/
  let t := { x ∈ s | 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬ IsTop x}
  suffices H : t.Countable by
    have : { x ∈ s | 𝓝[s ∩ Ioi x] x = ⊥ } ⊆ t ∪ {x | IsTop x} := by
      intro x hx
      by_cases h'x : IsTop x
      · simp [h'x]
      · simpa [-sep_and, t, h'x]
    apply Countable.mono this
    simp [H, (subsingleton_isTop α).countable]
  have (x) (hx : x ∈ t) : ∃ y > x, s ∩ Ioo x y = ∅ := by
    simp only [← empty_mem_iff_bot, mem_nhdsWithin_iff_exists_mem_nhds_inter,
      subset_empty_iff, IsTop, not_forall, not_le, mem_ofPred_eq, t] at hx
    rcases hx.2.1 with ⟨u, hu, h'u⟩
    obtain ⟨y, hxy, hy⟩ : ∃ y, x < y ∧ Ico x y ⊆ u := exists_Ico_subset_of_mem_nhds hu hx.2.2
    refine ⟨y, hxy, ?_⟩
    contrapose! h'u
    apply h'u.mono
    intro z hz
    exact ⟨hy ⟨hz.2.1.le, hz.2.2⟩, hz.1, hz.2.1⟩
  choose! y hy h'y using this
  apply Set.PairwiseDisjoint.countable_of_Ioo (y := y) _ hy
  simp only [PairwiseDisjoint, Set.Pairwise, Function.onFun]
  intro a ha b hb hab
  wlog! H : a < b generalizing a b with h
  · have : b < a := lt_of_le_of_ne H hab.symm
    exact (h hb ha hab.symm this).symm
  have : y a ≤ b := by
    by_contra!
    have : b ∈ s ∩ Ioo a (y a) := by simp [hb.1, H, this]
    simp [h'y a ha] at this
  rw [disjoint_iff_forall_ne]
  exact fun u hu v hv ↦ ((hu.2.trans_le this).trans hv.1).ne

Goal state after:
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : C < 0
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
⊢ Tendsto (fun x ↦ f x * g x) l atTop

Tactic:
have := (tendsto_neg_atBot_atTop.comp hf).atTop_mul_neg hC hg

Goal state after:
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : C < 0
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
this : Tendsto (fun x ↦ (Neg.neg ∘ f) x * g x) l atBot
⊢ Tendsto (fun x ↦ f x * g x) l atTop
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
a : α
⊢ (𝓝 a).HasBasis (fun ε ↦ 1 < ε) fun ε ↦ {b | |b / a|ₘ < ε}

Tactic:
by
  simp only [nhds_eq_iInf_mabs_div, mabs_div_comm (a := a)]
  refine hasBasis_biInf_principal' (fun x hx y hy => ?_) (exists_gt _)
  exact ⟨min x y, lt_min hx hy, fun _ hz => hz.trans_le (min_le_left _ _),
    fun _ hz => hz.trans_le (min_le_right _ _)⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℕ
c d : 𝕜
⊢ Tendsto (fun x ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d

Tactic:
by
  rcases eq_or_ne n 0 with (rfl | hn)
  · simp [tendsto_const_nhds_iff]
  rcases lt_trichotomy c 0 with (hc | rfl | hc)
  · have := tendsto_const_mul_pow_atBot_iff.2 ⟨hn, hc⟩
    simp [not_tendsto_nhds_of_tendsto_atBot this, hc.ne, hn]
  · simp [tendsto_const_nhds_iff]
  · have := tendsto_const_mul_pow_atTop_iff.2 ⟨hn, hc⟩
    simp [not_tendsto_nhds_of_tendsto_atTop this, hc.ne', hn]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
h : e.source ⊆ s
⊢ (e.restr s).source = e.source

Tactic:
simp [inter_eq_self_of_subset_left h]

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

Goal state before:
pp: case inr.a
α : Type u
ts : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
hα : Nonempty α
t : Set (Set α)
t_subs : t ⊆ {s | ∃ a, s = Ioi a ∨ s = Iio a}
t_count : t.Countable
ht : ts = generateFrom t
a : Set α → α
ha : ∀ s ∈ t, s = Ioi (a s) ∨ s = Iio (a s)
⊢ ∀ (a_1 x : Set α), x ∈ t → a_1 = Ioi (a x) ∨ a_1 = Iio (a x) → IsOpen[ts] a_1

Tactic:
grind [isOpen_Iio', isOpen_Ioi']

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 : 𝕜
⊢ x ∈ Ioc (a + toIocDiv hp a x • p) (a + p + toIocDiv hp a x • p)

Tactic:
← sub_mem_Ioc_iff_left,

Goal state after:
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ x - toIocDiv hp a x • p ∈ Ioc a (a + p)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case inl
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
hs : IsOpen[inst✝³] s
x : α
hx : x ∈ s
y : α
hy : y ≠ x
H : x < y
⊢ ∃ a b, a < b ∧ Ioo a b ⊆ s

Tactic:
obtain ⟨u, xu, hu⟩ : ∃ u, x < u ∧ Ico x u ⊆ s :=
      exists_Ico_subset_of_mem_nhds (hs.mem_nhds hx) ⟨y, H⟩

Goal state after:
case inl
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
hs : IsOpen[inst✝³] s
x : α
hx : x ∈ s
y : α
hy : y ≠ x
H : x < y
u : α
xu : x < u
hu : Ico x u ⊆ s
⊢ ∃ a b, a < b ∧ Ioo a b ⊆ s
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
A' : Type u_1
inst✝² : AddCommGroup A'
inst✝¹ : Module R A
inst✝ : Module R A'
f : A →ₗ[R] A'
hf : Function.Injective ⇑(dual f)
c : CharacterModule (A' ⧸ f.range)
b : A'
⊢ (dual (f.range.mkQ ∘ₗ f)) c = (dual f) 0

Tactic:
LinearMap.range_mkQ_comp,

Goal state after:
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
A' : Type u_1
inst✝² : AddCommGroup A'
inst✝¹ : Module R A
inst✝ : Module R A'
f : A →ₗ[R] A'
hf : Function.Injective ⇑(dual f)
c : CharacterModule (A' ⧸ f.range)
b : A'
⊢ (dual 0) c = (dual f) 0
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x : 𝕜
hx : x ∈ Ico a (a + p)
⊢ ↑x = (equivIco p a).symm ⟨x, hx⟩

Tactic:
equivIco,

Goal state after:
𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x : 𝕜
hx : x ∈ Ico a (a + p)
⊢ ↑x = (QuotientAddGroup.equivIcoMod ⋯ a).symm ⟨x, hx⟩
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
⊢ (∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = u) → addOrderOf u = n

Tactic:
rintro ⟨m, -, h₁, rfl⟩

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < n
m : ℕ
h₁ : m.gcd n = 1
⊢ addOrderOf ↑(↑m / ↑n * p) = n
Module: Mathlib.Algebra.Category.Grp.LeftExactFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
F : C ⥤ AddCommGrpCat
inst✝ : PreservesFiniteLimits F
X : C
this✝¹ : (F ⋙ forget AddCommGrpCat).Braided := Functor.Braided.ofChosenFiniteProducts (F ⋙ forget AddCommGrpCat)
this✝ : F.Monoidal := Functor.Monoidal.ofChosenFiniteProducts F
this : F.Additive
⊢ (𝟙
          ((MonTypeEquivalenceMon.inverse.obj
                ((forget₂ GrpCat MonCat).obj ((forget₂ CommGrpCat GrpCat).obj (toCommGrp.obj (F.obj X))))).X ⊗
            (MonTypeEquivalenceMon.inverse.obj
                ((forget₂ GrpCat MonCat).obj ((forget₂ CommGrpCat GrpCat).obj (toCommGrp.obj (F.obj X))))).X) ≫
        μ) ≫
      Multiplicative.toAdd.toIso.hom =
    (Multiplicative.toAdd.toIso.hom ⊗ₘ Multiplicative.toAdd.toIso.hom) ≫ μ

Tactic:
simp only [Category.id_comp]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
F : C ⥤ AddCommGrpCat
inst✝ : PreservesFiniteLimits F
X : C
this✝¹ : (F ⋙ forget AddCommGrpCat).Braided := Functor.Braided.ofChosenFiniteProducts (F ⋙ forget AddCommGrpCat)
this✝ : F.Monoidal := Functor.Monoidal.ofChosenFiniteProducts F
this : F.Additive
⊢ μ ≫ Multiplicative.toAdd.toIso.hom = (Multiplicative.toAdd.toIso.hom ⊗ₘ Multiplicative.toAdd.toIso.hom) ≫ μ
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x : PUnit.{u + 1}
⊢ (ConcreteCategory.hom (↟(Finsupp.lapply PUnit.unit))) (Finsupp.single x 1) = 1

Tactic:
erw [Finsupp.lapply_apply]

Goal state after:
R : Type u
inst✝ : CommRing R
x : PUnit.{u + 1}
⊢ (Finsupp.single x 1) PUnit.unit = 1
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
⊢ S.Exact → (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact ∧ S.δ₀.Exact

pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
⊢ (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact ∧ S.δ₀.Exact → S.Exact

Tactic:
· intro h
    constructor
    · rw [exact₂_iff]; swap
      · rw [isComplex₂_iff]
        exact h.toIsComplex.zero 0
      exact h.exact 0 (by lia)
    · exact Exact.mk (IsComplex.mk (fun i hi => h.toIsComplex.zero (i + 1)))
        (fun i hi => h.exact (i + 1))

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
⊢ (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact ∧ S.δ₀.Exact → S.Exact
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
p : (fun X ↦ X) P
⊢ (hom fst) p = (hom (pullback.fst f g)) ((hom h.isoPullback.hom) p)

Tactic:
← comp_apply h.isoPullback.hom (pullback.fst f g),

Goal state after:
P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
p : (fun X ↦ X) P
⊢ (hom fst) p = (hom (h.isoPullback.hom ≫ pullback.fst f g)) p
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.right
J : MultispanShape
l : J.L
r' : J.R
⊢ Small.{t, max w w'} (left l ⟶ right r')

pp: case right.left
J : MultispanShape
r : J.R
l' : J.L
⊢ Small.{t, max w w'} (right r ⟶ left l')

pp: case right.right
J : MultispanShape
r r' : J.R
⊢ Small.{t, max w w'} (right r ⟶ right r')

Tactic:
· let T₁ := { u : Unit // J.fst l = r' }
      let T₂ := { u : Unit // J.snd l = r' }
      let f : T₁ ⊕ T₂ → (left l ⟶ right r') :=
        Sum.elim (fun ⟨_, h⟩ ↦ by subst h; exact Hom.fst l)
          (fun ⟨_, h⟩ ↦ by subst h; exact Hom.snd l)
      refine small_of_surjective (f := f) ?_
      rintro (_ | _)
      · exact ⟨Sum.inl ⟨⟨⟩, rfl⟩, rfl⟩
      · exact ⟨Sum.inr ⟨⟨⟩, rfl⟩, rfl⟩

Goal state after:
case right.left
J : MultispanShape
r : J.R
l' : J.L
⊢ Small.{t, max w w'} (right r ⟶ left l')

case right.right
J : MultispanShape
r r' : J.R
⊢ Small.{t, max w w'} (right r ⟶ right r')
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: J : MultispanShape
⊢ Function.RightInverse
    (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:
by rintro (_ | _ | _) <;> rfl

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

Goal state before:
pp: case left.left.id
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.L
⊢ 𝟙 P ≫ ι a✝ = ι a✝

Tactic:
simp only [Category.id_comp]

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

Goal state before:
pp: case left.right.fst
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ 𝟙 P ≫ ι (J.fst a✝) ≫ I.fst a✝ = ι (J.fst a✝) ≫ I.fst a✝

Tactic:
simp only [Category.id_comp]

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

Goal state before:
pp: case left.right.snd
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ 𝟙 P ≫ ι (J.fst a✝) ≫ I.fst a✝ = ι (J.snd a✝) ≫ I.snd a✝

Tactic:
simp only [Category.id_comp]

Goal state after:
case left.right.snd
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ ι (J.fst a✝) ≫ I.fst a✝ = ι (J.snd a✝) ≫ I.snd a✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case right.right.id
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ 𝟙 P ≫ ι (J.fst a✝) ≫ I.fst a✝ = ι (J.fst a✝) ≫ I.fst a✝

Tactic:
simp only [Category.id_comp]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type w
inst✝ : LinearOrder ι
I : MultispanIndex (MultispanShape.prod ι) C
c : Multicofork I.toLinearOrder
h : I.SymmStruct
⊢ ∀ (a : (MultispanShape.prod ι).L),
    I.fst a ≫ c.π ((MultispanShape.prod ι).fst a) = I.snd a ≫ c.π ((MultispanShape.prod ι).snd a)

Tactic:
by
    rintro ⟨x, y⟩
    obtain hxy | rfl | hxy := lt_trichotomy x y
    · exact c.condition ⟨⟨x, y⟩, hxy⟩
    · simp [h.fst_eq_snd]
    · have := c.condition ⟨⟨y, x⟩, hxy⟩
      dsimp at this ⊢
      rw [← h.iso_hom_fst_assoc, ← h.iso_hom_snd_assoc, this]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type u
inst✝² : Category.{v, u} J
R : D ⥤ C
inst✝¹ : Reflective R
inst✝ : HasColimitsOfShape J C
F : J ⥤ D
⊢ HasColimit F

Tactic:
let c := (monadicLeftAdjoint R).mapCocone (colimit.cocone (F ⋙ R))

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type u
inst✝² : Category.{v, u} J
R : D ⥤ C
inst✝¹ : Reflective R
inst✝ : HasColimitsOfShape J C
F : J ⥤ D
c : Cocone ((F ⋙ R) ⋙ monadicLeftAdjoint R) := (monadicLeftAdjoint R).mapCocone (colimit.cocone (F ⋙ R))
⊢ HasColimit F
Module: Mathlib.RingTheory.Flat.CategoryTheory

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
M : ModuleCat R
inst✝ : Flat R ↑M
C : ShortComplex (ModuleCat R)
hC : Function.Exact ⇑(ConcreteCategory.hom C.f) ⇑(ConcreteCategory.hom C.g)
⊢ Function.Exact ⇑(ConcreteCategory.hom (C.map (tensorLeft M)).f) ⇑(ConcreteCategory.hom (C.map (tensorLeft M)).g)

Tactic:
exact lTensor_exact M hC

Goal state after:
Module: Mathlib.RingTheory.Flat.Stability

Goal state before:
pp: R : Type u
S : Type v
M : Type w
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower R S M
inst✝³ : Flat R S
inst✝² : Flat S M
P : Type u
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : Submodule R P
⊢ Injective ⇑((AlgebraTensorModule.lTensor S M) ((AlgebraTensorModule.lTensor S S) N.subtype))

Tactic:
apply Flat.lTensor_preserves_injective_linearMap

Goal state after:
R : Type u
S : Type v
M : Type w
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower R S M
inst✝³ : Flat R S
inst✝² : Flat S M
P : Type u
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : Submodule R P
⊢ Injective ⇑((AlgebraTensorModule.lTensor S S) N.subtype)
Module: Mathlib.RingTheory.Flat.Stability

Goal state before:
pp: R : Type u
S : Type v
M : Type w
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower R S M
inst✝³ : Flat R S
inst✝² : Flat S M
P : Type u
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : Submodule R P
⊢ Injective ⇑((AlgebraTensorModule.lTensor S S) N.subtype)

Tactic:
apply Flat.lTensor_preserves_injective_linearMap

Goal state after:
R : Type u
S : Type v
M : Type w
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower R S M
inst✝³ : Flat R S
inst✝² : Flat S M
P : Type u
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : Submodule R P
⊢ Injective ⇑N.subtype
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} D✝
J✝ : Type u
inst✝ : Category.{v, u} J✝
T : Comonad C
D : J✝ ⥤ T.Coalgebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
s : Cocone D
m : (liftedCocone D c t).pt ⟶ s.pt
J : ∀ (j : J✝), (liftedCocone D c t).ι.app j ≫ m = s.ι.app j
⊢ m = { f := t.desc (T.forget.mapCocone s), h := ⋯ }

Tactic:
by
    ext1
    apply t.hom_ext
    intro j
    simpa [t.fac ((forget T).mapCocone s) j] using congr_arg Coalgebra.Hom.f (J j)

Goal state after:
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: A : Type u_2
inst✝³ : CommSemiring A
C : Type u_4
inst✝² : Semiring C
inst✝¹ : Algebra A C
𝔓 : Ideal C
p : Ideal A
inst✝ : p.IsPrime
hPp : p = comap (algebraMap A C) 𝔓
⊢ Disjoint ↑(Algebra.algebraMapSubmonoid C p.primeCompl) ↑𝔓

Tactic:
SetLike.ext'_iff,

Goal state after:
A : Type u_2
inst✝³ : CommSemiring A
C : Type u_4
inst✝² : Semiring C
inst✝¹ : Algebra A C
𝔓 : Ideal C
p : Ideal A
inst✝ : p.IsPrime
hPp : ↑p = ↑(comap (algebraMap A C) 𝔓)
⊢ Disjoint ↑(Algebra.algebraMapSubmonoid C p.primeCompl) ↑𝔓
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
J : Ideal R
inst✝ : J.IsPrime
⊢ J ∈ J.minimalPrimes

Tactic:
exact ⟨⟨inferInstance, rfl.le⟩, fun _ h _ => h.2⟩

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

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
I : Submodule R R
N' : Submodule S N
r : R
hr : r ∈ I
n : N
hn : n ∈ restrictScalars R N'
⊢ r • n ∈ restrictScalars R (localized' S p (Algebra.linearMap R S) I • N')

Tactic:
← algebraMap_smul S,

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
I : Submodule R R
N' : Submodule S N
r : R
hr : r ∈ I
n : N
hn : n ∈ restrictScalars R N'
⊢ (algebraMap R S) r • n ∈ restrictScalars R (localized' S p (Algebra.linearMap R S) I • N')
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 ⊗[R] R[X]
a : A
p : R[X]
⊢ (p.sum fun n a_1 ↦ ↑includeLeft (a * (algebraMap R A) a_1) * 1 ⊗ₜ[R] X ^ n) = a ⊗ₜ[R] p

Tactic:
AlgHom.coe_toRingHom,

Goal state after:
case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ (p.sum fun n a_1 ↦ includeLeft (a * (algebraMap R A) a_1) * 1 ⊗ₜ[R] X ^ n) = a ⊗ₜ[R] p
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹⁶ : CommRing R
S : Type u_2
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : IsDomain R
inst✝¹² : IsDomain S
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : IsDomain Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R Rₚ
inst✝⁷ : Algebra R Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : Algebra Rₚ Sₚ
inst✝⁴ : IsScalarTower R S Sₚ
inst✝³ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝² : IsLocalization M Rₚ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝ : Module.IsTorsionFree R S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = map Sₚ (algebraMap R S) ⋯
⊢ RingHom.ker (algebraMap Rₚ Sₚ) = ⊥

Tactic:
RingHom.ker_eq_bot_iff_eq_zero

Goal state after:
R : Type u_1
inst✝¹⁶ : CommRing R
S : Type u_2
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : IsDomain R
inst✝¹² : IsDomain S
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : IsDomain Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R Rₚ
inst✝⁷ : Algebra R Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : Algebra Rₚ Sₚ
inst✝⁴ : IsScalarTower R S Sₚ
inst✝³ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝² : IsLocalization M Rₚ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝ : Module.IsTorsionFree R S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = map Sₚ (algebraMap R S) ⋯
⊢ ∀ (x : Rₚ), (algebraMap Rₚ Sₚ) x = 0 → x = 0
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: case mp
R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
N : Submonoid S
x : R
⊢ (∃ y ∈ N, ∃ z ∈ Submonoid.map (algebraMap R S) M, y * z = (algebraMap R S) x) →
    ∃ y z, (algebraMap R S) x = ↑y * (algebraMap R S) ↑z

Tactic:
rintro ⟨y, hy, _, ⟨z, hz, rfl⟩, e⟩
    exact ⟨⟨y, hy⟩, ⟨z, hz⟩, e.symm⟩

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
p : Submonoid R
inst✝ : IsLocalization p S
⊢ Module.Flat R S

Tactic:
by
  refine Module.Flat.iff_lTensor_injectiveₛ.mpr fun P _ _ N ↦ ?_
  have h := ((range N.subtype).isLocalizedModule S p (TensorProduct.mk R S P 1)).isBaseChange _ S
  let e := (LinearEquiv.ofInjective _ Subtype.val_injective).lTensor S ≪≫ₗ h.equiv.restrictScalars R
  have : N.subtype.lTensor S = Submodule.subtype _ ∘ₗ e.toLinearMap := by
    ext; change _ = (h.equiv _).1; simp [h.equiv_tmul, TensorProduct.smul_tmul']
  simpa [this] using! e.injective

Goal state after: