mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: S : Type u_1
inst✝⁵ : CommRing S
q : Ideal S
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R S
inst✝² : q.IsPrime
inst✝¹ : Algebra.EssFiniteType R S
inst✝ : Algebra.IsUnramifiedAt R q
p : Ideal R := under R q
Rp : Type u_2 := Localization.AtPrime p
Sq : Type u_1 := Localization.AtPrime q
this✝ : Algebra Rp Sq := Localization.AtPrime.algebraOfLiesOver p q
this : Algebra.EssFiniteType Rp Sq
⊢ IsCoatom (map (algebraMap R (Localization.AtPrime q)) (under R q))

Tactic:
← Ideal.isMaximal_def,

Goal state after:
S : Type u_1
inst✝⁵ : CommRing S
q : Ideal S
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R S
inst✝² : q.IsPrime
inst✝¹ : Algebra.EssFiniteType R S
inst✝ : Algebra.IsUnramifiedAt R q
p : Ideal R := under R q
Rp : Type u_2 := Localization.AtPrime p
Sq : Type u_1 := Localization.AtPrime q
this✝ : Algebra Rp Sq := Localization.AtPrime.algebraOfLiesOver p q
this : Algebra.EssFiniteType Rp Sq
⊢ (map (algebraMap R (Localization.AtPrime q)) (under R q)).IsMaximal
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: S : Type u_1
inst✝⁶ : CommRing S
q : Ideal S
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
inst✝³ : q.IsPrime
inst✝² : Algebra.EssFiniteType R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : PerfectField (under R q).ResidueField
h : IsCoatom (map (algebraMap R (Localization.AtPrime q)) (under R q))
⊢ Algebra.IsUnramifiedAt R q

Tactic:
← Ideal.isMaximal_def,

Goal state after:
S : Type u_1
inst✝⁶ : CommRing S
q : Ideal S
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
inst✝³ : q.IsPrime
inst✝² : Algebra.EssFiniteType R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : PerfectField (under R q).ResidueField
h : (map (algebraMap R (Localization.AtPrime q)) (under R q)).IsMaximal
⊢ Algebra.IsUnramifiedAt R q
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: case neg.hq
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : ¬q.IsPrime
⊢ ¬q.IsPrime

pp: case neg.hq
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : ¬q.IsPrime
⊢ ¬(g • q).IsPrime

Tactic:
<;>

Goal state after:
case neg.hq
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : ¬q.IsPrime
⊢ ¬q.IsPrime

case neg.hq
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : ¬q.IsPrime
⊢ ¬(g • q).IsPrime
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
x : M
⊢ x ∈ primaryComponent M I ↔ ∃ n, x ∈ torsionBySet A M ↑(I ^ n)

Tactic:
simp only [primaryComponent, mem_torsionBySet_iff, SetLike.coe_sort_coe, Subtype.forall]

Goal state after:
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
x : M
⊢ x ∈ ⨆ i, torsionBySet A M ↑(I ^ i) ↔ ∃ n, ∀ a ∈ I ^ n, a • x = 0
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: case pos
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h✝ : IsTorsion A M
x✝ : M
a : A
ha : a ∈ A⁰
hmem : x✝ ∈ torsionBySet A M ↑(⨅ i, i.maxPowDividing (span {a}))
ha0 : span {a} ≠ ⊥
this : Fintype ↑(mulSupport fun v ↦ v.maxPowDividing (span {a})) := Finite.fintype ⋯
S : Finset (HeightOneSpectrum A) := (mulSupport fun v ↦ v.maxPowDividing (span {a})).toFinset
x : A
h : ∀ i ∈ S, x ∈ i.maxPowDividing (span {a})
i : HeightOneSpectrum A
htop : i.maxPowDividing (span {a}) = ⊤
⊢ x ∈ i.maxPowDividing (span {a})

pp: case neg
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h✝ : IsTorsion A M
x✝ : M
a : A
ha : a ∈ A⁰
hmem : x✝ ∈ torsionBySet A M ↑(⨅ i, i.maxPowDividing (span {a}))
ha0 : span {a} ≠ ⊥
this : Fintype ↑(mulSupport fun v ↦ v.maxPowDividing (span {a})) := Finite.fintype ⋯
S : Finset (HeightOneSpectrum A) := (mulSupport fun v ↦ v.maxPowDividing (span {a})).toFinset
x : A
h : ∀ i ∈ S, x ∈ i.maxPowDividing (span {a})
i : HeightOneSpectrum A
htop : ¬i.maxPowDividing (span {a}) = ⊤
⊢ x ∈ i.maxPowDividing (span {a})

Tactic:
<;>

Goal state after:
case pos
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h✝ : IsTorsion A M
x✝ : M
a : A
ha : a ∈ A⁰
hmem : x✝ ∈ torsionBySet A M ↑(⨅ i, i.maxPowDividing (span {a}))
ha0 : span {a} ≠ ⊥
this : Fintype ↑(mulSupport fun v ↦ v.maxPowDividing (span {a})) := Finite.fintype ⋯
S : Finset (HeightOneSpectrum A) := (mulSupport fun v ↦ v.maxPowDividing (span {a})).toFinset
x : A
h : ∀ i ∈ S, x ∈ i.maxPowDividing (span {a})
i : HeightOneSpectrum A
htop : i.maxPowDividing (span {a}) = ⊤
⊢ x ∈ i.maxPowDividing (span {a})

case neg
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h✝ : IsTorsion A M
x✝ : M
a : A
ha : a ∈ A⁰
hmem : x✝ ∈ torsionBySet A M ↑(⨅ i, i.maxPowDividing (span {a}))
ha0 : span {a} ≠ ⊥
this : Fintype ↑(mulSupport fun v ↦ v.maxPowDividing (span {a})) := Finite.fintype ⋯
S : Finset (HeightOneSpectrum A) := (mulSupport fun v ↦ v.maxPowDividing (span {a})).toFinset
x : A
h : ∀ i ∈ S, x ∈ i.maxPowDividing (span {a})
i : HeightOneSpectrum A
htop : ¬i.maxPowDividing (span {a}) = ⊤
⊢ x ∈ i.maxPowDividing (span {a})
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 ∈ s.powerset, (-1) ^ #t • if ht : t.Nonempty then ∑ a ∈ t.inf' ht S, f a else ∑ a ∈ s.biUnion S, f a) =
    ∑ a ∈ s.biUnion S, (∏ i ∈ s, (1 - (↑(S i)).indicator 1 a)) • f a

Tactic:
simp only [Int.reduceNeg, prod_sub, sum_comm (s := s.biUnion S), sum_smul, mul_assoc]
      congr! with t
      split_ifs with ht
      · obtain ⟨i, hi⟩ := ht
        simp only [prod_const_one, prod_indicator_apply]
        simp only [smul_sum, Set.indicator, Set.mem_iInter, mem_coe, Pi.one_apply, mul_ite, mul_one,
          mul_zero, ite_smul, zero_smul, sum_ite, not_forall, sum_const_zero, add_zero]
        congr
        aesop
      · obtain rfl := not_nonempty_iff_eq_empty.1 ht
        simp

Goal state after:
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
⊢ ∑ a ∈ s.biUnion S, (∏ i ∈ s, (1 - (↑(S i)).indicator 1 a)) • f a =
    ∑ a ∈ s.biUnion S, (∏ i ∈ s, ((↑(s.biUnion S)).indicator 1 a - (↑(S i)).indicator 1 a)) • f a

Tactic:
congr! with t; rw [Set.indicator_of_mem ‹_›, Pi.one_apply]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: case inl
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
S : ι → Finset α
f : α → G
⊢ ∑ a ∈ ∅.biUnion S, (∏ i ∈ ∅, ((↑(∅.biUnion S)).indicator 1 a - (↑(S i)).indicator 1 a)) • f a = 0

pp: case inr
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
hs : s.Nonempty
⊢ ∑ a ∈ s.biUnion S, (∏ i ∈ s, ((↑(s.biUnion S)).indicator 1 a - (↑(S i)).indicator 1 a)) • f a = 0

Tactic:
<;>

Goal state after:
case inl
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
S : ι → Finset α
f : α → G
⊢ ∑ a ∈ ∅.biUnion S, (∏ i ∈ ∅, ((↑(∅.biUnion S)).indicator 1 a - (↑(S i)).indicator 1 a)) • f a = 0

case inr
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
hs : s.Nonempty
⊢ ∑ a ∈ s.biUnion S, (∏ i ∈ s, ((↑(s.biUnion S)).indicator 1 a - (↑(S i)).indicator 1 a)) • f a = 0
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case mp
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
⊢ (∀ (ε : ℝ), 0 < ε → sInf s < a + ε) → ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε

pp: case mpr
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
⊢ (∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε) → ∀ (ε : ℝ), 0 < ε → sInf s < a + ε

Tactic:
<;>

Goal state after:
case mp
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
⊢ (∀ (ε : ℝ), 0 < ε → sInf s < a + ε) → ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε

case mpr
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
⊢ (∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε) → ∀ (ε : ℝ), 0 < ε → sInf s < a + ε
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ι : Sort u_2
s : ι → ℝ≥0
⊢ ↑(⨅ i, s i) = ⨅ i, ↑(s i)

Tactic:
rw [iInf, iInf, coe_sInf, ← Set.range_comp]; rfl

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

Goal state before:
pp: case pos
r p : ℝ≥0
h : 1 ≤ r * p
h✝ : r = 0
⊢ r⁻¹ ≤ p

pp: case neg
r p : ℝ≥0
h : 1 ≤ r * p
h✝ : ¬r = 0
⊢ r⁻¹ ≤ p

Tactic:
<;>

Goal state after:
case pos
r p : ℝ≥0
h : 1 ≤ r * p
h✝ : r = 0
⊢ r⁻¹ ≤ p

case neg
r p : ℝ≥0
h : 1 ≤ r * p
h✝ : ¬r = 0
⊢ r⁻¹ ≤ p
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: a : ℝ
ha : 1 < a
⊢ ∃ k, 0 < k ∧ 1 / ↑k + 1 < a

Tactic:
contrapose! ha
    refine le_of_forall_lt_rat_imp_le ?_
    intro q hq
    refine (ha q.den (by positivity)).trans ?_
    rw [← le_sub_iff_add_le, div_le_iff₀ (by positivity), sub_mul, one_mul]
    norm_cast at hq ⊢
    rw [← q.num_div_den, one_lt_div (by positivity)] at hq
    rw [q.mul_den_eq_num]
    norm_cast at hq ⊢
    lia

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : R
h : ∀ (i : HeightOneSpectrum R), ¬i.maxPowDividing I = ⊤ → x ∈ i.maxPowDividing I
i : HeightOneSpectrum R
h✝ : i.maxPowDividing I = ⊤
⊢ x ∈ i.maxPowDividing I

pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : R
h : ∀ (i : HeightOneSpectrum R), ¬i.maxPowDividing I = ⊤ → x ∈ i.maxPowDividing I
i : HeightOneSpectrum R
h✝ : ¬i.maxPowDividing I = ⊤
⊢ x ∈ i.maxPowDividing I

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : R
h : ∀ (i : HeightOneSpectrum R), ¬i.maxPowDividing I = ⊤ → x ∈ i.maxPowDividing I
i : HeightOneSpectrum R
h✝ : i.maxPowDividing I = ⊤
⊢ x ∈ i.maxPowDividing I

case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : R
h : ∀ (i : HeightOneSpectrum R), ¬i.maxPowDividing I = ⊤ → x ∈ i.maxPowDividing I
i : HeightOneSpectrum R
h✝ : ¬i.maxPowDividing I = ⊤
⊢ x ∈ i.maxPowDividing I
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: case top
⊢ |∞.toReal| = ∞.toReal

pp: case coe
x✝ : ℝ≥0
⊢ |(↑x✝).toReal| = (↑x✝).toReal

Tactic:
<;>

Goal state after:
case top
⊢ |∞.toReal| = ∞.toReal

case coe
x✝ : ℝ≥0
⊢ |(↑x✝).toReal| = (↑x✝).toReal
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case neg.refine_1
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ 1

pp: case neg.refine_2
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
⊢ 0 ≤ if y = 0 then 0 else 1

Tactic:
<;>

Goal state after:
case neg.refine_1
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ 1

case neg.refine_2
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
⊢ 0 ≤ if y = 0 then 0 else 1
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
h : a.toNNReal < b.toNNReal
⊢ a < b

Tactic:
rwa [← coe_toNNReal ha, ← coe_toNNReal hb, coe_lt_coe]

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

Goal state before:
pp: case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
h✝ : x + y = 0
⊢ 0 ≤ 1

pp: case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
h✝ : ¬x + y = 0
⊢ 1 ≤ 1

pp: case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
h✝ : y = 0
⊢ 0 ≤ 0

pp: case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
h✝ : ¬y = 0
⊢ 0 ≤ 1

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
h✝ : x + y = 0
⊢ 0 ≤ 1

case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
h✝ : ¬x + y = 0
⊢ 1 ≤ 1

case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
h✝ : y = 0
⊢ 0 ≤ 0

case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
h✝ : ¬y = 0
⊢ 0 ≤ 1
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: case top
a : ℝ≥0∞
⊢ 0 < ∞.toNNReal ↔ 0 < ∞ ∧ ∞ < ∞

pp: case coe
a : ℝ≥0∞
x✝ : ℝ≥0
⊢ 0 < (↑x✝).toNNReal ↔ 0 < ↑x✝ ∧ ↑x✝ < ∞

Tactic:
<;>

Goal state after:
case top
a : ℝ≥0∞
⊢ 0 < ∞.toNNReal ↔ 0 < ∞ ∧ ∞ < ∞

case coe
a : ℝ≥0∞
x✝ : ℝ≥0
⊢ 0 < (↑x✝).toNNReal ↔ 0 < ↑x✝ ∧ ↑x✝ < ∞
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case neg.refine_1
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
⊢ (if x * y = 1 then 0 else 1) ≤ 1

pp: case neg.refine_2
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
⊢ 0 ≤ if y = 1 then 0 else 1

Tactic:
<;>

Goal state after:
case neg.refine_1
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
⊢ (if x * y = 1 then 0 else 1) ≤ 1

case neg.refine_2
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
⊢ 0 ≤ if y = 1 then 0 else 1
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
h✝ : x * y = 1
⊢ 0 ≤ 1

pp: case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
h✝ : ¬x * y = 1
⊢ 1 ≤ 1

pp: case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
h✝ : y = 1
⊢ 0 ≤ 0

pp: case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
h✝ : ¬y = 1
⊢ 0 ≤ 1

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
h✝ : x * y = 1
⊢ 0 ≤ 1

case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
h✝ : ¬x * y = 1
⊢ 1 ≤ 1

case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
h✝ : y = 1
⊢ 0 ≤ 0

case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
h✝ : ¬y = 1
⊢ 0 ≤ 1
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
h✝¹ : x + y = 0
h✝ : y = 0
⊢ 0 ≤ max 1 0

pp: case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
h✝¹ : x + y = 0
h✝ : ¬y = 0
⊢ 0 ≤ max 1 1

pp: case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
h✝¹ : ¬x + y = 0
h✝ : y = 0
⊢ 1 ≤ max 1 0

pp: case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
h✝¹ : ¬x + y = 0
h✝ : ¬y = 0
⊢ 1 ≤ max 1 1

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
h✝¹ : x + y = 0
h✝ : y = 0
⊢ 0 ≤ max 1 0

case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
h✝¹ : x + y = 0
h✝ : ¬y = 0
⊢ 0 ≤ max 1 1

case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
h✝¹ : ¬x + y = 0
h✝ : y = 0
⊢ 1 ≤ max 1 0

case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
h✝¹ : ¬x + y = 0
h✝ : ¬y = 0
⊢ 1 ≤ max 1 1
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: case mp
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : ↑s
⊢ s.ordConnectedProj x = s.ordConnectedProj y → [[↑x, ↑y]] ⊆ s

pp: case mpr
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : ↑s
⊢ [[↑x, ↑y]] ⊆ s → s.ordConnectedProj x = s.ordConnectedProj y

Tactic:
<;>

Goal state after:
case mp
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : ↑s
⊢ s.ordConnectedProj x = s.ordConnectedProj y → [[↑x, ↑y]] ⊆ s

case mpr
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : ↑s
⊢ [[↑x, ↑y]] ⊆ s → s.ordConnectedProj x = s.ordConnectedProj y
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: x : ℝ≥0∞
⊢ ¬x ≠ ∞ ↔ x = ∞

Tactic:
Classical.not_not

Goal state after:
x : ℝ≥0∞
⊢ x = ∞ ↔ x = ∞
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case top
b : ℝ≥0∞
c : ℝ≥0
⊢ ∞ + ↑c - (b + ↑c) = ∞ - b

pp: case coe
b : ℝ≥0∞
c x✝ : ℝ≥0
⊢ ↑x✝ + ↑c - (b + ↑c) = ↑x✝ - b

Tactic:
<;>

Goal state after:
case top
b : ℝ≥0∞
c : ℝ≥0
⊢ ∞ + ↑c - (b + ↑c) = ∞ - b

case coe
b : ℝ≥0∞
c x✝ : ℝ≥0
⊢ ↑x✝ + ↑c - (b + ↑c) = ↑x✝ - b
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case top
b : ℝ≥0
⊢ (∞ - ↑b).toNNReal = ∞.toNNReal - (↑b).toNNReal

pp: case coe
b x✝ : ℝ≥0
⊢ (↑x✝ - ↑b).toNNReal = (↑x✝).toNNReal - (↑b).toNNReal

Tactic:
<;>

Goal state after:
case top
b : ℝ≥0
⊢ (∞ - ↑b).toNNReal = ∞.toNNReal - (↑b).toNNReal

case coe
b x✝ : ℝ≥0
⊢ (↑x✝ - ↑b).toNNReal = (↑x✝).toNNReal - (↑b).toNNReal
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case h₁
ι : Type u_2
inst✝¹ : Preorder ι
inst✝ : IsCodirectedOrder ι
f g : ι → ℝ≥0∞
hf : Monotone f
hg : Monotone g
i j _k : ι
x✝ : _k ≤ i ∧ _k ≤ j
hi : _k ≤ i
hj : _k ≤ j
⊢ f _k ≤ f i

pp: case h₂
ι : Type u_2
inst✝¹ : Preorder ι
inst✝ : IsCodirectedOrder ι
f g : ι → ℝ≥0∞
hf : Monotone f
hg : Monotone g
i j _k : ι
x✝ : _k ≤ i ∧ _k ≤ j
hi : _k ≤ i
hj : _k ≤ j
⊢ g _k ≤ g j

Tactic:
<;>

Goal state after:
case h₁
ι : Type u_2
inst✝¹ : Preorder ι
inst✝ : IsCodirectedOrder ι
f g : ι → ℝ≥0∞
hf : Monotone f
hg : Monotone g
i j _k : ι
x✝ : _k ≤ i ∧ _k ≤ j
hi : _k ≤ i
hj : _k ≤ j
⊢ f _k ≤ f i

case h₂
ι : Type u_2
inst✝¹ : Preorder ι
inst✝ : IsCodirectedOrder ι
f g : ι → ℝ≥0∞
hf : Monotone f
hg : Monotone g
i j _k : ι
x✝ : _k ≤ i ∧ _k ≤ j
hi : _k ≤ i
hj : _k ≤ j
⊢ g _k ≤ g j
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case bot
p : EReal → Prop
hr : p ⊥
⊢ p ⊥ ∨ p ⊤ ∨ ∃ r, p ↑r

pp: case coe
p : EReal → Prop
a✝ : ℝ
hr : p ↑a✝
⊢ p ⊥ ∨ p ⊤ ∨ ∃ r, p ↑r

pp: case top
p : EReal → Prop
hr : p ⊤
⊢ p ⊥ ∨ p ⊤ ∨ ∃ r, p ↑r

Tactic:
<;>

Goal state after:
case bot
p : EReal → Prop
hr : p ⊥
⊢ p ⊥ ∨ p ⊤ ∨ ∃ r, p ↑r

case coe
p : EReal → Prop
a✝ : ℝ
hr : p ↑a✝
⊢ p ⊥ ∨ p ⊤ ∨ ∃ r, p ↑r

case top
p : EReal → Prop
hr : p ⊤
⊢ p ⊥ ∨ p ⊤ ∨ ∃ r, p ↑r
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case inl
p : EReal → Prop
h : p ⊥
⊢ ∃ r, p r

pp: case inr.inl
p : EReal → Prop
h : p ⊤
⊢ ∃ r, p r

pp: case inr.inr
p : EReal → Prop
r : ℝ
hr : p ↑r
⊢ ∃ r, p r

Tactic:
<;>

Goal state after:
case inl
p : EReal → Prop
h : p ⊥
⊢ ∃ r, p r

case inr.inl
p : EReal → Prop
h : p ⊤
⊢ ∃ r, p r

case inr.inr
p : EReal → Prop
r : ℝ
hr : p ↑r
⊢ ∃ r, p r
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case bot
y : EReal
⊢ ⊥ * y = y * ⊥

pp: case coe
y : EReal
a✝ : ℝ
⊢ ↑a✝ * y = y * ↑a✝

pp: case top
y : EReal
⊢ ⊤ * y = y * ⊤

Tactic:
<;>

Goal state after:
case bot
y : EReal
⊢ ⊥ * y = y * ⊥

case coe
y : EReal
a✝ : ℝ
⊢ ↑a✝ * y = y * ↑a✝

case top
y : EReal
⊢ ⊤ * y = y * ⊤
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case bot.bot
⊢ ⊥ * ⊥ = ⊥ * ⊥

pp: case bot.coe
a✝ : ℝ
⊢ ⊥ * ↑a✝ = ↑a✝ * ⊥

pp: case bot.top
⊢ ⊥ * ⊤ = ⊤ * ⊥

pp: case coe.bot
a✝ : ℝ
⊢ ↑a✝ * ⊥ = ⊥ * ↑a✝

pp: case coe.coe
a✝¹ a✝ : ℝ
⊢ ↑a✝¹ * ↑a✝ = ↑a✝ * ↑a✝¹

pp: case coe.top
a✝ : ℝ
⊢ ↑a✝ * ⊤ = ⊤ * ↑a✝

pp: case top.bot
⊢ ⊤ * ⊥ = ⊥ * ⊤

pp: case top.coe
a✝ : ℝ
⊢ ⊤ * ↑a✝ = ↑a✝ * ⊤

pp: case top.top
⊢ ⊤ * ⊤ = ⊤ * ⊤

Tactic:
<;>

Goal state after:
case bot.bot
⊢ ⊥ * ⊥ = ⊥ * ⊥

case bot.coe
a✝ : ℝ
⊢ ⊥ * ↑a✝ = ↑a✝ * ⊥

case bot.top
⊢ ⊥ * ⊤ = ⊤ * ⊥

case coe.bot
a✝ : ℝ
⊢ ↑a✝ * ⊥ = ⊥ * ↑a✝

case coe.coe
a✝¹ a✝ : ℝ
⊢ ↑a✝¹ * ↑a✝ = ↑a✝ * ↑a✝¹

case coe.top
a✝ : ℝ
⊢ ↑a✝ * ⊤ = ⊤ * ↑a✝

case top.bot
⊢ ⊤ * ⊥ = ⊥ * ⊤

case top.coe
a✝ : ℝ
⊢ ⊤ * ↑a✝ = ↑a✝ * ⊤

case top.top
⊢ ⊤ * ⊤ = ⊤ * ⊤