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

Goal state before:
pp: case mk.mk
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
i✝ : Quotient (MulAction.orbitRel Γ T)
x₀ : T
j✝ : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ | ((fun x ↦ γ • x) '' K₀ ∩ L₀).Nonempty}
bad_Γ_finite : bad_Γ_set.Finite
u v : Γ → Set T
hu : ∀ (γ : Γ), u γ ∈ 𝓝 (γ • x₀)
hv : ∀ (γ : Γ), v γ ∈ 𝓝 y₀
u_v_disjoint : ∀ (γ : Γ), Disjoint (u γ) (v γ)
U₀₀ : Set T := ⋂ γ ∈ bad_Γ_set, (fun x ↦ γ • x) ⁻¹' u γ
⊢ ∃ U ∈ 𝓝 (f x₀), ∃ V ∈ 𝓝 (f y₀), Disjoint U V

Tactic:
let U₀ := U₀₀ ∩ K₀

Goal state after:
case mk.mk
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst✝⁶ : Group Γ
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
inst✝³ : T2Space T
inst✝² : LocallyCompactSpace T
inst✝¹ : ContinuousConstSMul Γ T
inst✝ : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
i✝ : Quotient (MulAction.orbitRel Γ T)
x₀ : T
j✝ : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ | ((fun x ↦ γ • x) '' K₀ ∩ L₀).Nonempty}
bad_Γ_finite : bad_Γ_set.Finite
u v : Γ → Set T
hu : ∀ (γ : Γ), u γ ∈ 𝓝 (γ • x₀)
hv : ∀ (γ : Γ), v γ ∈ 𝓝 y₀
u_v_disjoint : ∀ (γ : Γ), Disjoint (u γ) (v γ)
U₀₀ : Set T := ⋂ γ ∈ bad_Γ_set, (fun x ↦ γ • x) ⁻¹' u γ
U₀ : Set T := U₀₀ ∩ K₀
⊢ ∃ U ∈ 𝓝 (f x₀), ∃ V ∈ 𝓝 (f y₀), Disjoint U V
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
⊢ ∃ V ∈ 𝓝 0, K * V ⊆ U

Tactic:
by
  refine hK.induction_on ?_ ?_ ?_ ?_
  · exact ⟨univ, by simp⟩
  · rintro s t hst ⟨V, hV, hV'⟩
    exact ⟨V, hV, (mul_subset_mul_right hst).trans hV'⟩
  · rintro s t ⟨V, V_in, hV'⟩ ⟨W, W_in, hW'⟩
    use V ∩ W, inter_mem V_in W_in
    rw [union_mul]
    exact
      union_subset ((mul_subset_mul_left V.inter_subset_left).trans hV')
        ((mul_subset_mul_left V.inter_subset_right).trans hW')
  · intro x hx
    have := tendsto_mul (show U ∈ 𝓝 (x * 0) by simpa using hU)
    rw [nhds_prod_eq, mem_map, mem_prod_iff] at this
    rcases this with ⟨t, ht, s, hs, h⟩
    rw [← image_subset_iff, image_mul_prod] at h
    exact ⟨t, mem_nhdsWithin_of_mem_nhds ht, s, hs, h⟩

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

Goal state before:
pp: M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
l : Filter (M × M)
hl : Disjoint l (cocompact (M × M))
⊢ Tendsto (fun x ↦ x.1 * x.2) ((𝓝 0).coprod (𝓝 0) ⊓ l) (𝓝 0)

Tactic:
have := calc
    (𝓝 0).coprod (𝓝 0) ⊓ l
    _ ≤ (𝓝 0).coprod (𝓝 0) ⊓ map Prod.fst l ×ˢ map Prod.snd l :=
      inf_le_inf_left _ le_prod_map_fst_snd
    _ ≤ 𝓝 0 ×ˢ map Prod.snd l ⊔ map Prod.fst l ×ˢ 𝓝 0 :=
      coprod_inf_prod_le _ _ _ _

Goal state after:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
l : Filter (M × M)
hl : Disjoint l (cocompact (M × M))
this : (𝓝 0).coprod (𝓝 0) ⊓ l ≤ 𝓝 0 ×ˢ map Prod.snd l ⊔ map Prod.fst l ×ˢ 𝓝 0
⊢ Tendsto (fun x ↦ x.1 * x.2) ((𝓝 0).coprod (𝓝 0) ⊓ l) (𝓝 0)
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_3
inst✝ : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
⊢ ContinuousMul M

Tactic:
rw [inf_eq_iInf]
  refine continuousMul_iInf fun b => ?_
  cases b <;> assumption

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

Goal state before:
pp: α : Type u
β : Type v
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : ContinuousInv α
inst✝¹ : ContinuousSMul α β
inst✝ : CompactSpace α
⊢ IsClosedMap Quotient.mk'

Tactic:
by
  intro t ht
  rw [← isQuotientMap_quotient_mk'.isClosed_preimage,
    MulAction.quotient_preimage_image_eq_union_mul]
  convert! ht.smul_left_of_isCompact (isCompact_univ (X := α))
  rw [← biUnion_univ, ← iUnion_smul_left_image]
  simp only [image_smul]

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U ∈ 𝓝 1, x ∉ U
x y : G
hspec : x ⤳ y
hne : ¬x = y
U : Set G
hU₁ : U ∈ 𝓝 1
hU : x * y⁻¹ ∉ U
⊢ U ∈ 𝓝 (y * y⁻¹)

Tactic:
by rwa [mul_inv_cancel]

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

Goal state before:
pp: G : Type w
H : Type x
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : IsTopologicalGroup G
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup H
f : G →* H
hf : Continuous[inst✝⁵, inst✝¹] ⇑f
hf' : DenseRange ⇑f
s : Subgroup G
hs : ↑s.topologicalClosure = ↑⊤
⊢ ↑(Subgroup.map f s).topologicalClosure = ↑⊤

Tactic:
simp only [Subgroup.topologicalClosure_coe, Subgroup.coe_top, ← dense_iff_closure_eq] at hs ⊢

Goal state after:
G : Type w
H : Type x
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : IsTopologicalGroup G
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup H
f : G →* H
hf : Continuous[inst✝⁵, inst✝¹] ⇑f
hf' : DenseRange ⇑f
s : Subgroup G
hs : Dense ↑s
⊢ Dense ↑(Subgroup.map f s)
Module: Mathlib.Order.Filter.AtTopBot.Ring

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atTop
hg : Tendsto g l atBot
this : Tendsto (fun x ↦ f x * (Neg.neg ∘ g) x) l atTop
⊢ Tendsto (fun x ↦ f x * g x) l atBot

Tactic:
simpa only [Function.comp_def, neg_mul_eq_mul_neg, neg_neg] using
    tendsto_neg_atTop_atBot.comp this

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

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n : ℕ
hn : 0 < ↑n
⊢ Tendsto (fun x ↦ x ^ ↑n) atTop atTop

Tactic:
simp [(Int.natCast_pos.mp hn).ne']

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 ↦ c / x) (𝓝[>] a) = 𝓝[<] (c / a)

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

Goal state after:
case e'_3.e'_4
H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : IsTopologicalGroup H
inst✝¹ : PartialOrder H
inst✝ : IsOrderedMonoid H
c a : H
⊢ Iio (c / a) = ⇑(Homeomorph.divLeft c) '' Ioi a
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 ↦ c / x) (𝓝[<] a) = 𝓝[>] (c / a)

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

Goal state after:
case e'_3.e'_4
H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : IsTopologicalGroup H
inst✝¹ : PartialOrder H
inst✝ : IsOrderedMonoid H
c a : H
⊢ Ioi (c / a) = ⇑(Homeomorph.divLeft c) '' Iio a
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
c a : G
⊢ map (fun x ↦ c / x) (𝓝[≠] a) = 𝓝[≠] (c / a)

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

Goal state after:
case e'_3.e'_4
G : Type w
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
c a : G
⊢ {c / a}ᶜ = ⇑(Homeomorph.divLeft c) '' {a}ᶜ
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_3
inst✝³ : Group G
inst✝² : UniformSpace G
inst✝¹ : IsRightUniformGroup G
inst✝ : WeaklyLocallyCompactSpace G
f : Filter G
hf : Cauchy f
this : f.NeBot
K : Set G
K_compact : IsCompact K
K_mem : K ∈ 𝓝 1
x : G
hx : ∀ᶠ (y : G) in f, y ∈ MulOpposite.op x • K
Kx_complete : IsComplete (MulOpposite.op x • K)
⊢ f ≤ 𝓟 (MulOpposite.op x • K)

Tactic:
simpa using hx

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
⊢ ({a | IsTop a} ∪ {a | ∃ b, a ⋖ b}).Countable

Tactic:
exact (subsingleton_isTop α).countable.union countable_setOfPred_covBy_right

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

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
h : a < b
s : Set α
⊢ [s ∈ 𝓝[<] b, s ∈ 𝓝[Ico a b] b, s ∈ 𝓝[Ioo a b] b, ∃ l ∈ Ico a b, Ioo l b ⊆ s, ∃ l ∈ Iio b, Ioo l b ⊆ s].TFAE

Tactic:
by -- 4 : `s` includes `(l, b)` for some `l < b`
  simpa using! TFAE_mem_nhdsGT h.dual (ofDual ⁻¹' s)

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 atTop
hg : Tendsto g l (𝓝 C)
this : Tendsto (fun x ↦ f x * -g x) l atTop
⊢ Tendsto (fun x ↦ f x * g x) l atBot

Tactic:
simpa only [Function.comp_def, neg_mul_eq_mul_neg, neg_neg] using
    tendsto_neg_atTop_atBot.comp this

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 : α → 𝕜
a : 𝕜
h : Tendsto f l (𝓝 a)
hg : Tendsto g l atTop
⊢ Tendsto (fun x ↦ f x * (g x)⁻¹) l (𝓝 0)

Tactic:
exact mul_zero a ▸ h.mul (tendsto_inv_atTop_zero.comp hg)

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

Goal state before:
pp: α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
h_nhds : ∀ (a : α), 𝓝 a = ⨅ r, ⨅ (_ : r > 1), 𝓟 {b | |a / b|ₘ < r}
a : α
⊢ ⨅ r, ⨅ (_ : r > 1), 𝓟 {b | |a / b|ₘ < r} = 𝓝 a

Tactic:
let := Preorder.topology α

Goal state after:
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
h_nhds : ∀ (a : α), 𝓝 a = ⨅ r, ⨅ (_ : r > 1), 𝓟 {b | |a / b|ₘ < r}
a : α
this : TopologicalSpace α := Preorder.topology α
⊢ ⨅ r, ⨅ (_ : r > 1), 𝓟 {b | |a / b|ₘ < r} = 𝓝 a
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 : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l atTop
⊢ Tendsto (fun x ↦ f x / g x) l (𝓝 0)

Tactic:
simp only [div_eq_mul_inv]
  exact bdd_le_mul_tendsto_zero hb hB hg.inv_tendsto_atTop

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

Goal state before:
pp: α : 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}
x : α
hx : x ∈ t
⊢ ∃ z < x, Ioc z x ⊆ a

Tactic:
apply exists_Ioc_subset_of_mem_nhds (ha.mem_nhds hx.2.1)

Goal state after:
α : 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 α := ⋯
x : α
hx : x ∈ t
⊢ ∃ l, l < 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 β := {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 | x ∈ t ∧ ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}.Countable

Tactic:
have I : InjOn f s := by
    apply StrictMonoOn.injOn
    intro x hx y hy hxy
    calc
      f x < z x := (hz x hx).1
      _ ≤ f y := (hz x hx).2 y hy.1 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
I : InjOn f s
⊢ {x | x ∈ t ∧ ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}.Countable
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 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : AddCircle p
hx : x ≠ ↑a
⊢ ContinuousAt (⇑(equivIoc p a)) x

Tactic:
induction x using QuotientAddGroup.induction_on
  rw [ContinuousAt, Filter.Tendsto, QuotientAddGroup.nhds_eq, Filter.map_map]
  exact (continuousAt_toIocMod hp.out a <| not_modEq_iff_ne_mod_zmultiples.mpr hx).codRestrict _

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)
u : AddCircle p
n : ℕ
h : 0 < n
⊢ addOrderOf u = n ↔ ∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = u

Tactic:
refine ⟨QuotientAddGroup.induction_on u ?_, ?_⟩

Goal state after:
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

case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
⊢ ∀ (z : 𝕜), addOrderOf ↑z = n → ∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = ↑z
Module: Mathlib.Algebra.Category.ModuleCat.Subobject

Goal state before:
pp: R : Type u
inst✝ : Ring R
M : ModuleCat R
S T : Submodule R ↑M
⊢ { toFun := fun N ↦ mk (↟N.subtype), invFun := fun S ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } S ≤
      { toFun := fun N ↦ mk (↟N.subtype), invFun := fun S ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } T ↔
    S ≤ T

Tactic:
by
        refine ⟨fun h => ?_, fun h => mk_le_mk_of_comm (↟(Submodule.inclusion h)) rfl⟩
        convert! LinearMap.range_comp_le_range (ofMkLEMk _ _ h).hom (ofHom T.subtype).hom
        · rw [← hom_comp, ofMkLEMk_comp]
          exact (Submodule.range_subtype _).symm
        · exact (Submodule.range_subtype _).symm

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

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
h : f a = f (a + p)
⊢ ∀ (a_1 b : ↑(Icc a (a + p))),
    EndpointIdent p a a_1 b → (Icc a (a + p)).domRestrict f a_1 = (Icc a (a + p)).domRestrict f b

Tactic:
by
            rintro _ _ ⟨_⟩
            exact h

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

Goal state before:
pp: C : Type u_2
inst✝² : Category.{v_2, u_2} C
inst✝¹ : Preadditive C
inst✝ : Balanced C
n : ℕ
S : ComposableArrows C n
hS : S.Exact
k : ℕ
hk : k + 3 ≤ n
h₀ : S.map' k (k + 1) ⋯ ⋯ = 0
h₁ : S.map' (k + 2) (k + 3) ⋯ hk = 0
⊢ IsIso (S.map' (k + 1) (k + 2) ⋯ ⋯)

Tactic:
by
  have := (hS.exact k).mono_g h₀
  have := (hS.exact (k + 1)).epi_f h₁
  apply isIso_of_mono_of_epi

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

Goal state before:
pp: case add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r ↦ r • F.map f') = (f₁.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r ↦ r • F.map f') = (f₂.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
⊢ (sum (f₁ ≫ g + f₂ ≫ g) fun f' r ↦ r • F.map f') =
    ((f₁ + f₂).sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'

Tactic:
Finsupp.sum_add_index',

Goal state after:
case add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r ↦ r • F.map f') = (f₁.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r ↦ r • F.map f') = (f₂.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
⊢ ((sum (f₁ ≫ g) fun f' r ↦ r • F.map f') + sum (f₂ ≫ g) fun f' r ↦ r • F.map f') =
    ((f₁ + f₂).sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'

case add.h_zero
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r ↦ r • F.map f') = (f₁.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r ↦ r • F.map f') = (f₂.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
⊢ ∀ (a : X ⟶ Z), 0 • F.map a = 0

case add.h_add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r ↦ r • F.map f') = (f₁.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r ↦ r • F.map f') = (f₂.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
⊢ ∀ (a : X ⟶ Z) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case add.h_zero
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r ↦ r • F.map f') = (f₁.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r ↦ r • F.map f') = (f₂.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
⊢ ∀ (a : X ⟶ Z), 0 • F.map a = 0

pp: case add.h_add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r ↦ r • F.map f') = (f₁.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r ↦ r • F.map f') = (f₂.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
⊢ ∀ (a : X ⟶ Z) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a

Tactic:
· intros; rw [zero_smul]

Goal state after:
case add.h_add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
g : Y ⟶ Z
f₁ f₂ : (X ⟶ Y) →₀ R
w₁ : (sum (f₁ ≫ g) fun f' r ↦ r • F.map f') = (f₁.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
w₂ : (sum (f₂ ≫ g) fun f' r ↦ r • F.map f') = (f₂.sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'
⊢ ∀ (a : X ⟶ Z) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case single.add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₁.sum fun f' r ↦ r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₂.sum fun f' r ↦ r • F.map f'
⊢ (sum (single f' r ≫ f₁ + single f' r ≫ f₂) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ (f₁ + f₂).sum fun f' r ↦ r • F.map f'

Tactic:
Finsupp.sum_add_index',

Goal state after:
case single.add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₁.sum fun f' r ↦ r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₂.sum fun f' r ↦ r • F.map f'
⊢ ((sum (single f' r ≫ f₁) fun f' r ↦ r • F.map f') + sum (single f' r ≫ f₂) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ (f₁ + f₂).sum fun f' r ↦ r • F.map f'

case single.add.h_zero
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₁.sum fun f' r ↦ r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₂.sum fun f' r ↦ r • F.map f'
⊢ ∀ (a : X ⟶ Z), 0 • F.map a = 0

case single.add.h_add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₁.sum fun f' r ↦ r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₂.sum fun f' r ↦ r • F.map f'
⊢ ∀ (a : X ⟶ Z) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a