mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddMonoid α
h : Periodic f c
⊢ Periodic f (0 • c)

pp: case succ
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddMonoid α
h : Periodic f c
n✝ : ℕ
a✝ : Periodic f (n✝ • c)
⊢ Periodic f ((n✝ + 1) • c)

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddMonoid α
h : Periodic f c
⊢ Periodic f (0 • c)

case succ
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddMonoid α
h : Periodic f c
n✝ : ℕ
a✝ : Periodic f (n✝ • c)
⊢ Periodic f ((n✝ + 1) • c)
Module: Mathlib.Order.Circular

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

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

Tactic:
<;>

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

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

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

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

Tactic:
<;>

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
⊢ Periodic f ((2 * n) • c)

Tactic:
rw [mul_comm, mul_zsmul, two_zsmul, ← two_nsmul]

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
⊢ Periodic f (n • 2 • c)
Module: Mathlib.Order.Circular

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : a ≤ b
⊢ btw a b c ∨ btw c b a

pp: case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
⊢ btw a b c ∨ btw c b a

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : a ≤ b
⊢ btw a b c ∨ btw c b a

case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
⊢ btw a b c ∨ btw c b a
Module: Mathlib.Order.Circular

Goal state before:
pp: case inl.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ btw a b c ∨ btw c b a

pp: case inl.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : a ≤ b
hcb : c ≤ b
⊢ btw a b c ∨ btw c b a

pp: case inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hbc : b ≤ c
⊢ btw a b c ∨ btw c b a

pp: case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hcb : c ≤ b
⊢ btw a b c ∨ btw c b a

Tactic:
<;>

Goal state after:
case inl.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ btw a b c ∨ btw c b a

case inl.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : a ≤ b
hcb : c ≤ b
⊢ btw a b c ∨ btw c b a

case inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hbc : b ≤ c
⊢ btw a b c ∨ btw c b a

case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
hcb : c ≤ b
⊢ btw a b c ∨ btw c b a
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: case domain_eq
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
x✝³ x✝² : ExtensionOf i f
x✝¹ : x✝³.toLinearPMap = x✝².toLinearPMap
x✝ : N
⊢ x✝ ∈ x✝³.domain ↔ x✝ ∈ x✝².domain

pp: case to_fun_eq
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
x✝³ x✝² : ExtensionOf i f
x✝¹ : x✝³.toLinearPMap = x✝².toLinearPMap
x✝ : N
ha✝ : x✝ ∈ x✝³.domain
hb✝ : x✝ ∈ x✝².domain
⊢ ↑x✝³.toLinearPMap ⟨x✝, ha✝⟩ = ↑x✝².toLinearPMap ⟨x✝, hb✝⟩

Tactic:
<;>

Goal state after:
case domain_eq
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
x✝³ x✝² : ExtensionOf i f
x✝¹ : x✝³.toLinearPMap = x✝².toLinearPMap
x✝ : N
⊢ x✝ ∈ x✝³.domain ↔ x✝ ∈ x✝².domain

case to_fun_eq
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
x✝³ x✝² : ExtensionOf i f
x✝¹ : x✝³.toLinearPMap = x✝².toLinearPMap
x✝ : N
ha✝ : x✝ ∈ x✝³.domain
hb✝ : x✝ ∈ x✝².domain
⊢ ↑x✝³.toLinearPMap ⟨x✝, ha✝⟩ = ↑x✝².toLinearPMap ⟨x✝, hb✝⟩
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c₁ c₂ : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h1 : Periodic f c₁
h2 : Antiperiodic f c₂
⊢ Antiperiodic f (c₁ - c₂)

Tactic:
by
  simpa only [sub_eq_add_neg] using h1.add_antiperiod h2.neg

Goal state after:
Module: Mathlib.Data.Nat.Cast.Field

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

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

Tactic:
<;>

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

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

Goal state before:
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
⊢ ↑d ≠ 0

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
⊢ ↑d ≠ 0

Tactic:
<;>

Goal state after:
case inr
K : Type u_1
inst✝¹ : DivisionSemiring K
d m n : ℕ
inst✝ : CharZero K
hn : d ∣ n
hm : d ∣ m
hd : ↑d ≠ 0
⊢ ↑d ≠ 0

case inr
K : Type u_1
inst✝¹ : DivisionSemiring K
d m n : ℕ
inst✝ : CharZero K
hn : d ∣ n
hm : d ∣ m
hd : ↑d ≠ 0
⊢ ↑d ≠ 0
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
⊢ (extensionOfMax i f).domain = ⊤

Tactic:
refine Submodule.eq_top_iff'.mpr fun y => ?_

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
⊢ y ∈ (extensionOfMax i f).domain
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: 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 + a) | a.Coprime x}) ≤
    #({x ∈ Ico k (k + n % a + a * i) ∪ Ico (k + n % a + a * i) (k + n % a + a * i + a) | a.Coprime x})

Tactic:
by
      gcongr
      apply Ico_subset_Ico_union_Ico

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

Goal state before:
pp: case inl
m n : ℕ
h✝ : m.Coprime n
hmn0 : m * n = 0
h : m = 0
⊢ φ (m * n) = φ m * φ n

pp: case inr
m n : ℕ
h✝ : m.Coprime n
hmn0 : m * n = 0
h : n = 0
⊢ φ (m * n) = φ m * φ n

Tactic:
<;>

Goal state after:
case inl
m n : ℕ
h✝ : m.Coprime n
hmn0 : m * n = 0
h : m = 0
⊢ φ (m * n) = φ m * φ n

case inr
m n : ℕ
h✝ : m.Coprime n
hmn0 : m * n = 0
h : n = 0
⊢ φ (m * n) = φ m * φ n
Module: Mathlib.Data.Set.Constructions

Goal state before:
pp: case inter.inl
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T1 T2 : Set α
a✝¹ : finiteInterClosure (insert A S) T1
a✝ : finiteInterClosure (insert A S) T2
h2 : T2 ∈ S ∨ ∃ Q ∈ S, T2 = A ∩ Q
h : T1 ∈ S
⊢ T1 ∩ T2 ∈ S ∨ ∃ Q ∈ S, T1 ∩ T2 = A ∩ Q

pp: case inter.inr
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T2 : Set α
a✝¹ : finiteInterClosure (insert A S) T2
h2 : T2 ∈ S ∨ ∃ Q ∈ S, T2 = A ∩ Q
Q : Set α
hQ : Q ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ Q)
⊢ A ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1 ∈ S, A ∩ Q ∩ T2 = A ∩ Q_1

Tactic:
<;>

Goal state after:
case inter.inl
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T1 T2 : Set α
a✝¹ : finiteInterClosure (insert A S) T1
a✝ : finiteInterClosure (insert A S) T2
h2 : T2 ∈ S ∨ ∃ Q ∈ S, T2 = A ∩ Q
h : T1 ∈ S
⊢ T1 ∩ T2 ∈ S ∨ ∃ Q ∈ S, T1 ∩ T2 = A ∩ Q

case inter.inr
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T2 : Set α
a✝¹ : finiteInterClosure (insert A S) T2
h2 : T2 ∈ S ∨ ∃ Q ∈ S, T2 = A ∩ Q
Q : Set α
hQ : Q ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ Q)
⊢ A ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1 ∈ S, A ∩ Q ∩ T2 = A ∩ Q_1
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case e'_2
n : ℕ
⊢ ((if 0 ∣ n then φ 0 else 0) + ∑ k ∈ Ico (0 + 1) n.succ, if k ∣ n then φ k else 0) =
    ∑ a ∈ Ico 1 (n + 1), if a ∣ n then φ a else 0

pp: case e'_2.hab
n : ℕ
⊢ 0 < n.succ

Tactic:
<;>

Goal state after:
case e'_2
n : ℕ
⊢ ((if 0 ∣ n then φ 0 else 0) + ∑ k ∈ Ico (0 + 1) n.succ, if k ∣ n then φ k else 0) =
    ∑ a ∈ Ico 1 (n + 1), if a ∣ n then φ a else 0

case e'_2.hab
n : ℕ
⊢ 0 < n.succ
Module: Mathlib.Data.Set.Constructions

Goal state before:
pp: case mp
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P Q : Set α
hQ : Q ∈ S
a✝¹ : finiteInterClosure (insert A S) (A ∩ Q)
R : Set α
hR : R ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ R)
x : α
⊢ x ∈ A ∩ Q ∩ (A ∩ R) → x ∈ A ∩ (Q ∩ R)

pp: case mpr
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P Q : Set α
hQ : Q ∈ S
a✝¹ : finiteInterClosure (insert A S) (A ∩ Q)
R : Set α
hR : R ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ R)
x : α
⊢ x ∈ A ∩ (Q ∩ R) → x ∈ A ∩ Q ∩ (A ∩ R)

Tactic:
<;>

Goal state after:
case mp
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P Q : Set α
hQ : Q ∈ S
a✝¹ : finiteInterClosure (insert A S) (A ∩ Q)
R : Set α
hR : R ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ R)
x : α
⊢ x ∈ A ∩ Q ∩ (A ∩ R) → x ∈ A ∩ (Q ∩ R)

case mpr
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P Q : Set α
hQ : Q ∈ S
a✝¹ : finiteInterClosure (insert A S) (A ∩ Q)
R : Set α
hR : R ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ R)
x : α
⊢ x ∈ A ∩ (Q ∩ R) → x ∈ A ∩ Q ∩ (A ∩ R)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ p ^ (1 - 1) * (p - 1) = p ^ 1 - 1

pp: p : ℕ
hp : Prime p
⊢ 0 < 1

Tactic:
<;>

Goal state after:
p : ℕ
hp : Prime p
⊢ p ^ (1 - 1) * (p - 1) = p ^ 1 - 1

p : ℕ
hp : Prime p
⊢ 0 < 1
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case zero
⊢ Odd (φ 0) ↔ 0 = 1 ∨ 0 = 2

pp: case succ.zero
⊢ Odd (φ (0 + 1)) ↔ 0 + 1 = 1 ∨ 0 + 1 = 2

pp: case succ.succ.zero
⊢ Odd (φ (0 + 1 + 1)) ↔ 0 + 1 + 1 = 1 ∨ 0 + 1 + 1 = 2

pp: case succ.succ.succ
n✝ : ℕ
⊢ Odd (φ (n✝ + 1 + 1 + 1)) ↔ n✝ + 1 + 1 + 1 = 1 ∨ n✝ + 1 + 1 + 1 = 2

Tactic:
<;>

Goal state after:
case zero
⊢ Odd (φ 0) ↔ 0 = 1 ∨ 0 = 2

case succ.zero
⊢ Odd (φ (0 + 1)) ↔ 0 + 1 = 1 ∨ 0 + 1 = 2

case succ.succ.zero
⊢ Odd (φ (0 + 1 + 1)) ↔ 0 + 1 + 1 = 1 ∨ 0 + 1 + 1 = 2

case succ.succ.succ
n✝ : ℕ
⊢ Odd (φ (n✝ + 1 + 1 + 1)) ↔ n✝ + 1 + 1 + 1 = 1 ∨ n✝ + 1 + 1 + 1 = 2
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case inl
han : 0 < 1
ha : φ 1 ≤ 1
⊢ 1 ∣ 2

pp: case inr
han : 0 < 2
ha : φ 2 ≤ 1
⊢ 2 ∣ 2

Tactic:
<;>

Goal state after:
case inl
han : 0 < 1
ha : φ 1 ≤ 1
⊢ 1 ∣ 2

case inr
han : 0 < 2
ha : φ 2 ≤ 1
⊢ 2 ∣ 2
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case mpr.inl
m n : ℕ
h : φ m = 1
⊢ (φ m).Coprime (φ n)

pp: case mpr.inr
m n : ℕ
h : φ n = 1
⊢ (φ m).Coprime (φ n)

Tactic:
<;>

Goal state after:
case mpr.inl
m n : ℕ
h : φ m = 1
⊢ (φ m).Coprime (φ n)

case mpr.inr
m n : ℕ
h : φ n = 1
⊢ (φ m).Coprime (φ n)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a b a1 a2 b1 b2 c1 : ℕ
⊢ ∀ (c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)

Tactic:
c2

Goal state after:
a b a1 a2 b1 b2 c1 c2 : ℕ
⊢ b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp a (- - -b) = -(toIcoDiv hp (-a) (- -b) + 1)

Tactic:
toIcoDiv_neg,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp a (- - -b) = -(-(toIocDiv hp (- -a) (-b) + 1) + 1)
Module: Mathlib.Topology.Basic

Goal state before:
pp: case pos
X : Type u
inst✝ : TopologicalSpace X
p : Prop
h✝ : p
⊢ IsOpen[inst✝] {_x | p}

pp: case neg
X : Type u
inst✝ : TopologicalSpace X
p : Prop
h✝ : ¬p
⊢ IsOpen[inst✝] {_x | p}

Tactic:
<;>

Goal state after:
case pos
X : Type u
inst✝ : TopologicalSpace X
p : Prop
h✝ : p
⊢ IsOpen[inst✝] {_x | p}

case neg
X : Type u
inst✝ : TopologicalSpace X
p : Prop
h✝ : ¬p
⊢ IsOpen[inst✝] {_x | p}
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ -b - toIcoDiv hp a (-b) • p = p - (b - toIocDiv hp (-a) b • p)

Tactic:
toIcoDiv_neg,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ -b - -(toIocDiv hp (-a) b + 1) • p = p - (b - toIocDiv hp (-a) b • p)
Module: Mathlib.Order.Filter.Lift

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

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

Tactic:
<;>

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

case true
α : Type u_1
β : Type u_2
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
⊢ (bif true then f else g).lift' s = bif true then f.lift' s else g.lift' s
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
z : ℤ
hz : c = z • p + b
⊢ toIocMod hp a b = toIocMod hp a (z • p + b)

Tactic:
toIocMod_zsmul_add

Goal state after:
case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
z : ℤ
hz : c = z • p + b
⊢ toIocMod hp a b = toIocMod hp a b
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
ι : Sort v
inst✝ : Finite ι
f : ι → Set X
⊢ interior (⋂₀ range f) = ⋂ i, interior (f i)

Tactic:
(finite_range f).interior_sInter,

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
ι : Sort v
inst✝ : Finite ι
f : ι → Set X
⊢ ⋂ s ∈ range f, interior s = ⋂ i, interior (f i)
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hS : S.Finite
⊢ closure (⋃₀ S) = ⋃ s ∈ S, closure s

Tactic:
rw [sUnion_eq_biUnion, hS.closure_biUnion]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
h : Disjoint (closure s) (closure t)
full : interior sᶜ ∪ interior tᶜ = univ
⊢ interior (s ∪ t) ⊆ interior s ∪ interior t

Tactic:
rw [← (interior _).inter_univ, ← full, inter_union_distrib_left]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
h : Disjoint (closure s) (closure t)
full : interior sᶜ ∪ interior tᶜ = univ
⊢ interior (s ∪ t) ∩ interior sᶜ ∪ interior (s ∪ t) ∩ interior tᶜ ⊆ interior s ∪ interior t
Module: Mathlib.Topology.Closure

Goal state before:
pp: case mp
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ Dense s → ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty

pp: case mpr
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty) → Dense s

Tactic:
<;>

Goal state after:
case mp
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ Dense s → ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty

case mpr
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty) → Dense s
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
p : X → Prop
⊢ IsOpen[inst✝] {x | ∀ᶠ (y : X) in 𝓝 x, p y}

Tactic:
simp only [← interior_setOfPred_eq, isOpen_interior]

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a x✝ : α
⊢ (∃ x, ¬x✝ - x • p ∉ Set.Ioo a (a + p)) ↔ ∃ i, x✝ - i • p ∈ Set.Ioo a (a + p)

Tactic:
Classical.not_not

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (frontier s)ᶜ = interior s ∪ interior sᶜ

Tactic:
rw [frontier_eq_inter_compl_interior]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ ((interior s)ᶜ ∩ (interior sᶜ)ᶜ)ᶜ = interior s ∪ interior sᶜ
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
x : X
f : Filter X
H : f ≤ 𝓝 x
inst✝ : f.NeBot
⊢ (𝓝 x ⊓ f).NeBot

Tactic:
inf_eq_right.mpr H

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
x : X
f : Filter X
H : f ≤ 𝓝 x
inst✝ : f.NeBot
⊢ f.NeBot
Module: Mathlib.Topology.Maps.Basic

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

Tactic:
isInducing_iff,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hg : IsInducing g
h : IsInducing (g ∘ f)
⊢ inst✝¹ = induced f inst✝²
Module: Mathlib.Topology.Order

Goal state before:
pp: case refl.refine_1.inter.inl
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
t✝ : Set α
a✝¹ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) t✝
h₂ : t✝ = ∅ ∨ t✝ = univ
a✝ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) ∅
⊢ ∅ ∩ t✝ = ∅ ∨ ∅ ∩ t✝ = univ

pp: case refl.refine_1.inter.inr
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
t✝ : Set α
a✝¹ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) t✝
h₂ : t✝ = ∅ ∨ t✝ = univ
a✝ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) univ
⊢ univ ∩ t✝ = ∅ ∨ univ ∩ t✝ = univ

Tactic:
<;>

Goal state after:
case refl.refine_1.inter.inl
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
t✝ : Set α
a✝¹ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) t✝
h₂ : t✝ = ∅ ∨ t✝ = univ
a✝ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) ∅
⊢ ∅ ∩ t✝ = ∅ ∨ ∅ ∩ t✝ = univ

case refl.refine_1.inter.inr
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
t✝ : Set α
a✝¹ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) t✝
h₂ : t✝ = ∅ ∨ t✝ = univ
a✝ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) univ
⊢ univ ∩ t✝ = ∅ ∨ univ ∩ t✝ = univ
Module: Mathlib.Topology.Order

Goal state before:
pp: case refl.refine_1.inter.inl.inl
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
a✝¹ a✝ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) ∅
⊢ ∅ ∩ ∅ = ∅ ∨ ∅ ∩ ∅ = univ

pp: case refl.refine_1.inter.inl.inr
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
a✝¹ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) ∅
a✝ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) univ
⊢ ∅ ∩ univ = ∅ ∨ ∅ ∩ univ = univ

pp: case refl.refine_1.inter.inr.inl
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
a✝¹ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) univ
a✝ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) ∅
⊢ univ ∩ ∅ = ∅ ∨ univ ∩ ∅ = univ

pp: case refl.refine_1.inter.inr.inr
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
a✝¹ a✝ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) univ
⊢ univ ∩ univ = ∅ ∨ univ ∩ univ = univ

Tactic:
<;>

Goal state after:
case refl.refine_1.inter.inl.inl
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
a✝¹ a✝ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) ∅
⊢ ∅ ∩ ∅ = ∅ ∨ ∅ ∩ ∅ = univ

case refl.refine_1.inter.inl.inr
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
a✝¹ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) ∅
a✝ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) univ
⊢ ∅ ∩ univ = ∅ ∨ ∅ ∩ univ = univ

case refl.refine_1.inter.inr.inl
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
a✝¹ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) univ
a✝ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) ∅
⊢ univ ∩ ∅ = ∅ ∨ univ ∩ ∅ = univ

case refl.refine_1.inter.inr.inr
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
a✝¹ a✝ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) univ
⊢ univ ∩ univ = ∅ ∨ univ ∩ univ = univ
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ DiscreteTopology α ↔ ∀ (x : α), 𝓝 x = pure x

Tactic:
simp only [discreteTopology_iff_singleton_mem_nhds]
  apply forall_congr' (fun x ↦ ?_)
  simp [le_antisymm_iff, pure_le_nhds x]

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

Goal state before:
pp: Y : Type u_2
Z : Type u_3
ι : Type u_4
g : Y → Z
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : ι → Y
l : Filter ι
y : Y
hg : IsInducing g
⊢ Tendsto f l (𝓝 y) ↔ Tendsto (g ∘ f) l (𝓝 (g y))

Tactic:
hg.nhds_eq_comap,

Goal state after:
Y : Type u_2
Z : Type u_3
ι : Type u_4
g : Y → Z
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : ι → Y
l : Filter ι
y : Y
hg : IsInducing g
⊢ Tendsto f l (comap g (𝓝 (g y))) ↔ Tendsto (g ∘ f) l (𝓝 (g y))
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
g : β → α
s : Set (TopologicalSpace α)
⊢ TopologicalSpace.induced g (sInf s) = sInf (TopologicalSpace.induced g '' s)

Tactic:
sInf_eq_iInf',

Goal state after:
α : Type u_1
β : Type u_2
g : β → α
s : Set (TopologicalSpace α)
⊢ TopologicalSpace.induced g (⨅ a, ↑a) = sInf (TopologicalSpace.induced g '' s)
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hf : IsInducing f
x : X
h : range f ∈ 𝓝 (f x)
⊢ ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)

Tactic:
ContinuousAt,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hf : IsInducing f
x : X
h : range f ∈ 𝓝 (f x)
⊢ Tendsto (g ∘ f) (𝓝 x) (𝓝 ((g ∘ f) x)) ↔ Tendsto g (𝓝 (f x)) (𝓝 (g (f x)))
Module: Mathlib.Topology.Maps.Basic

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

Tactic:
simp_rw [isEmbedding_iff, hg.isInducing.of_comp_iff, hg.injective.of_comp_iff f]

Goal state after: