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

Goal state before:
pp: α : Type u_1
⊢ ⨆ a, pure a = 𝓟 univ

Tactic:
← biSup_pure_eq_principal,

Goal state after:
α : Type u_1
⊢ ⨆ a, pure a = ⨆ a ∈ univ, pure a
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
f : Filter α
inst✝ : f.NeBot
c : β
s : Set β
h : c ∈ s
⊢ s ∈ map (fun x ↦ c) f ↔ s ∈ pure c

pp: case neg
α : Type u_1
β : Type u_2
f : Filter α
inst✝ : f.NeBot
c : β
s : Set β
h : c ∉ s
⊢ s ∈ map (fun x ↦ c) f ↔ s ∈ pure c

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
f : Filter α
inst✝ : f.NeBot
c : β
s : Set β
h : c ∈ s
⊢ s ∈ map (fun x ↦ c) f ↔ s ∈ pure c

case neg
α : Type u_1
β : Type u_2
f : Filter α
inst✝ : f.NeBot
c : β
s : Set β
h : c ∉ s
⊢ s ∈ map (fun x ↦ c) f ↔ s ∈ pure c
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: case mp
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
i : ι
hi : p i
ht : s i ⊆ t
t' : Set α
i' : ι'
hi' : p' i'
ht' : s' i' ⊆ t'
⊢ ∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t ∩ t'

Tactic:
exact ⟨⟨i, i'⟩, ⟨hi, hi'⟩, inter_subset_inter ht ht'⟩

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

Goal state before:
pp: α : Type u
⊢ ⊤ ≤ 𝓟 univ

Tactic:
by simp only [le_principal_iff, mem_top]

Goal state after:
Module: Mathlib.Order.Filter.Tendsto

Goal state before:
pp: α : Type u_1
β : Type u_2
mab : α → β
mba : β → α
f : Filter α
g : Filter β
h₁ : mab ∘ mba =ᶠ[g] id
h₂ : Tendsto mba g f
⊢ g ≤ map mab f

Tactic:
rw [← @map_id _ g, ← map_congr h₁, ← map_map]

Goal state after:
α : Type u_1
β : Type u_2
mab : α → β
mba : β → α
f : Filter α
g : Filter β
h₁ : mab ∘ mba =ᶠ[g] id
h₂ : Tendsto mba g f
⊢ map mab (map mba g) ≤ map mab f
Module: Mathlib.Order.Filter.Tendsto

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
a : Filter α
b : Filter β
c : Filter γ
hfg : Tendsto (g ∘ f) a c
hg : comap g c ≤ b
⊢ Tendsto f a b

Tactic:
rw [tendsto_iff_comap] at hfg ⊢
  calc
    a ≤ comap (g ∘ f) c := hfg
    _ ≤ comap f b := by simpa [comap_comap] using comap_mono hg

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ map inl f ≤ map inl ⊤

pp: case h₂
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ map inr g ≤ map inr ⊤

Tactic:
<;>

Goal state after:
case h₁
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ map inl f ≤ map inl ⊤

case h₂
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ map inr g ≤ map inr ⊤
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: case pos
α : Type u
f : Filter α
t : f.NeBot
p : Prop
h : p
⊢ (∀ᶠ (x : α) in f, p) ↔ p

pp: case neg
α : Type u
f : Filter α
t : f.NeBot
p : Prop
h : ¬p
⊢ (∀ᶠ (x : α) in f, p) ↔ p

Tactic:
<;>

Goal state after:
case pos
α : Type u
f : Filter α
t : f.NeBot
p : Prop
h : p
⊢ (∀ᶠ (x : α) in f, p) ↔ p

case neg
α : Type u
f : Filter α
t : f.NeBot
p : Prop
h : ¬p
⊢ (∀ᶠ (x : α) in f, p) ↔ p
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: case pos
α : Type u
f : Filter α
inst✝ : f.NeBot
p : Prop
h✝ : p
⊢ (∃ᶠ (x : α) in f, p) ↔ p

pp: case neg
α : Type u
f : Filter α
inst✝ : f.NeBot
p : Prop
h✝ : ¬p
⊢ (∃ᶠ (x : α) in f, p) ↔ p

Tactic:
<;>

Goal state after:
case pos
α : Type u
f : Filter α
inst✝ : f.NeBot
p : Prop
h✝ : p
⊢ (∃ᶠ (x : α) in f, p) ↔ p

case neg
α : Type u
f : Filter α
inst✝ : f.NeBot
p : Prop
h✝ : ¬p
⊢ (∃ᶠ (x : α) in f, p) ↔ p
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ (comap f G ⊓ F).NeBot ↔ (G ⊓ map f F).NeBot

Tactic:
rw [← map_neBot_iff, Filter.push_pull']

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case refine_1.hx
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : map m (pure x) = map m (pure y)
⊢ pure x ∈ Iic (𝓟 s)

pp: case refine_1.hy
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : map m (pure x) = map m (pure y)
⊢ pure y ∈ Iic (𝓟 s)

Tactic:
<;>

Goal state after:
case refine_1.hx
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : map m (pure x) = map m (pure y)
⊢ pure x ∈ Iic (𝓟 s)

case refine_1.hy
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : map m (pure x) = map m (pure y)
⊢ pure y ∈ Iic (𝓟 s)
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case refine_1.hx
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : map m (pure x) = map m (pure y)
⊢ pure x ≤ 𝓟 s

Tactic:
pure_le_principal

Goal state after:
case refine_1.hx
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : map m (pure x) = map m (pure y)
⊢ x ∈ s
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case refine_1.hy
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : map m (pure x) = map m (pure y)
⊢ pure y ≤ 𝓟 s

Tactic:
pure_le_principal

Goal state after:
case refine_1.hy
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : map m (pure x) = map m (pure y)
⊢ y ∈ s
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: case one
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : MulOneClass β
one : One α := ⋯
mul : Mul α := ⋯
⊢ e 1 = 1

pp: case mul
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : MulOneClass β
one : One α := ⋯
mul : Mul α := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y

Tactic:
<;>

Goal state after:
case one
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : MulOneClass β
one : One α := ⋯
mul : Mul α := ⋯
⊢ e 1 = 1

case mul
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : MulOneClass β
one : One α := ⋯
mul : Mul α := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: case one
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : MulOneClass β
one : One α := ⋯
mul : Mul α := ⋯
⊢ e 1 = 1

pp: case mul
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : MulOneClass β
one : One α := e.one
mul : Mul α := e.mul
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

Tactic:
<;>

Goal state after:
case one
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : MulOneClass β
one : One α := ⋯
mul : Mul α := ⋯
⊢ e 1 = 1

case mul
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : MulOneClass β
one : One α := e.one
mul : Mul α := e.mul
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: case one
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Monoid β
one : One α := ⋯
mul : Mul α := ⋯
pow : Pow α ℕ := ⋯
⊢ e 1 = 1

pp: case mul
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Monoid β
one : One α := ⋯
mul : Mul α := ⋯
pow : Pow α ℕ := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y

pp: case npow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Monoid β
one : One α := ⋯
mul : Mul α := ⋯
pow : Pow α ℕ := ⋯
⊢ ∀ (x : α) (n : ℕ), e (x ^ n) = e x ^ n

Tactic:
<;>

Goal state after:
case one
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Monoid β
one : One α := ⋯
mul : Mul α := ⋯
pow : Pow α ℕ := ⋯
⊢ e 1 = 1

case mul
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Monoid β
one : One α := ⋯
mul : Mul α := ⋯
pow : Pow α ℕ := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y

case npow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Monoid β
one : One α := ⋯
mul : Mul α := ⋯
pow : Pow α ℕ := ⋯
⊢ ∀ (x : α) (n : ℕ), e (x ^ n) = e x ^ n
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: case one
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Monoid β
one : One α := ⋯
mul : Mul α := ⋯
pow : Pow α ℕ := ⋯
⊢ e 1 = 1

pp: case mul
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Monoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

pp: case npow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Monoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
x✝ : α
n✝ : ℕ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝

Tactic:
<;>

Goal state after:
case one
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Monoid β
one : One α := ⋯
mul : Mul α := ⋯
pow : Pow α ℕ := ⋯
⊢ e 1 = 1

case mul
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Monoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

case npow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Monoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
x✝ : α
n✝ : ℕ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: case one
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommMonoid β
one : One α := ⋯
mul : Mul α := ⋯
pow : Pow α ℕ := ⋯
⊢ e 1 = 1

pp: case mul
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommMonoid β
one : One α := ⋯
mul : Mul α := ⋯
pow : Pow α ℕ := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y

pp: case npow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommMonoid β
one : One α := ⋯
mul : Mul α := ⋯
pow : Pow α ℕ := ⋯
⊢ ∀ (x : α) (n : ℕ), e (x ^ n) = e x ^ n

Tactic:
<;>

Goal state after:
case one
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommMonoid β
one : One α := ⋯
mul : Mul α := ⋯
pow : Pow α ℕ := ⋯
⊢ e 1 = 1

case mul
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommMonoid β
one : One α := ⋯
mul : Mul α := ⋯
pow : Pow α ℕ := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y

case npow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommMonoid β
one : One α := ⋯
mul : Mul α := ⋯
pow : Pow α ℕ := ⋯
⊢ ∀ (x : α) (n : ℕ), e (x ^ n) = e x ^ n
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: case one
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommMonoid β
one : One α := ⋯
mul : Mul α := ⋯
pow : Pow α ℕ := ⋯
⊢ e 1 = 1

pp: case mul
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommMonoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

pp: case npow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommMonoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
x✝ : α
n✝ : ℕ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝

Tactic:
<;>

Goal state after:
case one
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommMonoid β
one : One α := ⋯
mul : Mul α := ⋯
pow : Pow α ℕ := ⋯
⊢ e 1 = 1

case mul
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommMonoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

case npow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommMonoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
x✝ : α
n✝ : ℕ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: case one
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ e 1 = 1

pp: case mul
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y

pp: case inv
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ ∀ (x : α), e x⁻¹ = (e x)⁻¹

pp: case div
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ ∀ (x y : α), e (x / y) = e x / e y

pp: case npow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ ∀ (x : α) (n : ℕ), e (x ^ n) = e x ^ n

pp: case zpow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ ∀ (x : α) (n : ℤ), e (x ^ n) = e x ^ n

Tactic:
<;>

Goal state after:
case one
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ e 1 = 1

case mul
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y

case inv
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ ∀ (x : α), e x⁻¹ = (e x)⁻¹

case div
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ ∀ (x y : α), e (x / y) = e x / e y

case npow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ ∀ (x : α) (n : ℕ), e (x ^ n) = e x ^ n

case zpow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ ∀ (x : α) (n : ℤ), e (x ^ n) = e x ^ n
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: case one
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ e 1 = 1

pp: case mul
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

pp: case inv
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ : α
⊢ e x✝⁻¹ = (e x✝)⁻¹

pp: case div
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ y✝ : α
⊢ e (x✝ / y✝) = e x✝ / e y✝

pp: case npow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ : α
n✝ : ℕ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝

pp: case zpow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ : α
n✝ : ℤ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝

Tactic:
<;>

Goal state after:
case one
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ e 1 = 1

case mul
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

case inv
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ : α
⊢ e x✝⁻¹ = (e x✝)⁻¹

case div
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ y✝ : α
⊢ e (x✝ / y✝) = e x✝ / e y✝

case npow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ : α
n✝ : ℕ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝

case zpow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ : α
n✝ : ℤ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: case one
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ e 1 = 1

pp: case mul
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y

pp: case inv
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ ∀ (x : α), e x⁻¹ = (e x)⁻¹

pp: case div
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ ∀ (x y : α), e (x / y) = e x / e y

pp: case npow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ ∀ (x : α) (n : ℕ), e (x ^ n) = e x ^ n

pp: case zpow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ ∀ (x : α) (n : ℤ), e (x ^ n) = e x ^ n

Tactic:
<;>

Goal state after:
case one
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ e 1 = 1

case mul
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y

case inv
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ ∀ (x : α), e x⁻¹ = (e x)⁻¹

case div
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ ∀ (x y : α), e (x / y) = e x / e y

case npow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ ∀ (x : α) (n : ℕ), e (x ^ n) = e x ^ n

case zpow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ ∀ (x : α) (n : ℤ), e (x ^ n) = e x ^ n
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: case h.right.zero
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ P 0 (Nat.recOn 0 (u 0 0) fun n v ↦ u (n + 1) v)

pp: case h.right.succ
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
n✝ : ℕ
⊢ P (n✝ + 1) (Nat.recOn (n✝ + 1) (u 0 0) fun n v ↦ u (n + 1) v)

Tactic:
<;>

Goal state after:
case h.right.zero
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ P 0 (Nat.recOn 0 (u 0 0) fun n v ↦ u (n + 1) v)

case h.right.succ
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
n✝ : ℕ
⊢ P (n✝ + 1) (Nat.recOn (n✝ + 1) (u 0 0) fun n v ↦ u (n + 1) v)
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: case one
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ e 1 = 1

pp: case mul
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

pp: case inv
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ : α
⊢ e x✝⁻¹ = (e x✝)⁻¹

pp: case div
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ y✝ : α
⊢ e (x✝ / y✝) = e x✝ / e y✝

pp: case npow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ : α
n✝ : ℕ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝

pp: case zpow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ : α
n✝ : ℤ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝

Tactic:
<;>

Goal state after:
case one
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ e 1 = 1

case mul
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

case inv
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ : α
⊢ e x✝⁻¹ = (e x✝)⁻¹

case div
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ y✝ : α
⊢ e (x✝ / y✝) = e x✝ / e y✝

case npow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ : α
n✝ : ℕ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝

case zpow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ : α
n✝ : ℤ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: k b : ℕ
x✝ : 0 ≤ b
⊢ b ≤ b + k - k

Tactic:
by rw [Nat.add_sub_cancel_right]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.TransferInstance

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
A : Type u_3
B : Type u_4
e : A ≃ B
inst✝² : MonoidWithZero M₀
inst✝¹ : Zero B
inst✝ : MulActionWithZero M₀ B
⊢ MulActionWithZero M₀ A

Tactic:
letI := e.zero
  exact { e.smulWithZero M₀, e.mulAction M₀ with }

Goal state after: