harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem degree_lt_degree_mul_X (hp : p ≠ 0) : p.degree < (p * X).degree

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
this : Nontrivial R
⊢ p.degree < (p * X).degree

Tactic:
have : leadingCoeff p * leadingCoeff X ≠ 0 := by simpa

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
this✝ : Nontrivial R
this : p.leadingCoeff * X.leadingCoeff ≠ 0
⊢ p.degree < (p * X).degree

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
this✝ : Nontrivial R
this : p.leadingCoeff * X.leadingCoeff ≠ 0
⊢ p.degree < (p * X).degree

Tactic:
rw [degree_mul' this, degree_eq_natDegree hp, degree_X, ← Nat.cast_one, ← Nat.cast_add]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
this✝ : Nontrivial R
this : p.leadingCoeff * X.leadingCoeff ≠ 0
⊢ ↑p.natDegree < ↑(p.natDegree + 1)

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
⊢ p.degree < (p * X).degree

Tactic:
haveI := Nontrivial.of_polynomial_ne hp

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
this : Nontrivial R
⊢ p.degree < (p * X).degree

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
this : Nontrivial R
⊢ p.leadingCoeff * X.leadingCoeff ≠ 0

Tactic:
simpa

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
this✝ : Nontrivial R
this : p.leadingCoeff * X.leadingCoeff ≠ 0
⊢ ↑p.natDegree < ↑(p.natDegree + 1)

Tactic:
norm_cast

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
this✝ : Nontrivial R
this : p.leadingCoeff * X.leadingCoeff ≠ 0
⊢ p.natDegree < p.natDegree + 1

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
this✝ : Nontrivial R
this : p.leadingCoeff * X.leadingCoeff ≠ 0
⊢ p.natDegree < p.natDegree + 1

Tactic:
exact Nat.lt_succ_self _

Result:
no goals
-- Mathlib/GroupTheory/Torsion.lean
theorem torsion_eq_top (tG : IsTorsion G) : torsion G = ⊤

Proof state:
G : Type u_1
inst✝ : CommMonoid G
tG : IsTorsion G
⊢ torsion G = ⊤

Tactic:
ext

Result:
case h
G : Type u_1
inst✝ : CommMonoid G
tG : IsTorsion G
x✝ : G
⊢ x✝ ∈ torsion G ↔ x✝ ∈ ⊤

Proof state:
case h
G : Type u_1
inst✝ : CommMonoid G
tG : IsTorsion G
x✝ : G
⊢ x✝ ∈ torsion G ↔ x✝ ∈ ⊤

Tactic:
tauto

Result:
no goals
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem integral_add_measure {ν} (f : α →ₛ E) (hf : Integrable f (μ + ν)) :
    f.integral (μ + ν) = f.integral μ + f.integral ν

Proof state:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ E
ν : Measure α
f : α →ₛ E
hf : Integrable (⇑f) (μ + ν)
s : Set α
x✝ : MeasurableSet s
hμνs : (μ + ν) s < ⊤
⊢ weightedSMul (μ + ν) s = weightedSMul μ s + weightedSMul ν s

Tactic:
rw [lt_top_iff_ne_top, Measure.coe_add, Pi.add_apply, ENNReal.add_ne_top] at hμνs

Result:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ E
ν : Measure α
f : α →ₛ E
hf : Integrable (⇑f) (μ + ν)
s : Set α
x✝ : MeasurableSet s
hμνs : μ s ≠ ⊤ ∧ ν s ≠ ⊤
⊢ weightedSMul (μ + ν) s = weightedSMul μ s + weightedSMul ν s

Proof state:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ E
ν : Measure α
f : α →ₛ E
hf : Integrable (⇑f) (μ + ν)
⊢ setToSimpleFunc (weightedSMul (μ + ν)) f = setToSimpleFunc (weightedSMul μ) f + setToSimpleFunc (weightedSMul ν) f

Tactic:
refine setToSimpleFunc_add_left'
  (weightedSMul μ) (weightedSMul ν) (weightedSMul (μ + ν)) (fun s _ hμνs => ?_) hf

Result:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ E
ν : Measure α
f : α →ₛ E
hf : Integrable (⇑f) (μ + ν)
s : Set α
x✝ : MeasurableSet s
hμνs : (μ + ν) s < ⊤
⊢ weightedSMul (μ + ν) s = weightedSMul μ s + weightedSMul ν s

Proof state:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ E
ν : Measure α
f : α →ₛ E
hf : Integrable (⇑f) (μ + ν)
⊢ integral (μ + ν) f = integral μ f + integral ν f

Tactic:
simp_rw [integral_def]

Result:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ E
ν : Measure α
f : α →ₛ E
hf : Integrable (⇑f) (μ + ν)
⊢ setToSimpleFunc (weightedSMul (μ + ν)) f = setToSimpleFunc (weightedSMul μ) f + setToSimpleFunc (weightedSMul ν) f

Proof state:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ E
ν : Measure α
f : α →ₛ E
hf : Integrable (⇑f) (μ + ν)
s : Set α
x✝ : MeasurableSet s
hμνs : μ s ≠ ⊤ ∧ ν s ≠ ⊤
⊢ weightedSMul (μ + ν) s = weightedSMul μ s + weightedSMul ν s

Tactic:
rw [weightedSMul_add_measure _ _ hμνs.1 hμνs.2]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma rpow_le_iff_le_log (hx : 0 < x) (hy : 0 < y) : x ^ z ≤ y ↔ z * log x ≤ log y

Proof state:
x y z : ℝ
hx : 0 < x
hy : 0 < y
⊢ x ^ z ≤ y ↔ z * log x ≤ log y

Tactic:
rw [← log_le_log_iff (rpow_pos_of_pos hx _) hy, log_rpow hx]

Result:
no goals
-- Mathlib/Topology/Category/TopCat/EffectiveEpi.lean
theorem effectiveEpi_iff_isQuotientMap {B X : TopCat.{u}} (π : X ⟶ B) :
    EffectiveEpi π ↔ IsQuotientMap π

Proof state:
B X : TopCat
π : X ⟶ B
x✝ : EffectiveEpi π
⊢ IsQuotientMap ⇑(ConcreteCategory.hom π)

Tactic:
have hπ : RegularEpi π := inferInstance

Result:
B X : TopCat
π : X ⟶ B
x✝ : EffectiveEpi π
hπ : RegularEpi π
⊢ IsQuotientMap ⇑(ConcreteCategory.hom π)

Proof state:
B X : TopCat
π : X ⟶ B
x✝ : EffectiveEpi π
hπ : RegularEpi π
⊢ IsQuotientMap ⇑(ConcreteCategory.hom π)

Tactic:
exact isQuotientMap_of_isColimit_cofork _ hπ.isColimit

Result:
no goals

Proof state:
B X : TopCat
π : X ⟶ B
⊢ EffectiveEpi π ↔ IsQuotientMap ⇑(ConcreteCategory.hom π)

Tactic:
refine ⟨fun _ ↦ ?_, fun hπ ↦ ⟨⟨effectiveEpiStructOfQuotientMap π hπ⟩⟩⟩

Result:
B X : TopCat
π : X ⟶ B
x✝ : EffectiveEpi π
⊢ IsQuotientMap ⇑(ConcreteCategory.hom π)
-- Mathlib/MeasureTheory/Measure/Portmanteau.lean
theorem ProbabilityMeasure.tendsto_measure_of_null_frontier_of_tendsto {Ω ι : Type*} {L : Filter ι}
    [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] [HasOuterApproxClosed Ω]
    {μ : ProbabilityMeasure Ω} {μs : ι → ProbabilityMeasure Ω} (μs_lim : Tendsto μs L (𝓝 μ))
    {E : Set Ω} (E_nullbdry : μ (frontier E) = 0) : Tendsto (fun i ↦ μs i E) L (𝓝 (μ E))

Proof state:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : HasOuterApproxClosed Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
E : Set Ω
E_nullbdry : μ (frontier E) = 0
⊢ Tendsto (fun i => (μs i) E) L (𝓝 (μ E))

Tactic:
have key := tendsto_measure_of_null_frontier_of_tendsto' μs_lim (by simpa using E_nullbdry)

Result:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : HasOuterApproxClosed Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
E : Set Ω
E_nullbdry : μ (frontier E) = 0
key : Tendsto (fun i => ↑(μs i) E) L (𝓝 (↑μ E))
⊢ Tendsto (fun i => (μs i) E) L (𝓝 (μ E))

Proof state:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : HasOuterApproxClosed Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
E : Set Ω
E_nullbdry : μ (frontier E) = 0
key : Tendsto (fun i => ↑(μs i) E) L (𝓝 (↑μ E))
⊢ Tendsto (fun i => (μs i) E) L (𝓝 (μ E))

Tactic:
exact (ENNReal.tendsto_toNNReal (measure_ne_top (↑μ) E)).comp key

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : HasOuterApproxClosed Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
E : Set Ω
E_nullbdry : μ (frontier E) = 0
⊢ ↑μ (frontier ?m.46013) = 0

Tactic:
simpa using E_nullbdry

Result:
no goals
-- Mathlib/RingTheory/WittVector/IsPoly.lean
theorem poly_eq_of_wittPolynomial_bind_eq [Fact p.Prime] (f g : ℕ → MvPolynomial ℕ ℤ)
    (h : ∀ n, bind₁ f (wittPolynomial p _ n) = bind₁ g (wittPolynomial p _ n)) : f = g

Proof state:
case h.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial ℕ ℤ
h : ∀ (n : ℕ), (bind₁ f) (wittPolynomial p ℤ n) = (bind₁ g) (wittPolynomial p ℤ n)
n : ℕ
⊢ (MvPolynomial.map (Int.castRingHom ℚ)) (f n) = (MvPolynomial.map (Int.castRingHom ℚ)) (g n)

Tactic:
rw [← funext_iff] at h

Result:
case h.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial ℕ ℤ
h : (fun n => (bind₁ f) (wittPolynomial p ℤ n)) = fun n => (bind₁ g) (wittPolynomial p ℤ n)
n : ℕ
⊢ (MvPolynomial.map (Int.castRingHom ℚ)) (f n) = (MvPolynomial.map (Int.castRingHom ℚ)) (g n)

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial ℕ ℤ
h : ∀ (n : ℕ), (bind₁ f) (wittPolynomial p ℤ n) = (bind₁ g) (wittPolynomial p ℤ n)
⊢ f = g

Tactic:
ext1 n

Result:
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial ℕ ℤ
h : ∀ (n : ℕ), (bind₁ f) (wittPolynomial p ℤ n) = (bind₁ g) (wittPolynomial p ℤ n)
n : ℕ
⊢ f n = g n

Proof state:
case h.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial ℕ ℤ
h : (fun n => (bind₁ f) (wittPolynomial p ℤ n)) = fun n => (bind₁ g) (wittPolynomial p ℤ n)
n : ℕ
⊢ (MvPolynomial.map (Int.castRingHom ℚ)) (f n) = (MvPolynomial.map (Int.castRingHom ℚ)) (g n)

Tactic:
replace h :=
  congr_arg (fun fam => bind₁ (MvPolynomial.map (Int.castRingHom ℚ) ∘ fam) (xInTermsOfW p ℚ n)) h

Result:
case h.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial ℕ ℤ
n : ℕ
h :
  ((fun fam => (bind₁ (⇑(MvPolynomial.map (Int.castRingHom ℚ)) ∘ fam)) (xInTermsOfW p ℚ n)) fun n =>
      (bind₁ f) (wittPolynomial p ℤ n)) =
    (fun fam => (bind₁ (⇑(MvPolynomial.map (Int.castRingHom ℚ)) ∘ fam)) (xInTermsOfW p ℚ n)) fun n =>
      (bind₁ g) (wittPolynomial p ℤ n)
⊢ (MvPolynomial.map (Int.castRingHom ℚ)) (f n) = (MvPolynomial.map (Int.castRingHom ℚ)) (g n)

Proof state:
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial ℕ ℤ
h : ∀ (n : ℕ), (bind₁ f) (wittPolynomial p ℤ n) = (bind₁ g) (wittPolynomial p ℤ n)
n : ℕ
⊢ f n = g n

Tactic:
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective

Result:
case h.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial ℕ ℤ
h : ∀ (n : ℕ), (bind₁ f) (wittPolynomial p ℤ n) = (bind₁ g) (wittPolynomial p ℤ n)
n : ℕ
⊢ (MvPolynomial.map (Int.castRingHom ℚ)) (f n) = (MvPolynomial.map (Int.castRingHom ℚ)) (g n)

Proof state:
case h.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ℕ → MvPolynomial ℕ ℤ
n : ℕ
h :
  ((fun fam => (bind₁ (⇑(MvPolynomial.map (Int.castRingHom ℚ)) ∘ fam)) (xInTermsOfW p ℚ n)) fun n =>
      (bind₁ f) (wittPolynomial p ℤ n)) =
    (fun fam => (bind₁ (⇑(MvPolynomial.map (Int.castRingHom ℚ)) ∘ fam)) (xInTermsOfW p ℚ n)) fun n =>
      (bind₁ g) (wittPolynomial p ℤ n)
⊢ (MvPolynomial.map (Int.castRingHom ℚ)) (f n) = (MvPolynomial.map (Int.castRingHom ℚ)) (g n)

Tactic:
simpa only [Function.comp_def, map_bind₁, map_wittPolynomial, ← bind₁_bind₁,
  bind₁_wittPolynomial_xInTermsOfW, bind₁_X_right] using h

Result:
no goals
-- Mathlib/Probability/ConditionalProbability.lean
@[simp] lemma cond_univ [IsProbabilityMeasure μ] : μ[|Set.univ] = μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
⊢ μ[|univ] = μ

Tactic:
simp [cond, measure_univ, Measure.restrict_univ]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem neg_iff {f : NormedAddGroupHom V₁ V₂} : (-f).NormNoninc ↔ f.NormNoninc :=
  ⟨fun h x => by simpa using h x, fun h x => (norm_neg (f x)).le.trans (h x)⟩

Proof state:
V₁ : Type u_3
V₂ : Type u_4
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
h : (-f).NormNoninc
x : V₁
⊢ ‖f x‖ ≤ ‖x‖

Tactic:
simpa using h x

Result:
no goals
-- Mathlib/Topology/List.lean
theorem continuousAt_length : ∀ l : List α, ContinuousAt List.length l

Proof state:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
l : List α
a : α
ih : Tendsto length (𝓝 l) (pure l.length)
⊢ Tendsto (fun p => p.2.length.add 0) (𝓝 a ×ˢ 𝓝 l) (pure l.length)

Tactic:
exact Tendsto.comp ih tendsto_snd

Result:
no goals

Proof state:
case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
⊢ Tendsto length (pure []) (pure [].length)

Tactic:
exact tendsto_pure_pure _ _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ ∀ (l : List α), Tendsto length (𝓝 l) (pure l.length)

Tactic:
refine tendsto_nhds ?_ ?_

Result:
case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
⊢ Tendsto length (pure []) (pure [].length)

case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
⊢ ∀ (l : List α) (a : α),
    Tendsto length (𝓝 l) (pure l.length) → Tendsto (fun p => (p.1 :: p.2).length) (𝓝 a ×ˢ 𝓝 l) (pure (a :: l).length)

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ ∀ (l : List α), ContinuousAt length l

Tactic:
simp only [ContinuousAt, nhds_discrete]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ ∀ (l : List α), Tendsto length (𝓝 l) (pure l.length)

Proof state:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
⊢ ∀ (l : List α) (a : α),
    Tendsto length (𝓝 l) (pure l.length) → Tendsto (fun p => (p.1 :: p.2).length) (𝓝 a ×ˢ 𝓝 l) (pure (a :: l).length)

Tactic:
intro l a ih

Result:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
l : List α
a : α
ih : Tendsto length (𝓝 l) (pure l.length)
⊢ Tendsto (fun p => (p.1 :: p.2).length) (𝓝 a ×ˢ 𝓝 l) (pure (a :: l).length)

Proof state:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
l : List α
a : α
ih : Tendsto length (𝓝 l) (pure l.length)
⊢ Tendsto (fun p => p.2.length + 1) (𝓝 a ×ˢ 𝓝 l) (pure (l.length + 1))

Tactic:
refine Tendsto.comp (tendsto_pure_pure (fun x => x + 1) _) ?_

Result:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
l : List α
a : α
ih : Tendsto length (𝓝 l) (pure l.length)
⊢ Tendsto (fun p => p.2.length.add 0) (𝓝 a ×ˢ 𝓝 l) (pure l.length)

Proof state:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
l : List α
a : α
ih : Tendsto length (𝓝 l) (pure l.length)
⊢ Tendsto (fun p => (p.1 :: p.2).length) (𝓝 a ×ˢ 𝓝 l) (pure (a :: l).length)

Tactic:
dsimp only [List.length]

Result:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
l : List α
a : α
ih : Tendsto length (𝓝 l) (pure l.length)
⊢ Tendsto (fun p => p.2.length + 1) (𝓝 a ×ˢ 𝓝 l) (pure (l.length + 1))
-- Mathlib/RingTheory/WittVector/Defs.lean
theorem constantCoeff_wittAdd (n : ℕ) : constantCoeff (wittAdd p n) = 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ constantCoeff (wittAdd p n) = 0

Tactic:
apply constantCoeff_wittStructureInt p _ _ n

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ constantCoeff (X 0 + X 1) = 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ constantCoeff (X 0 + X 1) = 0

Tactic:
simp only [add_zero, RingHom.map_add, constantCoeff_X]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
theorem gramSchmidtOrthonormalBasis_inv_triangular' {i j : ι} (hij : i < j) :
    (gramSchmidtOrthonormalBasis h f).repr (f i) j = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : WellFoundedLT ι
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i j : ι
hij : i < j
⊢ (gramSchmidtOrthonormalBasis h f).repr (f i) j = 0

Tactic:
simpa [OrthonormalBasis.repr_apply_apply] using gramSchmidtOrthonormalBasis_inv_triangular h f hij

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem norm_integral_le_of_norm_le_const_ae {a b C : ℝ} {f : ℝ → E}
    (h : ∀ᵐ x, x ∈ Ι a b → ‖f x‖ ≤ C) : ‖∫ x in a..b, f x‖ ≤ C * |b - a|

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b C : ℝ
f : ℝ → E
h : ∀ᵐ (x : ℝ), x ∈ Ι a b → ‖f x‖ ≤ C
⊢ ‖∫ (x : ℝ) in Ι a b, f x ∂volume‖ ≤ C * |b - a|

Tactic:
convert norm_setIntegral_le_of_norm_le_const_ae'' _ measurableSet_Ioc h using 1

Result:
case h.e'_4
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b C : ℝ
f : ℝ → E
h : ∀ᵐ (x : ℝ), x ∈ Ι a b → ‖f x‖ ≤ C
⊢ C * |b - a| = C * (volume (Ioc (a ⊓ b) (a ⊔ b))).toReal

E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b C : ℝ
f : ℝ → E
h : ∀ᵐ (x : ℝ), x ∈ Ι a b → ‖f x‖ ≤ C
⊢ volume (Ioc (a ⊓ b) (a ⊔ b)) < ⊤

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b C : ℝ
f : ℝ → E
h : ∀ᵐ (x : ℝ), x ∈ Ι a b → ‖f x‖ ≤ C
⊢ volume (Ioc (a ⊓ b) (a ⊔ b)) < ⊤

Tactic:
simp only [Real.volume_Ioc, ENNReal.ofReal_lt_top]

Result:
no goals

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b C : ℝ
f : ℝ → E
h : ∀ᵐ (x : ℝ), x ∈ Ι a b → ‖f x‖ ≤ C
⊢ ‖∫ (x : ℝ) in a..b, f x‖ ≤ C * |b - a|

Tactic:
rw [norm_integral_eq_norm_integral_Ioc]

Result:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b C : ℝ
f : ℝ → E
h : ∀ᵐ (x : ℝ), x ∈ Ι a b → ‖f x‖ ≤ C
⊢ ‖∫ (x : ℝ) in Ι a b, f x ∂volume‖ ≤ C * |b - a|

Proof state:
case h.e'_4
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b C : ℝ
f : ℝ → E
h : ∀ᵐ (x : ℝ), x ∈ Ι a b → ‖f x‖ ≤ C
⊢ C * |b - a| = C * (volume (Ioc (a ⊓ b) (a ⊔ b))).toReal

Tactic:
rw [Real.volume_Ioc, max_sub_min_eq_abs, ENNReal.toReal_ofReal (abs_nonneg _)]

Result:
no goals
-- Mathlib/Analysis/Calculus/VectorField.lean
lemma pullbackWithin_eq_of_fderivWithin_eq
    {f : E → F} {M : E ≃L[𝕜] F} {x : E} (hf : M = fderivWithin 𝕜 f s x) (V : F → F) :
    pullbackWithin 𝕜 f V s x = M.symm (V (f x))

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
M : E ≃L[𝕜] F
x : E
hf : ↑M = fderivWithin 𝕜 f s x
V : F → F
⊢ pullbackWithin 𝕜 f V s x = M.symm (V (f x))

Tactic:
simp [pullbackWithin, ← hf]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem rTensor_id_apply (x : N ⊗[R] M) : (LinearMap.id : N →ₗ[R] N).rTensor M x = x

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : N ⊗[R] M
⊢ (rTensor M id) x = x

Tactic:
rw [rTensor_id, id_coe, _root_.id]

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem exists_large_sphere_aux (n d : ℕ) : ∃ k ∈ range (n * (d - 1) ^ 2 + 1),
    (↑(d ^ n) / ((n * (d - 1) ^ 2 :) + 1) : ℝ) ≤ #(sphere n d k)

Proof state:
case refine_2.ha
n d : ℕ
⊢ ↑(n * (d - 1) ^ 2) + 1 ≠ 0

Tactic:
exact (cast_add_one_pos _).ne'

Result:
no goals

Proof state:
case refine_1
n d : ℕ
x : Fin n → ℕ
hx : x ∈ box n d
⊢ ∑ i : Fin n, x i ^ 2 ∈ range (n * (d - 1) ^ 2 + 1)

Tactic:
rw [mem_range, Nat.lt_succ_iff]

Result:
case refine_1
n d : ℕ
x : Fin n → ℕ
hx : x ∈ box n d
⊢ ∑ i : Fin n, x i ^ 2 ≤ n * (d - 1) ^ 2

Proof state:
n d : ℕ
⊢ ∃ k ∈ range (n * (d - 1) ^ 2 + 1), ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))

Tactic:
refine exists_le_card_fiber_of_nsmul_le_card_of_maps_to (fun x hx => ?_) nonempty_range_succ ?_

Result:
case refine_1
n d : ℕ
x : Fin n → ℕ
hx : x ∈ box n d
⊢ ∑ i : Fin n, x i ^ 2 ∈ range (n * (d - 1) ^ 2 + 1)

case refine_2
n d : ℕ
⊢ #(range (n * (d - 1) ^ 2 + 1)) • (↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1)) ≤ ↑(#(box n d))

Proof state:
case refine_2
n d : ℕ
⊢ #(range (n * (d - 1) ^ 2 + 1)) • (↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1)) ≤ ↑(#(box n d))

Tactic:
rw [card_range, _root_.nsmul_eq_mul, mul_div_assoc', cast_add_one, mul_div_cancel_left₀,
  card_box]

Result:
case refine_2.ha
n d : ℕ
⊢ ↑(n * (d - 1) ^ 2) + 1 ≠ 0

Proof state:
case refine_1
n d : ℕ
x : Fin n → ℕ
hx : x ∈ box n d
⊢ ∑ i : Fin n, x i ^ 2 ≤ n * (d - 1) ^ 2

Tactic:
exact sum_sq_le_of_mem_box hx

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem dvd_of_one_le_padicValNat {n : ℕ} (hp : 1 ≤ padicValNat p n) : p ∣ n

Proof state:
p n : ℕ
hp : 1 ≤ padicValNat p n
⊢ p ∣ n

Tactic:
by_contra h

Result:
p n : ℕ
hp : 1 ≤ padicValNat p n
h : ¬p ∣ n
⊢ False

Proof state:
p n : ℕ
hp : 1 ≤ 0
h : ¬p ∣ n
⊢ False

Tactic:
exact lt_irrefl 0 (lt_of_lt_of_le zero_lt_one hp)

Result:
no goals

Proof state:
p n : ℕ
hp : 1 ≤ padicValNat p n
h : ¬p ∣ n
⊢ False

Tactic:
rw [padicValNat.eq_zero_of_not_dvd h] at hp

Result:
p n : ℕ
hp : 1 ≤ 0
h : ¬p ∣ n
⊢ False
-- Mathlib/RingTheory/WittVector/StructurePolynomial.lean
theorem wittStructureRat_prop (Φ : MvPolynomial idx ℚ) (n : ℕ) :
    bind₁ (wittStructureRat p Φ) (W_ ℚ n) = bind₁ (fun i => rename (Prod.mk i) (W_ ℚ n)) Φ :=
  calc
    bind₁ (wittStructureRat p Φ) (W_ ℚ n) =
        bind₁ (fun k => bind₁ (fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ)
          (bind₁ (xInTermsOfW p ℚ) (W_ ℚ n))

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ (bind₁ (wittStructureRat p Φ)) (W_ ℚ n) =
    (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) ((bind₁ (xInTermsOfW p ℚ)) (W_ ℚ n))

Tactic:
rw [bind₁_bind₁]

Result:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ (bind₁ (wittStructureRat p Φ)) (W_ ℚ n) =
    (bind₁ fun i => (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ i)) (W_ ℚ n)

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ (bind₁ (wittStructureRat p Φ)) (W_ ℚ n) =
    (bind₁ fun i => (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ i)) (W_ ℚ n)

Tactic:
exact eval₂Hom_congr (RingHom.ext_rat _ _) rfl rfl

Result:
no goals

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) ((bind₁ (xInTermsOfW p ℚ)) (W_ ℚ n)) =
    (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ n)) Φ

Tactic:
rw [bind₁_xInTermsOfW_wittPolynomial p _ n, bind₁_X_right]

Result:
no goals
-- Mathlib/Analysis/Analytic/IsolatedZeros.lean
theorem has_fpower_series_dslope_fslope (hp : HasFPowerSeriesAt f p z₀) :
    HasFPowerSeriesAt (dslope f z₀) p.fslope z₀

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hpd : deriv f z₀ = p.coeff 1
hp0 : p.coeff 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • p.coeff n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n => x ^ n • p.coeff n) (f (z₀ + x))
⊢ HasSum (fun n => x ^ n • p.coeff (n + 1)) (dslope f z₀ (z₀ + x))

Tactic:
by_cases h : x = 0

Result:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hpd : deriv f z₀ = p.coeff 1
hp0 : p.coeff 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • p.coeff n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n => x ^ n • p.coeff n) (f (z₀ + x))
h : x = 0
⊢ HasSum (fun n => x ^ n • p.coeff (n + 1)) (dslope f z₀ (z₀ + x))

case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hpd : deriv f z₀ = p.coeff 1
hp0 : p.coeff 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • p.coeff n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n => x ^ n • p.coeff n) (f (z₀ + x))
h : ¬x = 0
⊢ HasSum (fun n => x ^ n • p.coeff (n + 1)) (dslope f z₀ (z₀ + x))
-- Mathlib/Topology/Compactification/OnePoint.lean
theorem inseparable_iff {x y : OnePoint X} :
    Inseparable x y ↔ x = ∞ ∧ y = ∞ ∨ ∃ x' : X, x = x' ∧ ∃ y' : X, y = y' ∧ Inseparable x' y'

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : OnePoint X
⊢ Inseparable x y ↔ x = ∞ ∧ y = ∞ ∨ ∃ x', x = ↑x' ∧ ∃ y', y = ↑y' ∧ Inseparable x' y'

Tactic:
induction x using OnePoint.rec <;> induction y using OnePoint.rec <;>
  simp [not_inseparable_infty_coe, not_inseparable_coe_infty, coe_eq_coe, Inseparable.refl]

Result:
no goals