awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
f : α → β
lc : Filter γ
g : γ → α
hg : Tendsto g lc l
b : β
hb : f =ᶠ[l] fun (x : α) ↦ b
⊢ IsConstant (l := lc) (↑(f ∘ g) : lc.Germ β)

Tactic:
⟨b, hb.comp_tendsto hg⟩

Premises used: Filter.EventuallyEq.comp_tendsto, Exists.intro, Filter.Germ.IsConstant
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
f : α → β
lc : Filter γ
g : γ → α
hg : Tendsto g lc l
b : β
hb : f =ᶠ[l] fun (x : α) ↦ b
⊢ IsConstant (l := lc) (↑(f ∘ g) : lc.Germ β)

Tactic:
exact ⟨b, hb.comp_tendsto hg⟩
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
lc : Filter γ
g : γ → α
hg : Tendsto g lc l
f : α → β
hf : IsConstant ⟦f⟧
⊢ (compTendsto ⟦f⟧ g hg).IsConstant

Tactic:
?_
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
f : l.Germ β
lc : Filter γ
g : γ → α
hf : f.IsConstant
hg : Tendsto g lc l
h : ∀ (f : α → β) (hf : IsConstant ⟦f⟧), (compTendsto ⟦f⟧ g hg).IsConstant
⊢ (f.compTendsto g hg).IsConstant

Tactic:
induction f using Quotient.inductionOn with | _ f => ?_
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
lc : Filter γ
g : γ → α
hg : Tendsto g lc l
f : α → β
hf : IsConstant ⟦f⟧
⊢ (compTendsto ⟦f⟧ g hg).IsConstant

Tactic:
isConstant_comp_tendsto hf hg

Premises used: Filter.Germ.compTendsto, Filter.Germ.ofFun, Quotient.liftOn', Filter.Germ.compTendsto', Filter.Germ.map', Filter.Germ.isConstant_comp_tendsto, Filter.Germ.liftOn, Quot.map, Quotient.map', Filter.Germ.map
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
lc : Filter γ
g : γ → α
hg : Tendsto g lc l
f : α → β
hf : IsConstant ⟦f⟧
⊢ (compTendsto ⟦f⟧ g hg).IsConstant

Tactic:
exact isConstant_comp_tendsto hf hg

Premises used: Filter.Germ.isConstant_comp_tendsto
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : l.NeBot
a b : β
⊢ Eq (α := l.Germ β) (↑a : l.Germ β) (↑b : l.Germ β) ↔ a = b

Tactic:
coe_eq.trans const_eventuallyEq

Premises used: Filter.Germ.const, Filter.Germ.coe_eq, Filter.const_eventuallyEq, Iff.trans
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
a : β
f : β → γ
⊢ Eq (α := l.Germ γ) (map f (↑a : l.Germ β)) (↑(f a) : l.Germ γ)

Tactic:
rfl

Premises used: Filter.Germ.ofFun, Filter.Germ.const, Quotient.mk', rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
b : β
c : γ
f : β → γ → δ
⊢ Eq (α := l.Germ δ) (map₂ f (↑b : l.Germ β) (↑c : l.Germ γ)) (↑(f b c) : l.Germ δ)

Tactic:
rfl

Premises used: Filter.Germ.ofFun, Filter.Germ.const, Quotient.mk', rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
b : β
lc : Filter γ
g : γ → α
hg : Tendsto g lc l
⊢ compTendsto (↑b : l.Germ β) g hg = (↑b : lc.Germ β)

Tactic:
rfl

Premises used: Filter.Germ.compTendsto, Filter.Germ.ofFun, Filter.Germ.const, Filter.Germ.compTendsto', Filter.Germ.map', Quotient.mk', Quotient.map', Filter.Germ.map, rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
b : β
lc : Filter γ
g : lc.Germ α
hg : g.Tendsto l
⊢ compTendsto' (↑b : l.Germ β) g hg = (↑b : lc.Germ β)

Tactic:
inductionOn g (fun _ _ => rfl) hg

Premises used: Filter.Germ.inductionOn
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
l : Filter α
p : β → Prop
f : α → β
⊢ LiftPred (l := l) p (↑f : l.Germ β) ↔ ∀ᶠ (x : α) in l, p (f x)

Tactic:
Iff.rfl

Premises used: Quotient.liftOn', Filter.Eventually, Iff.rfl, Filter.Germ.LiftPred, Filter.Germ.liftOn
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
l : Filter α
p : β → Prop
x : β
hx : p x
⊢ LiftPred.{u_1, u_2} (α := α) (l := l) p (↑x : l.Germ β)

Tactic:
Eventually.of_forall fun _y => hx

Premises used: Quotient.liftOn', Filter.Eventually, Filter.Eventually.of_forall, Filter.Germ.LiftPred, Filter.Germ.liftOn
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : l.NeBot
p : β → Prop
x : β
⊢ LiftPred.{u_1, u_2} (α := α) (l := l) p (↑x : l.Germ β) ↔ p x

Tactic:
@eventually_const _ _ _ (p x)

Premises used: Quotient.liftOn', Set.Mem, Filter.Eventually, setOf, Filter.Germ.LiftPred, Filter.eventually_const, Filter.Germ.liftOn
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
r : β → γ → Prop
f : α → β
g : α → γ
⊢ LiftRel (l := l) r (↑f : l.Germ β) (↑g : l.Germ γ) ↔ ∀ᶠ (x : α) in l, r (f x) (g x)

Tactic:
Iff.rfl

Premises used: Filter.Eventually, Iff.rfl, Filter.Germ.LiftRel, Quotient.liftOn₂'
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
r : β → γ → Prop
x : β
y : γ
h : r x y
⊢ LiftRel.{u_1, u_2, u_3} (α := α) (l := l) r (↑x : l.Germ β) (↑y : l.Germ γ)

Tactic:
Eventually.of_forall fun _ => h

Premises used: Filter.Eventually, Filter.Germ.LiftRel, Filter.Eventually.of_forall, Quotient.liftOn₂'
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
inst : l.NeBot
r : β → γ → Prop
x : β
y : γ
⊢ LiftRel.{u_1, u_2, u_3} (α := α) (l := l) r (↑x : l.Germ β) (↑y : l.Germ γ) ↔ r x y

Tactic:
@eventually_const _ _ _ (r x y)

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.Germ.LiftRel, Filter.eventually_const, Quotient.liftOn₂'
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
l : Filter α
M : Type u_5
inst : Mul M
f g : α → M
⊢ (↑(f * g) : l.Germ M) = HMul.hMul (α := l.Germ M) (↑f : l.Germ M) (↑g : l.Germ M)

Tactic:
rfl

Premises used: Filter.Germ.ofFun, Quotient.map₂, Filter.Germ.map₂, Quotient.mk', rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
l : Filter α
M : Type u_5
inst : One M
⊢ Eq (α := l.Germ M) (↑1 : l.Germ M) 1

Tactic:
rfl

Premises used: Filter.Germ.ofFun, Filter.Germ.const, Quotient.mk', rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
l : Filter α
M : Type u_5
G : Type u_6
inst : SMul M G
n : M
f : α → G
⊢ (↑(n • f) : l.Germ G) = HSMul.hSMul (β := l.Germ G) n (↑f : l.Germ G)

Tactic:
rfl

Premises used: Filter.Germ.ofFun, Filter.Germ.map', Quotient.mk', Quot.map, Quotient.map', Filter.Germ.map, rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
l : Filter α
M : Type u_5
G : Type u_6
inst : SMul M G
n : M
a : G
⊢ (↑(n • a) : l.Germ G) = HSMul.hSMul (β := l.Germ G) n (↑a : l.Germ G)

Tactic:
rfl

Premises used: Filter.Germ.ofFun, Filter.Germ.const, Filter.Germ.map', Quotient.mk', Quot.map, Quotient.map', Filter.Germ.map, rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
l : Filter α
M : Type u_5
G : Type u_6
inst : Pow G M
f : α → G
n : M
⊢ (↑(f ^ n) : l.Germ G) = HPow.hPow (α := l.Germ G) (↑f : l.Germ G) n

Tactic:
rfl

Premises used: Filter.Germ.ofFun, Filter.Germ.map', Quotient.mk', Quot.map, Quotient.map', Filter.Germ.map, rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
l : Filter α
M : Type u_5
G : Type u_6
inst : Pow G M
a : G
n : M
⊢ (↑(a ^ n) : l.Germ G) = HPow.hPow (α := l.Germ G) (↑a : l.Germ G) n

Tactic:
rfl

Premises used: Filter.Germ.ofFun, Filter.Germ.const, Filter.Germ.map', Quotient.mk', Quot.map, Quotient.map', Filter.Germ.map, rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f g h : α → β
M : Type u_5
G : Type u_6
inst : Monoid M
⊢ Eq (α := l.Germ M) (↑1 : l.Germ M) 1

Tactic:
rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f g h : α → β
M : Type u_5
G : Type u_6
inst : Monoid M
x x_1 : α → M
⊢ (↑(x * x_1) : l.Germ M) = HMul.hMul (α := l.Germ M) (↑x : l.Germ M) (↑x_1 : l.Germ M)

Tactic:
rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f g h : α → β
M : Type u_5
G : Type u_6
inst : Monoid M
x : α → M
x_1 : ℕ
⊢ (↑(x ^ x_1) : l.Germ M) = HPow.hPow (α := l.Germ M) (↑x : l.Germ M) x_1

Tactic:
rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
l : Filter α
M : Type u_5
inst : Monoid M
⊢ Eq (α := (a : α → M) → l.Germ M) (⇑(coeMulHom l) : (a : α → M) → l.Germ M) ofFun

Tactic:
rfl

Premises used: Filter.Germ.ofFun, Quotient.mk', rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
l : Filter α
M : Type u_5
inst : NatCast M
n : ℕ
⊢ Eq (α := l.Germ M) (↑fun (x : α) ↦ (↑n : M) : l.Germ M) (↑n : l.Germ M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
l : Filter α
M : Type u_5
inst : NatCast M
n : ℕ
⊢ Eq (α := l.Germ M) (↑(↑n : M) : l.Germ M) (↑n : l.Germ M)

Tactic:
rfl

Premises used: Filter.Germ.const, rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
l : Filter α
M : Type u_5
inst : NatCast M
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq (α := l.Germ M) (↑(OfNat.ofNat n) : l.Germ M) (OfNat.ofNat n)

Tactic:
rfl

Premises used: Filter.Germ.ofFun, Quotient.mk', rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
l : Filter α
M : Type u_5
inst : NatCast M
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq (α := l.Germ M) (↑(OfNat.ofNat n) : l.Germ M) (OfNat.ofNat n)

Tactic:
rfl

Premises used: Filter.Germ.ofFun, Filter.Germ.const, Quotient.mk', rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
l : Filter α
M : Type u_5
inst : IntCast M
n : ℤ
⊢ Eq (α := l.Germ M) (↑fun (x : α) ↦ (↑n : M) : l.Germ M) (↑n : l.Germ M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f g h : α → β
M : Type u_5
G : Type u_6
inst : AddMonoidWithOne M
simp : Eq (α := α → M) 0 fun (x : α) ↦ 0
⊢ Eq (α := α → M) (↑0 : α → M) fun (x : α) ↦ 0

Tactic:
simp
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f g h : α → β
M : Type u_5
G : Type u_6
inst : AddMonoidWithOne M
⊢ Eq (α := α → M) 0 fun (x : α) ↦ 0

Tactic:
rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f g h : α → β
M : Type u_5
G : Type u_6
inst : AddMonoidWithOne M
x : ℕ
simp : HAdd.hAdd (α := α → M) (↑x : α → M) 1 = fun (x_1 : α) ↦ HAdd.hAdd (α := M) (↑x : M) 1
⊢ Eq (α := α → M) (↑(x + 1) : α → M)
    ((fun (f g : α → M) (x : α) ↦ ((fun (x1 x2 : M) ↦ x1 + x2) (f x) (g x) : M)) (↑x : α → M) fun (x : α) ↦ 1)

Tactic:
simp
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f g h : α → β
M : Type u_5
G : Type u_6
inst : AddMonoidWithOne M
x : ℕ
⊢ HAdd.hAdd (α := α → M) (↑x : α → M) 1 = fun (x_1 : α) ↦ HAdd.hAdd (α := M) (↑x : M) 1

Tactic:
rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
l : Filter α
G : Type u_6
inst : Inv G
f : α → G
⊢ Eq (α := l.Germ G) (↑f⁻¹ : l.Germ G) (↑f : l.Germ G)⁻¹

Tactic:
rfl

Premises used: Filter.Germ.ofFun, Filter.Germ.map', Quotient.mk', Quot.map, Quotient.map', Filter.Germ.map, rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
l : Filter α
G : Type u_6
inst : Inv G
a : G
⊢ Eq (α := l.Germ G) (↑a⁻¹ : l.Germ G) (↑a : l.Germ G)⁻¹

Tactic:
rfl

Premises used: Filter.Germ.ofFun, Filter.Germ.const, Filter.Germ.map', Quotient.mk', Quot.map, Quotient.map', Filter.Germ.map, rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
l : Filter α
M : Type u_5
inst : Div M
f g : α → M
⊢ (↑(f / g) : l.Germ M) = HDiv.hDiv (α := l.Germ M) (↑f : l.Germ M) (↑g : l.Germ M)

Tactic:
rfl

Premises used: Filter.Germ.ofFun, Quotient.map₂, Filter.Germ.map₂, Quotient.mk', rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
l : Filter α
M : Type u_5
inst : Div M
a b : M
⊢ (↑(a / b) : l.Germ M) = HDiv.hDiv (α := l.Germ M) (↑a : l.Germ M) (↑b : l.Germ M)

Tactic:
rfl

Premises used: Filter.Germ.ofFun, Filter.Germ.const, Quotient.map₂, Filter.Germ.map₂, Quotient.mk', rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f g h : α → β
M : Type u_5
G : Type u_6
inst : AddGroupWithOne G
x : ℕ
⊢ Eq (α := α → G) (↑(↑x : ℤ) : α → G) (↑x : α → G)

Tactic:
simp
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f g h : α → β
M : Type u_5
G : Type u_6
inst : AddGroupWithOne G
x : ℕ
simp : HAdd.hAdd (α := α → G) (-1) (-(↑x : α → G)) = fun (x_1 : α) ↦ HAdd.hAdd (α := G) (-1) (-(↑x : G))
⊢ Eq (α := α → G) (↑(Int.negSucc x) : α → G) ((fun (x : α → G) ↦ Neg.neg ∘ x) (↑(x + 1) : α → G))

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f g h : α → β
M : Type u_5
G : Type u_6
inst : AddGroupWithOne G
x : ℕ
⊢ HAdd.hAdd (α := α → G) (-1) (-(↑x : α → G)) = fun (x_1 : α) ↦ HAdd.hAdd (α := G) (-1) (-(↑x : G))

Tactic:
rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f g h : α → β
R : Type u_5
inst : Nontrivial R
inst_1 : l.NeBot
⊢ Nontrivial (l.Germ R)

Tactic:
let ⟨x, y, h⟩ := exists_pair_ne R
  ⟨⟨↑x, ↑y, mt const_inj.1 h⟩⟩

Premises used: Nontrivial, Filter.Germ.const, mt, _private.0.Filter.Germ.instNontrivial.match_1, Nontrivial.mk, Filter.Germ.const_inj, Filter.Germ, Exists.intro, Iff.mp, exists_pair_ne
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
l : Filter α
R : Type u_5
inst : Semiring R
⊢ Eq (α := (a : α → R) → l.Germ R) (⇑(coeRingHom l) : (a : α → R) → l.Germ R) ofFun

Tactic:
rfl

Premises used: Filter.Germ.ofFun, Quotient.mk', rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
l : Filter α
M : Type u_5
inst : SMul M β
c : α → M
f : α → β
⊢ (↑(c • f) : l.Germ β) = HSMul.hSMul (α := l.Germ M) (β := l.Germ β) (↑c : l.Germ M) (↑f : l.Germ β)

Tactic:
rfl

Premises used: Filter.Germ.ofFun, Quotient.map₂, Filter.Germ.map₂, Quotient.mk', rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst : Monoid M
inst_1 : MulAction M β
c₁ c₂ : M
f_2 : l.Germ β
f : α → β
norm_cast : (c₁ * c₂) • f =ᶠ[l] c₁ • c₂ • f
⊢ HSMul.hSMul (β := l.Germ β) (c₁ * c₂) (↑f : l.Germ β) = c₁ • HSMul.hSMul (β := l.Germ β) c₂ (↑f : l.Germ β)

Tactic:
norm_cast
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst : Monoid M
inst_1 : MulAction M β
c₁ c₂ : M
f_2 : l.Germ β
f : α → β
⊢ (c₁ * c₂) • f =ᶠ[l] c₁ • c₂ • f

Tactic:
simp [mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst : Monoid M
inst_1 : MulAction M β
f_2 : l.Germ β
f : α → β
norm_cast : HSMul.hSMul (α := M) 1 f =ᶠ[l] f
⊢ HSMul.hSMul (α := M) (β := l.Germ β) 1 (↑f : l.Germ β) = (↑f : l.Germ β)

Tactic:
norm_cast
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst : Monoid M
inst_1 : MulAction M β
f_2 : l.Germ β
f : α → β
⊢ HSMul.hSMul (α := M) 1 f =ᶠ[l] f

Tactic:
simp [one_smul]

Premises used: one_smul
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst : Monoid M
inst_1 : MulAction M β
c₁_1 c₂_1 : l.Germ M
f_2 : l.Germ β
c₁ c₂ : α → M
f : α → β
norm_cast : (c₁ * c₂) • f =ᶠ[l] c₁ • c₂ • f
⊢ HSMul.hSMul (β := l.Germ β) (HMul.hMul (α := l.Germ M) (↑c₁ : l.Germ M) (↑c₂ : l.Germ M)) (↑f : l.Germ β) =
    HSMul.hSMul (α := l.Germ M) (↑c₁ : l.Germ M)
      (HSMul.hSMul (α := l.Germ M) (β := l.Germ β) (↑c₂ : l.Germ M) (↑f : l.Germ β))

Tactic:
norm_cast
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst : Monoid M
inst_1 : MulAction M β
c₁_1 c₂_1 : l.Germ M
f_2 : l.Germ β
c₁ c₂ : α → M
f : α → β
⊢ (c₁ * c₂) • f =ᶠ[l] c₁ • c₂ • f

Tactic:
simp [mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst : Monoid M
inst_1 : MulAction M β
f_2 : l.Germ β
f : α → β
⊢ HSMul.hSMul (α := l.Germ M) (β := l.Germ β) 1 (↑f : l.Germ β) = (↑f : l.Germ β)

Tactic:
simp only [← coe_one, ← coe_smul', one_smul]

Premises used: Filter.Germ.coe_one, one_smul, Filter.Germ.coe_smul'
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst : Monoid M
inst_1 : AddMonoid N
inst_2 : DistribMulAction M N
c : M
⊢ HSMul.hSMul (β := l.Germ N) c 0 = 0

Tactic:
simp only [← coe_zero, ← coe_smul, smul_zero]

Premises used: smul_zero, Filter.Germ.coe_smul, Filter.Germ.coe_zero
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g_1 h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst : Monoid M
inst_1 : AddMonoid N
inst_2 : DistribMulAction M N
c : M
f_2 g_2 : l.Germ N
f g : α → N
norm_cast : c • (f + g) =ᶠ[l] c • f + c • g
⊢ c • HAdd.hAdd (α := l.Germ N) (↑f : l.Germ N) (↑g : l.Germ N) =
    HSMul.hSMul (β := l.Germ N) c (↑f : l.Germ N) + HSMul.hSMul (β := l.Germ N) c (↑g : l.Germ N)

Tactic:
norm_cast
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g_1 h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst : Monoid M
inst_1 : AddMonoid N
inst_2 : DistribMulAction M N
c : M
f_2 g_2 : l.Germ N
f g : α → N
⊢ c • (f + g) =ᶠ[l] c • f + c • g

Tactic:
simp [smul_add]

Premises used: smul_add
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst : Monoid M
inst_1 : AddMonoid N
inst_2 : DistribMulAction M N
c_1 : l.Germ M
c : α → M
⊢ HSMul.hSMul (α := l.Germ M) (β := l.Germ N) (↑c : l.Germ M) 0 = 0

Tactic:
simp only [← coe_zero, ← coe_smul', smul_zero]

Premises used: smul_zero, Filter.Germ.coe_zero, Filter.Germ.coe_smul'
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g_1 h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst : Monoid M
inst_1 : AddMonoid N
inst_2 : DistribMulAction M N
c_1 : l.Germ M
f_2 g_2 : l.Germ N
c : α → M
f g : α → N
norm_cast : c • (f + g) =ᶠ[l] c • f + c • g
⊢ HSMul.hSMul (α := l.Germ M) (↑c : l.Germ M) (HAdd.hAdd (α := l.Germ N) (↑f : l.Germ N) (↑g : l.Germ N)) =
    HSMul.hSMul (α := l.Germ M) (β := l.Germ N) (↑c : l.Germ M) (↑f : l.Germ N) +
      HSMul.hSMul (α := l.Germ M) (β := l.Germ N) (↑c : l.Germ M) (↑g : l.Germ N)

Tactic:
norm_cast
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g_1 h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst : Monoid M
inst_1 : AddMonoid N
inst_2 : DistribMulAction M N
c_1 : l.Germ M
f_2 g_2 : l.Germ N
c : α → M
f g : α → N
⊢ c • (f + g) =ᶠ[l] c • f + c • g

Tactic:
simp [smul_add]

Premises used: smul_add
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
c₁ c₂ : R
f_2 : l.Germ M
f : α → M
norm_cast : (c₁ + c₂) • f =ᶠ[l] c₁ • f + c₂ • f
⊢ HSMul.hSMul (β := l.Germ M) (c₁ + c₂) (↑f : l.Germ M) =
    HSMul.hSMul (β := l.Germ M) c₁ (↑f : l.Germ M) + HSMul.hSMul (β := l.Germ M) c₂ (↑f : l.Germ M)

Tactic:
norm_cast
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
c₁ c₂ : R
f_2 : l.Germ M
f : α → M
⊢ (c₁ + c₂) • f =ᶠ[l] c₁ • f + c₂ • f

Tactic:
simp [add_smul]

Premises used: add_smul
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f_2 : l.Germ M
f : α → M
norm_cast : HSMul.hSMul (α := R) 0 f =ᶠ[l] 0
⊢ HSMul.hSMul (α := R) (β := l.Germ M) 0 (↑f : l.Germ M) = 0

Tactic:
norm_cast
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f_2 : l.Germ M
f : α → M
⊢ HSMul.hSMul (α := R) 0 f =ᶠ[l] 0

Tactic:
simp [zero_smul]

Premises used: zero_smul
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
c₁_1 c₂_1 : l.Germ R
f_2 : l.Germ M
c₁ c₂ : α → R
f : α → M
norm_cast : (c₁ + c₂) • f =ᶠ[l] c₁ • f + c₂ • f
⊢ HSMul.hSMul (β := l.Germ M) (HAdd.hAdd (α := l.Germ R) (↑c₁ : l.Germ R) (↑c₂ : l.Germ R)) (↑f : l.Germ M) =
    HSMul.hSMul (α := l.Germ R) (β := l.Germ M) (↑c₁ : l.Germ R) (↑f : l.Germ M) +
      HSMul.hSMul (α := l.Germ R) (β := l.Germ M) (↑c₂ : l.Germ R) (↑f : l.Germ M)

Tactic:
norm_cast
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
c₁_1 c₂_1 : l.Germ R
f_2 : l.Germ M
c₁ c₂ : α → R
f : α → M
⊢ (c₁ + c₂) • f =ᶠ[l] c₁ • f + c₂ • f

Tactic:
simp [add_smul]

Premises used: add_smul
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f_2 : l.Germ M
f : α → M
⊢ HSMul.hSMul (α := l.Germ R) (β := l.Germ M) 0 (↑f : l.Germ M) = 0

Tactic:
simp only [← coe_zero, ← coe_smul', zero_smul]

Premises used: zero_smul, Filter.Germ.coe_zero, Filter.Germ.coe_smul'
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : LE β
⊢ Eq (α := l.Germ β → l.Germ β → Prop) (fun (x1 x2 : l.Germ β) ↦ x1 ≤ x2) (LiftRel fun (x1 x2 : β) ↦ x1 ≤ x2)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
l : Filter α
f g : α → β
inst : LE β
⊢ LE.le (α := l.Germ β) (↑f : l.Germ β) (↑g : l.Germ β) ↔ f ≤ᶠ[l] g

Tactic:
Iff.rfl

Premises used: Set.Mem, Filter.Eventually, Iff.rfl, setOf, Filter.Germ.LiftRel, Filter.EventuallyLE, Quotient.liftOn₂'
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : LE β
inst_1 : Zero β
f : α → β
⊢ LE.le (α := l.Germ β) 0 (↑f : l.Germ β) ↔ ∀ᶠ (x : α) in l, 0 ≤ f x

Tactic:
Iff.rfl

Premises used: Set.Mem, Filter.Eventually, Iff.rfl, setOf, Filter.Germ.LiftRel, Quotient.liftOn₂'
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : LE β
x y : β
⊢ x ≤ y → LE.le (α := l.Germ β) (↑x : l.Germ β) (↑y : l.Germ β)

Tactic:
liftRel_const

Premises used: Filter.Germ.liftRel_const
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : LE β
inst_1 : l.NeBot
x y : β
⊢ LE.le (α := l.Germ β) (↑x : l.Germ β) (↑y : l.Germ β) ↔ x ≤ y

Tactic:
liftRel_const_iff

Premises used: Filter.Germ.liftRel_const_iff
-- Module: Mathlib.Order.Filter.Germ.Basic
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : Bot β
⊢ Eq (α := l.Germ β) (↑⊥ : l.Germ β) ⊥

Tactic:
rfl

Premises used: rfl