harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem hausdorffMeasure_le_one_of_subsingleton {s : Set X} (hs : s.Subsingleton) {d : ℝ}
    (hd : 0 ≤ d) : μH[d] s ≤ 1

Proof state:
case inr.intro.inr
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
hs : s.Subsingleton
d : ℝ
hd : 0 ≤ d
x : X
hx : x ∈ s
dpos : 0 < d
this : NoAtoms μH[d]
⊢ μH[d] {x} ≤ 1

Tactic:
simp only [zero_le, measure_singleton]

Result:
no goals

Proof state:
case inr.intro.inr
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
hs : s.Subsingleton
d : ℝ
hd : 0 ≤ d
x : X
hx : x ∈ s
dpos : 0 < d
⊢ μH[d] {x} ≤ 1

Tactic:
haveI := noAtoms_hausdorff X dpos

Result:
case inr.intro.inr
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
hs : s.Subsingleton
d : ℝ
hd : 0 ≤ d
x : X
hx : x ∈ s
dpos : 0 < d
this : NoAtoms μH[d]
⊢ μH[d] {x} ≤ 1

Proof state:
case inr.intro
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
hs : s.Subsingleton
d : ℝ
hd : 0 ≤ d
x : X
hx : x ∈ s
⊢ μH[d] s ≤ 1

Tactic:
rw [(subsingleton_iff_singleton hx).1 hs]

Result:
case inr.intro
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
hs : s.Subsingleton
d : ℝ
hd : 0 ≤ d
x : X
hx : x ∈ s
⊢ μH[d] {x} ≤ 1

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
hs : s.Subsingleton
d : ℝ
hd : 0 ≤ d
⊢ μH[d] s ≤ 1

Tactic:
rcases eq_empty_or_nonempty s with (rfl | ⟨x, hx⟩)

Result:
case inl
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d : ℝ
hd : 0 ≤ d
hs : ∅.Subsingleton
⊢ μH[d] ∅ ≤ 1

case inr.intro
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
hs : s.Subsingleton
d : ℝ
hd : 0 ≤ d
x : X
hx : x ∈ s
⊢ μH[d] s ≤ 1

Proof state:
case inr.intro
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
hs : s.Subsingleton
d : ℝ
hd : 0 ≤ d
x : X
hx : x ∈ s
⊢ μH[d] {x} ≤ 1

Tactic:
rcases eq_or_lt_of_le hd with (rfl | dpos)

Result:
case inr.intro.inl
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
hs : s.Subsingleton
x : X
hx : x ∈ s
hd : 0 ≤ 0
⊢ μH[0] {x} ≤ 1

case inr.intro.inr
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
hs : s.Subsingleton
d : ℝ
hd : 0 ≤ d
x : X
hx : x ∈ s
dpos : 0 < d
⊢ μH[d] {x} ≤ 1

Proof state:
case inl
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d : ℝ
hd : 0 ≤ d
hs : ∅.Subsingleton
⊢ μH[d] ∅ ≤ 1

Tactic:
simp only [measure_empty, zero_le]

Result:
no goals

Proof state:
case inr.intro.inl
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
hs : s.Subsingleton
x : X
hx : x ∈ s
hd : 0 ≤ 0
⊢ μH[0] {x} ≤ 1

Tactic:
simp only [le_refl, hausdorffMeasure_zero_singleton]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma coe_zero : (↑(0 : Cocycle F G n) : Cochain F G n) = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
⊢ ↑0 = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/GroupTheory/Perm/Sign.lean
theorem sign_prodCongrLeft (σ : α → Perm β) : sign (prodCongrLeft σ) = ∏ k, sign (σ k)

Proof state:
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
⊢ ∀ (x : β × α), (prodComm β α) ((prodCongrLeft σ) x) = (prodCongrRight σ) ((prodComm β α) x)

Tactic:
rintro ⟨b, α⟩

Result:
case mk
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : Fintype α✝
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α✝ → Perm β
b : β
α : α✝
⊢ (prodComm β α✝) ((prodCongrLeft σ) (b, α)) = (prodCongrRight σ) ((prodComm β α✝) (b, α))

Proof state:
case mk
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : Fintype α✝
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α✝ → Perm β
b : β
α : α✝
⊢ (prodComm β α✝) ((prodCongrLeft σ) (b, α)) = (prodCongrRight σ) ((prodComm β α✝) (b, α))

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
⊢ sign (prodCongrLeft σ) = ∏ k : α, sign (σ k)

Tactic:
refine (sign_eq_sign_of_equiv _ _ (prodComm β α) ?_).trans (sign_prodCongrRight σ)

Result:
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
⊢ ∀ (x : β × α), (prodComm β α) ((prodCongrLeft σ) x) = (prodCongrRight σ) ((prodComm β α) x)
-- Mathlib/Topology/Compactness/Compact.lean
theorem IsCompact.union (hs : IsCompact s) (ht : IsCompact t) : IsCompact (s ∪ t)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (s ∪ t)

Tactic:
rw [union_eq_iUnion]

Result:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (⋃ b, bif b then s else t)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (⋃ b, bif b then s else t)

Tactic:
exact isCompact_iUnion fun b => by cases b <;> assumption

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsCompact t
b : Bool
⊢ IsCompact (bif b then s else t)

Tactic:
cases b <;> assumption

Result:
no goals
-- Mathlib/Geometry/Euclidean/Basic.lean
theorem reflection_symm (s : AffineSubspace ℝ P) [Nonempty s]
    [HasOrthogonalProjection s.direction] : (reflection s).symm = reflection s

Proof state:
case h
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
x✝ : P
⊢ (reflection s) ((reflection s).symm x✝) = (reflection s) ((reflection s) x✝)

Tactic:
simp

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
⊢ (reflection s).symm = reflection s

Tactic:
ext

Result:
case h
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
x✝ : P
⊢ (reflection s).symm x✝ = (reflection s) x✝

Proof state:
case h
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
x✝ : P
⊢ (reflection s).symm x✝ = (reflection s) x✝

Tactic:
rw [← (reflection s).injective.eq_iff]

Result:
case h
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
x✝ : P
⊢ (reflection s) ((reflection s).symm x✝) = (reflection s) ((reflection s) x✝)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/String/Basic.lean
theorem zero_addString_byteIdx (s : String) : ((0 : Pos) + s).byteIdx = s.utf8ByteSize

Proof state:
s : String
⊢ (0 + s).byteIdx = s.utf8ByteSize

Tactic:
simp only [addString_byteIdx, byteIdx_zero, Nat.zero_add]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem blsub_le_iff {o : Ordinal.{u}} {f : ∀ a < o, Ordinal.{max u v}} {a} :
    blsub.{_, v} o f ≤ a ↔ ∀ i h, f i h < a

Proof state:
case h.e'_2.h.a
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
a : Ordinal.{max u v}
a✝ : Ordinal.{u}
⊢ (∀ (h : a✝ < o), f a✝ h < a) ↔ ∀ (h : a✝ < o), succ (f a✝ h) ≤ a

Tactic:
simp_rw [succ_le_iff]

Result:
no goals

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
a : Ordinal.{max u v}
⊢ o.blsub f ≤ a ↔ ∀ (i : Ordinal.{u}) (h : i < o), f i h < a

Tactic:
convert bsup_le_iff.{_, v} (f := fun a ha => succ (f a ha)) (a := a) using 2

Result:
case h.e'_2.h.a
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
a : Ordinal.{max u v}
a✝ : Ordinal.{u}
⊢ (∀ (h : a✝ < o), f a✝ h < a) ↔ ∀ (h : a✝ < o), succ (f a✝ h) ≤ a
-- Mathlib/RingTheory/PowerSeries/Trunc.lean
theorem trunc_trunc_mul_trunc {n} (f g : R⟦X⟧) :
    trunc n (trunc n f * trunc n g : R⟦X⟧) = trunc n (f * g)

Proof state:
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
⊢ trunc n (↑(trunc n f) * ↑(trunc n g)) = trunc n (f * g)

Tactic:
rw [trunc_trunc_mul, trunc_mul_trunc]

Result:
no goals
-- Mathlib/NumberTheory/ADEInequality.lean
theorem Admissible.one_lt_sumInv {pqr : Multiset ℕ+} : Admissible pqr → 1 < sumInv pqr

Proof state:
case inr.inl.intro
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
⊢ 1 < sumInv pqr

Tactic:
rw [← H, D', sumInv_pqr]

Result:
case inr.inl.intro
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
⊢ 1 < (↑↑2)⁻¹ + (↑↑2)⁻¹ + (↑↑n)⁻¹

Proof state:
pqr : Multiset ℕ+
⊢ Admissible pqr → 1 < sumInv pqr

Tactic:
rw [Admissible]

Result:
pqr : Multiset ℕ+
⊢ (∃ q r, A' q r = pqr) ∨ (∃ r, D' r = pqr) ∨ E' 3 = pqr ∨ E' 4 = pqr ∨ E' 5 = pqr → 1 < sumInv pqr

Proof state:
case inr.inr.inr.inr
pqr : Multiset ℕ+
H : E' 5 = pqr
⊢ 1 < sumInv pqr

Tactic:
rw [← H, E', sumInv_pqr]

Result:
case inr.inr.inr.inr
pqr : Multiset ℕ+
H : E' 5 = pqr
⊢ 1 < (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑5)⁻¹

Proof state:
case inl.intro.intro
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 0 < (↑↑p')⁻¹ + (↑↑q')⁻¹

Tactic:
apply add_pos <;> simp only [PNat.pos, Nat.cast_pos, inv_pos]

Result:
no goals

Proof state:
case inl.intro.intro
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 1 < sumInv pqr

Tactic:
rw [← H, A', sumInv_pqr, add_assoc]

Result:
case inl.intro.intro
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 1 < (↑↑1)⁻¹ + ((↑↑p')⁻¹ + (↑↑q')⁻¹)

Proof state:
case inr.inl.intro
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
⊢ 1 < (↑↑2)⁻¹ + (↑↑2)⁻¹ + (↑↑n)⁻¹

Tactic:
norm_num

Result:
no goals

Proof state:
case inr.inr.inl
pqr : Multiset ℕ+
H : E' 3 = pqr
⊢ 1 < sumInv pqr

case inr.inr.inr.inl
pqr : Multiset ℕ+
H : E' 4 = pqr
⊢ 1 < sumInv pqr

case inr.inr.inr.inr
pqr : Multiset ℕ+
H : E' 5 = pqr
⊢ 1 < sumInv pqr

Tactic:
all_goals
  rw [← H, E', sumInv_pqr]
  norm_num

Result:
no goals

Proof state:
pqr : Multiset ℕ+
⊢ (∃ q r, A' q r = pqr) ∨ (∃ r, D' r = pqr) ∨ E' 3 = pqr ∨ E' 4 = pqr ∨ E' 5 = pqr → 1 < sumInv pqr

Tactic:
rintro (⟨p', q', H⟩ | ⟨n, H⟩ | H | H | H)

Result:
case inl.intro.intro
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 1 < sumInv pqr

case inr.inl.intro
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
⊢ 1 < sumInv pqr

case inr.inr.inl
pqr : Multiset ℕ+
H : E' 3 = pqr
⊢ 1 < sumInv pqr

case inr.inr.inr.inl
pqr : Multiset ℕ+
H : E' 4 = pqr
⊢ 1 < sumInv pqr

case inr.inr.inr.inr
pqr : Multiset ℕ+
H : E' 5 = pqr
⊢ 1 < sumInv pqr

Proof state:
case inl.intro.intro
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 1 < (↑↑1)⁻¹ + ((↑↑p')⁻¹ + (↑↑q')⁻¹)

Tactic:
simp only [lt_add_iff_pos_right, PNat.one_coe, inv_one, Nat.cast_one]

Result:
case inl.intro.intro
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 0 < (↑↑p')⁻¹ + (↑↑q')⁻¹

Proof state:
case inr.inr.inr.inr
pqr : Multiset ℕ+
H : E' 5 = pqr
⊢ 1 < (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑5)⁻¹

Tactic:
norm_num

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Coloring.lean
theorem chromaticNumber_pos [Nonempty V] {n : ℕ} (hc : G.Colorable n) : 0 < G.chromaticNumber

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Nonempty V
n : ℕ
hc : G.Colorable n
m : ℕ
hm : m ∈ {n | G.Colorable n}
h' : m < Nat.succ 0
⊢ False

Tactic:
obtain ⟨i, hi⟩ := hm.some (Classical.arbitrary V)

Result:
case mk
V : Type u
G : SimpleGraph V
inst✝ : Nonempty V
n : ℕ
hc : G.Colorable n
m : ℕ
hm : m ∈ {n | G.Colorable n}
h' : m < Nat.succ 0
i : ℕ
hi : i < m
⊢ False

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Nonempty V
n : ℕ
hc : G.Colorable n
⊢ 0 < sInf {n' | G.Colorable n'}

Tactic:
apply le_csInf (colorable_set_nonempty_of_colorable hc)

Result:
V : Type u
G : SimpleGraph V
inst✝ : Nonempty V
n : ℕ
hc : G.Colorable n
⊢ ∀ b ∈ {n | G.Colorable n}, Nat.succ 0 ≤ b

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Nonempty V
n : ℕ
hc : G.Colorable n
m : ℕ
hm : m ∈ {n | G.Colorable n}
h' : ¬Nat.succ 0 ≤ m
⊢ False

Tactic:
simp only [not_le] at h'

Result:
V : Type u
G : SimpleGraph V
inst✝ : Nonempty V
n : ℕ
hc : G.Colorable n
m : ℕ
hm : m ∈ {n | G.Colorable n}
h' : m < Nat.succ 0
⊢ False

Proof state:
case mk
V : Type u
G : SimpleGraph V
inst✝ : Nonempty V
n : ℕ
hc : G.Colorable n
m : ℕ
hm : m ∈ {n | G.Colorable n}
h' : m < Nat.succ 0
i : ℕ
hi : i < m
⊢ False

Tactic:
have h₁ : i < 0 := lt_of_lt_of_le hi (Nat.le_of_lt_succ h')

Result:
case mk
V : Type u
G : SimpleGraph V
inst✝ : Nonempty V
n : ℕ
hc : G.Colorable n
m : ℕ
hm : m ∈ {n | G.Colorable n}
h' : m < Nat.succ 0
i : ℕ
hi : i < m
h₁ : i < 0
⊢ False

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Nonempty V
n : ℕ
hc : G.Colorable n
⊢ ∀ b ∈ {n | G.Colorable n}, Nat.succ 0 ≤ b

Tactic:
intro m hm

Result:
V : Type u
G : SimpleGraph V
inst✝ : Nonempty V
n : ℕ
hc : G.Colorable n
m : ℕ
hm : m ∈ {n | G.Colorable n}
⊢ Nat.succ 0 ≤ m

Proof state:
case mk
V : Type u
G : SimpleGraph V
inst✝ : Nonempty V
n : ℕ
hc : G.Colorable n
m : ℕ
hm : m ∈ {n | G.Colorable n}
h' : m < Nat.succ 0
i : ℕ
hi : i < m
h₁ : i < 0
⊢ False

Tactic:
exact Nat.not_lt_zero _ h₁

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Nonempty V
n : ℕ
hc : G.Colorable n
m : ℕ
hm : m ∈ {n | G.Colorable n}
⊢ Nat.succ 0 ≤ m

Tactic:
by_contra h'

Result:
V : Type u
G : SimpleGraph V
inst✝ : Nonempty V
n : ℕ
hc : G.Colorable n
m : ℕ
hm : m ∈ {n | G.Colorable n}
h' : ¬Nat.succ 0 ≤ m
⊢ False

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Nonempty V
n : ℕ
hc : G.Colorable n
⊢ 0 < G.chromaticNumber

Tactic:
rw [hc.chromaticNumber_eq_sInf, Nat.cast_pos]

Result:
V : Type u
G : SimpleGraph V
inst✝ : Nonempty V
n : ℕ
hc : G.Colorable n
⊢ 0 < sInf {n' | G.Colorable n'}
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem prev : ∀ {s}, Valid s → s.toString.1 = m₁ ++ c :: m₂ →
    s.prev ⟨utf8Len m₁ + c.utf8Size⟩ = ⟨utf8Len m₁⟩
  | _, h, e => by
    let ⟨l, m, r, h⟩ := h.validFor
    simp only [h.toString] at e; subst e; simp [h.prev]

Proof state:
m₁ : List Char
c : Char
m₂ : List Char
x✝ : Substring
h✝ : x✝.Valid
e : x✝.toString.data = m₁ ++ c :: m₂
l m r : List Char
h : ValidFor l m r x✝
⊢ x✝.prev { byteIdx := utf8Len m₁ + c.utf8Size } = { byteIdx := utf8Len m₁ }

Tactic:
simp only [h.toString] at e

Result:
m₁ : List Char
c : Char
m₂ : List Char
x✝ : Substring
h✝ : x✝.Valid
l m r : List Char
h : ValidFor l m r x✝
e : m = m₁ ++ c :: m₂
⊢ x✝.prev { byteIdx := utf8Len m₁ + c.utf8Size } = { byteIdx := utf8Len m₁ }

Proof state:
m₁ : List Char
c : Char
m₂ : List Char
x✝ : Substring
h✝ : x✝.Valid
l r : List Char
h : ValidFor l (m₁ ++ c :: m₂) r x✝
⊢ x✝.prev { byteIdx := utf8Len m₁ + c.utf8Size } = { byteIdx := utf8Len m₁ }

Tactic:
simp [h.prev]

Result:
no goals

Proof state:
m₁ : List Char
c : Char
m₂ : List Char
x✝ : Substring
h✝ : x✝.Valid
l m r : List Char
h : ValidFor l m r x✝
e : m = m₁ ++ c :: m₂
⊢ x✝.prev { byteIdx := utf8Len m₁ + c.utf8Size } = { byteIdx := utf8Len m₁ }

Tactic:
subst e

Result:
m₁ : List Char
c : Char
m₂ : List Char
x✝ : Substring
h✝ : x✝.Valid
l r : List Char
h : ValidFor l (m₁ ++ c :: m₂) r x✝
⊢ x✝.prev { byteIdx := utf8Len m₁ + c.utf8Size } = { byteIdx := utf8Len m₁ }

Proof state:
m₁ : List Char
c : Char
m₂ : List Char
x✝ : Substring
h : x✝.Valid
e : x✝.toString.data = m₁ ++ c :: m₂
⊢ x✝.prev { byteIdx := utf8Len m₁ + c.utf8Size } = { byteIdx := utf8Len m₁ }

Tactic:
let ⟨l, m, r, h⟩ := h.validFor

Result:
m₁ : List Char
c : Char
m₂ : List Char
x✝ : Substring
h✝ : x✝.Valid
e : x✝.toString.data = m₁ ++ c :: m₂
l m r : List Char
h : ValidFor l m r x✝
⊢ x✝.prev { byteIdx := utf8Len m₁ + c.utf8Size } = { byteIdx := utf8Len m₁ }
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem Monic.mul_natDegree_lt_iff (h : Monic p) {q : R[X]} :
    (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : q = 0
this : 0 < p.natDegree ↔ p.natDegree ≠ 0
⊢ (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0

Tactic:
simpa [hq, ← h.natDegree_eq_zero_iff_eq_one]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : ¬q = 0
⊢ (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0

Tactic:
simp [h.natDegree_mul', hq]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
⊢ (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0

Tactic:
by_cases hq : q = 0

Result:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : q = 0
⊢ (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : ¬q = 0
⊢ (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : q = 0
⊢ 0 < p.natDegree ↔ p.natDegree ≠ 0

Tactic:
exact ⟨fun h => h.ne', fun h => lt_of_le_of_ne (Nat.zero_le _) h.symm⟩

Result:
no goals

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : q = 0
⊢ (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0

Tactic:
suffices 0 < p.natDegree ↔ p.natDegree ≠ 0 by simpa [hq, ← h.natDegree_eq_zero_iff_eq_one]

Result:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : q = 0
⊢ 0 < p.natDegree ↔ p.natDegree ≠ 0
-- Mathlib/Topology/Algebra/Group/Basic.lean
/-- Let `A` and `B` be topological groups, and let `φ : A → B` be a continuous surjective group
homomorphism. Assume furthermore that `φ` is a quotient map (i.e., `V ⊆ B`
is open iff `φ⁻¹ V` is open). Then `φ` is an open quotient map, and in particular an open map. -/
@[to_additive "Let `A` and `B` be topological additive groups, and let `φ : A → B` be a continuous
surjective additive group homomorphism. Assume furthermore that `φ` is a quotient map (i.e., `V ⊆ B`
is open iff `φ⁻¹ V` is open). Then `φ` is an open quotient map, and in particular an open map."]
lemma MonoidHom.isOpenQuotientMap_of_isQuotientMap {A : Type*} [Group A]
    [TopologicalSpace A] [IsTopologicalGroup A] {B : Type*} [Group B] [TopologicalSpace B]
    {F : Type*} [FunLike F A B] [MonoidHomClass F A B] {φ : F}
    (hφ : IsQuotientMap φ) : IsOpenQuotientMap φ where
    surjective := hφ.surjective
    continuous := hφ.continuous
    isOpenMap

Proof state:
case h.mpr.intro.intro.intro.intro.intro.intro
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : IsTopologicalGroup A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen U
x k : A
hk : φ k = 1
hx : x ∈ (fun h => (fun x => x * k) ⁻¹' U) hk
⊢ x ∈ ⇑φ ⁻¹' (⇑φ '' U)

Tactic:
use x * k, hx

Result:
case right
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : IsTopologicalGroup A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen U
x k : A
hk : φ k = 1
hx : x ∈ (fun h => (fun x => x * k) ⁻¹' U) hk
⊢ φ (x * k) = φ x

Proof state:
case h.mpr
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : IsTopologicalGroup A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen U
x : A
⊢ x ∈ ⋃ k ∈ (↑φ).ker, (fun x => x * k) ⁻¹' U → x ∈ ⇑φ ⁻¹' (⇑φ '' U)

Tactic:
rintro ⟨_, ⟨k, rfl⟩, _, ⟨(hk : φ k = 1), rfl⟩, hx⟩

Result:
case h.mpr.intro.intro.intro.intro.intro.intro
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : IsTopologicalGroup A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen U
x k : A
hk : φ k = 1
hx : x ∈ (fun h => (fun x => x * k) ⁻¹' U) hk
⊢ x ∈ ⇑φ ⁻¹' (⇑φ '' U)

Proof state:
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : IsTopologicalGroup A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
⊢ IsOpenMap ⇑φ

Tactic:
intro U hU

Result:
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : IsTopologicalGroup A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen U
⊢ IsOpen (⇑φ '' U)
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
/-- The main proof of the lower bound part of the Akra-Bazzi theorem. The factor
`1 + ε n` does not change the asymptotic order, but is needed for the induction step to go
through. -/
lemma smoothingFn_mul_asympBound_isBigO_T :
    (fun (n : ℕ) => (1 + ε n) * asympBound g a b n) =O[atTop] T

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
h_b_floor : 0 < ⌊b' * ↑n₀⌋₊
h_smoothing_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < 1 + ε ↑y
h_smoothing_pos' : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < 1 + ε ↑y
h_asympBound_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < asympBound g a b y
h_asympBound_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < asympBound g a b (r i y)
h_asympBound_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < asympBound g a b y
n₀_pos : 0 < n₀
h_smoothing_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < 1 + ε ↑(r i y)
bound2 : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), b i ^ p a b * ↑y ^ p a b * (1 + ε ↑y) ≤ ↑(r i y) ^ p a b * (1 + ε ↑(r i y))
h_smoothingFn_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < 1 + ε ↑y
h_sumTransform : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), sumTransform (p a b) g (r i y) y ≤ c₁ * g ↑y
h_bi_le_r : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), b (min_bi b) / 2 * ↑y ≤ ↑(r i y)
h_exp : ∀ (y : ℕ), n₀ ≤ y → ⌈rexp 1⌉₊ ≤ y
h_base_nonempty : (Ico ⌊b (min_bi b) / 2 * ↑n₀⌋₊ n₀).Nonempty
base_min : ℝ := (Ico ⌊b' * ↑n₀⌋₊ n₀).inf' h_base_nonempty fun n => T n / ((1 + ε ↑n) * asympBound g a b n)
base_min_def : base_min = (Ico ⌊b' * ↑n₀⌋₊ n₀).inf' h_base_nonempty fun n => T n / ((1 + ε ↑n) * asympBound g a b n)
C : ℝ := (2 * c₁)⁻¹ ⊓ base_min
hC_pos : 0 < C
h_base : ∀ n ∈ Ico ⌊b' * ↑n₀⌋₊ n₀, C * ((1 + ε ↑n) * asympBound g a b n) ≤ T n
n : ℕ
h_ind : ∀ m < n, m ≥ n₀ → 0 < asympBound g a b m → 0 < 1 + ε ↑m → C * ((1 + ε ↑m) * asympBound g a b m) ≤ T m
hn : n ≥ n₀
h_asympBound_pos' : 0 < asympBound g a b n
h_one_sub_smoothingFn_pos' : 0 < 1 + ε ↑n
i : α
⊢ ⌊b' * ↑n₀⌋₊ ≤ r i n

Tactic:
exact_mod_cast calc ⌊b' * ↑n₀⌋₊ ≤ b' * n₀ := Nat.floor_le <| by positivity
                            _ ≤ b' * n := by gcongr
                            _ ≤ r i n := h_bi_le_r n hn i

Result:
no goals