harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/AEMeasurable.lean
lemma map_sum {ι : Type*} {m : ι → Measure α} {f : α → β} (hf : AEMeasurable f (Measure.sum m)) :
    Measure.map f (Measure.sum m) = Measure.sum (fun i ↦ Measure.map f (m i))

Proof state:
case h
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
ι : Type u_7
m : ι → Measure α
f : α → β
hf : AEMeasurable f (sum m)
s : Set β
hs : MeasurableSet s
⊢ ∑' (i : ι), (m i) (f ⁻¹' s) = ∑' (i : ι), (map f (m i)) s

Tactic:
have M i : AEMeasurable f (m i) := hf.mono_measure (le_sum m i)

Result:
case h
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
ι : Type u_7
m : ι → Measure α
f : α → β
hf : AEMeasurable f (sum m)
s : Set β
hs : MeasurableSet s
M : ∀ (i : ι), AEMeasurable f (m i)
⊢ ∑' (i : ι), (m i) (f ⁻¹' s) = ∑' (i : ι), (map f (m i)) s

Proof state:
case h
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
ι : Type u_7
m : ι → Measure α
f : α → β
hf : AEMeasurable f (sum m)
s : Set β
hs : MeasurableSet s
⊢ (map f (sum m)) s = (sum fun i => map f (m i)) s

Tactic:
rw [map_apply_of_aemeasurable hf hs, sum_apply₀ _ (hf.nullMeasurable hs), sum_apply _ hs]

Result:
case h
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
ι : Type u_7
m : ι → Measure α
f : α → β
hf : AEMeasurable f (sum m)
s : Set β
hs : MeasurableSet s
⊢ ∑' (i : ι), (m i) (f ⁻¹' s) = ∑' (i : ι), (map f (m i)) s

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
ι : Type u_7
m : ι → Measure α
f : α → β
hf : AEMeasurable f (sum m)
⊢ map f (sum m) = sum fun i => map f (m i)

Tactic:
ext s hs

Result:
case h
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
ι : Type u_7
m : ι → Measure α
f : α → β
hf : AEMeasurable f (sum m)
s : Set β
hs : MeasurableSet s
⊢ (map f (sum m)) s = (sum fun i => map f (m i)) s

Proof state:
case h
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
ι : Type u_7
m : ι → Measure α
f : α → β
hf : AEMeasurable f (sum m)
s : Set β
hs : MeasurableSet s
M : ∀ (i : ι), AEMeasurable f (m i)
⊢ ∑' (i : ι), (m i) (f ⁻¹' s) = ∑' (i : ι), (map f (m i)) s

Tactic:
simp_rw [map_apply_of_aemeasurable (M _) hs]

Result:
no goals
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem fst_invOf (x : tsze R M) [Invertible x] [Invertible x.fst] : (⅟x).fst = ⅟(x.fst)

Proof state:
R : Type u
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Semiring R
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : Module R M
x : tsze R M
inst✝¹ : Invertible x
inst✝ : Invertible x.fst
this : Invertible x.fst := x.invertibleFstOfInvertible
⊢ (⅟x).fst = ⅟x.fst

Tactic:
convert (rfl : _ = ⅟ x.fst)

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Semiring R
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : Module R M
x : tsze R M
inst✝¹ : Invertible x
inst✝ : Invertible x.fst
⊢ (⅟x).fst = ⅟x.fst

Tactic:
letI := invertibleFstOfInvertible x

Result:
R : Type u
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Semiring R
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : Module R M
x : tsze R M
inst✝¹ : Invertible x
inst✝ : Invertible x.fst
this : Invertible x.fst := x.invertibleFstOfInvertible
⊢ (⅟x).fst = ⅟x.fst
-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem eq_zero_iff_coeFn_eq_zero {f : lp E p} : f = 0 ↔ ⇑f = 0

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
⊢ f = 0 ↔ ↑f = 0

Tactic:
rw [lp.ext_iff, coeFn_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/PiTensorProduct.lean
@[simp] lemma piTensorHomMap₂_tprod_tprod_tprod
    (f : ∀ i, s i →ₗ[R] t i →ₗ[R] t' i) (a : ∀ i, s i) (b : ∀ i, t i) :
    piTensorHomMap₂ (tprod R f) (tprod R a) (tprod R b) = tprod R (fun i ↦ f i (a i) (b i))

Proof state:
ι : Type u_1
R : Type u_4
inst✝⁶ : CommSemiring R
s : ι → Type u_7
inst✝⁵ : (i : ι) → AddCommMonoid (s i)
inst✝⁴ : (i : ι) → Module R (s i)
t : ι → Type u_11
t' : ι → Type u_12
inst✝³ : (i : ι) → AddCommMonoid (t i)
inst✝² : (i : ι) → Module R (t i)
inst✝¹ : (i : ι) → AddCommMonoid (t' i)
inst✝ : (i : ι) → Module R (t' i)
f : (i : ι) → s i →ₗ[R] t i →ₗ[R] t' i
a : (i : ι) → s i
b : (i : ι) → t i
⊢ ((piTensorHomMap₂ ((tprod R) f)) ((tprod R) a)) ((tprod R) b) = ⨂ₜ[R] (i : ι), ((f i) (a i)) (b i)

Tactic:
simp [piTensorHomMapFun₂, piTensorHomMap₂]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma sub_pos {x y : EReal} : 0 < x - y ↔ y < x

Proof state:
x y : EReal
⊢ 0 < x - y ↔ y < x

Tactic:
cases x <;> cases y <;> simp [← EReal.coe_sub]

Result:
no goals
-- Mathlib/ModelTheory/Order.lean
theorem dlo_isComplete : Language.order.dlo.IsComplete :=
  aleph0_categorical_dlo.{0}.isComplete ℵ₀ _ le_rfl (by simp [one_le_aleph0])
    ⟨by
      letI : Language.order.Structure ℚ := orderStructure ℚ
      exact Theory.ModelType.of _ ℚ⟩
    fun _ => inferInstance

Proof state:
⊢ Language.order.dlo.ModelType

Tactic:
letI : Language.order.Structure ℚ := orderStructure ℚ

Result:
this : Language.order.Structure ℚ := orderStructure ℚ
⊢ Language.order.dlo.ModelType

Proof state:
⊢ lift.{0, 0} Language.order.card ≤ lift.{0, 0} ℵ₀

Tactic:
simp [one_le_aleph0]

Result:
no goals

Proof state:
this : Language.order.Structure ℚ := orderStructure ℚ
⊢ Language.order.dlo.ModelType

Tactic:
exact Theory.ModelType.of _ ℚ

Result:
no goals
-- Mathlib/GroupTheory/Frattini.lean
lemma frattini_le_comap_frattini_of_surjective (hφ : Function.Surjective φ) :
    frattini G ≤ (frattini H).comap φ

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
⊢ ∀ i ∈ {H_1 | IsCoatom H_1}, ⨅ a ∈ {H | IsCoatom H}, a ≤ comap φ i

Tactic:
intro M hM

Result:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM : M ∈ {H_1 | IsCoatom H_1}
⊢ ⨅ a ∈ {H | IsCoatom H}, a ≤ comap φ M

Proof state:
case hi
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM : M ∈ {H_1 | IsCoatom H_1}
⊢ comap φ M ∈ {H | IsCoatom H}

Tactic:
exact isCoatom_comap_of_surjective hφ hM

Result:
no goals

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
⊢ frattini G ≤ comap φ (frattini H)

Tactic:
simp_rw [frattini, Order.radical, comap_iInf, le_iInf_iff]

Result:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
⊢ ∀ i ∈ {H_1 | IsCoatom H_1}, ⨅ a ∈ {H | IsCoatom H}, a ≤ comap φ i

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM : M ∈ {H_1 | IsCoatom H_1}
⊢ ⨅ a ∈ {H | IsCoatom H}, a ≤ comap φ M

Tactic:
apply biInf_le

Result:
case hi
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM : M ∈ {H_1 | IsCoatom H_1}
⊢ comap φ M ∈ {H | IsCoatom H}
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem IsPath.nil {u : V} : (nil : G.Walk u u).IsPath

Proof state:
V : Type u
G : SimpleGraph V
u : V
⊢ Walk.nil.IsPath

Tactic:
constructor <;> simp

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem degree_sub_of_lt {f g : MvPolynomial σ R} (h : m.degree g ≺[m] m.degree f) :
    m.degree (f - g) = m.degree f

Proof state:
case h
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.toSyn (m.degree (-g)) < m.toSyn (m.degree f)

Tactic:
simp only [degree_neg, h]

Result:
no goals

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.degree (f + -g) = m.degree f

Tactic:
apply degree_add_of_lt

Result:
case h
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.toSyn (m.degree (-g)) < m.toSyn (m.degree f)

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.degree (f - g) = m.degree f

Tactic:
rw [sub_eq_add_neg]

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.degree (f + -g) = m.degree f
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem find_root_2 (self : UnionFind) (x : Fin self.size) :
    (self.find x).2.1.1 = self.rootD x

Proof state:
self : UnionFind
x : Fin self.size
⊢ ↑(self.find x).snd.val = self.rootD ↑x

Tactic:
simp [find, findAux_root, rootD]

Result:
no goals
-- Mathlib/Algebra/Polynomial/DenomsClearable.lean
theorem denomsClearable_zero (N : ℕ) (a : R) (bu : bi * i b = 1) : DenomsClearable a b N 0 i :=
  ⟨0, bi, bu, by
    simp only [eval_zero, RingHom.map_zero, mul_zero, Polynomial.map_zero]⟩

Proof state:
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
b : R
bi : K
N : ℕ
a : R
bu : bi * i b = 1
⊢ i 0 = i b ^ N * eval (i a * bi) (Polynomial.map i 0)

Tactic:
simp only [eval_zero, RingHom.map_zero, mul_zero, Polynomial.map_zero]

Result:
no goals
-- Mathlib/Order/Irreducible.lean
theorem SupPrime.le_finset_sup (ha : SupPrime a) : a ≤ s.sup f ↔ ∃ i ∈ s, a ≤ f i

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a : α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
ha : SupPrime a
⊢ a ≤ s.sup f ↔ ∃ i ∈ s, a ≤ f i

Tactic:
induction' s using Finset.induction with i s _ ih

Result:
case empty
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a : α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
ha : SupPrime a
⊢ a ≤ ∅.sup f ↔ ∃ i ∈ ∅, a ≤ f i

case insert
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a : α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
ha : SupPrime a
i : ι
s : Finset ι
a✝ : i ∉ s
ih : a ≤ s.sup f ↔ ∃ i ∈ s, a ≤ f i
⊢ a ≤ (insert i s).sup f ↔ ∃ i_1 ∈ insert i s, a ≤ f i_1

Proof state:
case insert
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a : α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
ha : SupPrime a
i : ι
s : Finset ι
a✝ : i ∉ s
ih : a ≤ s.sup f ↔ ∃ i ∈ s, a ≤ f i
⊢ a ≤ (insert i s).sup f ↔ ∃ i_1 ∈ insert i s, a ≤ f i_1

Tactic:
simp only [exists_prop, exists_mem_insert, sup_insert, ha.le_sup, ih]

Result:
no goals

Proof state:
case empty
ι : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
a : α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
ha : SupPrime a
⊢ a ≤ ∅.sup f ↔ ∃ i ∈ ∅, a ≤ f i

Tactic:
simp [ha.ne_bot]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_fin_two (A : Matrix (Fin 2) (Fin 2) R) : det A = A 0 0 * A 1 1 - A 0 1 * A 1 0

Proof state:
R : Type v
inst✝ : CommRing R
A : Matrix (Fin 2) (Fin 2) R
⊢ (-1) ^ 0 * A 0 0 * A 1 1 + (-1) ^ (0 + 1) * A 0 1 * A 1 0 = A 0 0 * A 1 1 - A 0 1 * A 1 0

Tactic:
ring

Result:
no goals

Proof state:
R : Type v
inst✝ : CommRing R
A : Matrix (Fin 2) (Fin 2) R
⊢ A.det = A 0 0 * A 1 1 - A 0 1 * A 1 0

Tactic:
simp only [det_succ_row_zero, det_unique, Fin.default_eq_zero, submatrix_apply,
  Fin.succ_zero_eq_one, Fin.sum_univ_succ, Fin.val_zero, Fin.zero_succAbove, univ_unique,
  Fin.val_succ, Fin.val_eq_zero, Fin.succ_succAbove_zero, sum_singleton]

Result:
R : Type v
inst✝ : CommRing R
A : Matrix (Fin 2) (Fin 2) R
⊢ (-1) ^ 0 * A 0 0 * A 1 1 + (-1) ^ (0 + 1) * A 0 1 * A 1 0 = A 0 0 * A 1 1 - A 0 1 * A 1 0
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem NormedSpace.sphere_nonempty [Nontrivial E] {x : E} {r : ℝ} :
    (sphere x r).Nonempty ↔ 0 ≤ r

Proof state:
case intro
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
y : E
hy : y ≠ x
hr : 0 ≤ r
this : ‖y - x‖ ≠ 0
⊢ r • ‖y - x‖⁻¹ • (y - x) + x ∈ sphere x r

Tactic:
simp only [mem_sphere_iff_norm, add_sub_cancel_right, norm_smul, Real.norm_eq_abs, norm_inv,
  norm_norm, ne_eq, norm_eq_zero]

Result:
case intro
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
y : E
hy : y ≠ x
hr : 0 ≤ r
this : ‖y - x‖ ≠ 0
⊢ |r| * (|‖y - x‖|⁻¹ * ‖y - x‖) = r

Proof state:
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ (sphere x r).Nonempty ↔ 0 ≤ r

Tactic:
obtain ⟨y, hy⟩ := exists_ne x

Result:
case intro
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
y : E
hy : y ≠ x
⊢ (sphere x r).Nonempty ↔ 0 ≤ r

Proof state:
case intro
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
y : E
hy : y ≠ x
hr : 0 ≤ r
this : ‖y - x‖ ≠ 0
⊢ |r| * (|‖y - x‖|⁻¹ * ‖y - x‖) = r

Tactic:
simp only [abs_norm, ne_eq, norm_eq_zero]

Result:
case intro
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
y : E
hy : y ≠ x
hr : 0 ≤ r
this : ‖y - x‖ ≠ 0
⊢ |r| * (‖y - x‖⁻¹ * ‖y - x‖) = r

Proof state:
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
y : E
hy : y ≠ x
hr : 0 ≤ r
⊢ ‖y - x‖ ≠ 0

Tactic:
simpa [sub_eq_zero]

Result:
no goals

Proof state:
case intro
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
y : E
hy : y ≠ x
hr : 0 ≤ r
this : ‖y - x‖ ≠ 0
⊢ |r| * (‖y - x‖⁻¹ * ‖y - x‖) = r

Tactic:
rw [inv_mul_cancel₀ this, mul_one, abs_eq_self.mpr hr]

Result:
no goals

Proof state:
case intro
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
y : E
hy : y ≠ x
⊢ (sphere x r).Nonempty ↔ 0 ≤ r

Tactic:
refine ⟨fun h => nonempty_closedBall.1 (h.mono sphere_subset_closedBall), fun hr =>
  ⟨r • ‖y - x‖⁻¹ • (y - x) + x, ?_⟩⟩

Result:
case intro
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
y : E
hy : y ≠ x
hr : 0 ≤ r
⊢ r • ‖y - x‖⁻¹ • (y - x) + x ∈ sphere x r

Proof state:
case intro
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
y : E
hy : y ≠ x
hr : 0 ≤ r
⊢ r • ‖y - x‖⁻¹ • (y - x) + x ∈ sphere x r

Tactic:
have : ‖y - x‖ ≠ 0 := by simpa [sub_eq_zero]

Result:
case intro
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
y : E
hy : y ≠ x
hr : 0 ≤ r
this : ‖y - x‖ ≠ 0
⊢ r • ‖y - x‖⁻¹ • (y - x) + x ∈ sphere x r
-- Mathlib/Analysis/NormedSpace/RCLike.lean
theorem ContinuousLinearMap.opNorm_bound_of_ball_bound {r : ℝ} (r_pos : 0 < r) (c : ℝ)
    (f : E →L[𝕜] 𝕜) (h : ∀ z ∈ closedBall (0 : E) r, ‖f z‖ ≤ c) : ‖f‖ ≤ c / r

Proof state:
case hM
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →L[𝕜] 𝕜
h : ∀ z ∈ closedBall 0 r, ‖f z‖ ≤ c
⊢ ∀ (x : E), ‖f x‖ ≤ c / r * ‖x‖

Tactic:
apply LinearMap.bound_of_ball_bound' r_pos

Result:
case hM.h
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →L[𝕜] 𝕜
h : ∀ z ∈ closedBall 0 r, ‖f z‖ ≤ c
⊢ ∀ z ∈ closedBall 0 r, ‖↑f z‖ ≤ c

Proof state:
case hM.h
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →L[𝕜] 𝕜
h : ∀ z ∈ closedBall 0 r, ‖f z‖ ≤ c
⊢ ∀ z ∈ closedBall 0 r, ‖↑f z‖ ≤ c

Tactic:
exact fun z hz => h z hz

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →L[𝕜] 𝕜
h : ∀ z ∈ closedBall 0 r, ‖f z‖ ≤ c
⊢ 0 ∈ closedBall 0 r

Tactic:
simp only [norm_zero, mem_closedBall, dist_zero_left, r_pos.le]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →L[𝕜] 𝕜
h : ∀ z ∈ closedBall 0 r, ‖f z‖ ≤ c
⊢ 0 ≤ c

Tactic:
exact
  (norm_nonneg _).trans
    (h 0 (by simp only [norm_zero, mem_closedBall, dist_zero_left, r_pos.le]))

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →L[𝕜] 𝕜
h : ∀ z ∈ closedBall 0 r, ‖f z‖ ≤ c
⊢ ‖f‖ ≤ c / r

Tactic:
apply ContinuousLinearMap.opNorm_le_bound

Result:
case hMp
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →L[𝕜] 𝕜
h : ∀ z ∈ closedBall 0 r, ‖f z‖ ≤ c
⊢ 0 ≤ c / r

case hM
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →L[𝕜] 𝕜
h : ∀ z ∈ closedBall 0 r, ‖f z‖ ≤ c
⊢ ∀ (x : E), ‖f x‖ ≤ c / r * ‖x‖

Proof state:
case hMp
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →L[𝕜] 𝕜
h : ∀ z ∈ closedBall 0 r, ‖f z‖ ≤ c
⊢ 0 ≤ c / r

Tactic:
apply div_nonneg _ r_pos.le

Result:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →L[𝕜] 𝕜
h : ∀ z ∈ closedBall 0 r, ‖f z‖ ≤ c
⊢ 0 ≤ c
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
theorem le_sin_mul {x : ℝ} (hx : 0 ≤ x) (hx' : x ≤ 1) : x ≤ sin (π / 2 * x)

Proof state:
x : ℝ
hx : 0 ≤ x
hx' : x ≤ 1
⊢ x ≤ sin (π / 2 * x)

Tactic:
simpa [mul_comm x] using
  strictConcaveOn_sin_Icc.concaveOn.2 ⟨le_rfl, pi_pos.le⟩
    ⟨pi_div_two_pos.le, half_le_self pi_pos.le⟩ (sub_nonneg.2 hx') hx

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem testBit_mul_pow_two :
    testBit (2 ^ i * a) j = (decide (j ≥ i) && testBit a (j-i))

Proof state:
i a j : Nat
gen : (2 ^ i * a).testBit j = (!decide (j < i) && a.testBit (j - i))
⊢ (2 ^ i * a).testBit j = (decide (j ≥ i) && a.testBit (j - i))

Tactic:
rw [gen]

Result:
i a j : Nat
gen : (2 ^ i * a).testBit j = (!decide (j < i) && a.testBit (j - i))
⊢ (!decide (j < i) && a.testBit (j - i)) = (decide (j ≥ i) && a.testBit (j - i))

Proof state:
case inr
i a j : Nat
gen : (2 ^ i * a).testBit j = (!decide (j < i) && a.testBit (j - i))
p : j ≥ i
⊢ (!decide (j < i) && a.testBit (j - i)) = (decide (j ≥ i) && a.testBit (j - i))

Tactic:
simp [p, Nat.not_le_of_lt, Nat.not_lt_of_le]

Result:
no goals

Proof state:
i a j : Nat
gen : (2 ^ i * a).testBit j = (!decide (j < i) && a.testBit (j - i))
⊢ (!decide (j < i) && a.testBit (j - i)) = (decide (j ≥ i) && a.testBit (j - i))

Tactic:
cases Nat.lt_or_ge j i with
| _ p => simp [p, Nat.not_le_of_lt, Nat.not_lt_of_le]

Result:
no goals

Proof state:
i a j : Nat
⊢ (2 ^ i * a).testBit j = (decide (j ≥ i) && a.testBit (j - i))

Tactic:
have gen := testBit_mul_pow_two_add a (Nat.two_pow_pos i) j

Result:
i a j : Nat
gen : (2 ^ i * a + 0).testBit j = if j < i then testBit 0 j else a.testBit (j - i)
⊢ (2 ^ i * a).testBit j = (decide (j ≥ i) && a.testBit (j - i))

Proof state:
i a j : Nat
gen : (2 ^ i * a + 0).testBit j = if j < i then testBit 0 j else a.testBit (j - i)
⊢ (2 ^ i * a).testBit j = (decide (j ≥ i) && a.testBit (j - i))

Tactic:
simp at gen

Result:
i a j : Nat
gen : (2 ^ i * a).testBit j = (!decide (j < i) && a.testBit (j - i))
⊢ (2 ^ i * a).testBit j = (decide (j ≥ i) && a.testBit (j - i))
-- Mathlib/Algebra/Squarefree/Basic.lean
theorem Squarefree.eq_zero_or_one_of_pow_of_not_isUnit [Monoid R] {x : R} {n : ℕ}
    (h : Squarefree (x ^ n)) (h' : ¬ IsUnit x) :
    n = 0 ∨ n = 1

Proof state:
R : Type u_1
inst✝ : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : 2 ≤ n
⊢ IsUnit x

Tactic:
have : x * x ∣ x ^ n := by rw [← sq]; exact pow_dvd_pow x h'

Result:
R : Type u_1
inst✝ : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : 2 ≤ n
this : x * x ∣ x ^ n
⊢ IsUnit x

Proof state:
R : Type u_1
inst✝ : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : n ≠ 0 ∧ n ≠ 1
⊢ IsUnit x

Tactic:
replace h' : 2 ≤ n := by omega

Result:
R : Type u_1
inst✝ : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : 2 ≤ n
⊢ IsUnit x

Proof state:
R : Type u_1
inst✝ : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : 2 ≤ n
⊢ x * x ∣ x ^ n

Tactic:
rw [← sq]

Result:
R : Type u_1
inst✝ : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : 2 ≤ n
⊢ x ^ 2 ∣ x ^ n

Proof state:
R : Type u_1
inst✝ : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : 2 ≤ n
⊢ x ^ 2 ∣ x ^ n

Tactic:
exact pow_dvd_pow x h'

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : ¬IsUnit x
⊢ n = 0 ∨ n = 1

Tactic:
contrapose! h'

Result:
R : Type u_1
inst✝ : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : n ≠ 0 ∧ n ≠ 1
⊢ IsUnit x

Proof state:
R : Type u_1
inst✝ : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : n ≠ 0 ∧ n ≠ 1
⊢ 2 ≤ n

Tactic:
omega

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : 2 ≤ n
this : x * x ∣ x ^ n
⊢ IsUnit x

Tactic:
exact h.squarefree_of_dvd this x (refl _)

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem sdiff_eq_self_iff_disjoint : x \ y = x ↔ Disjoint y x :=
  calc
    x \ y = x ↔ x \ y = x \ ⊥

Proof state:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ y = x ↔ x \ y = x \ ⊥

Tactic:
rw [sdiff_bot]

Result:
no goals

Proof state:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y = x ⊓ ⊥ ↔ Disjoint y x

Tactic:
rw [inf_bot_eq, inf_comm, disjoint_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/PreservesSheafification.lean
lemma W_isInvertedBy_whiskeringRight_presheafToSheaf :
    J.W.IsInvertedBy (((whiskeringRight Cᵒᵖ A B).obj F) ⋙ presheafToSheaf J B)

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝³ : Category.{u_3, u_1} A
inst✝² : Category.{u_4, u_2} B
F : A ⥤ B
inst✝¹ : J.PreservesSheafification F
inst✝ : HasWeakSheafify J B
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
hf : J.W f
⊢ IsIso ((presheafToSheaf J B).map (whiskerRight f F))

Tactic:
rw [← W_iff]

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝³ : Category.{u_3, u_1} A
inst✝² : Category.{u_4, u_2} B
F : A ⥤ B
inst✝¹ : J.PreservesSheafification F
inst✝ : HasWeakSheafify J B
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
hf : J.W f
⊢ J.W (whiskerRight f F)

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝³ : Category.{u_3, u_1} A
inst✝² : Category.{u_4, u_2} B
F : A ⥤ B
inst✝¹ : J.PreservesSheafification F
inst✝ : HasWeakSheafify J B
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
hf : J.W f
⊢ J.W (whiskerRight f F)

Tactic:
exact J.W_of_preservesSheafification F _ hf

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝³ : Category.{u_3, u_1} A
inst✝² : Category.{u_4, u_2} B
F : A ⥤ B
inst✝¹ : J.PreservesSheafification F
inst✝ : HasWeakSheafify J B
⊢ J.W.IsInvertedBy ((whiskeringRight Cᵒᵖ A B).obj F ⋙ presheafToSheaf J B)

Tactic:
intro P₁ P₂ f hf

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝³ : Category.{u_3, u_1} A
inst✝² : Category.{u_4, u_2} B
F : A ⥤ B
inst✝¹ : J.PreservesSheafification F
inst✝ : HasWeakSheafify J B
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
hf : J.W f
⊢ IsIso (((whiskeringRight Cᵒᵖ A B).obj F ⋙ presheafToSheaf J B).map f)

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝³ : Category.{u_3, u_1} A
inst✝² : Category.{u_4, u_2} B
F : A ⥤ B
inst✝¹ : J.PreservesSheafification F
inst✝ : HasWeakSheafify J B
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
hf : J.W f
⊢ IsIso (((whiskeringRight Cᵒᵖ A B).obj F ⋙ presheafToSheaf J B).map f)

Tactic:
dsimp

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝³ : Category.{u_3, u_1} A
inst✝² : Category.{u_4, u_2} B
F : A ⥤ B
inst✝¹ : J.PreservesSheafification F
inst✝ : HasWeakSheafify J B
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
hf : J.W f
⊢ IsIso ((presheafToSheaf J B).map (whiskerRight f F))