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

Goal state before:
pp: case refine_1
Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
S : Set β
hA : UniformEquicontinuousOn (u ∘ Subtype.val) S
hu : Continuous[tY, Pi.topologicalSpace] (S.domRestrict ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
x y : β
hxS : (x, y).1 ∈ S
hyS : (x, y).2 ∈ S
hxy : A ⊆ (fun f ↦ (u f x, u f y)) ⁻¹' V
⊢ Continuous[tY, uα.toTopologicalSpace] fun f ↦ u f x

pp: case refine_2
Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
S : Set β
hA : UniformEquicontinuousOn (u ∘ Subtype.val) S
hu : Continuous[tY, Pi.topologicalSpace] (S.domRestrict ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
x y : β
hxS : (x, y).1 ∈ S
hyS : (x, y).2 ∈ S
hxy : A ⊆ (fun f ↦ (u f x, u f y)) ⁻¹' V
⊢ Continuous[tY, uα.toTopologicalSpace] fun f ↦ u f y

Tactic:
· exact (continuous_apply ⟨x, hxS⟩).comp hu

Goal state after:
case refine_2
Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
S : Set β
hA : UniformEquicontinuousOn (u ∘ Subtype.val) S
hu : Continuous[tY, Pi.topologicalSpace] (S.domRestrict ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
x y : β
hxS : (x, y).1 ∈ S
hyS : (x, y).2 ∈ S
hxy : A ⊆ (fun f ↦ (u f x, u f y)) ⁻¹' V
⊢ Continuous[tY, uα.toTopologicalSpace] fun f ↦ u f y
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
𝔖 : Set (Set α)
f : γ → β
⊢ uniformSpace α γ 𝔖 = UniformSpace.comap (fun x ↦ f ∘ x) (uniformSpace α β 𝔖)

Tactic:
by
  -- We reduce this to `UniformFun.comap_eq` using the fact that `comap` distributes
  -- on `iInf`.
  simp_rw [UniformOnFun.uniformSpace, UniformSpace.comap_iInf, UniformFun.comap_eq, ←
    UniformSpace.comap_comap]
  -- By definition, `∀ S ∈ 𝔖, (f ∘ —) ∘ S.domRestrict = S.domRestrict ∘ (f ∘ —)`.
  rfl

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

Goal state before:
pp: M : Type u_1
X : Type u_2
Y : Type u_3
α : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : SMul M X
inst✝² : ContinuousSMul M X
f : Y → M
g : Y → X
b : Y
s : Set Y
inst✝¹ : SMul Mᵐᵒᵖ X
inst✝ : IsCentralScalar M X
⊢ Continuous[instTopologicalSpaceProd, inst✝⁵] fun p ↦ p.1 • p.2

Tactic:
by
    suffices Continuous fun p : M × X => MulOpposite.op p.fst • p.snd from
      this.comp (MulOpposite.continuous_unop.prodMap continuous_id)
    simpa only [op_smul_eq_smul] using (continuous_smul : Continuous fun p : M × X => _)

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

Goal state after:
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
⊢ Set.univ = ⇑(Equiv.vaddConst (Classical.arbitrary P)) '' Set.univ
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
φ : (i : ι) → δ i → α
𝔗 : (i : ι) → Set (Set (δ i))
h_image : ∀ (i : ι), MapsTo (fun x ↦ φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x ↦ φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → ↑(φ i ⁻¹' S) → ↑S := fun S i ↦ S.restrictPreimage (φ i)
this :
  ∀ S ∈ 𝔖,
    UniformFun.uniformSpace (↑S) β =
      ⨅ i, UniformSpace.comap (fun x ↦ x ∘ ψ S i) (UniformFun.uniformSpace (↑(φ i ⁻¹' S)) β)
S : Set α
hS : S ∈ 𝔖
⊢ ⨅ i, UniformSpace.comap (⇑(ofFun (𝔗 i)) ∘ (fun x ↦ x ∘ φ i) ∘ ⇑(toFun 𝔖)) (uniformSpace (δ i) β (𝔗 i)) ≤
    UniformSpace.comap (⇑UniformFun.ofFun ∘ S.domRestrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑S) β)

Tactic:
· simp_rw [this S hS, uniformSpace, UniformSpace.comap_iInf, ← UniformSpace.comap_comap]
    exact iInf_mono fun i ↦ iInf₂_le_of_le _ (h_preimage i hS) le_rfl

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

Goal state before:
pp: α : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : ContinuousConstSMul G α
c : G
s : Set α
hs : closure[inst✝³] s = univ
⊢ c • univ = univ

Tactic:
smul_set_univ

Goal state after:
α : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : ContinuousConstSMul G α
c : G
s : Set α
hs : closure[inst✝³] s = univ
⊢ univ = univ
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
h : ∀ i ∈ l, ContinuousOn (f i) t
⊢ ContinuousOn (fun a ↦ (List.map (fun i ↦ f i a) l).prod) t

Tactic:
by
  intro x hx
  rw [continuousWithinAt_iff_continuousAt_domRestrict _ hx]
  refine tendsto_list_prod _ fun i hi => ?_
  specialize h i hi x hx
  rw [continuousWithinAt_iff_continuousAt_domRestrict _ hx] at h
  exact h

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
X : Type u_5
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace M
inst✝⁶ : Monoid M
inst✝⁵ : ContinuousMul M
R : Type u_6
A : Type u_7
inst✝⁴ : Monoid A
inst✝³ : SMul R A
inst✝² : SMulCommClass R A A
inst✝¹ : TopologicalSpace A
inst✝ : SeparatelyContinuousMul A
q : R
⊢ Continuous[inst✝¹, inst✝¹] fun x ↦ q • x

Tactic:
by
    simp +singlePass only [← mul_smul_one q (_ : A)]
    fun_prop

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

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul α α
s : Set α
a b : α
h : s ∈ 𝓝 b
⊢ {a} * s ∈ 𝓝 (a * b)

Tactic:
← smul_eq_mul,

Goal state after:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul α α
s : Set α
a b : α
h : s ∈ 𝓝 b
⊢ {a} * s ∈ 𝓝 (a • b)
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul α α
s : Set α
a b : α
h : s ∈ 𝓝 b
⊢ {a} * s ∈ 𝓝 (a • b)

Tactic:
← smul_eq_mul,

Goal state after:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul α α
s : Set α
a b : α
h : s ∈ 𝓝 b
⊢ {a} • s ∈ 𝓝 (a • b)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous fun x ↦ f x ^ Int.negSucc n

Tactic:
simp_rw [zpow_negSucc]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous fun x ↦ (f x ^ (n + 1))⁻¹
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
α : Type u
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun k ↦ b / f k) l (𝓝 (b / c))
⊢ Tendsto f l (𝓝 c)

Tactic:
convert! h.inv.mul_const b with k <;> rw [inv_div, div_mul_cancel]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k : α
hk : 0 < k
b : α
x✝ : 1 ≤ b
⊢ b ≤ k * b / k

Tactic:
mul_div_assoc,

Goal state after:
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k : α
hk : 0 < k
b : α
x✝ : 1 ≤ b
⊢ b ≤ k * (b / k)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : (𝓝 1).HasBasis p U
⊢ (𝓤 α).HasBasis p fun i ↦ {x | x.1 / x.2 ∈ U i}

Tactic:
uniformity_eq_comap_nhds_one_swapped

Goal state after:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : (𝓝 1).HasBasis p U
⊢ (Filter.comap (fun x ↦ x.1 / x.2) (𝓝 1)).HasBasis p fun i ↦ {x | x.1 / x.2 ∈ U i}
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
⊢ Tendsto (fun x ↦ r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot

Tactic:
rcases lt_trichotomy r 0 with (hr | rfl | hr)

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
hr : r < 0
⊢ Tendsto (fun x ↦ r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot

case inr.inl
α : Type u_1
β : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
l : Filter β
f : β → α
inst✝ : l.NeBot
⊢ Tendsto (fun x ↦ 0 * f x) l atTop ↔ 0 < 0 ∧ Tendsto f l atTop ∨ 0 < 0 ∧ Tendsto f l atBot

case inr.inr
α : Type u_1
β : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
hr : 0 < r
⊢ Tendsto (fun x ↦ r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
g₀ : G
hg₀ : g₀ ∈ interior V
g : G
x✝ : g ∈ K
⊢ g₀ * g⁻¹ * g ∈ interior V

Tactic:
inv_mul_cancel_right

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
g₀ : G
hg₀ : g₀ ∈ interior V
g : G
x✝ : g ∈ K
⊢ g₀ ∈ interior V
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]

Goal state after:
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 (Subtype.val ∘ (unitsEquivPos R).toFun)
Module: Mathlib.Logic.Equiv.PartialEquiv

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

Tactic:
inter_eq_self_of_subset_right h

Goal state after:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
h : s ⊆ e.source
⊢ ↑e '' s = ↑e '' s
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_1 : 𝕜) in 𝓝[<] x, x_1 ∈ Ico (a + toIocDiv hp a x • p) (a + p + toIocDiv hp a x • p)

Tactic:
apply Ico_mem_nhdsLT_of_mem

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 ∈ Ioc (a + toIocDiv hp a x • p) (a + p + toIocDiv hp a x • p)
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case h
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx✝ : ↑y ∈ {x | n • x = 0}
hx : n • y ∈ zmultiples p
m' : ℤ
this : NeZero n
m : ℤ × Fin n := (Int.divModEquiv n) m'
hm : (fun x ↦ x • p) (m.1 * ↑n + ↑↑m.2) = n • y
⊢ m.1 • ↑p = 0 ∧ n • (y - m.1 • p) = ↑m.2 • p

Tactic:
coe_period,

Goal state after:
case h
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx✝ : ↑y ∈ {x | n • x = 0}
hx : n • y ∈ zmultiples p
m' : ℤ
this : NeZero n
m : ℤ × Fin n := (Int.divModEquiv n) m'
hm : (fun x ↦ x • p) (m.1 * ↑n + ↑↑m.2) = n • y
⊢ m.1 • 0 = 0 ∧ n • (y - m.1 • p) = ↑m.2 • p
Module: Mathlib.Algebra.Category.Grp.LargeColimits

Goal state before:
pp: case refine_1
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
χ ψ : CharacterModule ↑c.pt
eq : (CharacterModule.dual (Quot.desc F c).toIntLinearMap) χ = (CharacterModule.dual (Quot.desc F c).toIntLinearMap) ψ
⊢ χ = ψ

Tactic:
apply AddEquiv.ulift.symm.addMonoidHomCongrRightEquiv.injective
    apply ofHom_injective
    refine hc.hom_ext (fun j ↦ ?_)
    ext x
    erw [ConcreteCategory.comp_apply, ConcreteCategory.comp_apply, ← Quot.ι_desc _ c j x]
    exact DFunLike.congr_fun eq (Quot.ι F j x)

Goal state after:
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 𝕜
y : 𝕜
hy : y ∈ Ioc a (a + p)
⊢ ↑((equivIoc p a) ↑y) = y

Tactic:
have : equivIoc p a y = ⟨y, hy⟩ := (equivIoc p a).right_inv ⟨y, hy⟩
  simp [this]

Goal state after:
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 𝕜
ha : a ∈ Ico 0 p
h0 : 0 ∈ Ico 0 (0 + p)
ha' : a ∈ Ico 0 (0 + p)
⊢ ↑a = 0 ↔ a = 0

Tactic:
rw [← AddCircle.coe_eq_coe_iff_of_mem_Ico ha' h0, QuotientAddGroup.mk_zero]

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
⊢ (a / ↑n) • ↑p = 0

pp: case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
⊢ 0 ≤ a % ↑n

Tactic:
coe_period,

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
⊢ (a / ↑n) • 0 = 0

case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
⊢ 0 ≤ a % ↑n
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
⊢ ↑n ≠ 0

Tactic:
exact_mod_cast h.ne'

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

Goal state before:
pp: case inl
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
⊢ ∀ (x : 𝕜) (hx : x ∈ Icc a (a + p)),
    x ≠ a + p →
      Quot.mk (EndpointIdent p a)
          (Set.inclusion ⋯ ((equivIco p a) ((Quot.mk (EndpointIdent p a) ⟨x, hx⟩).liftOn (fun x ↦ ↑↑x) ⋯))) =
        Quot.mk (EndpointIdent p a) ⟨x, hx⟩

Tactic:
intro x hx h

Goal state after:
case inl
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
hx : x ∈ Icc a (a + p)
h : x ≠ a + p
⊢ Quot.mk (EndpointIdent p a)
      (Set.inclusion ⋯ ((equivIco p a) ((Quot.mk (EndpointIdent p a) ⟨x, hx⟩).liftOn (fun x ↦ ↑↑x) ⋯))) =
    Quot.mk (EndpointIdent p a) ⟨x, hx⟩
Module: Mathlib.Algebra.Homology.ExactSequence

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

pp: case mp.right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ S.δ₀.Exact

Tactic:
· rw [exact₂_iff]; swap
      · rw [isComplex₂_iff]
        exact h.toIsComplex.zero 0
      exact h.exact 0 (by lia)

Goal state after:
case mp.right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ S.δ₀.Exact
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A : C
a : A ⟶ S.L₁.X₂
b : A ⟶ S.L₀.X₃
h : a ≫ S.L₁.g = b ≫ S.v₀₁.τ₃
⊢ pullback.lift a b h ≫ S.φ₂ = a ≫ S.v₁₂.τ₂

Tactic:
simp [φ₂]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ 𝟙 (Opposite.op S.L₃.X₁) ≫ S.op.δ = S.δ.op ≫ 𝟙 (Opposite.op S.L₀.X₃)

Tactic:
simp only [id_comp, comp_id, S.op_δ]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
⊢ (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker

Tactic:
by
  simpa only [moduleCat_exact_iff_range_eq_ker] using hS

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
b : J.R
⊢ K.π.app (WalkingMulticospan.right b) = K.ι (J.snd b) ≫ I.snd b

Tactic:
← app_right_eq_ι_comp_snd

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
b : J.R
⊢ K.π.app (WalkingMulticospan.right b) = K.π.app (WalkingMulticospan.right b)
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ F G : ComposableArrows C n
app : (i : Fin (n + 1)) → F.obj i ≅ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ (app ⟨i + 1, ⋯⟩).hom = (app ⟨i, ⋯⟩).hom ≫ G.map' i (i + 1) ⋯ hi
i : ℕ
hi : i < n
⊢ F.map' i (i + 1) ⋯ hi ≫ (app ⟨i + 1, ⋯⟩).hom ≫ (app ⟨i + 1, ⋯⟩).inv =
    (app ⟨i, ⋯⟩).hom ≫ (app ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi

Tactic:
Iso.hom_inv_id,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ F G : ComposableArrows C n
app : (i : Fin (n + 1)) → F.obj i ≅ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ (app ⟨i + 1, ⋯⟩).hom = (app ⟨i, ⋯⟩).hom ≫ G.map' i (i + 1) ⋯ hi
i : ℕ
hi : i < n
⊢ F.map' i (i + 1) ⋯ hi ≫ 𝟙 (F.obj ⟨i + 1, ⋯⟩) = (app ⟨i, ⋯⟩).hom ≫ (app ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi
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
⊢ Flat R M

Tactic:
by
  rw [Flat.iff_lTensor_injectiveₛ]
  introv
  rw [← coe_lTensor (A := S), ← EquivLike.injective_comp (cancelBaseChange R S S _ _),
    ← LinearEquiv.coe_coe, ← LinearMap.coe_comp, lTensor_comp_cancelBaseChange,
    LinearMap.coe_comp, LinearEquiv.coe_coe, EquivLike.comp_injective]
  iterate 2 apply Flat.lTensor_preserves_injective_linearMap
  exact Subtype.val_injective

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
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := empty D
c : Cocone (F ⋙ R)
h : IsColimit c
this✝¹ : HasColimit (F ⋙ R)
this✝ : HasColimit F
this : CreatesColimitsOfSize.{v, v, v₂, v₁, u₂, u₁} R := comonadicCreatesColimits R
A : PreservesColimit F R := preservesColimit_of_createsColimit_and_hasColimit F R
⊢ R.obj (colimit.cocone F).1 ≅ c.pt

Tactic:
apply (isColimitOfPreserves _ (colimit.isColimit F)).coconePointUniqueUpToIso h

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

Goal state before:
pp: A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring A
inst✝³ : Semiring B
inst✝² : Algebra A B
inst✝¹ : FaithfulSMul A B
p : Ideal A
hp : p ≠ ⊥
P : Ideal B
inst✝ : P.LiesOver p
⊢ P ≠ ⊥

Tactic:
contrapose hp

Goal state after:
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring A
inst✝³ : Semiring B
inst✝² : Algebra A B
inst✝¹ : FaithfulSMul A B
p : Ideal A
P : Ideal B
inst✝ : P.LiesOver p
hp : P = ⊥
⊢ p = ⊥
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: A : Type u_3
B : Type u_4
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
P : Ideal B
p : Ideal A
inst✝ : P.LiesOver p
hp : p ≠ ⊤
⊢ Nontrivial (B ⧸ P)

Tactic:
by
  rwa [Quotient.nontrivial_iff, ne_top_iff_of_liesOver _ p]

Goal state after:
Module: Mathlib.RingTheory.IsPrimary

Goal state before:
pp: case insert.inl
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
f : ι → Submodule R M
a i : ι
ha : a ∉ ∅
IH :
  ∀ {i : ι},
    i ∈ ∅ →
      (∀ ⦃y : ι⦄, y ∈ ∅ → (f y).IsPrimary) →
        (∀ ⦃y : ι⦄, y ∈ ∅ → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical) → (∅.inf f).IsPrimary
hi : i ∈ insert a ∅
hs : ∀ ⦃y : ι⦄, y ∈ insert a ∅ → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ insert a ∅ → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical
⊢ ((insert a ∅).inf f).IsPrimary

pp: case insert.inr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
f : ι → Submodule R M
a : ι
s : Finset ι
ha : a ∉ s
IH :
  ∀ {i : ι},
    i ∈ s →
      (∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary) →
        (∀ ⦃y : ι⦄, y ∈ s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical) → (s.inf f).IsPrimary
i : ι
hi : i ∈ insert a s
hs : ∀ ⦃y : ι⦄, y ∈ insert a s → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ insert a s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical
y : ι
hy : y ∈ s
⊢ ((insert a s).inf f).IsPrimary

Tactic:
· simp only [insert_empty_eq, mem_singleton] at hi
      simpa [hi] using hs

Goal state after:
case insert.inr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
f : ι → Submodule R M
a : ι
s : Finset ι
ha : a ∉ s
IH :
  ∀ {i : ι},
    i ∈ s →
      (∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary) →
        (∀ ⦃y : ι⦄, y ∈ s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical) → (s.inf f).IsPrimary
i : ι
hi : i ∈ insert a s
hs : ∀ ⦃y : ι⦄, y ∈ insert a s → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ insert a s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical
y : ι
hy : y ∈ s
⊢ ((insert a s).inf f).IsPrimary
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ I.radical.minimalPrimes = I.minimalPrimes

Tactic:
rw [Ideal.minimalPrimes, Ideal.minimalPrimes]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ {p | I.radical.IsMinimalPrime p} = {p | I.IsMinimalPrime p}