awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst : ∀ (i : ι), (f i).NeBot
i : ι
s : Set (α i)
hs : s ∈ map (eval (β := α) i) (pi (α := α) f)
⊢ s ∈ f i
have rcases : ∀ (I : Set ι) (hIf : I.Finite) (t : (i : ι) → Set (α i)) (htf : ∀ (i : ι), t i ∈ f i)
  (hI : I.pi (α := α) t ⊆ eval (β := α) i ⁻¹' s), s ∈ f i
Tactic: rcases mem_pi.1 (mem_map.1 hs) with ⟨I, hIf, t, htf, hI⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst : ∀ (i : ι), (f i).NeBot
i : ι
s : Set (α i)
hs : s ∈ map (eval (β := α) i) (pi (α := α) f)
I : Set ι
hIf : I.Finite
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : I.pi (α := α) t ⊆ eval (β := α) i ⁻¹' s
⊢ s ∈ f i
have hI₁ : eval (β := α) i '' I.pi (α := α) t ⊆ s
Tactic: rw [← image_subset_iff] at hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst : ∀ (i : ι), (f i).NeBot
i : ι
s : Set (α i)
hs : s ∈ map (eval (β := α) i) (pi (α := α) f)
I : Set ι
hIf : I.Finite
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : eval (β := α) i '' I.pi (α := α) t ⊆ s
⊢ s ∈ f i
have refine : (I.pi (α := α) t).Nonempty
Tactic: refine mem_of_superset (htf i) ((subset_eval_image_pi ?_ _).trans hI)
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f₁ f₂ : (i : ι) → Filter (α i)
inst : ∀ (i : ι), (f₁ i).NeBot
⊢ pi (α := α) f₁ = pi (α := α) f₂ ↔ f₁ = f₂
have refine : ∀ (h : pi (α := α) f₁ = pi (α := α) f₂), f₁ = f₂
Tactic: refine ⟨fun h => ?_, congr_arg pi⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
f₁ f₂ : (i : ι) → Filter (α i)
inst : ∀ (i : ι), (f₁ i).NeBot
h : pi (α := α) f₁ = pi (α := α) f₂
⊢ f₁ = f₂
have hle : f₁ ≤ f₂
Tactic: have hle : f₁ ≤ f₂ := pi_le_pi.1 h.le
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
f₁ f₂ : (i : ι) → Filter (α i)
inst : ∀ (i : ι), (f₁ i).NeBot
h : pi (α := α) f₁ = pi (α := α) f₂
hle : f₁ ≤ f₂
⊢ f₁ = f₂
have this : ∀ (i : ι), (f₂ i).NeBot
Tactic: haveI : ∀ i, NeBot (f₂ i) := fun i => neBot_of_le (hle i)
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
β : ι → Type u_3
m : (i : ι) → α i → β i
⊢ LE.le (α := Filter ((i : ι) → β i)) (map (fun (k : (i : ι) → α i) (i : ι) ↦ m i (k i)) (Filter.coprodᵢ (α := α) f))
    (Filter.coprodᵢ (α := β) fun (i : ι) ↦ map (m i) (f i))
have simp : ∀ (x : Set ((i : ι) → β i)),
  (∀ (i : ι), ∃ (t₁ : Set (β i)), m i ⁻¹' t₁ ∈ f i ∧ eval (β := β) i ⁻¹' t₁ ⊆ x) →
    ∀ (i : ι), ∃ t₁ ∈ f i, eval (β := α) i ⁻¹' t₁ ⊆ (fun (k : (i : ι) → α i) (i : ι) ↦ m i (k i)) ⁻¹' x
Tactic: simp only [le_def, mem_map, mem_coprodᵢ_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
β : ι → Type u_3
m : (i : ι) → α i → β i
s : Set ((i : ι) → β i)
h : ∀ (i : ι), ∃ (t₁ : Set (β i)), m i ⁻¹' t₁ ∈ f i ∧ eval (β := β) i ⁻¹' t₁ ⊆ s
i : ι
⊢ ∃ t₁ ∈ f i, eval (β := α) i ⁻¹' t₁ ⊆ (fun (k : (i : ι) → α i) (i : ι) ↦ m i (k i)) ⁻¹' s
have obtain : ∀ (t : Set (β i)) (H : m i ⁻¹' t ∈ f i) (hH : eval (β := β) i ⁻¹' t ⊆ s),
  ∃ t₁ ∈ f i, eval (β := α) i ⁻¹' t₁ ⊆ (fun (k : (i : ι) → α i) (i : ι) ↦ m i (k i)) ⁻¹' s
Tactic: obtain ⟨t, H, hH⟩ := h i
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : InvolutiveInv α
f : Filter α
s : Set α
hs : s ∈ f
⊢ s⁻¹ ∈ f⁻¹
have rwa : Inv.inv ⁻¹' s⁻¹ ∈ f
Tactic: rwa [mem_inv, inv_preimage, inv_inv]
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : InvolutiveInv α
f : Filter α
s : Set α
hs : s ∈ f
rwa : Inv.inv ⁻¹' s⁻¹ ∈ f
⊢ s⁻¹ ∈ f⁻¹
have rwa₁ : s⁻¹⁻¹ ∈ f
Tactic: rwa [mem_inv, inv_preimage, inv_inv]
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst : InvolutiveInv α
f_1 g : Filter α
s : Set α
f : Filter α
⊢ map (Inv.inv ∘ Inv.inv) f = f
have rw : map id f = f
Tactic: rw [inv_involutive.comp_self, map_id]
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst : InvolutiveInv α
f_1 g : Filter α
s : Set α
f : Filter α
rw : map id f = f
⊢ map (Inv.inv ∘ Inv.inv) f = f
have rw₁ : f = f
Tactic: rw [inv_involutive.comp_self, map_id]
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : InvolutiveInv α
f g : Filter α
⊢ f⁻¹ ≤ g ↔ f ≤ g⁻¹
have rw : f⁻¹⁻¹ ≤ g⁻¹ ↔ f ≤ g⁻¹
Tactic: rw [← Filter.inv_le_inv_iff, inv_inv]
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : InvolutiveInv α
f g : Filter α
rw : f⁻¹⁻¹ ≤ g⁻¹ ↔ f ≤ g⁻¹
⊢ f⁻¹ ≤ g ↔ f ≤ g⁻¹
have rw₁ : f ≤ g⁻¹ ↔ f ≤ g⁻¹
Tactic: rw [← Filter.inv_le_inv_iff, inv_inv]
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : Monoid α
f : Filter α
s : Set α
hs : s ∈ f
n : ℕ
⊢ s ^ (n + 1) ∈ f ^ (n + 1)
have rw : s ^ (n + 1) ∈ f ^ n * f
Tactic: rw [pow_succ]
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : Monoid α
n : ℕ
hn : n ≠ 0
⊢ HPow.hPow (α := Filter α) ⊥ n = ⊥
have rw : HPow.hPow (α := Filter α) ⊥ (n - 1 + 1) = ⊥
Tactic: rw [← Nat.sub_one_add_one hn, pow_succ', bot_mul]
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : Monoid α
n : ℕ
hn : n ≠ 0
rw : HPow.hPow (α := Filter α) ⊥ (n - 1 + 1) = ⊥
⊢ HPow.hPow (α := Filter α) ⊥ n = ⊥
have rw₁ : ⊥ * HPow.hPow (α := Filter α) ⊥ (n - 1) = ⊥
Tactic: rw [← Nat.sub_one_add_one hn, pow_succ', bot_mul]
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : Monoid α
n : ℕ
hn : n ≠ 0
rw : HPow.hPow (α := Filter α) ⊥ (n - 1 + 1) = ⊥
rw₁ : ⊥ * HPow.hPow (α := Filter α) ⊥ (n - 1) = ⊥
⊢ HPow.hPow (α := Filter α) ⊥ n = ⊥
have rw₂ : Eq.{u_2 + 1} (α := Filter α) ⊥ ⊥
Tactic: rw [← Nat.sub_one_add_one hn, pow_succ', bot_mul]
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : Monoid α
f : Filter α
hf : 1 ≤ f
⊢ f * ⊤ = ⊤
have refine : ∀ s ∈ f * ⊤, Membership.mem (γ := Filter α) ⊤ s
Tactic: refine top_le_iff.1 fun s => ?_
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : Monoid α
f : Filter α
hf : 1 ≤ f
s : Set α
⊢ s ∈ f * ⊤ → Membership.mem (γ := Filter α) ⊤ s
have simp : (∃ t₁ ∈ f, t₁ * univ ⊆ s) → s = univ
Tactic: simp only [mem_mul, mem_top, exists_eq_left]
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : Monoid α
f : Filter α
hf : 1 ≤ f
s t : Set α
ht : t ∈ f
hs : t * univ ⊆ s
⊢ s = univ
have rwa : ∀ (hs : univ ⊆ s), s = univ
Tactic: rwa [mul_univ_of_one_mem (mem_one.1 <| hf ht), univ_subset_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : Monoid α
f : Filter α
hf : 1 ≤ f
s t : Set α
ht : t ∈ f
hs : t * univ ⊆ s
rwa : ∀ (hs : univ ⊆ s), s = univ
⊢ s = univ
have rwa₁ : ∀ (hs : s = univ), s = univ
Tactic: rwa [mul_univ_of_one_mem (mem_one.1 <| hf ht), univ_subset_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : Monoid α
f : Filter α
hf : 1 ≤ f
⊢ ⊤ * f = ⊤
have refine : ∀ s ∈ ⊤ * f, Membership.mem (γ := Filter α) ⊤ s
Tactic: refine top_le_iff.1 fun s => ?_
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : Monoid α
f : Filter α
hf : 1 ≤ f
s : Set α
⊢ s ∈ ⊤ * f → Membership.mem (γ := Filter α) ⊤ s
have simp : (∃ t₂ ∈ f, univ * t₂ ⊆ s) → s = univ
Tactic: simp only [mem_mul, mem_top, exists_eq_left]
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : Monoid α
f : Filter α
hf : 1 ≤ f
s t : Set α
ht : t ∈ f
hs : univ * t ⊆ s
⊢ s = univ
have rwa : ∀ (hs : univ ⊆ s), s = univ
Tactic: rwa [univ_mul_of_one_mem (mem_one.1 <| hf ht), univ_subset_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : Monoid α
f : Filter α
hf : 1 ≤ f
s t : Set α
ht : t ∈ f
hs : univ * t ⊆ s
rwa : ∀ (hs : univ ⊆ s), s = univ
⊢ s = univ
have rwa₁ : ∀ (hs : s = univ), s = univ
Tactic: rwa [univ_mul_of_one_mem (mem_one.1 <| hf ht), univ_subset_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : Monoid α
n : ℕ
h : n + 2 ≠ 0
⊢ HPow.hPow (α := Filter α) ⊤ (n + 2) = ⊤
have rw : HPow.hPow (α := Filter α) ⊤ (n + 1) * ⊤ = ⊤
Tactic: rw [pow_succ, top_pow n.succ_ne_zero, top_mul_top]
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : Monoid α
n : ℕ
h : n + 2 ≠ 0
rw : HPow.hPow (α := Filter α) ⊤ (n + 1) * ⊤ = ⊤
⊢ HPow.hPow (α := Filter α) ⊤ (n + 2) = ⊤
have rw₁ : HMul.hMul (α := Filter α) ⊤ ⊤ = ⊤
Tactic: rw [pow_succ, top_pow n.succ_ne_zero, top_mul_top]
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : Monoid α
n : ℕ
h : n + 2 ≠ 0
rw : HPow.hPow (α := Filter α) ⊤ (n + 1) * ⊤ = ⊤
rw₁ : HMul.hMul (α := Filter α) ⊤ ⊤ = ⊤
⊢ HPow.hPow (α := Filter α) ⊤ (n + 2) = ⊤
have rw₂ : Eq.{u_2 + 1} (α := Filter α) ⊤ ⊤
Tactic: rw [pow_succ, top_pow n.succ_ne_zero, top_mul_top]
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
f g : Filter α
⊢ f * g = 1 ↔ ∃ (a : α) (b : α), f = pure a ∧ g = pure b ∧ a * b = 1
have refine_1 : ∀ (hfg : f * g = 1), ∃ (a : α) (b : α), f = pure a ∧ g = pure b ∧ a * b = 1
Tactic: refine ⟨fun hfg => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
f g : Filter α
refine_1 : ∀ (hfg : f * g = 1), ∃ (a : α) (b : α), f = pure a ∧ g = pure b ∧ a * b = 1
⊢ f * g = 1 ↔ ∃ (a : α) (b : α), f = pure a ∧ g = pure b ∧ a * b = 1
have refine_2 : (∃ (a : α) (b : α), f = pure a ∧ g = pure b ∧ a * b = 1) → f * g = 1
Tactic: refine ⟨fun hfg => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
f g : Filter α
hfg : f * g = 1
⊢ ∃ (a : α) (b : α), f = pure a ∧ g = pure b ∧ a * b = 1
have refine_1 : ∀ (t₁ : Set α) (h₁ : t₁ ∈ f) (t₂ : Set α) (h₂ : t₂ ∈ g) (h : t₁ * t₂ ⊆ 1),
  ∃ (a : α) (b : α), f = pure a ∧ g = pure b ∧ a * b = 1
Tactic: obtain ⟨t₁, h₁, t₂, h₂, h⟩ : (1 : Set α) ∈ f * g := hfg.symm ▸ one_mem_one
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (hypothesis)
Goal:
α : Type u_2
inst : DivisionMonoid α
f g : Filter α
hfg : f * g = 1
t₁ : Set α
h₁ : t₁ ∈ f
t₂ : Set α
h₂ : t₂ ∈ g
h : t₁ * t₂ ⊆ 1
⊢ ∃ (a : α) (b : α), f = pure a ∧ g = pure b ∧ a * b = 1
have hfg₁ : (f * g).NeBot
Tactic: have hfg : (f * g).NeBot := hfg.symm.subst one_neBot
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (hypothesis)
Goal:
α : Type u_2
inst : DivisionMonoid α
f g : Filter α
hfg_1 : f * g = 1
t₁ : Set α
h₁ : t₁ ∈ f
t₂ : Set α
h₂ : t₂ ∈ g
h : t₁ * t₂ ⊆ 1
hfg : (f * g).NeBot
⊢ ∃ (a : α) (b : α), f = pure a ∧ g = pure b ∧ a * b = 1
have h₃ : ∃ (a : α) (b : α), t₁ = {a} ∧ t₂ = {b} ∧ a * b = 1
Tactic: rw [(hfg.nonempty_of_mem <| mul_mem_mul h₁ h₂).subset_one_iff, Set.mul_eq_one_iff] at h
Cleared hypotheses: h, hfg
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
f g : Filter α
hfg_1 : f * g = 1
t₁ : Set α
h₁ : t₁ ∈ f
t₂ : Set α
h₂ : t₂ ∈ g
h : ∃ (a : α) (b : α), t₁ = {a} ∧ t₂ = {b} ∧ a * b = 1
hfg : (f * g).NeBot
⊢ ∃ (a : α) (b : α), f = pure a ∧ g = pure b ∧ a * b = 1
have refine_1 : ∀ (a b : α) (h₁ : {a} ∈ f) (h : a * b = 1) (h₂ : {b} ∈ g), ∃ (a : α) (b : α), f = pure a ∧ g = pure b ∧ a * b = 1
Tactic: obtain ⟨a, b, rfl, rfl, h⟩ := h
Cleared hypotheses: t₁, h₁, t₂, h₂, h
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
f g : Filter α
hfg_1 : f * g = 1
hfg : (f * g).NeBot
a b : α
h₁ : {a} ∈ f
h : a * b = 1
h₂ : {b} ∈ g
⊢ ∃ (a : α) (b : α), f = pure a ∧ g = pure b ∧ a * b = 1
have refine_1 : f = pure a
Tactic: refine ⟨a, b, ?_, ?_, h⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
f g : Filter α
hfg_1 : f * g = 1
hfg : (f * g).NeBot
a b : α
h₁ : {a} ∈ f
h : a * b = 1
h₂ : {b} ∈ g
refine_1 : f = pure a
⊢ ∃ (a : α) (b : α), f = pure a ∧ g = pure b ∧ a * b = 1
have refine_1₁ : g = pure b
Tactic: refine ⟨a, b, ?_, ?_, h⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
f g : Filter α
hfg_1 : f * g = 1
hfg : (f * g).NeBot
a b : α
h₁ : {a} ∈ f
h : a * b = 1
h₂ : {b} ∈ g
⊢ f = pure a
have refine_1 : f ≤ pure a
Tactic: rwa [← hfg.of_mul_left.le_pure_iff, le_pure_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
f g : Filter α
hfg_1 : f * g = 1
hfg : (f * g).NeBot
a b : α
h₁ : {a} ∈ f
h : a * b = 1
h₂ : {b} ∈ g
⊢ g = pure b
have refine_1 : g ≤ pure b
Tactic: rwa [← hfg.of_mul_right.le_pure_iff, le_pure_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
a b : α
h : a * b = 1
⊢ HMul.hMul (α := Filter α) (pure a) (pure b) = 1
have refine_2 : Eq (α := Filter α) (pure (a * b)) 1
Tactic: rw [pure_mul_pure, h, pure_one]
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
a b : α
h : a * b = 1
refine_2 : Eq (α := Filter α) (pure (a * b)) 1
⊢ HMul.hMul (α := Filter α) (pure a) (pure b) = 1
have refine_2₁ : Eq.{u_2 + 1} (α := Filter α) (pure 1) 1
Tactic: rw [pure_mul_pure, h, pure_one]
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
a b : α
h : a * b = 1
refine_2 : Eq (α := Filter α) (pure (a * b)) 1
refine_2₁ : Eq.{u_2 + 1} (α := Filter α) (pure 1) 1
⊢ HMul.hMul (α := Filter α) (pure a) (pure b) = 1
have refine_2₂ : Eq.{u_2 + 1} (α := Filter α) 1 1
Tactic: rw [pure_mul_pure, h, pure_one]
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst : DivisionMonoid α
f g s t : Filter α
h : s * t = 1
⊢ s⁻¹ = t
have obtain : ∀ (a b : α) (hab : a * b = 1) (h : HMul.hMul (α := Filter α) (pure a) (pure b) = 1),
  Eq (α := Filter α) (pure a)⁻¹ (pure b)
Tactic: obtain ⟨a, b, rfl, rfl, hab⟩ := Filter.mul_eq_one_iff.1 h
Cleared hypotheses: s, t, h
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst : DivisionMonoid α
f g : Filter α
a b : α
hab : a * b = 1
h : HMul.hMul (α := Filter α) (pure a) (pure b) = 1
⊢ Eq (α := Filter α) (pure a)⁻¹ (pure b)
have rw : Eq (α := Filter α) (pure a⁻¹) (pure b)
Tactic: rw [inv_pure, inv_eq_of_mul_eq_one_right hab]
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst : DivisionMonoid α
f g : Filter α
a b : α
hab : a * b = 1
h : HMul.hMul (α := Filter α) (pure a) (pure b) = 1
rw : Eq (α := Filter α) (pure a⁻¹) (pure b)
⊢ Eq (α := Filter α) (pure a)⁻¹ (pure b)
have rw₁ : Eq (α := Filter α) (pure b) (pure b)
Tactic: rw [inv_pure, inv_eq_of_mul_eq_one_right hab]
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
f : Filter α
⊢ IsUnit f ↔ ∃ (a : α), f = pure a ∧ IsUnit a
have mp : IsUnit f → ∃ (a : α), f = pure a ∧ IsUnit a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
f : Filter α
mp : IsUnit f → ∃ (a : α), f = pure a ∧ IsUnit a
⊢ IsUnit f ↔ ∃ (a : α), f = pure a ∧ IsUnit a
have mpr : (∃ (a : α), f = pure a ∧ IsUnit a) → IsUnit f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
u : (Filter α)ˣ
⊢ ∃ (a : α), (↑u : Filter α) = pure a ∧ IsUnit a
have mp : ∀ (a b : α) (ha : (↑u : Filter α) = pure a) (hb : (↑u⁻¹ : Filter α) = pure b) (h : a * b = 1),
  ∃ (a : α), (↑u : Filter α) = pure a ∧ IsUnit a
Tactic: obtain ⟨a, b, ha, hb, h⟩ := Filter.mul_eq_one_iff.1 u.mul_inv
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
u : (Filter α)ˣ
a b : α
ha : (↑u : Filter α) = pure a
hb : (↑u⁻¹ : Filter α) = pure b
h : a * b = 1
⊢ ∃ (a : α), (↑u : Filter α) = pure a ∧ IsUnit a
have mp : Eq (α := Filter α) (pure (b * a)) (pure 1)
Tactic: refine ⟨a, ha, ⟨a, b, h, pure_injective ?_⟩, rfl⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : DivisionMonoid α
u : (Filter α)ˣ
a b : α
ha : (↑u : Filter α) = pure a
hb : (↑u⁻¹ : Filter α) = pure b
h : a * b = 1
⊢ Eq (α := Filter α) (pure (b * a)) (pure 1)
have mp : (↑u⁻¹ : Filter α) * (↑u : Filter α) = pure 1
Tactic: rw [← pure_mul_pure, ← ha, ← hb]
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : Group α
f g : Filter α
⊢ 1 ≤ f / g ↔ ¬Disjoint f g
have refine_1 : ∀ (h : 1 ≤ f / g) (hfg : Disjoint f g), False
Tactic: refine ⟨fun h hfg => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : Group α
f g : Filter α
refine_1 : ∀ (h : 1 ≤ f / g) (hfg : Disjoint f g), False
⊢ 1 ≤ f / g ↔ ¬Disjoint f g
have refine_2 : ¬Disjoint f g → 1 ≤ f / g
Tactic: refine ⟨fun h hfg => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
inst : Group α
f g : Filter α
h : 1 ≤ f / g
hfg : Disjoint f g
⊢ False
have refine_1 : ∀ (s : Set α) (hs : s ∈ f) (t : Set α) (ht : t ∈ g) (hst : ∅ = s ∩ t), False
Tactic: obtain ⟨s, hs, t, ht, hst⟩ := hfg.le_bot (mem_bot : ∅ ∈ ⊥)
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst : SMul α β
inst_1 : SMul α γ
inst_2 : SMul β γ
inst_3 : IsScalarTower α β γ
a : α
b : β
f : Filter γ
⊢ (a • b) • f = a • b • f
have simp : Eq (α := Filter γ) (map (fun (b_1 : γ) ↦ a • b • b_1) f) (map ((fun (b : γ) ↦ a • b) ∘ fun (b_1 : γ) ↦ b • b_1) f)
Tactic: simp only [← Filter.map_smul, map_map, smul_assoc]
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst : SMul α β
inst_1 : SMul α γ
inst_2 : SMul β γ
inst_3 : IsScalarTower α β γ
a : α
f : Filter β
g : Filter γ
⊢ (a • f) • g = a • f • g
have refine : ∀ (x : β) (x_1 : γ), a • x • x_1 = (a • x) • x_1
Tactic: refine (map_map₂_distrib_left fun _ _ => ?_).symm
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst : Monoid α
inst_1 : MulAction α β
f : Filter β
⊢ map (fun (x2 : β) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := α) 1 x2) f = f
have simp_rw : map (fun (x2 : β) ↦ x2) f = f
Tactic: simp_rw [one_smul, map_id']
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst : Monoid α
inst_1 : AddMonoid β
inst_2 : DistribMulAction α β
x : α
⊢ Eq (α := Filter β) (pure (HSMul.hSMul (β := β) x 0)) 0
have rw : Eq.{u_3 + 1} (α := Filter β) (pure 0) 0
Tactic: rw [smul_zero, pure_zero]
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst : Monoid α
inst_1 : AddMonoid β
inst_2 : DistribMulAction α β
x : α
rw : Eq.{u_3 + 1} (α := Filter β) (pure 0) 0
⊢ Eq (α := Filter β) (pure (HSMul.hSMul (β := β) x 0)) 0
have rw₁ : Eq.{u_3 + 1} (α := Filter β) 0 0
Tactic: rw [smul_zero, pure_zero]
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst : Monoid α
inst_1 : Monoid β
inst_2 : MulDistribMulAction α β
x : α
⊢ Eq (α := Set β) {HSMul.hSMul (β := β) x 1} 1
have rw : Eq (α := Set β) {1} 1
Tactic: rw [smul_one, singleton_one]
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst : Monoid α
inst_1 : Monoid β
inst_2 : MulDistribMulAction α β
x : α
rw : Eq (α := Set β) {1} 1
⊢ Eq (α := Set β) {HSMul.hSMul (β := β) x 1} 1
have rw₁ : Eq.{u_3 + 1} (α := Set β) 1 1
Tactic: rw [smul_one, singleton_one]
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
g : Filter β
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := α) 0 g ≤ 0
have refine : ∀ (s : Set β) (hs : Membership.mem (γ := Filter β) 0 s),
  (fun (x : β) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := α) 0 x) ⁻¹' s ∈ g
Tactic: refine fun s hs => mem_smul_filter.2 ?_
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
g : Filter β
s : Set β
hs : Membership.mem (γ := Filter β) 0 s
⊢ (fun (x : β) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := α) 0 x) ⁻¹' s ∈ g
have h : Eq (α := Set β) ((fun (x : β) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := α) 0 x) ⁻¹' s) univ
Tactic: convert! @univ_mem _ g
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
g : Filter β
s : Set β
hs : Membership.mem (γ := Filter β) 0 s
⊢ Eq (α := Set β) ((fun (x : β) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := α) 0 x) ⁻¹' s) univ
have h : ∀ (a : β), Membership.mem (γ := Set β) ((fun (x : β) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := α) 0 x) ⁻¹' s) a
Tactic: refine eq_univ_iff_forall.2 fun a => ?_
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
g : Filter β
s : Set β
hs : Membership.mem (γ := Filter β) 0 s
a : β
⊢ Membership.mem (γ := Set β) ((fun (x : β) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := α) 0 x) ⁻¹' s) a
have h : HSMul.hSMul.{u_2, u_3, u_3} (α := α) 0 a ∈ s
Tactic: rwa [mem_preimage, zero_smul]
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
g : Filter β
s : Set β
hs : Membership.mem (γ := Filter β) 0 s
a : β
h : HSMul.hSMul.{u_2, u_3, u_3} (α := α) 0 a ∈ s
⊢ Membership.mem (γ := Set β) ((fun (x : β) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := α) 0 x) ⁻¹' s) a
have h₁ : 0 ∈ s
Tactic: rwa [mem_preimage, zero_smul]
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
g : Filter β
hg : g.NeBot
s : Set β
hs : s ∈ g
⊢ Membership.mem (γ := Filter β) 0 ((fun (x : β) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := α) 0 x) '' s)
have simp_rw : Membership.mem (γ := Filter β) 0 {0}
Tactic: simp_rw [zero_smul, (hg.nonempty_of_mem hs).image_const]
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Monoid γ
inst_1 : MulAction γ β
m : α → β
c : γ
f : Filter α
g : Filter β
hc : IsUnit c
⊢ Tendsto (c • m) f (c • g) ↔ Tendsto m f g
have rcases : ∀ (d : γ) (hd : d * c = 1), Tendsto (c • m) f (c • g) ↔ Tendsto m f g
Tactic: rcases hc.exists_left_inv with ⟨d, hd⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Pointwise (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Monoid γ
inst_1 : MulAction γ β
m : α → β
c : γ
f : Filter α
g : Filter β
hc : IsUnit c
d : γ
hd : d * c = 1
⊢ Tendsto (c • m) f (c • g) ↔ Tendsto m f g
have refine : ∀ (H : Tendsto (c • m) f (c • g)), Tendsto m f g
Tactic: refine ⟨fun H ↦ ?_, fun H ↦ tendsto_map.comp H⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set (α × β)
f : Filter α
g : Filter β
⊢ s ∈ f ×ˢ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s
have mp : s ∈ f ×ˢ g → ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s
Tactic: constructor