harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/LpSeminorm/Trim.lean
theorem eLpNorm_trim (hm : m ≤ m0) {f : α → E} (hf : StronglyMeasurable[m] f) :
    eLpNorm f p (μ.trim hm) = eLpNorm f p μ

Proof state:
case pos
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hm : m ≤ m0
f : α → E
hf : StronglyMeasurable f
h0 : p = 0
⊢ eLpNorm f p (μ.trim hm) = eLpNorm f p μ

Tactic:
simp [h0]

Result:
no goals

Proof state:
case neg
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hm : m ≤ m0
f : α → E
hf : StronglyMeasurable f
h0 : ¬p = 0
h_top : ¬p = ⊤
⊢ eLpNorm f p (μ.trim hm) = eLpNorm f p μ

Tactic:
simpa only [eLpNorm_eq_eLpNorm' h0 h_top] using eLpNorm'_trim hm hf

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hm : m ≤ m0
f : α → E
hf : StronglyMeasurable f
⊢ eLpNorm f p (μ.trim hm) = eLpNorm f p μ

Tactic:
by_cases h0 : p = 0

Result:
case pos
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hm : m ≤ m0
f : α → E
hf : StronglyMeasurable f
h0 : p = 0
⊢ eLpNorm f p (μ.trim hm) = eLpNorm f p μ

case neg
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hm : m ≤ m0
f : α → E
hf : StronglyMeasurable f
h0 : ¬p = 0
⊢ eLpNorm f p (μ.trim hm) = eLpNorm f p μ

Proof state:
case pos
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hm : m ≤ m0
f : α → E
hf : StronglyMeasurable f
h0 : ¬p = 0
h_top : p = ⊤
⊢ eLpNorm f p (μ.trim hm) = eLpNorm f p μ

Tactic:
simpa only [h_top, eLpNorm_exponent_top] using eLpNormEssSup_trim hm hf

Result:
no goals

Proof state:
case neg
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hm : m ≤ m0
f : α → E
hf : StronglyMeasurable f
h0 : ¬p = 0
⊢ eLpNorm f p (μ.trim hm) = eLpNorm f p μ

Tactic:
by_cases h_top : p = ∞

Result:
case pos
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hm : m ≤ m0
f : α → E
hf : StronglyMeasurable f
h0 : ¬p = 0
h_top : p = ⊤
⊢ eLpNorm f p (μ.trim hm) = eLpNorm f p μ

case neg
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hm : m ≤ m0
f : α → E
hf : StronglyMeasurable f
h0 : ¬p = 0
h_top : ¬p = ⊤
⊢ eLpNorm f p (μ.trim hm) = eLpNorm f p μ
-- Mathlib/Analysis/SpecialFunctions/Log/ENNRealLog.lean
@[simp]
lemma log_ofReal (x : ℝ) : log (ENNReal.ofReal x) = if x ≤ 0 then ⊥ else ↑(Real.log x)

Proof state:
x : ℝ
⊢ (ENNReal.ofReal x).log = if x ≤ 0 then ⊥ else ↑(Real.log x)

Tactic:
simp only [log, ENNReal.none_eq_top, ENNReal.ofReal_ne_top, IsEmpty.forall_iff,
  ENNReal.ofReal_eq_zero, EReal.coe_ennreal_ofReal, if_false]

Result:
x : ℝ
⊢ (if x ≤ 0 then ⊥ else ↑(Real.log (ENNReal.ofReal x).toReal)) = if x ≤ 0 then ⊥ else ↑(Real.log x)

Proof state:
x : ℝ
⊢ (if x ≤ 0 then ⊥ else ↑(Real.log (ENNReal.ofReal x).toReal)) = if x ≤ 0 then ⊥ else ↑(Real.log x)

Tactic:
split_ifs with h_nonpos

Result:
case pos
x : ℝ
h_nonpos : x ≤ 0
⊢ ⊥ = ⊥

case neg
x : ℝ
h_nonpos : ¬x ≤ 0
⊢ ↑(Real.log (ENNReal.ofReal x).toReal) = ↑(Real.log x)

Proof state:
case neg
x : ℝ
h_nonpos : ¬x ≤ 0
⊢ ↑(Real.log (ENNReal.ofReal x).toReal) = ↑(Real.log x)

Tactic:
rw [ENNReal.toReal_ofReal (not_le.mp h_nonpos).le]

Result:
no goals

Proof state:
case pos
x : ℝ
h_nonpos : x ≤ 0
⊢ ⊥ = ⊥

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Basic.lean
theorem HasIntegral.smul (hf : HasIntegral I l f vol y) (c : ℝ) :
    HasIntegral I l (c • f) vol (c • y)

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y : F
hf : HasIntegral I l f vol y
c : ℝ
⊢ HasIntegral I l (c • f) vol (c • y)

Tactic:
simpa only [HasIntegral, ← integralSum_smul] using
  (tendsto_const_nhds : Tendsto _ _ (𝓝 c)).smul hf

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem range'_eq_mk_range' (start size step) :
    range' start size step = Vector.mk (Array.range' start size step) (by simp)

Proof state:
start size step : Nat
⊢ range' start size step = { toArray := Array.range' start size step, size_toArray := ⋯ }

Tactic:
rfl

Result:
no goals

Proof state:
start size step : Nat
⊢ (Array.range' start size step).size = size

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem min_firstDiff_le (x y z : ∀ n, E n) (h : x ≠ z) :
    min (firstDiff x y) (firstDiff y z) ≤ firstDiff x z

Proof state:
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
h : x ≠ z
H : firstDiff x z < firstDiff x y ∧ firstDiff x z < firstDiff y z
⊢ False

Tactic:
refine apply_firstDiff_ne h ?_

Result:
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
h : x ≠ z
H : firstDiff x z < firstDiff x y ∧ firstDiff x z < firstDiff y z
⊢ x (firstDiff x z) = z (firstDiff x z)

Proof state:
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
h : x ≠ z
H : firstDiff x z < firstDiff x y ∧ firstDiff x z < firstDiff y z
⊢ x (firstDiff x z) = z (firstDiff x z)

Tactic:
calc
  x (firstDiff x z) = y (firstDiff x z) := apply_eq_of_lt_firstDiff H.1
  _ = z (firstDiff x z) := apply_eq_of_lt_firstDiff H.2

Result:
no goals

Proof state:
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
h : x ≠ z
⊢ firstDiff x y ⊓ firstDiff y z ≤ firstDiff x z

Tactic:
by_contra! H

Result:
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
h : x ≠ z
H : firstDiff x z < firstDiff x y ⊓ firstDiff y z
⊢ False

Proof state:
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
h : x ≠ z
H : firstDiff x z < firstDiff x y ⊓ firstDiff y z
⊢ False

Tactic:
rw [lt_min_iff] at H

Result:
E : ℕ → Type u_1
x y z : (n : ℕ) → E n
h : x ≠ z
H : firstDiff x z < firstDiff x y ∧ firstDiff x z < firstDiff y z
⊢ False
-- Mathlib/Computability/Partrec.lean
theorem mem_rfind {p : ℕ →. Bool} {n : ℕ} :
    n ∈ rfind p ↔ true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m :=
  ⟨fun h => ⟨rfind_spec h, @rfind_min _ _ h⟩, fun ⟨h₁, h₂⟩ => by
    let ⟨m, hm⟩ := dom_iff_mem.1 <| (@rfind_dom p).2 ⟨_, h₁, fun {m} mn => (h₂ mn).fst⟩
    rcases lt_trichotomy m n with (h | h | h)
    · injection mem_unique (h₂ h) (rfind_spec hm)
    · rwa [← h]
    · injection mem_unique h₁ (rfind_min hm h)⟩

Proof state:
case inr.inr
p : ℕ →. Bool
n : ℕ
x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
m : ℕ
hm : m ∈ rfind p
h : n < m
⊢ n ∈ rfind p

Tactic:
injection mem_unique h₁ (rfind_min hm h)

Result:
no goals

Proof state:
case inr.inl
p : ℕ →. Bool
n : ℕ
x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
m : ℕ
hm : m ∈ rfind p
h : m = n
⊢ n ∈ rfind p

Tactic:
rwa [← h]

Result:
no goals

Proof state:
p : ℕ →. Bool
n : ℕ
x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
⊢ n ∈ rfind p

Tactic:
let ⟨m, hm⟩ := dom_iff_mem.1 <| (@rfind_dom p).2 ⟨_, h₁, fun {m} mn => (h₂ mn).fst⟩

Result:
p : ℕ →. Bool
n : ℕ
x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
m : ℕ
hm : m ∈ rfind p
⊢ n ∈ rfind p

Proof state:
case inl
p : ℕ →. Bool
n : ℕ
x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
m : ℕ
hm : m ∈ rfind p
h : m < n
⊢ n ∈ rfind p

Tactic:
injection mem_unique (h₂ h) (rfind_spec hm)

Result:
no goals

Proof state:
p : ℕ →. Bool
n : ℕ
x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
m : ℕ
hm : m ∈ rfind p
⊢ n ∈ rfind p

Tactic:
rcases lt_trichotomy m n with (h | h | h)

Result:
case inl
p : ℕ →. Bool
n : ℕ
x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
m : ℕ
hm : m ∈ rfind p
h : m < n
⊢ n ∈ rfind p

case inr.inl
p : ℕ →. Bool
n : ℕ
x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
m : ℕ
hm : m ∈ rfind p
h : m = n
⊢ n ∈ rfind p

case inr.inr
p : ℕ →. Bool
n : ℕ
x✝ : true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
h₁ : true ∈ p n
h₂ : ∀ {m : ℕ}, m < n → false ∈ p m
m : ℕ
hm : m ∈ rfind p
h : n < m
⊢ n ∈ rfind p
-- Mathlib/Analysis/Convex/Exposed.lean
theorem inter_right (hC : IsExposed 𝕜 B C) (hCA : C ⊆ A) : IsExposed 𝕜 (A ∩ B) C

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B C : Set E
hC : IsExposed 𝕜 B C
hCA : C ⊆ A
⊢ IsExposed 𝕜 (B ∩ A) C

Tactic:
exact hC.inter_left hCA

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B C : Set E
hC : IsExposed 𝕜 B C
hCA : C ⊆ A
⊢ IsExposed 𝕜 (A ∩ B) C

Tactic:
rw [inter_comm]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B C : Set E
hC : IsExposed 𝕜 B C
hCA : C ⊆ A
⊢ IsExposed 𝕜 (B ∩ A) C
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma toReal_toENNReal {x : EReal} (hx : 0 ≤ x) : x.toENNReal.toReal = x.toReal

Proof state:
case pos
x : EReal
hx : 0 ≤ x
h : x = ⊤
⊢ x.toENNReal.toReal = x.toReal

Tactic:
simp [h]

Result:
no goals

Proof state:
case neg
x : EReal
hx : 0 ≤ x
h : ¬x = ⊤
⊢ x.toENNReal.toReal = x.toReal

Tactic:
simp [h, toReal_nonneg hx]

Result:
no goals

Proof state:
x : EReal
hx : 0 ≤ x
⊢ x.toENNReal.toReal = x.toReal

Tactic:
by_cases h : x = ⊤

Result:
case pos
x : EReal
hx : 0 ≤ x
h : x = ⊤
⊢ x.toENNReal.toReal = x.toReal

case neg
x : EReal
hx : 0 ≤ x
h : ¬x = ⊤
⊢ x.toENNReal.toReal = x.toReal
-- Mathlib/Analysis/Calculus/VectorField.lean
theorem lieBracketWithin_of_mem_nhdsWithin (st : t ∈ 𝓝[s] x) (hs : UniqueDiffWithinAt 𝕜 s x)
    (hV : DifferentiableWithinAt 𝕜 V t x) (hW : DifferentiableWithinAt 𝕜 W t x) :
    lieBracketWithin 𝕜 V W s x = lieBracketWithin 𝕜 V W t x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
s t : Set E
x : E
st : t ∈ 𝓝[s] x
hs : UniqueDiffWithinAt 𝕜 s x
hV : DifferentiableWithinAt 𝕜 V t x
hW : DifferentiableWithinAt 𝕜 W t x
⊢ lieBracketWithin 𝕜 V W s x = lieBracketWithin 𝕜 V W t x

Tactic:
simp [lieBracketWithin, fderivWithin_of_mem_nhdsWithin st hs hV,
  fderivWithin_of_mem_nhdsWithin st hs hW]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem find?_range'_eq_some {s n : Nat} {i : Nat} {p : Nat → Bool} :
    (range' s n).find? p = some i ↔ p i ∧ i ∈ range' s n ∧ ∀ j, s ≤ j → j < i → !p j

Proof state:
case mpr
s n i : Nat
p : Nat → Bool
h : p i = true
⊢ ((s ≤ i ∧ i < s + n) ∧ ∀ (j : Nat), s ≤ j → j < i → p j = false) →
    ∃ as,
      (∃ x k, k ≤ n ∧ as = range' s k ∧ s + k = i ∧ 0 < n - k ∧ x = range' (i + 1) (n - k - 1)) ∧
        ∀ (a : Nat), a ∈ as → p a = false

Tactic:
rintro ⟨⟨h₁, h₂⟩, h₃⟩

Result:
case mpr.intro.intro
s n i : Nat
p : Nat → Bool
h : p i = true
h₃ : ∀ (j : Nat), s ≤ j → j < i → p j = false
h₁ : s ≤ i
h₂ : i < s + n
⊢ ∃ as,
    (∃ x k, k ≤ n ∧ as = range' s k ∧ s + k = i ∧ 0 < n - k ∧ x = range' (i + 1) (n - k - 1)) ∧
      ∀ (a : Nat), a ∈ as → p a = false

Proof state:
case mpr.intro.intro.refine_1
s n i : Nat
p : Nat → Bool
h : p i = true
h₃ : ∀ (j : Nat), s ≤ j → j < i → p j = false
h₁ : s ≤ i
h₂ : i < s + n
⊢ i - s ≤ n ∧
    range' s (i - s) = range' s (i - s) ∧
      s + (i - s) = i ∧ 0 < n - (i - s) ∧ range' (i + 1) (n - (i - s) - 1) = range' (i + 1) (n - (i - s) - 1)

Tactic:
simp

Result:
case mpr.intro.intro.refine_1
s n i : Nat
p : Nat → Bool
h : p i = true
h₃ : ∀ (j : Nat), s ≤ j → j < i → p j = false
h₁ : s ≤ i
h₂ : i < s + n
⊢ i - s ≤ n ∧ s + (i - s) = i ∧ 0 < n - (i - s)
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem next : ∀ {s}, Valid s → s.toString.1 = m₁ ++ c :: m₂ →
    s.next ⟨utf8Len m₁⟩ = ⟨utf8Len m₁ + c.utf8Size⟩
  | _, h, e => by
    let ⟨l, m, r, h⟩ := h.validFor
    simp only [h.toString] at e; subst e; simp [h.next]

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✝.next { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + c.utf8Size }

Tactic:
simp [h.next]

Result:
no goals

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

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✝.next { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + c.utf8Size }

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✝.next { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + c.utf8Size }

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✝.next { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + c.utf8Size }

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✝.next { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + c.utf8Size }

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✝.next { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + c.utf8Size }
-- Mathlib/Data/Vector/MapLemmas.lean
theorem mapAccumr₂_mapAccumr_left (f₁ : γ → β → σ₁ → σ₁ × ζ) (f₂ : α → σ₂ → σ₂ × γ) :
    (mapAccumr₂ f₁ (mapAccumr f₂ xs s₂).snd ys s₁)
    = let m := (mapAccumr₂ (fun x y s =>
          let r₂ := f₂ x s.snd
          let r₁ := f₁ r₂.snd y s.fst
          ((r₁.fst, r₂.fst), r₁.snd)
        ) xs ys (s₁, s₂))
      (m.fst.fst, m.snd)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
ys : Vector β n
f₁ : γ → β → σ₁ → σ₁ × ζ
f₂ : α → σ₂ → σ₂ × γ
⊢ mapAccumr₂ f₁ (mapAccumr f₂ xs s₂).2 ys s₁ =
    let m :=
      mapAccumr₂
        (fun x y s =>
          let r₂ := f₂ x s.2;
          let r₁ := f₁ r₂.2 y s.1;
          ((r₁.1, r₂.1), r₁.2))
        xs ys (s₁, s₂);
    (m.1.1, m.2)

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂ <;> simp_all

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem OrthonormalBasis.det_to_matrix_orthonormalBasis : ‖a.toBasis.det b‖ = 1

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
this : (a.toBasis.toMatrix ⇑b).det * star (a.toBasis.toMatrix ⇑b).det = 1
⊢ ‖a.toBasis.det ⇑b‖ = 1

Tactic:
rw [star_def, RCLike.mul_conj] at this

Result:
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
this : ↑‖(a.toBasis.toMatrix ⇑b).det‖ ^ 2 = 1
⊢ ‖a.toBasis.det ⇑b‖ = 1

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
this : ‖(a.toBasis.toMatrix ⇑b).det‖ ^ 2 = 1
⊢ ‖a.toBasis.det ⇑b‖ = 1

Tactic:
rwa [pow_eq_one_iff_of_nonneg (norm_nonneg _) two_ne_zero] at this

Result:
no goals

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
this : ↑‖(a.toBasis.toMatrix ⇑b).det‖ ^ 2 = 1
⊢ ‖a.toBasis.det ⇑b‖ = 1

Tactic:
norm_cast at this

Result:
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
this : ‖(a.toBasis.toMatrix ⇑b).det‖ ^ 2 = 1
⊢ ‖a.toBasis.det ⇑b‖ = 1

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
⊢ ‖a.toBasis.det ⇑b‖ = 1

Tactic:
have := (Matrix.det_of_mem_unitary (a.toMatrix_orthonormalBasis_mem_unitary b)).2

Result:
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
this : (a.toBasis.toMatrix ⇑b).det * star (a.toBasis.toMatrix ⇑b).det = 1
⊢ ‖a.toBasis.det ⇑b‖ = 1
-- Mathlib/GroupTheory/CoprodI.lean
theorem toList_getLast? {i j} (w : NeWord M i j) : w.toList.getLast? = Option.some ⟨j, w.last⟩

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j : ι
w : NeWord M i j
⊢ w.toList.getLast? = some ⟨j, w.last⟩

Tactic:
rw [← Option.mem_def]

Result:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j : ι
w : NeWord M i j
⊢ ⟨j, w.last⟩ ∈ w.toList.getLast?

Proof state:
case append
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : ⟨j✝, _w₁✝.last⟩ ∈ _w₁✝.toList.getLast?
_w₂_ih✝ : ⟨l✝, _w₂✝.last⟩ ∈ _w₂✝.toList.getLast?
⊢ ⟨l✝, (_w₁✝.append _hne✝ _w₂✝).last⟩ ∈ (_w₁✝.append _hne✝ _w₂✝).toList.getLast?

Tactic:
exact List.mem_getLast?_append_of_mem_getLast? (by assumption)

Result:
no goals

Proof state:
case singleton
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
⊢ (singleton x✝ a✝).toList.getLast? = some ⟨i✝, (singleton x✝ a✝).last⟩

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : ⟨j✝, _w₁✝.last⟩ ∈ _w₁✝.toList.getLast?
_w₂_ih✝ : ⟨l✝, _w₂✝.last⟩ ∈ _w₂✝.toList.getLast?
⊢ ⟨l✝, (_w₁✝.append _hne✝ _w₂✝).last⟩ ∈ _w₂✝.toList.getLast?

Tactic:
assumption

Result:
no goals

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j : ι
w : NeWord M i j
⊢ ⟨j, w.last⟩ ∈ w.toList.getLast?

Tactic:
induction w

Result:
case singleton
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
⊢ ⟨i✝, (singleton x✝ a✝).last⟩ ∈ (singleton x✝ a✝).toList.getLast?

case append
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : ⟨j✝, _w₁✝.last⟩ ∈ _w₁✝.toList.getLast?
_w₂_ih✝ : ⟨l✝, _w₂✝.last⟩ ∈ _w₂✝.toList.getLast?
⊢ ⟨l✝, (_w₁✝.append _hne✝ _w₂✝).last⟩ ∈ (_w₁✝.append _hne✝ _w₂✝).toList.getLast?

Proof state:
case singleton
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
⊢ ⟨i✝, (singleton x✝ a✝).last⟩ ∈ (singleton x✝ a✝).toList.getLast?

Tactic:
rw [Option.mem_def]

Result:
case singleton
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
⊢ (singleton x✝ a✝).toList.getLast? = some ⟨i✝, (singleton x✝ a✝).last⟩
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem NNReal.tendsto_algebraMap_inverse_atTop_nhds_zero_nat (𝕜 : Type*) [Semiring 𝕜]
    [Algebra ℝ≥0 𝕜] [TopologicalSpace 𝕜] [ContinuousSMul ℝ≥0 𝕜] :
    Tendsto (algebraMap ℝ≥0 𝕜 ∘ fun n : ℕ ↦ (n : ℝ≥0)⁻¹) atTop (𝓝 0)

Proof state:
𝕜 : Type u_4
inst✝³ : Semiring 𝕜
inst✝² : Algebra ℝ≥0 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : ContinuousSMul ℝ≥0 𝕜
⊢ Tendsto (⇑(algebraMap ℝ≥0 𝕜) ∘ fun n => (↑n)⁻¹) atTop (𝓝 0)

Tactic:
convert (continuous_algebraMap ℝ≥0 𝕜).continuousAt.tendsto.comp
  tendsto_inverse_atTop_nhds_zero_nat

Result:
case h.e'_5.h.e'_3
𝕜 : Type u_4
inst✝³ : Semiring 𝕜
inst✝² : Algebra ℝ≥0 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : ContinuousSMul ℝ≥0 𝕜
⊢ 0 = (algebraMap ℝ≥0 𝕜) 0

Proof state:
case h.e'_5.h.e'_3
𝕜 : Type u_4
inst✝³ : Semiring 𝕜
inst✝² : Algebra ℝ≥0 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : ContinuousSMul ℝ≥0 𝕜
⊢ 0 = (algebraMap ℝ≥0 𝕜) 0

Tactic:
rw [map_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/Charpoly/Basic.lean
theorem pow_eq_aeval_mod_charpoly (k : ℕ) : f ^ k = aeval f (X ^ k %ₘ f.charpoly)

Proof state:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
k : ℕ
⊢ f ^ k = (aeval f) (X ^ k %ₘ f.charpoly)

Tactic:
rw [← aeval_eq_aeval_mod_charpoly, map_pow, aeval_X]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem norm_integral_le_of_norm_le_const [IsFiniteMeasure μ] {f : α → G} {C : ℝ}
    (h : ∀ᵐ x ∂μ, ‖f x‖ ≤ C) : ‖∫ x, f x ∂μ‖ ≤ C * (μ univ).toReal :=
  calc
    ‖∫ x, f x ∂μ‖ ≤ ∫ _, C ∂μ := norm_integral_le_of_norm_le (integrable_const C) h
    _ = C * (μ univ).toReal

Proof state:
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → G
C : ℝ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
⊢ ∫ (x : α), C ∂μ = C * (μ univ).toReal

Tactic:
rw [integral_const, smul_eq_mul, mul_comm]

Result:
no goals