harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
theorem cfc_tsub {A : Type*} [TopologicalSpace A] [Ring A] [PartialOrder A] [StarRing A]
    [StarOrderedRing A] [Algebra ℝ A] [IsTopologicalRing A] [T2Space A]
    [ContinuousFunctionalCalculus ℝ (IsSelfAdjoint : A → Prop)]
    [NonnegSpectrumClass ℝ A] (f g : ℝ≥0 → ℝ≥0)
    (a : A) (hfg : ∀ x ∈ spectrum ℝ≥0 a, g x ≤ f x) (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Ring A
inst✝⁷ : PartialOrder A
inst✝⁶ : StarRing A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : IsTopologicalRing A
inst✝² : T2Space A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ spectrum ℝ≥0 a, g x ≤ f x
ha : autoParam (0 ≤ a) _auto✝
hf : autoParam (ContinuousOn f (spectrum ℝ≥0 a)) _auto✝
hg : autoParam (ContinuousOn g (spectrum ℝ≥0 a)) _auto✝
ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
this : Set.EqOn (fun x => ↑(f x.toNNReal - g x.toNNReal)) (fun x => ↑(f x.toNNReal) - ↑(g x.toNNReal)) (spectrum ℝ a)
⊢ cfc (fun x => ↑(f x.toNNReal) - ↑(g x.toNNReal)) a =
    cfc (fun x => ↑(f x.toNNReal)) a - cfc (fun x => ↑(g x.toNNReal)) a

Tactic:
refine cfc_sub _ _ a ?_ ?_

Result:
case refine_1
A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Ring A
inst✝⁷ : PartialOrder A
inst✝⁶ : StarRing A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : IsTopologicalRing A
inst✝² : T2Space A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ spectrum ℝ≥0 a, g x ≤ f x
ha : autoParam (0 ≤ a) _auto✝
hf : autoParam (ContinuousOn f (spectrum ℝ≥0 a)) _auto✝
hg : autoParam (ContinuousOn g (spectrum ℝ≥0 a)) _auto✝
ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
this : Set.EqOn (fun x => ↑(f x.toNNReal - g x.toNNReal)) (fun x => ↑(f x.toNNReal) - ↑(g x.toNNReal)) (spectrum ℝ a)
⊢ ContinuousOn (fun x => ↑(f x.toNNReal)) (spectrum ℝ a)

case refine_2
A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Ring A
inst✝⁷ : PartialOrder A
inst✝⁶ : StarRing A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : IsTopologicalRing A
inst✝² : T2Space A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ spectrum ℝ≥0 a, g x ≤ f x
ha : autoParam (0 ≤ a) _auto✝
hf : autoParam (ContinuousOn f (spectrum ℝ≥0 a)) _auto✝
hg : autoParam (ContinuousOn g (spectrum ℝ≥0 a)) _auto✝
ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
this : Set.EqOn (fun x => ↑(f x.toNNReal - g x.toNNReal)) (fun x => ↑(f x.toNNReal) - ↑(g x.toNNReal)) (spectrum ℝ a)
⊢ ContinuousOn (fun x => ↑(g x.toNNReal)) (spectrum ℝ a)
-- Mathlib/MeasureTheory/Measure/Complex.lean
theorem absolutelyContinuous_ennreal_iff (c : ComplexMeasure α) (μ : VectorMeasure α ℝ≥0∞) :
    c ≪ᵥ μ ↔ ComplexMeasure.re c ≪ᵥ μ ∧ ComplexMeasure.im c ≪ᵥ μ

Proof state:
case mp.right
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ ↑(im c) i = 0

Tactic:
simp [h hi]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : re c ≪ᵥ μ ∧ im c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ ↑0 + ↑0 * Complex.I = 0

Tactic:
simp

Result:
no goals

Proof state:
case mpr
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : re c ≪ᵥ μ ∧ im c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ ↑0 + ↑0 * Complex.I = 0

α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : re c ≪ᵥ μ ∧ im c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ (↑c i).im = 0

α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : re c ≪ᵥ μ ∧ im c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ (↑c i).re = 0

Tactic:
exacts [by simp, h.2 hi, h.1 hi]

Result:
no goals

Proof state:
case mp.right
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : c ≪ᵥ μ
⊢ im c ≪ᵥ μ

Tactic:
intro i hi

Result:
case mp.right
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ ↑(im c) i = 0

Proof state:
case mpr
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : re c ≪ᵥ μ ∧ im c ≪ᵥ μ
⊢ c ≪ᵥ μ

Tactic:
intro i hi

Result:
case mpr
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : re c ≪ᵥ μ ∧ im c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ ↑c i = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
⊢ c ≪ᵥ μ ↔ re c ≪ᵥ μ ∧ im c ≪ᵥ μ

Tactic:
constructor <;> intro h

Result:
case mp
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : c ≪ᵥ μ
⊢ re c ≪ᵥ μ ∧ im c ≪ᵥ μ

case mpr
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : re c ≪ᵥ μ ∧ im c ≪ᵥ μ
⊢ c ≪ᵥ μ

Proof state:
case mpr
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : re c ≪ᵥ μ ∧ im c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ ↑c i = 0

Tactic:
rw [← Complex.re_add_im (c i), (_ : (c i).re = 0), (_ : (c i).im = 0)]

Result:
case mpr
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : re c ≪ᵥ μ ∧ im c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ ↑0 + ↑0 * Complex.I = 0

α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : re c ≪ᵥ μ ∧ im c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ (↑c i).im = 0

α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : re c ≪ᵥ μ ∧ im c ≪ᵥ μ
i : Set α
hi : ↑μ i = 0
⊢ (↑c i).re = 0
-- Mathlib/GroupTheory/Coxeter/Length.lean
theorem isLeftDescent_iff {w : W} {i : B} :
    cs.IsLeftDescent w i ↔ ℓ (s i * w) + 1 = ℓ w

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.IsLeftDescent w i ↔ cs.length (cs.simple i * w) + 1 = cs.length w

Tactic:
unfold IsLeftDescent

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w) < cs.length w ↔ cs.length (cs.simple i * w) + 1 = cs.length w

Proof state:
case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w) + 1 = cs.length w → cs.length (cs.simple i * w) < cs.length w

Tactic:
omega

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w) < cs.length w ↔ cs.length (cs.simple i * w) + 1 = cs.length w

Tactic:
constructor

Result:
case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w) < cs.length w → cs.length (cs.simple i * w) + 1 = cs.length w

case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w) + 1 = cs.length w → cs.length (cs.simple i * w) < cs.length w

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
a✝ : cs.length (cs.simple i * w) < cs.length w
⊢ ¬cs.length (cs.simple i * w) = cs.length w + 1

Tactic:
omega

Result:
no goals

Proof state:
case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
a✝ : cs.length (cs.simple i * w) < cs.length w
⊢ cs.length (cs.simple i * w) + 1 = cs.length w

Tactic:
exact (cs.length_simple_mul w i).resolve_left (by omega)

Result:
no goals

Proof state:
case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w) < cs.length w → cs.length (cs.simple i * w) + 1 = cs.length w

Tactic:
intro _

Result:
case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
a✝ : cs.length (cs.simple i * w) < cs.length w
⊢ cs.length (cs.simple i * w) + 1 = cs.length w
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem rootSet_maps_to' {p : T[X]} {S S'} [CommRing S] [IsDomain S] [Algebra T S] [CommRing S']
    [IsDomain S'] [Algebra T S'] (hp : p.map (algebraMap T S') = 0 → p.map (algebraMap T S) = 0)
    (f : S →ₐ[T] S') : (p.rootSet S).MapsTo f (p.rootSet S') := fun x hx => by
  rw [mem_rootSet'] at hx ⊢
  rw [aeval_algHom, AlgHom.comp_apply, hx.2, _root_.map_zero]
  exact ⟨mt hp hx.1, rfl⟩

Proof state:
T : Type w
inst✝⁶ : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra T S
inst✝² : CommRing S'
inst✝¹ : IsDomain S'
inst✝ : Algebra T S'
hp : map (algebraMap T S') p = 0 → map (algebraMap T S) p = 0
f : S →ₐ[T] S'
x : S
hx : x ∈ p.rootSet S
⊢ f x ∈ p.rootSet S'

Tactic:
rw [mem_rootSet'] at hx ⊢

Result:
T : Type w
inst✝⁶ : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra T S
inst✝² : CommRing S'
inst✝¹ : IsDomain S'
inst✝ : Algebra T S'
hp : map (algebraMap T S') p = 0 → map (algebraMap T S) p = 0
f : S →ₐ[T] S'
x : S
hx : map (algebraMap T S) p ≠ 0 ∧ (aeval x) p = 0
⊢ map (algebraMap T S') p ≠ 0 ∧ (aeval (f x)) p = 0

Proof state:
T : Type w
inst✝⁶ : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra T S
inst✝² : CommRing S'
inst✝¹ : IsDomain S'
inst✝ : Algebra T S'
hp : map (algebraMap T S') p = 0 → map (algebraMap T S) p = 0
f : S →ₐ[T] S'
x : S
hx : map (algebraMap T S) p ≠ 0 ∧ (aeval x) p = 0
⊢ map (algebraMap T S') p ≠ 0 ∧ (aeval (f x)) p = 0

Tactic:
rw [aeval_algHom, AlgHom.comp_apply, hx.2, _root_.map_zero]

Result:
T : Type w
inst✝⁶ : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra T S
inst✝² : CommRing S'
inst✝¹ : IsDomain S'
inst✝ : Algebra T S'
hp : map (algebraMap T S') p = 0 → map (algebraMap T S) p = 0
f : S →ₐ[T] S'
x : S
hx : map (algebraMap T S) p ≠ 0 ∧ (aeval x) p = 0
⊢ map (algebraMap T S') p ≠ 0 ∧ 0 = 0

Proof state:
T : Type w
inst✝⁶ : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra T S
inst✝² : CommRing S'
inst✝¹ : IsDomain S'
inst✝ : Algebra T S'
hp : map (algebraMap T S') p = 0 → map (algebraMap T S) p = 0
f : S →ₐ[T] S'
x : S
hx : map (algebraMap T S) p ≠ 0 ∧ (aeval x) p = 0
⊢ map (algebraMap T S') p ≠ 0 ∧ 0 = 0

Tactic:
exact ⟨mt hp hx.1, rfl⟩

Result:
no goals
-- Mathlib/Algebra/EuclideanDomain/Basic.lean
theorem gcd_eq_gcd_ab (a b : R) : (gcd a b : R) = a * gcdA a b + b * gcdB a b

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ b = a * 0 + b * 1

Tactic:
rw [mul_one, mul_zero, zero_add]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ EuclideanDomain.P a b (a, 1, 0)

Tactic:
dsimp [P]

Result:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ a = a * 1 + b * 0

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ gcd a b = a * gcdA a b + b * gcdB a b

Tactic:
have :=
  @xgcdAux_P _ _ _ a b a b 1 0 0 1 (by dsimp [P]; rw [mul_one, mul_zero, add_zero])
    (by dsimp [P]; rw [mul_one, mul_zero, zero_add])

Result:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
this : EuclideanDomain.P a b (xgcdAux a 1 0 b 0 1)
⊢ gcd a b = a * gcdA a b + b * gcdB a b

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ EuclideanDomain.P a b (b, 0, 1)

Tactic:
dsimp [P]

Result:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ b = a * 0 + b * 1

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ a = a * 1 + b * 0

Tactic:
rw [mul_one, mul_zero, add_zero]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
this : EuclideanDomain.P a b (xgcdAux a 1 0 b 0 1)
⊢ gcd a b = a * gcdA a b + b * gcdB a b

Tactic:
rwa [xgcdAux_val, xgcd_val] at this

Result:
no goals
-- Mathlib/Analysis/Normed/Module/FiniteDimension.lean
theorem isOpen_setOf_nat_le_rank (n : ℕ) :
    IsOpen { f : E →L[𝕜] F | ↑n ≤ (f : E →ₗ[𝕜] F).rank }

Proof state:
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type w
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace 𝕜
n : ℕ
t : Finset E
x✝ : t ∈ fun i => i.card = n
⊢ IsOpen {x | LinearIndependent 𝕜 fun (x_1 : ↑↑t) => ↑x ↑x_1}

Tactic:
have : Continuous fun f : E →L[𝕜] F => fun x : (t : Set E) => f x :=
  continuous_pi fun x => (ContinuousLinearMap.apply 𝕜 F (x : E)).continuous

Result:
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type w
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace 𝕜
n : ℕ
t : Finset E
x✝ : t ∈ fun i => i.card = n
this : Continuous fun f x => f ↑x
⊢ IsOpen {x | LinearIndependent 𝕜 fun (x_1 : ↑↑t) => ↑x ↑x_1}

Proof state:
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type w
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace 𝕜
n : ℕ
⊢ IsOpen (⋃ i, ⋃ (_ : i.card = n), {x | LinearIndependent 𝕜 fun (x_1 : ↑↑i) => ↑x ↑x_1})

Tactic:
refine isOpen_biUnion fun t _ => ?_

Result:
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type w
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace 𝕜
n : ℕ
t : Finset E
x✝ : t ∈ fun i => i.card = n
⊢ IsOpen {x | LinearIndependent 𝕜 fun (x_1 : ↑↑t) => ↑x ↑x_1}

Proof state:
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type w
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace 𝕜
n : ℕ
⊢ IsOpen {f | ↑n ≤ (↑f).rank}

Tactic:
simp only [LinearMap.le_rank_iff_exists_linearIndependent_finset, setOf_exists, ← exists_prop]

Result:
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type w
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace 𝕜
n : ℕ
⊢ IsOpen (⋃ i, ⋃ (_ : i.card = n), {x | LinearIndependent 𝕜 fun (x_1 : ↑↑i) => ↑x ↑x_1})

Proof state:
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type w
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace 𝕜
n : ℕ
t : Finset E
x✝ : t ∈ fun i => i.card = n
this : Continuous fun f x => f ↑x
⊢ IsOpen {x | LinearIndependent 𝕜 fun (x_1 : ↑↑t) => ↑x ↑x_1}

Tactic:
exact isOpen_setOf_linearIndependent.preimage this

Result:
no goals
-- Mathlib/Analysis/Convex/EGauge.lean
lemma egauge_ball_le_of_one_lt_norm (hc : 1 < ‖c‖) (h₀ : r ≠ 0 ∨ ‖x‖ ≠ 0) :
    egauge 𝕜 (ball 0 r) x ≤ ‖c‖ₑ * ‖x‖ₑ / r

Proof state:
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ≥0
hc : 1 < ‖c‖
h₀ : r ≠ 0 ∨ ‖x‖ ≠ 0
⊢ egauge 𝕜 (ball 0 ↑r) x ≤ ‖c‖ₑ * ‖x‖ₑ / ↑r

Tactic:
letI : NontriviallyNormedField 𝕜 := ⟨c, hc⟩

Result:
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ≥0
hc : 1 < ‖c‖
h₀ : r ≠ 0 ∨ ‖x‖ ≠ 0
this : NontriviallyNormedField 𝕜 := NontriviallyNormedField.mk ⋯
⊢ egauge 𝕜 (ball 0 ↑r) x ≤ ‖c‖ₑ * ‖x‖ₑ / ↑r

Proof state:
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ≥0
hc : 1 < ‖c‖
h₀ : r ≠ 0 ∨ ‖x‖ ≠ 0
this : NontriviallyNormedField 𝕜 := NontriviallyNormedField.mk ⋯
hr : 0 < r
hx : ‖x‖ = 0
⊢ ‖x‖ₑ = 0

Tactic:
simpa [enorm, ← coe_nnnorm, NNReal.coe_eq_zero] using hx

Result:
no goals

Proof state:
case inr
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ≥0
hc : 1 < ‖c‖
h₀ : r ≠ 0 ∨ ‖x‖ ≠ 0
this : NontriviallyNormedField 𝕜 := NontriviallyNormedField.mk ⋯
hr : 0 < r
⊢ egauge 𝕜 (ball 0 ↑r) x ≤ ‖c‖ₑ * ‖x‖ₑ / ↑r

Tactic:
rcases eq_or_ne ‖x‖ 0 with hx | hx

Result:
case inr.inl
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ≥0
hc : 1 < ‖c‖
h₀ : r ≠ 0 ∨ ‖x‖ ≠ 0
this : NontriviallyNormedField 𝕜 := NontriviallyNormedField.mk ⋯
hr : 0 < r
hx : ‖x‖ = 0
⊢ egauge 𝕜 (ball 0 ↑r) x ≤ ‖c‖ₑ * ‖x‖ₑ / ↑r

case inr.inr
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ≥0
hc : 1 < ‖c‖
h₀ : r ≠ 0 ∨ ‖x‖ ≠ 0
this : NontriviallyNormedField 𝕜 := NontriviallyNormedField.mk ⋯
hr : 0 < r
hx : ‖x‖ ≠ 0
⊢ egauge 𝕜 (ball 0 ↑r) x ≤ ‖c‖ₑ * ‖x‖ₑ / ↑r

Proof state:
case inr.inl
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c✝ : 𝕜
x : E
r : ℝ≥0
hc✝ : 1 < ‖c✝‖
h₀ : r ≠ 0 ∨ ‖x‖ ≠ 0
this : NontriviallyNormedField 𝕜 := NontriviallyNormedField.mk ⋯
hr : 0 < r
hx : ‖x‖ = 0
hx' : ‖x‖ₑ = 0
c : 𝕜
hc : c ∉ {0}
⊢ x ∈ c • ball 0 ↑r

Tactic:
simp [mem_smul_set_iff_inv_smul_mem₀ hc, norm_smul, hx, hr]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean
lemma neg'_add'_self (f : L.obj X ⟶ L.obj Y) :
    add' W (neg' W f) f = L.map 0

Proof state:
case intro
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
α : W.LeftFraction X Y
this : IsIso (L.map α.s)
⊢ (LeftFraction₂.mk (-α.f) α.f α.s ⋯).add.map L ⋯ = L.map 0

Tactic:
simp only [← cancel_mono (L.map α.s), LeftFraction.map_comp_map_s, ← L.map_comp,
  Limits.zero_comp, neg_add_cancel]

Result:
no goals

Proof state:
case intro
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
α : W.LeftFraction X Y
this : IsIso (L.map α.s)
⊢ add' W (neg' W (α.map L ⋯)) (α.map L ⋯) = L.map 0

Tactic:
rw [add'_eq W _ _ (LeftFraction₂.mk (-α.f) α.f α.s α.hs) (neg'_eq W _ _ rfl) rfl]

Result:
case intro
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
α : W.LeftFraction X Y
this : IsIso (L.map α.s)
⊢ (LeftFraction₂.mk (-α.f) α.f α.s ⋯).add.map L ⋯ = L.map 0

Proof state:
case intro
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
α : W.LeftFraction X Y
⊢ add' W (neg' W (α.map L ⋯)) (α.map L ⋯) = L.map 0

Tactic:
have := inverts L W _ α.hs

Result:
case intro
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
α : W.LeftFraction X Y
this : IsIso (L.map α.s)
⊢ add' W (neg' W (α.map L ⋯)) (α.map L ⋯) = L.map 0

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
⊢ add' W (neg' W f) f = L.map 0

Tactic:
obtain ⟨α, rfl⟩ := exists_leftFraction L W f

Result:
case intro
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
α : W.LeftFraction X Y
⊢ add' W (neg' W (α.map L ⋯)) (α.map L ⋯) = L.map 0
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem mem_biUnionIndex (hJ : J ∈ π.biUnion πi) : J ∈ πi (π.biUnionIndex πi J)

Proof state:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π.biUnion πi
⊢ J ∈ πi (π.biUnionIndex πi J)

Tactic:
convert (π.mem_biUnion.1 hJ).choose_spec.2 <;> exact dif_pos hJ

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem flatten_toArray_map_toArray (xss : List (List α)) :
    (xss.map List.toArray).toArray.flatten = xss.flatten.toArray

Proof state:
case cons
α : Type u_1
xs : List α
xss : List (List α)
ih : ∀ (as : Array α), List.foldl (fun r a => r ++ a) as (List.map List.toArray xss) = as ++ xss.flatten.toArray
as : Array α
⊢ List.foldl (fun r a => r ++ a) as (List.map List.toArray (xs :: xss)) = as ++ (xs :: xss).flatten.toArray

Tactic:
simp [ih]

Result:
no goals

Proof state:
α : Type u_1
xss : List (List α)
this : ∀ (as : Array α), List.foldl (fun r a => r ++ a) as (List.map List.toArray xss) = as ++ xss.flatten.toArray
⊢ List.foldl (fun r a => r ++ a) #[] (List.map List.toArray xss) = xss.flatten.toArray

Tactic:
simpa using this #[]

Result:
no goals

Proof state:
case nil
α : Type u_1
as : Array α
⊢ List.foldl (fun r a => r ++ a) as (List.map List.toArray []) = as ++ [].flatten.toArray

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
xss : List (List α)
⊢ ∀ (as : Array α), List.foldl (fun r a => r ++ a) as (List.map List.toArray xss) = as ++ xss.flatten.toArray

Tactic:
intro as

Result:
α : Type u_1
xss : List (List α)
as : Array α
⊢ List.foldl (fun r a => r ++ a) as (List.map List.toArray xss) = as ++ xss.flatten.toArray

Proof state:
α : Type u_1
xss : List (List α)
as : Array α
⊢ List.foldl (fun r a => r ++ a) as (List.map List.toArray xss) = as ++ xss.flatten.toArray

Tactic:
induction xss generalizing as with
| nil => simp
| cons xs xss ih => simp [ih]

Result:
no goals

Proof state:
α : Type u_1
xss : List (List α)
⊢ (List.map List.toArray xss).toArray.flatten = xss.flatten.toArray

Tactic:
simp [flatten]

Result:
α : Type u_1
xss : List (List α)
⊢ List.foldl (fun r a => r ++ a) #[] (List.map List.toArray xss) = xss.flatten.toArray

Proof state:
α : Type u_1
xss : List (List α)
⊢ List.foldl (fun r a => r ++ a) #[] (List.map List.toArray xss) = xss.flatten.toArray

Tactic:
suffices ∀ as, List.foldl (fun r a => r ++ a) as (List.map List.toArray xss) = as ++ xss.flatten.toArray by
  simpa using this #[]

Result:
α : Type u_1
xss : List (List α)
⊢ ∀ (as : Array α), List.foldl (fun r a => r ++ a) as (List.map List.toArray xss) = as ++ xss.flatten.toArray
-- Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean
theorem abs_def (q : ℚ) : |q| = q.num.natAbs /. q.den

Proof state:
case inr
q : ℚ
hq : 0 ≤ q
⊢ q = ↑q.num.natAbs /. ↑q.den

Tactic:
rw [← num_divInt_den q, ← zero_divInt, Rat.divInt_le_divInt Int.zero_lt_one (mod_cast q.pos),
  mul_one, zero_mul] at hq

Result:
case inr
q : ℚ
hq✝ : 0 ≤ q.num /. ↑q.den
hq : 0 ≤ q.num
⊢ q = ↑q.num.natAbs /. ↑q.den

Proof state:
case inl
q : ℚ
hq : q ≤ 0
⊢ |q| = ↑q.num.natAbs /. ↑q.den

Tactic:
rw [abs_of_nonpos hq]

Result:
case inl
q : ℚ
hq : q ≤ 0
⊢ -q = ↑q.num.natAbs /. ↑q.den

Proof state:
case inl
q : ℚ
hq✝ : q.num /. ↑q.den ≤ 0
hq : q.num ≤ 0
⊢ -q = ↑q.num.natAbs /. ↑q.den

Tactic:
rw [Int.ofNat_natAbs_of_nonpos hq, ← neg_def]

Result:
no goals

Proof state:
case inr
q : ℚ
hq : 0 ≤ q
⊢ |q| = ↑q.num.natAbs /. ↑q.den

Tactic:
rw [abs_of_nonneg hq]

Result:
case inr
q : ℚ
hq : 0 ≤ q
⊢ q = ↑q.num.natAbs /. ↑q.den

Proof state:
case inl
q : ℚ
hq : q ≤ 0
⊢ -q = ↑q.num.natAbs /. ↑q.den

Tactic:
rw [← num_divInt_den q, ← zero_divInt, Rat.divInt_le_divInt (mod_cast q.pos) Int.zero_lt_one,
  mul_one, zero_mul] at hq

Result:
case inl
q : ℚ
hq✝ : q.num /. ↑q.den ≤ 0
hq : q.num ≤ 0
⊢ -q = ↑q.num.natAbs /. ↑q.den

Proof state:
case inr
q : ℚ
hq✝ : 0 ≤ q.num /. ↑q.den
hq : 0 ≤ q.num
⊢ q = ↑q.num.natAbs /. ↑q.den

Tactic:
rw [Int.natAbs_of_nonneg hq, num_divInt_den]

Result:
no goals

Proof state:
q : ℚ
⊢ |q| = ↑q.num.natAbs /. ↑q.den

Tactic:
rcases le_total q 0 with hq | hq

Result:
case inl
q : ℚ
hq : q ≤ 0
⊢ |q| = ↑q.num.natAbs /. ↑q.den

case inr
q : ℚ
hq : 0 ≤ q
⊢ |q| = ↑q.num.natAbs /. ↑q.den