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

Goal state before:
pp: G : Type u
inst✝⁵ : TopologicalSpace G
H : Type v
inst✝⁴ : TopologicalSpace H
M : Type u_1
N : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : TopologicalSpace N
inst✝¹ : Mul M
inst✝ : Mul N
⊢ Continuous id

Tactic:
;

Goal state after:
G : Type u
inst✝⁵ : TopologicalSpace G
H : Type v
inst✝⁴ : TopologicalSpace H
M : Type u_1
N : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : TopologicalSpace N
inst✝¹ : Mul M
inst✝ : Mul N
⊢ Continuous id
Module: Mathlib.Topology.Algebra.ContinuousMonoidHom

Goal state before:
pp: case e'_2
G : Type u
inst✝³ : TopologicalSpace G
H : Type v
inst✝² : TopologicalSpace H
inst✝¹ : Mul G
inst✝ : Mul H
e : G ≃* H
he : ∀ (s : Set H), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s
s : Set G
⊢ s = ⇑e ⁻¹' ⇑e.symm ⁻¹' s

Tactic:
;

Goal state after:
case e'_2
G : Type u
inst✝³ : TopologicalSpace G
H : Type v
inst✝² : TopologicalSpace H
inst✝¹ : Mul G
inst✝ : Mul H
e : G ≃* H
he : ∀ (s : Set H), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s
s : Set G
⊢ s = ⇑e ⁻¹' ⇑e.symm ⁻¹' s
Module: Mathlib.Topology.Algebra.Ring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f g : RingTopology R
a✝ : f.toTopologicalSpace = g.toTopologicalSpace
⊢ f = g

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : Ring R
f g : RingTopology R
a✝ : f.toTopologicalSpace = g.toTopologicalSpace
⊢ f = g
Module: Mathlib.Topology.Algebra.Ring.Basic

Goal state before:
pp: case mk
R : Type u_1
inst✝ : Ring R
g : RingTopology R
toTopologicalSpace✝ : TopologicalSpace R
toIsTopologicalRing✝ : IsTopologicalRing R
a✝ :
  { toTopologicalSpace := toTopologicalSpace✝, toIsTopologicalRing := toIsTopologicalRing✝ }.toTopologicalSpace =
    g.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace✝, toIsTopologicalRing := toIsTopologicalRing✝ } = g

Tactic:
;

Goal state after:
case mk
R : Type u_1
inst✝ : Ring R
g : RingTopology R
toTopologicalSpace✝ : TopologicalSpace R
toIsTopologicalRing✝ : IsTopologicalRing R
a✝ :
  { toTopologicalSpace := toTopologicalSpace✝, toIsTopologicalRing := toIsTopologicalRing✝ }.toTopologicalSpace =
    g.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace✝, toIsTopologicalRing := toIsTopologicalRing✝ } = g
Module: Mathlib.Topology.Algebra.Ring.Basic

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝ : Ring R
toTopologicalSpace✝¹ : TopologicalSpace R
toIsTopologicalRing✝¹ : IsTopologicalRing R
toTopologicalSpace✝ : TopologicalSpace R
toIsTopologicalRing✝ : IsTopologicalRing R
a✝ :
  { toTopologicalSpace := toTopologicalSpace✝¹, toIsTopologicalRing := toIsTopologicalRing✝¹ }.toTopologicalSpace =
    { toTopologicalSpace := toTopologicalSpace✝, toIsTopologicalRing := toIsTopologicalRing✝ }.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace✝¹, toIsTopologicalRing := toIsTopologicalRing✝¹ } =
    { toTopologicalSpace := toTopologicalSpace✝, toIsTopologicalRing := toIsTopologicalRing✝ }

Tactic:
;

Goal state after:
case mk.mk
R : Type u_1
inst✝ : Ring R
toTopologicalSpace✝¹ : TopologicalSpace R
toIsTopologicalRing✝¹ : IsTopologicalRing R
toTopologicalSpace✝ : TopologicalSpace R
toIsTopologicalRing✝ : IsTopologicalRing R
a✝ :
  { toTopologicalSpace := toTopologicalSpace✝¹, toIsTopologicalRing := toIsTopologicalRing✝¹ }.toTopologicalSpace =
    { toTopologicalSpace := toTopologicalSpace✝, toIsTopologicalRing := toIsTopologicalRing✝ }.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace✝¹, toIsTopologicalRing := toIsTopologicalRing✝¹ } =
    { toTopologicalSpace := toTopologicalSpace✝, toIsTopologicalRing := toIsTopologicalRing✝ }
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
this : Continuous fun x ↦ (↑x)⁻¹
⊢ Continuous fun x ↦ ↑((unitsEquivPos R).invFun x)⁻¹

Tactic:
by
      simpa [Topology.IsEmbedding.subtypeVal.continuous_iff, Function.comp_def]

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

Goal state before:
pp: case inl
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x ↦ a ^ x
ha₀ : 1 < a
m : ℤ
hm : a ^ (m - 1) < a ^ m
hm' : a ^ m < a ^ (m - 1) * a * a
⊢ ∃ a_1, (fun x ↦ a ^ x) a_1 = a ^ (m - 1)

pp: case inr
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
⊢ ∃ a_1, (fun x ↦ a ^ x) a_1 = b

Tactic:
;

Goal state after:
case inl
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x ↦ a ^ x
ha₀ : 1 < a
m : ℤ
hm : a ^ (m - 1) < a ^ m
hm' : a ^ m < a ^ (m - 1) * a * a
⊢ ∃ a_1, (fun x ↦ a ^ x) a_1 = a ^ (m - 1)

case inr
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
⊢ ∃ a_1, (fun x ↦ a ^ x) a_1 = b
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : FirstCountableTopology G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : CompleteSpace G
this✝¹ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : (𝓤 (G ⧸ N)).IsCountablyGenerated
u : ℕ → Set G
hu : (𝓝 1).HasAntitoneBasis u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : (𝓝 1).HasBasis (fun x ↦ True) fun x ↦ mk '' u x
v_anti : Antitone fun x ↦ mk '' u x
x : ℕ → G ⧸ N
hx : CauchySeq x
key₀ : ∀ (i j : ℕ), ∃ M, j < M ∧ ∀ (a b : ℕ), M ≤ a → M ≤ b → ∀ (g : G), x b = ↑g → ∃ g', g / g' ∈ u i ∧ x a = ↑g'
φ : ℕ → ℕ := fun n ↦ Nat.recOn n (Classical.choose ⋯) fun k yk ↦ Classical.choose ⋯
hφ :
  ∀ (n : ℕ),
    φ n < φ (n + 1) ∧
      ∀ (a b : ℕ), φ (n + 1) ≤ a → φ (n + 1) ≤ b → ∀ (g : G), x b = ↑g → ∃ g', g / g' ∈ u (n + 1) ∧ x a = ↑g'
x' : (n : ℕ) → (g : G) ×' x (φ (n + 1)) = ↑g :=
  fun n ↦ Nat.recOn n ⟨Classical.choose ⋯, ⋯⟩ fun k hk ↦ ⟨Classical.choose ⋯, ⋯⟩
hx' : ∀ (n : ℕ), (x' n).fst / (x' (n + 1)).fst ∈ u (n + 1)
h𝓤G : (𝓤 G).HasBasis (fun x ↦ True) fun i ↦ {x | x.2 / x.1 ∈ u i}
⊢ ∀ (i : ℕ), True → ∃ N_1, ∀ n ≥ N_1, ((x' n).fst, (x' N_1).fst) ∈ {x | x.2 / x.1 ∈ u i}

Tactic:
simp only [mem_ofPred_eq, forall_true_left]

Goal state after:
G : Type u
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : FirstCountableTopology G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : CompleteSpace G
this✝¹ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : (𝓤 (G ⧸ N)).IsCountablyGenerated
u : ℕ → Set G
hu : (𝓝 1).HasAntitoneBasis u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : (𝓝 1).HasBasis (fun x ↦ True) fun x ↦ mk '' u x
v_anti : Antitone fun x ↦ mk '' u x
x : ℕ → G ⧸ N
hx : CauchySeq x
key₀ : ∀ (i j : ℕ), ∃ M, j < M ∧ ∀ (a b : ℕ), M ≤ a → M ≤ b → ∀ (g : G), x b = ↑g → ∃ g', g / g' ∈ u i ∧ x a = ↑g'
φ : ℕ → ℕ := fun n ↦ Nat.recOn n (Classical.choose ⋯) fun k yk ↦ Classical.choose ⋯
hφ :
  ∀ (n : ℕ),
    φ n < φ (n + 1) ∧
      ∀ (a b : ℕ), φ (n + 1) ≤ a → φ (n + 1) ≤ b → ∀ (g : G), x b = ↑g → ∃ g', g / g' ∈ u (n + 1) ∧ x a = ↑g'
x' : (n : ℕ) → (g : G) ×' x (φ (n + 1)) = ↑g :=
  fun n ↦ Nat.recOn n ⟨Classical.choose ⋯, ⋯⟩ fun k hk ↦ ⟨Classical.choose ⋯, ⋯⟩
hx' : ∀ (n : ℕ), (x' n).fst / (x' (n + 1)).fst ∈ u (n + 1)
h𝓤G : (𝓤 G).HasBasis (fun x ↦ True) fun i ↦ {x | x.2 / x.1 ∈ u i}
⊢ ∀ (i : ℕ), ∃ N_1, ∀ n ≥ N_1, (x' N_1).fst / (x' n).fst ∈ u i
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
us : UniformSpace G
inst✝² : IsRightUniformGroup G
inst✝¹ : FirstCountableTopology G
N : Subgroup G
inst✝ : N.Normal
hG : CompleteSpace G
⊢ CompleteSpace (G ⧸ N)

Tactic:
by
  have : IsTopologicalGroup.rightUniformSpace G = us := by
    ext : 1
    rw [@IsRightUniformGroup.uniformity_eq (G := G) us _ _]
    rfl
  rw [← this] at hG
  infer_instance

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : OrderTopology α
a x : α
⊢ ⨅ (_ : (Equiv.divLeft a) x > 1), 𝓟 {a_1 | a / a_1 < (Equiv.divLeft a) x} = ⨅ (_ : x ∈ Iio a), 𝓟 (Ioi x)

Tactic:
;

Goal state after:
case refine_1
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : OrderTopology α
a x : α
⊢ ⨅ (_ : (Equiv.divLeft a) x > 1), 𝓟 {a_1 | a / a_1 < (Equiv.divLeft a) x} = ⨅ (_ : x ∈ Iio a), 𝓟 (Ioi x)
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: case refine_2
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : OrderTopology α
a x : α
⊢ ⨅ (_ : (Equiv.divRight a) x > 1), 𝓟 {a_1 | ((Equiv.divRight a) x)⁻¹ < a / a_1} = ⨅ (_ : x ∈ Ioi a), 𝓟 (Iio x)

Tactic:
;

Goal state after:
case refine_2
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : OrderTopology α
a x : α
⊢ ⨅ (_ : (Equiv.divRight a) x > 1), 𝓟 {a_1 | ((Equiv.divRight a) x)⁻¹ < a / a_1} = ⨅ (_ : x ∈ Ioi a), 𝓟 (Iio x)
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 : α
this : TopologicalSpace α := Preorder.topology α
⊢ ⨅ r, ⨅ (_ : r > 1), 𝓟 {b | |a / b|ₘ < r} = 𝓝 a

Tactic:
;

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.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
x : α
hx hx' : x ∈ e.source ∩ s
⊢ ↑e.symm (↑e x) = ↑e'.symm (↑e x)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
x : α
hx hx' : x ∈ e.source ∩ s
⊢ ↑e.symm (↑e x) = ↑e'.symm (↑e x)
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 : 𝕜
hc : c ≠ 0
⊢ Tendsto (fun x ↦ c * x ^ n) atTop (𝓝 d) ↔ n = 0 ∧ c = d

Tactic:
simp [tendsto_const_mul_pow_nhds_iff', hc]

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

Goal state before:
pp: α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
t : OrderTopology α
s : Set α
⊢ IsOpen[Preorder.topology α] s ↔ GenerateOpen {s | ∃ a, s = Ioi a ∨ s = Iio a} s

Tactic:
;

Goal state after:
α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
t : OrderTopology α
s : Set α
⊢ IsOpen[Preorder.topology α] s ↔ GenerateOpen {s | ∃ a, s = Ioi a ∨ s = Iio a} s
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e'✝ e' : PartialEquiv β γ
h : e.target = e'.source
x : α
hx : x ∈ e.source
⊢ (↑e.symm ∘ ↑e'.symm) ((↑e' ∘ ↑e) x) = x

Tactic:
simp [hx, ← h]

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

Goal state before:
pp: α : Type u
β : Type v
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
f : β → α
a : α
x : Filter β
⊢ ((∀ i ∈ Iio a, ∀ᶠ (a : β) in x, f a ∈ Ioi i) ∧ ∀ i ∈ Ioi a, ∀ᶠ (a : β) in x, f a ∈ Iio i) ↔
    (∀ a' < a, ∀ᶠ (b : β) in x, a' < f b) ∧ ∀ a' > a, ∀ᶠ (b : β) in x, f b < a'

Tactic:
;

Goal state after:
α : Type u
β : Type v
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
f : β → α
a : α
x : Filter β
⊢ ((∀ i ∈ Iio a, ∀ᶠ (a : β) in x, f a ∈ Ioi i) ∧ ∀ i ∈ Ioi a, ∀ᶠ (a : β) in x, f a ∈ Iio i) ↔
    (∀ a' < a, ∀ᶠ (b : β) in x, a' < f b) ∧ ∀ a' > a, ∀ᶠ (b : β) in x, f b < a'
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
A : (e.trans e.symm).source = e.source
x : α
hx : x ∈ (e.trans e.symm).source
⊢ ↑(e.trans e.symm) x = ↑(ofSet e.source) x

Tactic:
rw [A] at hx

Goal state after:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
A : (e.trans e.symm).source = e.source
x : α
hx : x ∈ e.source
⊢ ↑(e.trans e.symm) x = ↑(ofSet e.source) x
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case hs
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
η : Type u_5
ε : Type u_6
e : PartialEquiv α β
f : PartialEquiv β γ
e' : PartialEquiv δ η
f' : PartialEquiv η ε
x : α
y : δ
⊢ (x ∈ e.source ∧ y ∈ e'.source) ∧ ↑e x ∈ f.source ∧ ↑e' y ∈ f'.source ↔
    (x ∈ e.source ∧ ↑e x ∈ f.source) ∧ y ∈ e'.source ∧ ↑e' y ∈ f'.source

Tactic:
;

Goal state after:
case hs
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
η : Type u_5
ε : Type u_6
e : PartialEquiv α β
f : PartialEquiv β γ
e' : PartialEquiv δ η
f' : PartialEquiv η ε
x : α
y : δ
⊢ (x ∈ e.source ∧ y ∈ e'.source) ∧ ↑e x ∈ f.source ∧ ↑e' y ∈ f'.source ↔
    (x ∈ e.source ∧ ↑e x ∈ f.source) ∧ y ∈ e'.source ∧ ↑e' y ∈ f'.source
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
hu : ∃ u, a < u
hl : ∃ l, l < a
⊢ (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b) = (⨅ i, ⨅ (_ : i < a), 𝓟 (Ioi i)) ⊓ ⨅ i, ⨅ (_ : a < i), 𝓟 (Iio i)

Tactic:
;

Goal state after:
α : Type u
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
hu : ∃ u, a < u
hl : ∃ l, l < a
⊢ (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b) = (⨅ i, ⨅ (_ : i < a), 𝓟 (Ioi i)) ⊓ ⨅ i, ⨅ (_ : a < i), 𝓟 (Iio i)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x✝ : TopologicalSpace α := Preorder.topology α
⊢ induced f inst✝¹ ≤ Preorder.topology α

Tactic:
;

Goal state after:
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x✝ : TopologicalSpace α := Preorder.topology α
⊢ induced f inst✝¹ ≤ Preorder.topology α
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
⊢ induced f inst✝¹ = Preorder.topology α

Tactic:
;

Goal state after:
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
⊢ induced f inst✝¹ = Preorder.topology α
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
S : ShortComplex C
hS : S.Exact
h₁ : P S.X₁
h₃ : P S.X₃
d : S.HomologyData := S.homologyData
this : Epi d.left.f'
⊢ P S.X₂

Tactic:
have := hS.mono_g' d.right

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
S : ShortComplex C
hS : S.Exact
h₁ : P S.X₁
h₃ : P S.X₃
d : S.HomologyData := S.homologyData
this✝ : Epi d.left.f'
this : Mono d.right.g'
⊢ P S.X₂
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'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
f : A →ₗ[R] B
r : R
c : CharacterModule B
x : A
⊢ (AddMonoidHom.comp (r • c) f.toAddMonoidHom) x = ((RingHom.id R) r • AddMonoidHom.comp c f.toAddMonoidHom) x

Tactic:
;

Goal state after:
R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
A' : Type u_1
inst✝⁴ : AddCommGroup A'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
f : A →ₗ[R] B
r : R
c : CharacterModule B
x : A
⊢ (AddMonoidHom.comp (r • c) f.toAddMonoidHom) x = ((RingHom.id R) r • AddMonoidHom.comp c f.toAddMonoidHom) x
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'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
e : A ≃ₗ[R] B
c : CharacterModule B
x✝ : B
⊢ ((dual ↑e.symm ∘ₗ dual ↑e) c) x✝ = (LinearMap.id c) x✝

Tactic:
;

Goal state after:
R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
A' : Type u_1
inst✝⁴ : AddCommGroup A'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
e : A ≃ₗ[R] B
c : CharacterModule B
x✝ : B
⊢ ((dual ↑e.symm ∘ₗ dual ↑e) c) x✝ = (LinearMap.id c) x✝
Module: Mathlib.Topology.Instances.AddCircle.Defs

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

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

Goal state after:
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
x✝ : 𝕜
⊢ toIcoDiv hp a x = toIocDiv hp a x
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'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
e : A ≃ₗ[R] B
c : CharacterModule A
x✝ : A
⊢ ((dual ↑e ∘ₗ dual ↑e.symm) c) x✝ = (LinearMap.id c) x✝

Tactic:
;

Goal state after:
R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
A' : Type u_1
inst✝⁴ : AddCommGroup A'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
e : A ≃ₗ[R] B
c : CharacterModule A
x✝ : A
⊢ ((dual ↑e ∘ₗ dual ↑e.symm) c) x✝ = (LinearMap.id c) x✝
Module: Mathlib.Algebra.Category.Grp.IsFinite

Goal state before:
pp: ⊢ Finite ↑(of PUnit.{u + 1})

Tactic:
;

Goal state after:
⊢ Finite ↑(of PUnit.{u + 1})
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'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
c : CharacterModule (A ⊗[R] B)
r : R
a : A
x✝ : B
⊢ (AddMonoidHom.comp c ↑((mk R A B) (r • a))) x✝ = ((RingHom.id R) r • AddMonoidHom.comp c ↑((mk R A B) a)) x✝

Tactic:
;

Goal state after:
R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
A' : Type u_1
inst✝⁴ : AddCommGroup A'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
c : CharacterModule (A ⊗[R] B)
r : R
a : A
x✝ : B
⊢ (AddMonoidHom.comp c ↑((mk R A B) (r • a))) x✝ = ((RingHom.id R) r • AddMonoidHom.comp c ↑((mk R A B) a)) x✝
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'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
r : R
c : CharacterModule (A ⊗[R] B)
x✝¹ : A
x✝ : B
⊢ ({ toFun := fun x ↦ AddMonoidHom.comp (r • c) ↑((mk R A B) x), map_add' := ⋯, map_smul' := ⋯ } x✝¹) x✝ =
    (((RingHom.id R) r • { toFun := fun x ↦ AddMonoidHom.comp c ↑((mk R A B) x), map_add' := ⋯, map_smul' := ⋯ }) x✝¹)
      x✝

Tactic:
;

Goal state after:
R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
A' : Type u_1
inst✝⁴ : AddCommGroup A'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
r : R
c : CharacterModule (A ⊗[R] B)
x✝¹ : A
x✝ : B
⊢ ({ toFun := fun x ↦ AddMonoidHom.comp (r • c) ↑((mk R A B) x), map_add' := ⋯, map_smul' := ⋯ } x✝¹) x✝ =
    (((RingHom.id R) r • { toFun := fun x ↦ AddMonoidHom.comp c ↑((mk R A B) x), map_add' := ⋯, map_smul' := ⋯ }) x✝¹)
      x✝
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'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
x✝ : CharacterModule (A ⊗[R] B)
z : A ⊗[R] B
⊢ ((uncurry ∘ₗ curry) x✝) z = (LinearMap.id x✝) z

Tactic:
;

Goal state after:
R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
A' : Type u_1
inst✝⁴ : AddCommGroup A'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
x✝ : CharacterModule (A ⊗[R] B)
z : A ⊗[R] B
⊢ ((uncurry ∘ₗ curry) x✝) z = (LinearMap.id x✝) z
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: A : Type uA
inst✝ : AddCommGroup A
a : A
h : a ≠ 0
⊢ ∃ c, c a ≠ 0

Tactic:
;

Goal state after:
A : Type uA
inst✝ : AddCommGroup A
a : A
h : a ≠ 0
⊢ ∃ c, c a ≠ 0
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: A : Type uA
inst✝ : AddCommGroup A
a : A
h : ∀ (c : CharacterModule A), c a = 0
⊢ a = 0

Tactic:
contrapose! h; exact exists_character_apply_ne_zero_of_ne_zero h

Goal state after:
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'
h : Function.Surjective ⇑(dual f)
a : A
h0 : f a = 0
c : CharacterModule A'
⊢ ((dual f) c) a = 0

Tactic:
;

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'
h : Function.Surjective ⇑(dual f)
a : A
h0 : f a = 0
c : CharacterModule A'
⊢ ((dual f) c) a = 0
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) ψ
⊢ (fun f ↦ ofHom f) (AddEquiv.ulift.symm.addMonoidHomCongrRightEquiv χ) =
    (fun f ↦ ofHom f) (AddEquiv.ulift.symm.addMonoidHomCongrRightEquiv ψ)

Tactic:
refine hc.hom_ext (fun j ↦ ?_)

Goal state after:
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) ψ
j : J
⊢ c.ι.app j ≫ (fun f ↦ ofHom f) (AddEquiv.ulift.symm.addMonoidHomCongrRightEquiv χ) =
    c.ι.app j ≫ (fun f ↦ ofHom f) (AddEquiv.ulift.symm.addMonoidHomCongrRightEquiv ψ)