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

Goal state before:
pp: case inl.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hbd : b < d
hdc : d < c
⊢ a < d ∧ d < c

Tactic:
;

Goal state after:
case inl.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hbd : b < d
hdc : d < c
⊢ a < d ∧ d < c
Module: Mathlib.Order.Circular

Goal state before:
pp: case inl.inr.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hdc : d < c
hcb : c < b
⊢ a < d ∧ d < c

Tactic:
;

Goal state after:
case inl.inr.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hdc : d < c
hcb : c < b
⊢ a < d ∧ d < c
Module: Mathlib.Order.Circular

Goal state before:
pp: case inl.inr.inr
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hcb : c < b
hbd : b < d
⊢ a < d ∧ d < c

Tactic:
;

Goal state after:
case inl.inr.inr
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hcb : c < b
hbd : b < d
⊢ a < d ∧ d < c
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inl.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hbd : b < d
hdc : d < c
⊢ a < d ∧ d < c

Tactic:
;

Goal state after:
case inr.inl.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hbd : b < d
hdc : d < c
⊢ a < d ∧ d < c
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inl.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hbd : b < d
hdc : d < c
⊢ d < c ∧ c < a

Tactic:
;

Goal state after:
case inr.inl.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hbd : b < d
hdc : d < c
⊢ d < c ∧ c < a
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inl.inr.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hdc : d < c
hcb : c < b
⊢ a < d ∧ d < c

Tactic:
;

Goal state after:
case inr.inl.inr.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hdc : d < c
hcb : c < b
⊢ a < d ∧ d < c
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inl.inr.inr
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hcb : c < b
hbd : b < d
⊢ a < d ∧ d < c

Tactic:
;

Goal state after:
case inr.inl.inr.inr
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hcb : c < b
hbd : b < d
⊢ a < d ∧ d < c
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inr.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hbd : b < d
hdc : d < c
⊢ a < d ∧ d < c

Tactic:
;

Goal state after:
case inr.inr.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hbd : b < d
hdc : d < c
⊢ a < d ∧ d < c
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inr.inr.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hdc : d < c
hcb : c < b
⊢ a < d ∧ d < c

Tactic:
;

Goal state after:
case inr.inr.inr.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hdc : d < c
hcb : c < b
⊢ a < d ∧ d < c
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inr.inr.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hdc : d < c
hcb : c < b
⊢ d < c ∧ c < a

Tactic:
;

Goal state after:
case inr.inr.inr.inl
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hdc : d < c
hcb : c < b
⊢ d < c ∧ c < a
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inr.inr.inr
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
⊢ a < d ∧ d < c

Tactic:
;

Goal state after:
case inr.inr.inr.inr
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
⊢ a < d ∧ d < c
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inr.inr.inr
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
⊢ d < c ∧ c < a

Tactic:
;

Goal state after:
case inr.inr.inr.inr
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
⊢ d < c ∧ c < a
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝ : NonAssocRing α
h : Periodic f c
n : ℕ
⊢ f (x - ↑n * c) = f x

Tactic:
simpa only [nsmul_eq_mul] using h.sub_nsmul_eq n

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inr.inr.inr
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
⊢ c < a ∧ a < d

Tactic:
;

Goal state after:
case inr.inr.inr.inr
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
⊢ c < a ∧ a < d
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
i1 : a * b ^ m < a * b ^ (n + 1)
⊢ m = n

Tactic:
have i2 := hx.2.1.trans_lt hx.1.2

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
i1 : a * b ^ m < a * b ^ (n + 1)
i2 : a * b ^ n < a * b ^ (m + 1)
⊢ m = n
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
r r' : R
eq1 : r • y = r' • y
⊢ (extendIdealTo i f h y) r = (extendIdealTo i f h y) r'

Tactic:
rw [← sub_eq_zero, ← map_sub]
  convert! ExtensionOfMaxAdjoin.extendIdealTo_wd' i f h (r - r') _
  rw [sub_smul, sub_eq_zero, eq1]

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑x = ↑⟨a, ha⟩ + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
⊢ ↑(fst i x) - a ∈ (extensionOfMax i f).domain

Tactic:
;

Goal state after:
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑x = ↑⟨a, ha⟩ + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
⊢ ↑(fst i x) - a ∈ (extensionOfMax i f).domain
Module: Mathlib.Data.Nat.Cast.Field

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
k : ℕ
hn : ↑0 ≠ 0
⊢ False

Tactic:
;

Goal state after:
K : Type u_1
inst✝ : DivisionSemiring K
k : ℕ
hn : ↑0 ≠ 0
⊢ False
Module: Mathlib.Data.Nat.Cast.Field

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : DivisionSemiring K
m n : ℕ
inst✝ : CharZero K
hn : 0 ∣ n
hm : 0 ∣ m
⊢ ↑(m / 0) / ↑(n / 0) = ↑m / ↑n

pp: case inr
K : Type u_1
inst✝¹ : DivisionSemiring K
d m n : ℕ
inst✝ : CharZero K
hn : d ∣ n
hm : d ∣ m
hd : d ≠ 0
⊢ ↑(m / d) / ↑(n / d) = ↑m / ↑n

Tactic:
;

Goal state after:
case inl
K : Type u_1
inst✝¹ : DivisionSemiring K
m n : ℕ
inst✝ : CharZero K
hn : 0 ∣ n
hm : 0 ∣ m
⊢ ↑(m / 0) / ↑(n / 0) = ↑m / ↑n

case inr
K : Type u_1
inst✝¹ : DivisionSemiring K
d m n : ℕ
inst✝ : CharZero K
hn : d ∣ n
hm : d ∣ m
hd : d ≠ 0
⊢ ↑(m / d) / ↑(n / d) = ↑m / ↑n
Module: Mathlib.Data.Nat.Periodic

Goal state before:
pp: case e_a.e_f
n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ p = (fun x ↦ p x) ∘ fun x ↦ x % a

Tactic:
;

Goal state after:
case e_a.e_f
n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ p = (fun x ↦ p x) ∘ fun x ↦ x % a
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
Q : Type v
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
h : Baer R Q
f : M →ₗ[R] N
hf : Function.Injective ⇑f
g : M →ₗ[R] Q
this : Fact (Function.Injective ⇑f)
x y : N
⊢ ↑(extensionOfMax f g).toLinearPMap ⟨x + y, ⋯⟩ = ↑(extensionOfMax f g).toLinearPMap (⟨x, ⋯⟩ + ⟨y, ⋯⟩)

Tactic:
;

Goal state after:
R : Type u
inst✝⁶ : Ring R
Q : Type v
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
h : Baer R Q
f : M →ₗ[R] N
hf : Function.Injective ⇑f
g : M →ₗ[R] Q
this : Fact (Function.Injective ⇑f)
x y : N
⊢ ↑(extensionOfMax f g).toLinearPMap ⟨x + y, ⋯⟩ = ↑(extensionOfMax f g).toLinearPMap (⟨x, ⋯⟩ + ⟨y, ⋯⟩)
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
Q : Type v
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
h : Baer R Q
f : M →ₗ[R] N
hf : Function.Injective ⇑f
g : M →ₗ[R] Q
this : Fact (Function.Injective ⇑f)
r : R
x : N
⊢ ↑(extensionOfMax f g).toLinearPMap ⟨r • x, ⋯⟩ = ↑(extensionOfMax f g).toLinearPMap ((RingHom.id R) r • ⟨x, ⋯⟩)

Tactic:
;

Goal state after:
R : Type u
inst✝⁶ : Ring R
Q : Type v
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
h : Baer R Q
f : M →ₗ[R] N
hf : Function.Injective ⇑f
g : M →ₗ[R] Q
this : Fact (Function.Injective ⇑f)
r : R
x : N
⊢ ↑(extensionOfMax f g).toLinearPMap ⟨r • x, ⋯⟩ = ↑(extensionOfMax f g).toLinearPMap ((RingHom.id R) r • ⟨x, ⋯⟩)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a n : ℕ
⊢ #({x ∈ Ico n (n + a) | a.Coprime x}) = φ a

Tactic:
rw [totient, filter_Ico_card_eq_of_periodic, count_eq_card_filter_range]
  exact periodic_coprime a

Goal state after:
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a k n : ℕ
a_ne_zero : a ≠ 0
x✝ : ℕ
⊢ #({x ∈ Ico k (k + (n % a + a * x✝)) | a.Coprime x}) ≤ φ a * (x✝ + 1)

Tactic:
induction n / a with

Goal state after:
case succ
a k n : ℕ
a_ne_zero : a ≠ 0
i : ℕ
ih : #({x ∈ Ico k (k + (n % a + a * i)) | a.Coprime x}) ≤ φ a * (i + 1)
⊢ #({x ∈ Ico k (k + (n % a + a * (i + 1))) | a.Coprime x}) ≤ φ a * (i + 1 + 1)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
hn : 2 < n
this✝ : Fact (1 < n)
this : NeZero n
⊢ 2 = orderOf (-1)

Tactic:
← orderOf_units,

Goal state after:
n : ℕ
hn : 2 < n
this✝ : Fact (1 < n)
this : NeZero n
⊢ 2 = orderOf ↑(-1)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
hn : 2 < n
⊢ Even (φ n)

Tactic:
have : Fact (1 < n) := ⟨one_lt_two.trans hn⟩
  have : NeZero n := NeZero.of_gt hn
  suffices 2 = orderOf (-1 : (ZMod n)ˣ) by
    rw [← ZMod.card_units_eq_totient, even_iff_two_dvd, this]
    exact orderOf_dvd_card
  rw [← orderOf_units, Units.coe_neg_one, orderOf_neg_one, ringChar.eq (ZMod n) n, if_neg hn.ne']

Goal state after:
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case inl
n : ℕ
hnd : 0 ∣ n
⊢ φ (n / 0) = #({k ∈ range n | n.gcd k = 0})

pp: case inr
n d : ℕ
hnd : d ∣ n
hd0 : d > 0
⊢ φ (n / d) = #({k ∈ range n | n.gcd k = d})

Tactic:
;

Goal state after:
case inl
n : ℕ
hnd : 0 ∣ n
⊢ φ (n / 0) = #({k ∈ range n | n.gcd k = 0})

case inr
n d : ℕ
hnd : d ∣ n
hd0 : d > 0
⊢ φ (n / d) = #({k ∈ range n | n.gcd k = d})
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case mp
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
hap : ¬p ∣ a
b : ℕ
h : b < p ^ n ∧ b * p = a
⊢ False

Tactic:
;

Goal state after:
case mp
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
hap : ¬p ∣ a
b : ℕ
h : b < p ^ n ∧ b * p = a
⊢ False
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: case inr.inr
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
h✝¹ : Nonempty α
h✝ : Nonempty β
⊢ atTop ×ˢ atTop = atTop

Tactic:
simpa [atTop, prod_iInf_left, prod_iInf_right, iInf_prod] using iInf_comm

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Preorder β
l : Filter α
p : β → Prop
f : α → β
hf : Tendsto f l atTop
h_evtl : ∀ᶠ (x : β) in atTop, ∀ (y : β), x ≤ y → p y
⊢ ∀ᶠ (x : α) in l, ∀ (y : β), f x ≤ y → p y

Tactic:
;

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Preorder β
l : Filter α
p : β → Prop
f : α → β
hf : Tendsto f l atTop
h_evtl : ∀ᶠ (x : β) in atTop, ∀ (y : β), x ≤ y → p y
⊢ ∀ᶠ (x : α) in l, ∀ (y : β), f x ≤ y → p y
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Preorder β
l : Filter α
p : β → Prop
f : α → β
hf : Tendsto f l atBot
h_evtl : ∀ᶠ (x : β) in atBot, ∀ y ≤ x, p y
⊢ ∀ᶠ (x : α) in l, ∀ y ≤ f x, p y

Tactic:
;

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Preorder β
l : Filter α
p : β → Prop
f : α → β
hf : Tendsto f l atBot
h_evtl : ∀ᶠ (x : β) in atBot, ∀ y ≤ x, p y
⊢ ∀ᶠ (x : α) in l, ∀ y ≤ f x, p y
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ k < n, ∀ (b : ℕ), N k ≤ b → p (n * b + k)
b : ℕ
hb : ((Finset.range n).sup fun x ↦ n * N x) ≤ b
⊢ p b

Tactic:
← Nat.div_add_mod b n

Goal state after:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ k < n, ∀ (b : ℕ), N k ≤ b → p (n * b + k)
b : ℕ
hb : ((Finset.range n).sup fun x ↦ n * N x) ≤ b
⊢ p (n * (b / n) + b % n)
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α : Type u_3
γ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder γ
f g : α → γ
hf : Tendsto f atBot atBot
hg : Tendsto g atBot atBot
⊢ Tendsto (Prod.map f g) atBot atBot

Tactic:
rw [← prod_atBot_atBot_eq]
  exact hf.prod_map_prod_atBot hg

Goal state after:
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case pos
n : ℕ
hn : n = 0
⊢ φ n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)

pp: case neg
n : ℕ
hn : ¬n = 0
⊢ φ n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)

Tactic:
;

Goal state after:
case pos
n : ℕ
hn : n = 0
⊢ φ n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)

case neg
n : ℕ
hn : ¬n = 0
⊢ φ n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
⊢ (∃ x, Tendsto x atTop l ∧ ∃ᶠ (x_1 : ℕ) in atTop, p (x x_1)) ↔
    ∃ x, Tendsto x atTop l ∧ ∃ᶠ (x_1 : ℕ) in atTop, p (x x_1)

Tactic:
;

Goal state after:
ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
⊢ (∃ x, Tendsto x atTop l ∧ ∃ᶠ (x_1 : ℕ) in atTop, p (x x_1)) ↔
    ∃ x, Tendsto x atTop l ∧ ∃ᶠ (x_1 : ℕ) in atTop, p (x x_1)
Module: Mathlib.Topology.ContinuousMap.Defs

Goal state before:
pp: case mk
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
g : C(X, Y)
toFun✝ : X → Y
continuous_toFun✝ : Continuous[inst✝¹, inst✝] toFun✝
h : { toFun := toFun✝, continuous_toFun := continuous_toFun✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, continuous_toFun := continuous_toFun✝ } = g

Tactic:
;

Goal state after:
case mk
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
g : C(X, Y)
toFun✝ : X → Y
continuous_toFun✝ : Continuous[inst✝¹, inst✝] toFun✝
h : { toFun := toFun✝, continuous_toFun := continuous_toFun✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, continuous_toFun := continuous_toFun✝ } = g
Module: Mathlib.Topology.ContinuousMap.Defs

Goal state before:
pp: case mk.mk
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
toFun✝¹ : X → Y
continuous_toFun✝¹ : Continuous[inst✝¹, inst✝] toFun✝¹
toFun✝ : X → Y
continuous_toFun✝ : Continuous[inst✝¹, inst✝] toFun✝
h :
  { toFun := toFun✝¹, continuous_toFun := continuous_toFun✝¹ }.toFun =
    { toFun := toFun✝, continuous_toFun := continuous_toFun✝ }.toFun
⊢ { toFun := toFun✝¹, continuous_toFun := continuous_toFun✝¹ } =
    { toFun := toFun✝, continuous_toFun := continuous_toFun✝ }

Tactic:
;

Goal state after:
case mk.mk
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
toFun✝¹ : X → Y
continuous_toFun✝¹ : Continuous[inst✝¹, inst✝] toFun✝¹
toFun✝ : X → Y
continuous_toFun✝ : Continuous[inst✝¹, inst✝] toFun✝
h :
  { toFun := toFun✝¹, continuous_toFun := continuous_toFun✝¹ }.toFun =
    { toFun := toFun✝, continuous_toFun := continuous_toFun✝ }.toFun
⊢ { toFun := toFun✝¹, continuous_toFun := continuous_toFun✝¹ } =
    { toFun := toFun✝, continuous_toFun := continuous_toFun✝ }
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
t t' : TopologicalSpace X
h : ∀ (s : Set X), IsOpen[t] s ↔ IsOpen[t'] s
x✝ : Set X
⊢ IsOpen[t] x✝ ↔ IsOpen[t'] x✝

Tactic:
;

Goal state after:
X : Type u
t t' : TopologicalSpace X
h : ∀ (s : Set X), IsOpen[t] s ↔ IsOpen[t'] s
x✝ : Set X
⊢ IsOpen[t] x✝ ↔ IsOpen[t'] x✝
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
s₁ s₂ : Set X
inst✝ : TopologicalSpace X
h₁ : IsOpen[inst✝] s₁
h₂ : IsOpen[inst✝] s₂
⊢ IsOpen[inst✝] (⋃ b, bif b then s₁ else s₂)

Tactic:
;

Goal state after:
X : Type u
s₁ s₂ : Set X
inst✝ : TopologicalSpace X
h₁ : IsOpen[inst✝] s₁
h₂ : IsOpen[inst✝] s₂
⊢ IsOpen[inst✝] (⋃ b, bif b then s₁ else s₂)
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
⊢ IsOpen[inst✝] (⋃₀ ∅)

Tactic:
;

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
⊢ IsOpen[inst✝] (⋃₀ ∅)
Module: Mathlib.Topology.Basic

Goal state before:
pp: case empty
X : Type u
inst✝ : TopologicalSpace X
s : Set (Set X)
h : ∀ t ∈ ∅, IsOpen[inst✝] t
⊢ IsOpen[inst✝] univ

Tactic:
;

Goal state after:
case empty
X : Type u
inst✝ : TopologicalSpace X
s : Set (Set X)
h : ∀ t ∈ ∅, IsOpen[inst✝] t
⊢ IsOpen[inst✝] univ
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Set α → Filter β
m : γ → β
⊢ ⨅ i ∈ f, comap m (g i) = ⨅ s ∈ f, (comap m ∘ g) s

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Set α → Filter β
m : γ → β
⊢ ⨅ i ∈ f, comap m (g i) = ⨅ s ∈ f, (comap m ∘ g) s
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
⊢ (⨅ b, bif b then f else g).lift' s = ⨅ b, bif b then f.lift' s else g.lift' s

Tactic:
lift'_iInf hs

Goal state after:
α : Type u_1
β : Type u_2
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
⊢ ⨅ i, (bif i then f else g).lift' s = ⨅ b, bif b then f.lift' s else g.lift' s
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
⊢ (fun s ↦ (g₁ s).lift fun s ↦ (f₂.lift g₂).lift' fun t ↦ s ×ˢ t) = fun s ↦
    f₂.lift fun t ↦ (g₁ s).lift fun s ↦ (g₂ t).lift' fun t ↦ s ×ˢ t

Tactic:
;

Goal state after:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
⊢ (fun s ↦ (g₁ s).lift fun s ↦ (f₂.lift g₂).lift' fun t ↦ s ×ˢ t) = fun s ↦
    f₂.lift fun t ↦ (g₁ s).lift fun s ↦ (g₂ t).lift' fun t ↦ s ×ˢ t
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
x : Set α₁
⊢ (fun s ↦ (f₂.lift g₂).lift' fun t ↦ s ×ˢ t) = fun t ↦ f₂.lift fun s ↦ (g₂ s).lift' fun t_1 ↦ t ×ˢ t_1

Tactic:
;

Goal state after:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
x : Set α₁
⊢ (fun s ↦ (f₂.lift g₂).lift' fun t ↦ s ×ˢ t) = fun t ↦ f₂.lift fun s ↦ (g₂ s).lift' fun t_1 ↦ t ×ˢ t_1
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : closure s ⊆ s
⊢ IsClosed (closure s)

Tactic:
;

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : closure s ⊆ s
⊢ IsClosed (closure s)
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
f : Filter X
h : x ∈ s
o : IsOpen[inst✝] s
sf : 𝓟 s ≤ f
⊢ ⨅ s ∈ {s | x ∈ s ∧ IsOpen[inst✝] s}, 𝓟 s ≤ f

Tactic:
;

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
f : Filter X
h : x ∈ s
o : IsOpen[inst✝] s
sf : 𝓟 s ≤ f
⊢ ⨅ s ∈ {s | x ∈ s ∧ IsOpen[inst✝] s}, 𝓟 s ≤ f
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u_2
t t' : TopologicalSpace X
H : ∀ (x : X), 𝓝 x = 𝓝 x
x✝ : Set X
⊢ IsOpen[t] x✝ ↔ IsOpen[t'] x✝

Tactic:
;

Goal state after:
X : Type u_2
t t' : TopologicalSpace X
H : ∀ (x : X), 𝓝 x = 𝓝 x
x✝ : Set X
⊢ IsOpen[t] x✝ ↔ IsOpen[t'] x✝
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed (closure s ∩ closure sᶜ)

Tactic:
;

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed (closure s ∩ closure sᶜ)
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : IsClosed s
A : frontier s = s \ interior s
⊢ interior (s \ interior s) ⊆ interior s

Tactic:
;

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : IsClosed s
A : frontier s = s \ interior s
⊢ interior (s \ interior s) ⊆ interior s
Module: Mathlib.Topology.Continuous

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
x : X
g : Y → Z
hf : ContinuousAt f x
hg : ContinuousAt g (f x)
⊢ ContinuousAt (g ∘ f) x

Tactic:
;

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
x : X
g : Y → Z
hf : ContinuousAt f x
hg : ContinuousAt g (f x)
⊢ ContinuousAt (g ∘ f) x
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ pure x ≤ F.lift' closure[inst✝] ↔ (F.lift' closure[inst✝] ⊓ pure x).NeBot

Tactic:
inf_comm

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ pure x ≤ F.lift' closure[inst✝] ↔ (pure x ⊓ F.lift' closure[inst✝]).NeBot
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a < b - toIocDiv hp a b • p
hr : b - toIocDiv hp a b • p ≤ a + p
⊢ a + toIocDiv hp a b • p + p = a + p + toIocDiv hp a b • p

Tactic:
;

Goal state after:
α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a < b - toIocDiv hp a b • p
hr : b - toIocDiv hp a b • p ≤ a + p
⊢ a + toIocDiv hp a b • p + p = a + p + toIocDiv hp a b • p
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
hr : b - toIcoDiv hp a b • p < a + p
⊢ a + toIcoDiv hp a b • p + p = a + p + toIcoDiv hp a b • p

Tactic:
;

Goal state after:
α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
hr : b - toIcoDiv hp a b • p < a + p
⊢ a + toIcoDiv hp a b • p + p = a + p + toIcoDiv hp a b • p
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
h : IsClosed[inst✝] t
⊢ 𝓝ˢ s ≤ 𝓝ˢ (s ∩ t) ⊔ 𝓟 tᶜ

Tactic:
;

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
h : IsClosed[inst✝] t
⊢ 𝓝ˢ s ≤ 𝓝ˢ (s ∩ t) ⊔ 𝓟 tᶜ