mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ ∑ t, (-1) ^ #↑t • ∑ a ∈ (↑t).inf' ⋯ S, f a +
      ∑ x ∈ {x ∈ s.powerset | ¬x.Nonempty}.attach, (-1) ^ #↑x • ∑ a ∈ s.biUnion S, f a =
    ∑ t ∈ s.powerset, (-1) ^ #t • if ht : t.Nonempty then ∑ a ∈ t.inf' ht S, f a else ∑ a ∈ s.biUnion S, f a

Tactic:
;

Goal state after:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ ∑ t, (-1) ^ #↑t • ∑ a ∈ (↑t).inf' ⋯ S, f a +
      ∑ x ∈ {x ∈ s.powerset | ¬x.Nonempty}.attach, (-1) ^ #↑x • ∑ a ∈ s.biUnion S, f a =
    ∑ t ∈ s.powerset, (-1) ^ #t • if ht : t.Nonempty then ∑ a ∈ t.inf' ht S, f a else ∑ a ∈ s.biUnion S, f a
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: case a.a
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
t : α
a✝¹ : t ∈ s.biUnion S
x✝ : ι
a✝ : x✝ ∈ s
⊢ 1 = (↑(s.biUnion S)).indicator 1 t

Tactic:
;

Goal state after:
case a.a
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
t : α
a✝¹ : t ∈ s.biUnion S
x✝ : ι
a✝ : x✝ ∈ s
⊢ 1 = (↑(s.biUnion S)).indicator 1 t
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: f : ℕ → ℚ
H : IsCauSeq abs f
ε : ℝ
ε0 : ε > 0
δ : ℚ
δ0 : 0 < δ
δε : ↑δ < ε
i : ℕ
hi : ∀ j ≥ i, |f j - f i| < δ
j : ℕ
ij : j ≥ i
⊢ |↑(f j) - ↑(f i)| < ε

Tactic:
;

Goal state after:
f : ℕ → ℚ
H : IsCauSeq abs f
ε : ℝ
ε0 : ε > 0
δ : ℚ
δ0 : 0 < δ
δε : ↑δ < ε
i : ℕ
hi : ∀ j ≥ i, |f j - f i| < δ
j : ℕ
ij : j ≥ i
⊢ |↑(f j) - ↑(f i)| < ε
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: f : ℕ → ℚ
H : IsCauSeq abs fun i ↦ ↑(f i)
ε : ℚ
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, |↑(f j) - ↑(f i)| < ↑ε
j : ℕ
ij : j ≥ i
⊢ |f j - f i| < ε

Tactic:
;

Goal state after:
f : ℕ → ℚ
H : IsCauSeq abs fun i ↦ ↑(f i)
ε : ℚ
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, |↑(f j) - ↑(f i)| < ↑ε
j : ℕ
ij : j ≥ i
⊢ |f j - f i| < ε
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ v.asIdeal ^ Multiset.count ⟨Associates.mk v.asIdeal, ⋯⟩ (factors' I) =
    v.asIdeal ^ Multiset.count v.asIdeal (normalizedFactors I)

Tactic:
← Multiset.count_map_eq_count' _ _ Subtype.val_injective,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ v.asIdeal ^ Multiset.count (↑⟨Associates.mk v.asIdeal, ⋯⟩) (Multiset.map Subtype.val (factors' I)) =
    v.asIdeal ^ Multiset.count v.asIdeal (normalizedFactors I)
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x : ℚ≥0
y : ℝ≥0
⊢ 0 ≤ ↑x * ↑y

Tactic:
;

Goal state after:
x : ℚ≥0
y : ℝ≥0
⊢ 0 ≤ ↑x * ↑y
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case inl
⊢ sSup (-∅) = -sInf ∅

pp: case inr
s : Set ℝ
hn : s.Nonempty
⊢ sSup (-s) = -sInf s

Tactic:
;

Goal state after:
case inl
⊢ sSup (-∅) = -sInf ∅

case inr
s : Set ℝ
hn : s.Nonempty
⊢ sSup (-s) = -sInf s
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ι : Sort u_2
s : ι → ℝ≥0
⊢ sSup (Set.range (toReal ∘ fun i ↦ s i)) = sSup (Set.range fun i ↦ ↑(s i))

Tactic:
;

Goal state after:
ι : Sort u_2
s : ι → ℝ≥0
⊢ sSup (Set.range (toReal ∘ fun i ↦ s i)) = sSup (Set.range fun i ↦ ↑(s i))
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ι : Sort u_2
s : ι → ℝ≥0
⊢ sInf (Set.range (toReal ∘ fun i ↦ s i)) = sInf (Set.range fun i ↦ ↑(s i))

Tactic:
;

Goal state after:
ι : Sort u_2
s : ι → ℝ≥0
⊢ sInf (Set.range (toReal ∘ fun i ↦ s i)) = sInf (Set.range fun i ↦ ↑(s i))
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ
⊢ r.toNNReal < 1 ↔ r < 1

Tactic:
by simp only [← not_le, one_le_toNNReal]

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: p q : ℝ
hp : 0 ≤ p
⊢ ↑(p * q).toNNReal = ↑(p.toNNReal * q.toNNReal)

Tactic:
by simp [mul_max_of_nonneg, hp]

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ ⟨0, ⋯⟩ = 0

Tactic:
;

Goal state after:
⊢ ⟨0, ⋯⟩ = 0
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ ⟨1, ⋯⟩ = 1

Tactic:
;

Goal state after:
⊢ ⟨1, ⋯⟩ = 1
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x y : ℝ
⊢ ⟨|x| * |y|, ⋯⟩ = ⟨|x|, ⋯⟩ * ⟨|y|, ⋯⟩

Tactic:
;

Goal state after:
x y : ℝ
⊢ ⟨|x| * |y|, ⋯⟩ = ⟨|x|, ⋯⟩ * ⟨|y|, ⋯⟩
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ 2 = 1 + 1

Tactic:
;

Goal state after:
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ 2 = 1 + 1
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case hab
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ 1 / ↑k * ↑k + 1 ≤ (1 / ↑k + 1) ^ k

Tactic:
;

Goal state after:
case hab
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ 1 / ↑k * ↑k + 1 ≤ (1 / ↑k + 1) ^ k
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case pos
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hu1 : g < 1
⊢ f ↑g < f 1

Tactic:
;

Goal state after:
case pos
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hu1 : g < 1
⊢ f ↑g < f 1
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : FunLike F E ℝ
inst✝¹ : AddGroup E
inst✝ : NonarchAddGroupSeminormClass F E
f : F
x✝¹ x✝ a : E
⊢ f (a - a) ≤ f a

Tactic:
exact le_trans (map_sub_le_max _ _ _) (by rw [max_self (f a)])

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case mk
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p q g : GroupSeminorm E
toFun✝ : E → ℝ
map_one'✝ : toFun✝ 1 = 0
mul_le'✝ : ∀ (x y : E), toFun✝ (x * y) ≤ toFun✝ x + toFun✝ y
inv'✝ : ∀ (x : E), toFun✝ x⁻¹ = toFun✝ x
h :
  (fun f ↦ f.toFun) { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝ } = (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝ } = g

Tactic:
;

Goal state after:
case mk
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p q g : GroupSeminorm E
toFun✝ : E → ℝ
map_one'✝ : toFun✝ 1 = 0
mul_le'✝ : ∀ (x y : E), toFun✝ (x * y) ≤ toFun✝ x + toFun✝ y
inv'✝ : ∀ (x : E), toFun✝ x⁻¹ = toFun✝ x
h :
  (fun f ↦ f.toFun) { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝ } = (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝ } = g
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case mk.mk
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p q : GroupSeminorm E
toFun✝¹ : E → ℝ
map_one'✝¹ : toFun✝¹ 1 = 0
mul_le'✝¹ : ∀ (x y : E), toFun✝¹ (x * y) ≤ toFun✝¹ x + toFun✝¹ y
inv'✝¹ : ∀ (x : E), toFun✝¹ x⁻¹ = toFun✝¹ x
toFun✝ : E → ℝ
map_one'✝ : toFun✝ 1 = 0
mul_le'✝ : ∀ (x y : E), toFun✝ (x * y) ≤ toFun✝ x + toFun✝ y
inv'✝ : ∀ (x : E), toFun✝ x⁻¹ = toFun✝ x
h :
  (fun f ↦ f.toFun) { toFun := toFun✝¹, map_one' := map_one'✝¹, mul_le' := mul_le'✝¹, inv' := inv'✝¹ } =
    (fun f ↦ f.toFun) { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝ }
⊢ { toFun := toFun✝¹, map_one' := map_one'✝¹, mul_le' := mul_le'✝¹, inv' := inv'✝¹ } =
    { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝ }

Tactic:
;

Goal state after:
case mk.mk
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p q : GroupSeminorm E
toFun✝¹ : E → ℝ
map_one'✝¹ : toFun✝¹ 1 = 0
mul_le'✝¹ : ∀ (x y : E), toFun✝¹ (x * y) ≤ toFun✝¹ x + toFun✝¹ y
inv'✝¹ : ∀ (x : E), toFun✝¹ x⁻¹ = toFun✝¹ x
toFun✝ : E → ℝ
map_one'✝ : toFun✝ 1 = 0
mul_le'✝ : ∀ (x y : E), toFun✝ (x * y) ≤ toFun✝ x + toFun✝ y
inv'✝ : ∀ (x : E), toFun✝ x⁻¹ = toFun✝ x
h :
  (fun f ↦ f.toFun) { toFun := toFun✝¹, map_one' := map_one'✝¹, mul_le' := mul_le'✝¹, inv' := inv'✝¹ } =
    (fun f ↦ f.toFun) { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝ }
⊢ { toFun := toFun✝¹, map_one' := map_one'✝¹, mul_le' := mul_le'✝¹, inv' := inv'✝¹ } =
    { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝ }
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case neg
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hu1 : ¬g < 1
⊢ f ↑g⁻¹ < 1

Tactic:
have hfg0 : f g ≠ 0 :=
        fun h0 ↦ (Units.ne_zero g) ((map_eq_zero f).mp h0)
      have hg1' : 1 < g := lt_of_le_of_ne (not_lt.mp hu1) hg1.symm
      rw [Units.val_inv_eq_inv_val, map_inv₀, inv_lt_one_iff hfg0, ← map_one f]
      exact hf hg1'

Goal state after:
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: α : Type u_1
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
a : AddUnits ℝ≥0∞
⊢ ↑a ≤ ↑a + ↑(-a)

Tactic:
;

Goal state after:
α : Type u_1
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
a : AddUnits ℝ≥0∞
⊢ ↑a ≤ ↑a + ↑(-a)
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: r : ℝ≥0
⊢ ↑r = ENNReal.ofReal ↑r

Tactic:
ENNReal.ofReal,

Goal state after:
r : ℝ≥0
⊢ ↑r = ↑(↑r).toNNReal
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: z : ℝ≥0∞
⊢ ↑z.toReal.toNNReal = ↑z.toNNReal

Tactic:
;

Goal state after:
z : ℝ≥0∞
⊢ ↑z.toReal.toNNReal = ↑z.toNNReal
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ ENNReal.ofReal (p + q) = ENNReal.ofReal p + ENNReal.ofReal q

Tactic:
ENNReal.ofReal,

Goal state after:
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ ↑(p + q).toNNReal = ENNReal.ofReal p + ENNReal.ofReal q
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ ↑(p + q).toNNReal = ENNReal.ofReal p + ENNReal.ofReal q

Tactic:
ENNReal.ofReal,

Goal state after:
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ ↑(p + q).toNNReal = ↑p.toNNReal + ENNReal.ofReal q
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ ↑(p + q).toNNReal = ↑p.toNNReal + ENNReal.ofReal q

Tactic:
ENNReal.ofReal,

Goal state after:
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ ↑(p + q).toNNReal = ↑p.toNNReal + ↑q.toNNReal
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: p q : ℝ
h : 0 ≤ q
⊢ ENNReal.ofReal p ≤ ENNReal.ofReal q ↔ p ≤ q

Tactic:
ENNReal.ofReal,

Goal state after:
p q : ℝ
h : 0 ≤ q
⊢ ↑p.toNNReal ≤ ENNReal.ofReal q ↔ p ≤ q
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: p q : ℝ
h : 0 ≤ q
⊢ ↑p.toNNReal ≤ ENNReal.ofReal q ↔ p ≤ q

Tactic:
ENNReal.ofReal,

Goal state after:
p q : ℝ
h : 0 ≤ q
⊢ ↑p.toNNReal ≤ ↑q.toNNReal ↔ p ≤ q
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ ENNReal.ofReal p = ENNReal.ofReal q ↔ p = q

Tactic:
ENNReal.ofReal,

Goal state after:
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ ↑p.toNNReal = ENNReal.ofReal q ↔ p = q
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ ↑p.toNNReal = ENNReal.ofReal q ↔ p = q

Tactic:
ENNReal.ofReal,

Goal state after:
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ ↑p.toNNReal = ↑q.toNNReal ↔ p = q
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: p q : ℝ
h : 0 < q
⊢ ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q

Tactic:
ENNReal.ofReal,

Goal state after:
p q : ℝ
h : 0 < q
⊢ ↑p.toNNReal < ENNReal.ofReal q ↔ p < q
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: p q : ℝ
h : 0 < q
⊢ ↑p.toNNReal < ENNReal.ofReal q ↔ p < q

Tactic:
ENNReal.ofReal,

Goal state after:
p q : ℝ
h : 0 < q
⊢ ↑p.toNNReal < ↑q.toNNReal ↔ p < q
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p q g : NonarchAddGroupSeminorm E
toFun✝ : E → ℝ
map_zero'✝ : toFun✝ 0 = 0
add_le_max'✝ :
  ∀ (r s : E),
    { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun (r + s) ≤
      max ({ toFun := toFun✝, map_zero' := map_zero'✝ }.toFun r) ({ toFun := toFun✝, map_zero' := map_zero'✝ }.toFun s)
neg'✝ :
  ∀ (r : E),
    { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun (-r) = { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun r
h :
  (fun f ↦ f.toFun) { toFun := toFun✝, map_zero' := map_zero'✝, add_le_max' := add_le_max'✝, neg' := neg'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_zero' := map_zero'✝, add_le_max' := add_le_max'✝, neg' := neg'✝ } = g

Tactic:
;

Goal state after:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p q g : NonarchAddGroupSeminorm E
toFun✝ : E → ℝ
map_zero'✝ : toFun✝ 0 = 0
add_le_max'✝ :
  ∀ (r s : E),
    { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun (r + s) ≤
      max ({ toFun := toFun✝, map_zero' := map_zero'✝ }.toFun r) ({ toFun := toFun✝, map_zero' := map_zero'✝ }.toFun s)
neg'✝ :
  ∀ (r : E),
    { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun (-r) = { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun r
h :
  (fun f ↦ f.toFun) { toFun := toFun✝, map_zero' := map_zero'✝, add_le_max' := add_le_max'✝, neg' := neg'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_zero' := map_zero'✝, add_le_max' := add_le_max'✝, neg' := neg'✝ } = g
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: p q : ℝ
hp : 0 ≤ p
⊢ ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q

Tactic:
ENNReal.ofReal,

Goal state after:
p q : ℝ
hp : 0 ≤ p
⊢ ↑p.toNNReal < ENNReal.ofReal q ↔ p < q
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: p q : ℝ
hp : 0 ≤ p
⊢ ↑p.toNNReal < ENNReal.ofReal q ↔ p < q

Tactic:
ENNReal.ofReal,

Goal state after:
p q : ℝ
hp : 0 ≤ p
⊢ ↑p.toNNReal < ↑q.toNNReal ↔ p < q
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case mk
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p q : NonarchAddGroupSeminorm E
toFun✝ : E → ℝ
map_zero'✝ : toFun✝ 0 = 0
add_le_max'✝¹ :
  ∀ (r s : E),
    { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun (r + s) ≤
      max ({ toFun := toFun✝, map_zero' := map_zero'✝ }.toFun r) ({ toFun := toFun✝, map_zero' := map_zero'✝ }.toFun s)
neg'✝¹ :
  ∀ (r : E),
    { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun (-r) = { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun r
toZeroHom✝ : ZeroHom E ℝ
add_le_max'✝ : ∀ (r s : E), toZeroHom✝.toFun (r + s) ≤ max (toZeroHom✝.toFun r) (toZeroHom✝.toFun s)
neg'✝ : ∀ (r : E), toZeroHom✝.toFun (-r) = toZeroHom✝.toFun r
h :
  (fun f ↦ f.toFun) { toFun := toFun✝, map_zero' := map_zero'✝, add_le_max' := add_le_max'✝¹, neg' := neg'✝¹ } =
    (fun f ↦ f.toFun) { toZeroHom := toZeroHom✝, add_le_max' := add_le_max'✝, neg' := neg'✝ }
⊢ { toFun := toFun✝, map_zero' := map_zero'✝, add_le_max' := add_le_max'✝¹, neg' := neg'✝¹ } =
    { toZeroHom := toZeroHom✝, add_le_max' := add_le_max'✝, neg' := neg'✝ }

Tactic:
;

Goal state after:
case mk
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p q : NonarchAddGroupSeminorm E
toFun✝ : E → ℝ
map_zero'✝ : toFun✝ 0 = 0
add_le_max'✝¹ :
  ∀ (r s : E),
    { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun (r + s) ≤
      max ({ toFun := toFun✝, map_zero' := map_zero'✝ }.toFun r) ({ toFun := toFun✝, map_zero' := map_zero'✝ }.toFun s)
neg'✝¹ :
  ∀ (r : E),
    { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun (-r) = { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun r
toZeroHom✝ : ZeroHom E ℝ
add_le_max'✝ : ∀ (r s : E), toZeroHom✝.toFun (r + s) ≤ max (toZeroHom✝.toFun r) (toZeroHom✝.toFun s)
neg'✝ : ∀ (r : E), toZeroHom✝.toFun (-r) = toZeroHom✝.toFun r
h :
  (fun f ↦ f.toFun) { toFun := toFun✝, map_zero' := map_zero'✝, add_le_max' := add_le_max'✝¹, neg' := neg'✝¹ } =
    (fun f ↦ f.toFun) { toZeroHom := toZeroHom✝, add_le_max' := add_le_max'✝, neg' := neg'✝ }
⊢ { toFun := toFun✝, map_zero' := map_zero'✝, add_le_max' := add_le_max'✝¹, neg' := neg'✝¹ } =
    { toZeroHom := toZeroHom✝, add_le_max' := add_le_max'✝, neg' := neg'✝ }
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p q : NonarchAddGroupSeminorm E
r s : E
⊢ 0 ≤ max 0 0

Tactic:
;

Goal state after:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p q : NonarchAddGroupSeminorm E
r s : E
⊢ 0 ≤ max 0 0
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p q : NonarchAddGroupSeminorm E
r s : E
⊢ 0 ≤ 0

Tactic:
;

Goal state after:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p q : NonarchAddGroupSeminorm E
r s : E
⊢ 0 ≤ 0
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : Group E
p q g : GroupNorm E
toFun✝ : E → ℝ
map_one'✝ : toFun✝ 1 = 0
mul_le'✝ : ∀ (x y : E), toFun✝ (x * y) ≤ toFun✝ x + toFun✝ y
inv'✝ : ∀ (x : E), toFun✝ x⁻¹ = toFun✝ x
eq_one_of_map_eq_zero'✝ :
  ∀ (x : E), { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝ }.toFun x = 0 → x = 1
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝,
        eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝,
      eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero'✝ } =
    g

Tactic:
;

Goal state after:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : Group E
p q g : GroupNorm E
toFun✝ : E → ℝ
map_one'✝ : toFun✝ 1 = 0
mul_le'✝ : ∀ (x y : E), toFun✝ (x * y) ≤ toFun✝ x + toFun✝ y
inv'✝ : ∀ (x : E), toFun✝ x⁻¹ = toFun✝ x
eq_one_of_map_eq_zero'✝ :
  ∀ (x : E), { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝ }.toFun x = 0 → x = 1
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝,
        eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝,
      eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero'✝ } =
    g
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case mk
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : Group E
p q : GroupNorm E
toFun✝ : E → ℝ
map_one'✝ : toFun✝ 1 = 0
mul_le'✝ : ∀ (x y : E), toFun✝ (x * y) ≤ toFun✝ x + toFun✝ y
inv'✝ : ∀ (x : E), toFun✝ x⁻¹ = toFun✝ x
eq_one_of_map_eq_zero'✝¹ :
  ∀ (x : E), { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝ }.toFun x = 0 → x = 1
toGroupSeminorm✝ : GroupSeminorm E
eq_one_of_map_eq_zero'✝ : ∀ (x : E), toGroupSeminorm✝.toFun x = 0 → x = 1
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝,
        eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero'✝¹ } =
    (fun f ↦ f.toFun) { toGroupSeminorm := toGroupSeminorm✝, eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero'✝ }
⊢ { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝,
      eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero'✝¹ } =
    { toGroupSeminorm := toGroupSeminorm✝, eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero'✝ }

Tactic:
;

Goal state after:
case mk
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : Group E
p q : GroupNorm E
toFun✝ : E → ℝ
map_one'✝ : toFun✝ 1 = 0
mul_le'✝ : ∀ (x y : E), toFun✝ (x * y) ≤ toFun✝ x + toFun✝ y
inv'✝ : ∀ (x : E), toFun✝ x⁻¹ = toFun✝ x
eq_one_of_map_eq_zero'✝¹ :
  ∀ (x : E), { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝ }.toFun x = 0 → x = 1
toGroupSeminorm✝ : GroupSeminorm E
eq_one_of_map_eq_zero'✝ : ∀ (x : E), toGroupSeminorm✝.toFun x = 0 → x = 1
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝,
        eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero'✝¹ } =
    (fun f ↦ f.toFun) { toGroupSeminorm := toGroupSeminorm✝, eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero'✝ }
⊢ { toFun := toFun✝, map_one' := map_one'✝, mul_le' := mul_le'✝, inv' := inv'✝,
      eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero'✝¹ } =
    { toGroupSeminorm := toGroupSeminorm✝, eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero'✝ }
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p q g : NonarchAddGroupNorm E
toFun✝ : E → ℝ
map_zero'✝ : toFun✝ 0 = 0
add_le_max'✝ :
  ∀ (r s : E),
    { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun (r + s) ≤
      max ({ toFun := toFun✝, map_zero' := map_zero'✝ }.toFun r) ({ toFun := toFun✝, map_zero' := map_zero'✝ }.toFun s)
neg'✝ :
  ∀ (r : E),
    { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun (-r) = { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun r
eq_zero_of_map_eq_zero'✝ :
  ∀ (x : E),
    { toFun := toFun✝, map_zero' := map_zero'✝, add_le_max' := add_le_max'✝, neg' := neg'✝ }.toFun x = 0 → x = 0
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝, map_zero' := map_zero'✝, add_le_max' := add_le_max'✝, neg' := neg'✝,
        eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_zero' := map_zero'✝, add_le_max' := add_le_max'✝, neg' := neg'✝,
      eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ } =
    g

Tactic:
;

Goal state after:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p q g : NonarchAddGroupNorm E
toFun✝ : E → ℝ
map_zero'✝ : toFun✝ 0 = 0
add_le_max'✝ :
  ∀ (r s : E),
    { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun (r + s) ≤
      max ({ toFun := toFun✝, map_zero' := map_zero'✝ }.toFun r) ({ toFun := toFun✝, map_zero' := map_zero'✝ }.toFun s)
neg'✝ :
  ∀ (r : E),
    { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun (-r) = { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun r
eq_zero_of_map_eq_zero'✝ :
  ∀ (x : E),
    { toFun := toFun✝, map_zero' := map_zero'✝, add_le_max' := add_le_max'✝, neg' := neg'✝ }.toFun x = 0 → x = 0
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝, map_zero' := map_zero'✝, add_le_max' := add_le_max'✝, neg' := neg'✝,
        eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_zero' := map_zero'✝, add_le_max' := add_le_max'✝, neg' := neg'✝,
      eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ } =
    g