mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
⊢ IsUniformInducing ⇑(Equiv.piComm fun a ↦ δ)

Tactic:
constructor
    change comap (Prod.map Function.swap Function.swap) _ = _
    erw [← uniformity_comap]
    congr
    rw [Pi.uniformSpace, UniformSpace.ofCoreEq_toCore, Pi.uniformSpace,
      UniformSpace.ofCoreEq_toCore, UniformSpace.comap_iInf, UniformOnFun.iInf_eq]
    refine iInf_congr fun i => ?_
    rw [← UniformSpace.comap_comap, UniformOnFun.comap_eq]
    rfl

Goal state after:
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: case mp
α : Type u_2
inst✝ : DivisionMonoid α
f : Filter α
⊢ IsUnit f → ∃ a, f = pure a ∧ IsUnit a

pp: case mpr
α : Type u_2
inst✝ : DivisionMonoid α
f : Filter α
⊢ (∃ a, f = pure a ∧ IsUnit a) → IsUnit f

Tactic:
· rintro ⟨u, rfl⟩
    obtain ⟨a, b, ha, hb, h⟩ := Filter.mul_eq_one_iff.1 u.mul_inv
    refine ⟨a, ha, ⟨a, b, h, pure_injective ?_⟩, rfl⟩
    rw [← pure_mul_pure, ← ha, ← hb]
    exact u.inv_mul

Goal state after:
case mpr
α : Type u_2
inst✝ : DivisionMonoid α
f : Filter α
⊢ (∃ a, f = pure a ∧ IsUnit a) → IsUnit f
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
h : c < 0
⊢ (fun x ↦ x * c) ⁻¹' Ioo a b = Ioo (b / c) (a / c)

Tactic:
simp [← Ioi_inter_Iio, h, inter_comm]

Goal state after:
Module: Mathlib.Topology.Algebra.MulAction

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝⁵ : AddGroup G
inst✝⁴ : AddTorsor G P
inst✝³ : TopologicalSpace G
inst✝² : PreconnectedSpace G
inst✝¹ : TopologicalSpace P
inst✝ : ContinuousVAdd G P
⊢ IsPreconnected Set.univ

Tactic:
convert!
        isPreconnected_univ.image (Equiv.vaddConst (Classical.arbitrary P) : G → P)
          (continuous_id.vadd continuous_const).continuousOn
      rw [Set.image_univ, Equiv.range_eq_univ]

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : IsTopologicalGroup H
inst✝¹ : PartialOrder H
inst✝ : IsOrderedMonoid H
c a : H
⊢ map (fun x ↦ x / c) (𝓝[>] a) = 𝓝[>] (a / c)

Tactic:
convert! (Homeomorph.divRight c).isEmbedding.map_nhdsWithin_eq .. using 2
  simp

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : IsTopologicalGroup H
inst✝¹ : PartialOrder H
inst✝ : IsOrderedMonoid H
c a : H
⊢ map (fun x ↦ x / c) (𝓝[<] a) = 𝓝[<] (a / c)

Tactic:
convert! (Homeomorph.divRight c).isEmbedding.map_nhdsWithin_eq .. using 2
  simp

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
⊢ ∀ {K L : Set G}, IsCompact K → IsCompact L → {γ | ((fun x ↦ γ • x) '' K ∩ L).Nonempty}.Finite

Tactic:
intro K L hK hL

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
⊢ {γ | ((fun x ↦ γ • x) '' K ∩ L).Nonempty}.Finite
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : (⇑S.subtype ⁻¹' ((fun p ↦ p.1 / p.2) '' L ×ˢ K)ᶜ)ᶜ.Finite
⊢ {γ | ((fun x ↦ γ • x) '' K ∩ L).Nonempty}.Finite

Tactic:
preimage_compl,

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : (⇑S.subtype ⁻¹' (fun p ↦ p.1 / p.2) '' L ×ˢ K)ᶜᶜ.Finite
⊢ {γ | ((fun x ↦ γ • x) '' K ∩ L).Nonempty}.Finite
Module: Mathlib.Topology.Algebra.Ring.Basic

Goal state before:
pp: R : Type u_2
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
hmul_left : ∀ (x₀ : R), Tendsto (fun x ↦ x₀ * x) (𝓝 0) (𝓝 0)
hmul_right : ∀ (x₀ : R), Tendsto (fun x ↦ x * x₀) (𝓝 0) (𝓝 0)
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ p.1 * p.2

Tactic:
refine continuous_of_continuousAt_zero₂ (AddMonoidHom.mul (R := R)) ?_ ?_ ?_

Goal state after:
case refine_1
R : Type u_2
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
hmul_left : ∀ (x₀ : R), Tendsto (fun x ↦ x₀ * x) (𝓝 0) (𝓝 0)
hmul_right : ∀ (x₀ : R), Tendsto (fun x ↦ x * x₀) (𝓝 0) (𝓝 0)
⊢ ContinuousAt (fun x ↦ (AddMonoidHom.mul x.1) x.2) (0, 0)

case refine_2
R : Type u_2
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
hmul_left : ∀ (x₀ : R), Tendsto (fun x ↦ x₀ * x) (𝓝 0) (𝓝 0)
hmul_right : ∀ (x₀ : R), Tendsto (fun x ↦ x * x₀) (𝓝 0) (𝓝 0)
⊢ ∀ (x : R), ContinuousAt (⇑(AddMonoidHom.mul x)) 0

case refine_3
R : Type u_2
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
hmul_left : ∀ (x₀ : R), Tendsto (fun x ↦ x₀ * x) (𝓝 0) (𝓝 0)
hmul_right : ∀ (x₀ : R), Tendsto (fun x ↦ x * x₀) (𝓝 0) (𝓝 0)
⊢ ∀ (y : R), ContinuousAt (fun x ↦ (AddMonoidHom.mul x) y) 0
Module: Mathlib.Topology.Algebra.Field

Goal state before:
pp: K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
R : Type u_2
inst✝⁵ : DivisionSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : PosMulReflectLT R
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousInv₀ R
⊢ Continuous (unitsEquivPos R).toFun

Tactic:
rw [Topology.IsEmbedding.subtypeVal.continuous_iff]
    exact Continuous.subtype_val (p := (0 ≤ ·)) Units.continuous_val

Goal state after:
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹² : TopologicalSpace α
inst✝¹¹ : AddCommGroup α
inst✝¹⁰ : IsTopologicalAddGroup α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : AddCommGroup β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : AddCommGroup γ
inst✝⁵ : IsTopologicalAddGroup γ
inst✝⁴ : TopologicalSpace δ
inst✝³ : AddCommGroup δ
inst✝² : UniformSpace G
inst✝¹ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝².toTopologicalSpace] fun p ↦ (φ p.1) p.2
W' : Set G
W'_nhds : W' ∈ 𝓝 0
inst✝ : IsUniformAddGroup G
x₀ : α
y₀ : γ
ee : β × β → α × α := fun u ↦ (e u.1, e u.2)
ff : δ × δ → γ × γ := fun u ↦ (f u.1, f u.2)
lim_φ : Tendsto (fun p ↦ (φ p.1) p.2) (𝓝 (0, 0)) (𝓝 0)
lim_φ_sub_sub :
  Tendsto (fun p ↦ (fun p ↦ (φ p.1) p.2) (p.1.2 - p.1.1, p.2.2 - p.2.1))
    (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0)
W : Set G
W_nhds : W ∈ 𝓝 0
W4 : ∀ {v w s t : G}, v ∈ W → w ∈ W → s ∈ W → t ∈ W → v + w + s + t ∈ W'
U₁ : Set β
U₁_nhds : U₁ ∈ comap (⇑e) (𝓝 x₀)
V₁ : Set δ
V₁_nhds : V₁ ∈ comap (⇑f) (𝓝 y₀)
H : ∀ x ∈ U₁, ∀ x' ∈ U₁, ∀ y ∈ V₁, ∀ y' ∈ V₁, (fun p ↦ (φ p.1) p.2) (x' - x, y' - y) ∈ W
x₁ : β
x₁_in : x₁ ∈ U₁
y₁ : δ
y₁_in : y₁ ∈ V₁
cont_flip : Continuous[instTopologicalSpaceProd, inst✝².toTopologicalSpace] fun p ↦ (φ.flip p.1) p.2
U₂ : Set β
U₂_nhds : U₂ ∈ comap (⇑e) (𝓝 x₀)
HU : ∀ x ∈ U₂, ∀ x' ∈ U₂, (fun p ↦ (φ p.1) p.2) (x' - x, y₁) ∈ W
V₂ : Set δ
V₂_nhds : V₂ ∈ comap (⇑f) (𝓝 y₀)
HV : ∀ x ∈ V₂, ∀ x' ∈ V₂, (fun p ↦ (φ.flip p.1) p.2) (x' - x, x₁) ∈ W
x : β
xU₁ : x ∈ U₁
xU₂ : x ∈ U₂
x' : β
x'U₁ : x' ∈ U₁
x'U₂ : x' ∈ U₂
y : δ
yV₁ : y ∈ V₁
yV₂ : y ∈ V₂
y' : δ
y'V₁ : y' ∈ V₁
y'V₂ : y' ∈ V₂
⊢ (φ x') y' - (φ x) y = (φ x') y₁ - (φ x) y₁ + ((φ x') y' - (φ x') y₁ - ((φ x) y' - (φ x) y₁)) + ((φ x) y' - (φ x) y)

Tactic:
abel

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]
⊢ toIocDiv hp a =ᶠ[𝓝 x] fun x_1 ↦ toIocDiv hp a x

Tactic:
rw [← nhdsLE_sup_nhdsGT, Filter.EventuallyEq, Filter.eventually_sup]

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_1 : 𝕜) in 𝓝[≤] x, toIocDiv hp a x_1 = toIocDiv hp a x) ∧
    ∀ᶠ (x_1 : 𝕜) in 𝓝[>] x, toIocDiv hp a x_1 = toIocDiv hp a x
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℤ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
⊢ {x | n • x = 0}.encard ≤ ↑n.natAbs

Tactic:
convert!
    card_torsion_le_of_isSMulRegular p _ (Int.natAbs_ne_zero.mpr h0)
      (IsSMulRegular.natAbs_iff.mpr hn) using 1

Goal state after:
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℤ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
⊢ {x | n • x = 0}.encard = {x | n.natAbs • x = 0}.encard
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : AddCommGroup 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsOrderedAddMonoid 𝕜
hp : 0 < p
n : ℤ
hx : 0 < n • p
⊢ 0 < n

Tactic:
contrapose! hx

Goal state after:
𝕜 : Type u_1
inst✝² : AddCommGroup 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsOrderedAddMonoid 𝕜
hp : 0 < p
n : ℤ
hx : n ≤ 0
⊢ n • p ≤ 0
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := ⋯
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst✝³] a
t : Set α := ⋯
z : α → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
this : t.PairwiseDisjoint fun x ↦ Ioc (z x) x
x : α
hx : x ∈ t
⊢ Ioo (z x) (y x) ⊆ Ioc (z x) x

Tactic:
subset_def,

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst✝³] a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : α → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
this : t.PairwiseDisjoint fun x ↦ Ioc (z x) x
x : α
hx : x ∈ t
⊢ ∀ x_1 ∈ Ioo (z x) (y x), x_1 ∈ Ioc (z x) x
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 y : 𝕜
hx : x ∈ Ico a (a + p)
hy : y ∈ Ico a (a + p)
⊢ ↑x = ↑y ↔ x = y

Tactic:
by
  refine ⟨fun h => ?_, by tauto⟩
  suffices (⟨x, hx⟩ : Ico a (a + p)) = ⟨y, hy⟩ by exact Subtype.mk.inj this
  apply_fun equivIco p a at h
  rw [← (equivIco p a).right_inv ⟨x, hx⟩, ← (equivIco p a).right_inv ⟨y, hy⟩]
  exact h

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

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : n > 0
⊢ Nat.card ↑{m | m < n ∧ m.gcd n = 1} = n.totient

Tactic:
n.totient_eq_card_lt_and_coprime

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : n > 0
⊢ Nat.card ↑{m | m < n ∧ m.gcd n = 1} = Nat.card ↑{m | m < n ∧ n.Coprime m}
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case right
𝕜 : Type u_1
B : Type u_2
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
⊢ ContinuousWithinAt (Subtype.val ∘ fun x ↦ ⟨toIcoMod ⋯ a x, ⋯⟩) (Ici x) x

Tactic:
apply continuousWithinAt_toIcoMod_Ici

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat

Goal state before:
pp: R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ S.Exact ↔ Function.Exact ⇑(ConcreteCategory.hom S.f) ⇑(ConcreteCategory.hom S.g)

Tactic:
by
  rw [moduleCat_exact_iff_range_eq_ker, LinearMap.exact_iff]
  tauto

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
i j k : Fin (n + 1 + 1)
hij : i ≤ j
hjk : j ≤ k
⊢ map F f i k ⋯ = map F f i j hij ≫ map F f j k hjk

Tactic:
obtain ⟨i, hi⟩ := i

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
j k : Fin (n + 1 + 1)
hjk : j ≤ k
i : ℕ
hi : i < n + 1 + 1
hij : ⟨i, hi⟩ ≤ j
⊢ map F f ⟨i, hi⟩ k ⋯ = map F f ⟨i, hi⟩ j hij ≫ map F f j k hjk
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
inst✝ : Reflective R
X : (reflectorAdjunction R).toMonad.Algebra
⊢ X.a ≫ (reflectorAdjunction R).unit.app X.A = 𝟙 ((reflector R ⋙ R).obj X.A)

Tactic:
dsimp only [Functor.id_obj]
        rw [← (reflectorAdjunction R).unit_naturality]
        dsimp only [Functor.comp_obj, Adjunction.toMonad_coe]
        rw [unit_obj_eq_map_unit, ← Functor.map_comp, ← Functor.map_comp]
        dsimp [X.unit]
        simpa using congrArg (fun t ↦ R.map ((reflector R).map t)) X.unit

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✝¹ : Coreflective R
inst✝ : HasLimitsOfShape J C
F : J ⥤ D
c : Cone ((F ⋙ R) ⋙ comonadicRightAdjoint R) := (comonadicRightAdjoint R).mapCone (limit.cone (F ⋙ R))
this : PreservesLimitsOfShape J (comonadicRightAdjoint R) := PreservesLimitsOfSize.preservesLimitsOfShape
t : IsLimit c := isLimitOfPreserves (comonadicRightAdjoint R) (limit.isLimit (F ⋙ R))
⊢ HasLimit F

Tactic:
apply HasLimit.mk ⟨_, (IsLimit.postcomposeHomEquiv _ _).symm t⟩

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✝¹ : Coreflective R
inst✝ : HasLimitsOfShape J C
F : J ⥤ D
c : Cone ((F ⋙ R) ⋙ comonadicRightAdjoint R) := ⋯
this : PreservesLimitsOfShape J (comonadicRightAdjoint R) := ⋯
t : IsLimit c := ⋯
⊢ (F ⋙ R) ⋙ comonadicRightAdjoint R ≅ F
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
hn :
  ∀ (obj : Fin (n + 1) → C) (mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ),
    ∃ F e, ∀ (i : ℕ) (hi : i < n), mapSucc ⟨i, hi⟩ = (e ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi ≫ (e ⟨i + 1, ⋯⟩).hom
obj : Fin (n + 1 + 1) → C
mapSucc : (i : Fin (n + 1)) → obj i.castSucc ⟶ obj i.succ
⊢ ∃ F e, ∀ (i : ℕ) (hi : i < n + 1), mapSucc ⟨i, hi⟩ = (e ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi ≫ (e ⟨i + 1, ⋯⟩).hom

Tactic:
| succ n hn =>

Goal state after:
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
x y : N
x✝¹ : x ∈ {x | ∃ m ∈ M', ∃ s, IsLocalizedModule.mk' f m s = x}
x✝ : y ∈ {x | ∃ m ∈ M', ∃ s, IsLocalizedModule.mk' f m s = x}
m : M
hm : m ∈ M'
s : ↥p
hx : IsLocalizedModule.mk' f m s = x
n : M
hn : n ∈ M'
t : ↥p
hy : IsLocalizedModule.mk' f n t = y
⊢ IsLocalizedModule.mk' f (t • m + s • n) (s * t) = IsLocalizedModule.mk' f m s + IsLocalizedModule.mk' f n t

Tactic:
IsLocalizedModule.mk'_add_mk'

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
x y : N
x✝¹ : x ∈ {x | ∃ m ∈ M', ∃ s, IsLocalizedModule.mk' f m s = x}
x✝ : y ∈ {x | ∃ m ∈ M', ∃ s, IsLocalizedModule.mk' f m s = x}
m : M
hm : m ∈ M'
s : ↥p
hx : IsLocalizedModule.mk' f m s = x
n : M
hn : n ∈ M'
t : ↥p
hy : IsLocalizedModule.mk' f n t = y
⊢ IsLocalizedModule.mk' f (t • m + s • n) (s * t) = IsLocalizedModule.mk' f (t • m + s • n) (s * t)
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case ih.refine_2
R : Type u_1
inst✝¹ : CommSemiring R
I J : Ideal R
inst✝ : J.IsPrime
e : I ≤ J
S : Set (Ideal R)ᵒᵈ := {p | IsPrime p ∧ I ≤ OrderDual.ofDual p}
c : Set (Ideal R)
hc : c ⊆ S
hc' : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
⊢ ∀ z ∈ c, z ≤ OrderDual.toDual (sInf c)

Tactic:
rintro z hz

Goal state after:
case ih.refine_2
R : Type u_1
inst✝¹ : CommSemiring R
I J : Ideal R
inst✝ : J.IsPrime
e : I ≤ J
S : Set (Ideal R)ᵒᵈ := {p | IsPrime p ∧ I ≤ OrderDual.ofDual p}
c : Set (Ideal R)
hc : c ⊆ S
hc' : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
z : (Ideal R)ᵒᵈ
hz : z ∈ c
⊢ z ≤ OrderDual.toDual (sInf c)
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case ih.refine_2
R : Type u_1
inst✝¹ : CommSemiring R
I J : Ideal R
inst✝ : J.IsPrime
e : I ≤ J
S : Set (Ideal R)ᵒᵈ := {p | IsPrime p ∧ I ≤ OrderDual.ofDual p}
c : Set (Ideal R)
hc : c ⊆ S
hc' : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
z : (Ideal R)ᵒᵈ
hz : z ∈ c
⊢ z ≤ OrderDual.toDual (sInf c)

Tactic:
OrderDual.le_toDual

Goal state after:
case ih.refine_2
R : Type u_1
inst✝¹ : CommSemiring R
I J : Ideal R
inst✝ : J.IsPrime
e : I ≤ J
S : Set (Ideal R)ᵒᵈ := {p | IsPrime p ∧ I ≤ OrderDual.ofDual p}
c : Set (Ideal R)
hc : c ⊆ S
hc' : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
z : (Ideal R)ᵒᵈ
hz : z ∈ c
⊢ sInf c ≤ OrderDual.ofDual z
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
m : Submodule R M
n : Submodule R N
x : M
hx : x ∈ m
y : N
⊢ x ⊗ₜ[R] y ∈ (map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range

Tactic:
exact Submodule.mem_sup_left ⟨⟨x, hx⟩ ⊗ₜ y, rfl⟩

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

Goal state before:
pp: case refine_2
R✝ : Type u_1
inst✝¹⁸ : CommSemiring R✝
S✝ : Type u_2
inst✝¹⁷ : CommSemiring S✝
inst✝¹⁶ : Algebra R✝ S✝
P✝ : Type u_3
inst✝¹⁵ : CommSemiring P✝
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ₚ✝
Sₚ : Type u_5
inst✝⁹ : CommSemiring Sₚ
inst✝⁸ : Algebra S✝ Sₚ
inst✝⁷ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ
inst✝⁶ : Algebra Rₚ✝ Sₚ
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_8
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
x : R
s : ↥p.primeCompl
s' : R
hs : (Ideal.Quotient.mk p) s' = ((Ideal.Quotient.mk p) ↑s)⁻¹
⊢ ∃ a, (Ideal.Quotient.mk (maximalIdeal Rₚ)) ((algebraMap R Rₚ) a) = (Ideal.Quotient.mk (maximalIdeal Rₚ)) (mk' Rₚ x s)

Tactic:
use x * s'

Goal state after:
case h
R✝ : Type u_1
inst✝¹⁸ : CommSemiring R✝
S✝ : Type u_2
inst✝¹⁷ : CommSemiring S✝
inst✝¹⁶ : Algebra R✝ S✝
P✝ : Type u_3
inst✝¹⁵ : CommSemiring P✝
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ₚ✝
Sₚ : Type u_5
inst✝⁹ : CommSemiring Sₚ
inst✝⁸ : Algebra S✝ Sₚ
inst✝⁷ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ
inst✝⁶ : Algebra Rₚ✝ Sₚ
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_8
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
x : R
s : ↥p.primeCompl
s' : R
hs : (Ideal.Quotient.mk p) s' = ((Ideal.Quotient.mk p) ↑s)⁻¹
⊢ (Ideal.Quotient.mk (maximalIdeal Rₚ)) ((algebraMap R Rₚ) (x * s')) =
    (Ideal.Quotient.mk (maximalIdeal Rₚ)) (mk' Rₚ x s)
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
x y : α
eq : x * y = 1
this : y = 1 - y * x + y
⊢ y * x = 1

Tactic:
right_eq_add,

Goal state after:
case refine_2
α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
x y : α
eq : x * y = 1
this : 1 - y * x = 0
⊢ y * x = 1
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
this : x = 1 - y * x + x
⊢ y * x = 1

Tactic:
right_eq_add,

Goal state after:
case refine_2
α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
this : 1 - y * x = 0
⊢ y * x = 1
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPl : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ ContainsIdentities fun {R S} [CommRing R] [CommRing S] ↦ P

Tactic:
introv R
  exact hPl.of_bijective _ _ Function.bijective_id

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

Goal state before:
pp: R✝ : Type u_1
inst✝¹⁸ : CommSemiring R✝
S✝ : Type u_2
inst✝¹⁷ : CommSemiring S✝
inst✝¹⁶ : Algebra R✝ S✝
P✝ : Type u_3
inst✝¹⁵ : CommSemiring P✝
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ₚ✝
Sₚ : Type u_5
inst✝⁹ : CommSemiring Sₚ
inst✝⁸ : Algebra S✝ Sₚ
inst✝⁷ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ
inst✝⁶ : Algebra Rₚ✝ Sₚ
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_8
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
n : ℕ
⊢ (R ⧸ p ^ n) ≃ₐ[R] Rₚ ⧸ maximalIdeal Rₚ ^ n

Tactic:
refine AlgEquiv.ofAlgHom (Ideal.Quotient.liftₐ _ (Algebra.ofId _ _) ?_) ?_ ?_ ?_
  · simp_rw [ofId_apply, ← RingHom.mem_ker, ← SetLike.le_def]
    rw [← Quotient.mk_comp_algebraMap, ← RingHom.comap_ker, mk_ker, ← under_def,
      under_maximalIdeal_pow p]
  · refine Ideal.Quotient.liftₐ _
      (IsLocalization.liftAlgHom (f := Ideal.Quotient.mkₐ R (p ^ n)) fun (u : p.primeCompl) ↦
        Ideal.Quotient.isUnit_mk_pow_of_notMem _ <| mem_primeCompl_iff.mp u.prop) fun x hx ↦ ?_
    obtain ⟨a, b, rfl⟩ := IsLocalization.exists_mk'_eq p.primeCompl x
    rw [IsLocalization.mk'_mem_iff, ← Ideal.mem_under, under_maximalIdeal_pow p] at hx
    simpa [lift_mk', Quotient.eq_zero_iff_mem] using hx
  · rw [← AlgHom.cancel_right (Ideal.Quotient.mkₐ_surjective _ _)]
    exact IsLocalization.algHom_ext (W := p.primeCompl) (A := R) (by ext)
  · rw [← AlgHom.cancel_right (Ideal.Quotient.mkₐ_surjective _ _)]
    ext

Goal state after: