harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem ContinuousLinearEquiv.iteratedFDerivWithin_comp_left (g : F ≃L[𝕜] G) (f : E → F)
    (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) (i : ℕ) :
    iteratedFDerivWithin 𝕜 i (g ∘ f) s x =
      (g : F →L[𝕜] G).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x)

Proof state:
case succ.H
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
g : F ≃L[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : E},
    x ∈ s → iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x = (↑g).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x)
x : E
hx : x ∈ s
m : Fin (i + 1) → E
⊢ (iteratedFDerivWithin 𝕜 (i + 1) (⇑g ∘ f) s x) m =
    ((↑g).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 (i + 1) f s x)) m

Tactic:
rw [iteratedFDerivWithin_succ_apply_left]

Result:
case succ.H
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
g : F ≃L[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : E},
    x ∈ s → iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x = (↑g).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x)
x : E
hx : x ∈ s
m : Fin (i + 1) → E
⊢ ((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s) s x) (m 0)) (tail m) =
    ((↑g).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 (i + 1) f s x)) m
-- Mathlib/Data/Num/Lemmas.lean
theorem pred_succ : ∀ n : ZNum, n.pred.succ = n
  | 0 => rfl
  | ZNum.neg p => show toZNumNeg (pos p).succ'.pred' = _ by rw [PosNum.pred'_succ']; rfl
  | ZNum.pos p => by rw [ZNum.pred, ← toZNum_succ, Num.succ, PosNum.succ'_pred', toZNum]

Proof state:
p : PosNum
⊢ (pos p).toZNumNeg = ZNum.neg p

Tactic:
rfl

Result:
no goals

Proof state:
p : PosNum
⊢ (ZNum.pos p).pred.succ = ZNum.pos p

Tactic:
rw [ZNum.pred, ← toZNum_succ, Num.succ, PosNum.succ'_pred', toZNum]

Result:
no goals

Proof state:
p : PosNum
⊢ (pos p).succ'.pred'.toZNumNeg = ZNum.neg p

Tactic:
rw [PosNum.pred'_succ']

Result:
p : PosNum
⊢ (pos p).toZNumNeg = ZNum.neg p
-- Mathlib/CategoryTheory/Functor/OfSequence.lean
lemma map_id (i : ℕ) : map f i i (by omega) = 𝟙 _

Proof state:
case succ
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n✝ : ℕ
hi : ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)), map f n✝ n✝ ⋯ = 𝟙 (X n✝)
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
⊢ map f (n✝ + 1) (n✝ + 1) ⋯ = 𝟙 (X (n✝ + 1))

Tactic:
apply hi

Result:
no goals

Proof state:
case succ
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n✝ : ℕ
hi : ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)), map f n✝ n✝ ⋯ = 𝟙 (X n✝)
⊢ ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)), map f (n✝ + 1) (n✝ + 1) ⋯ = 𝟙 (X (n✝ + 1))

Tactic:
intro X f

Result:
case succ
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n✝ : ℕ
hi : ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)), map f n✝ n✝ ⋯ = 𝟙 (X n✝)
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
⊢ map f (n✝ + 1) (n✝ + 1) ⋯ = 𝟙 (X (n✝ + 1))

Proof state:
case zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X✝ : ℕ → C
f✝ : (n : ℕ) → X✝ n ⟶ X✝ (n + 1)
⊢ map f✝ 0 0 ⋯ = 𝟙 (X✝ 0)

Tactic:
rfl

Result:
no goals

Proof state:
case zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
⊢ ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)), map f 0 0 ⋯ = 𝟙 (X 0)

Tactic:
intros

Result:
case zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X✝ : ℕ → C
f✝ : (n : ℕ) → X✝ n ⟶ X✝ (n + 1)
⊢ map f✝ 0 0 ⋯ = 𝟙 (X✝ 0)

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
i : ℕ
⊢ ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)), map f i i ⋯ = 𝟙 (X i)

Tactic:
induction i with
| zero => intros; rfl
| succ _ hi =>
    intro X f
    apply hi

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
i : ℕ
⊢ map f i i ⋯ = 𝟙 (X i)

Tactic:
revert X f

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
i : ℕ
⊢ ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)), map f i i ⋯ = 𝟙 (X i)

Proof state:
C : Type u_1
inst✝ : Category.{?u.2973, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
i : ℕ
⊢ i ≤ i

Tactic:
omega

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem div_le_iff' {x y z : ℝ≥0∞} (h1 : y ≠ 0) (h2 : y ≠ ∞) :
    x / y ≤ z ↔ x ≤ y * z

Proof state:
x y z : ℝ≥0∞
h1 : y ≠ 0
h2 : y ≠ ⊤
⊢ x / y ≤ z ↔ x ≤ y * z

Tactic:
rw [mul_comm, ENNReal.div_le_iff h1 h2]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem insertWith.valid_aux [IsTotal α (· ≤ ·)] [DecidableRel (α := α) (· ≤ ·)] (f : α → α) (x : α)
    (hf : ∀ y, x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x) :
    ∀ {t o₁ o₂},
      Valid' o₁ t o₂ →
        Bounded nil o₁ x →
          Bounded nil x o₂ →
            Valid' o₁ (insertWith f x t) o₂ ∧ Raised (size t) (size (insertWith f x t))
  | nil, _, _, _, bl, br => ⟨valid'_singleton bl br, Or.inr rfl⟩
  | node sz l y r, o₁, o₂, h, bl, br => by
    rw [insertWith, cmpLE]
    split_ifs with h_1 h_2 <;> dsimp only
    · rcases h with ⟨⟨lx, xr⟩, hs, hb⟩
      rcases hf _ ⟨h_1, h_2⟩ with ⟨xf, fx⟩
      refine
        ⟨⟨⟨lx.mono_right (le_trans h_2 xf), xr.mono_left (le_trans fx h_1)⟩, hs, hb⟩, Or.inl rfl⟩
    · rcases insertWith.valid_aux f x hf h.left bl (lt_of_le_not_le h_1 h_2) with ⟨vl, e⟩
      suffices H : _ by
        refine ⟨vl.balanceL h.right H, ?_⟩
        rw [size_balanceL vl.3 h.3.2.2 vl.2 h.2.2.2 H, h.2.size_eq]
        exact (e.add_right _).add_right _
      exact Or.inl ⟨_, e, h.3.1⟩
    · have : y < x := lt_of_le_not_le ((total_of (· ≤ ·) _ _).resolve_left h_1) h_1
      rcases insertWith.valid_aux f x hf h.right this br with ⟨vr, e⟩
      suffices H : _ by
        refine ⟨h.left.balanceR vr H, ?_⟩
        rw [size_balanceR h.3.2.1 vr.3 h.2.2.1 vr.2 H, h.2.size_eq]
        exact (e.add_left _).add_right _
      exact Or.inr ⟨_, e, h.3.1⟩

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : IsTotal α fun x1 x2 => x1 ≤ x2
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : nil.Bounded o₁ ↑x
br : nil.Bounded (↑x) o₂
h_1 : x ≤ y
h_2 : ¬y ≤ x
vl : Valid' o₁ (insertWith f x l) ↑y
e : Raised l.size (insertWith f x l).size
H : ?m.300294
⊢ Valid' o₁ ((insertWith f x l).balanceL y r) o₂ ∧ Raised (node sz l y r).size ((insertWith f x l).balanceL y r).size

Tactic:
refine ⟨vl.balanceL h.right H, ?_⟩

Result:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : IsTotal α fun x1 x2 => x1 ≤ x2
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
f : α → α
x : α
hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x
sz : ℕ
l : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ (node sz l y r) o₂
bl : nil.Bounded o₁ ↑x
br : nil.Bounded (↑x) o₂
h_1 : x ≤ y
h_2 : ¬y ≤ x
vl : Valid' o₁ (insertWith f x l) ↑y
e : Raised l.size (insertWith f x l).size
H :
  (∃ l', Raised l' (insertWith f x l).size ∧ BalancedSz l' r.size) ∨
    ∃ r', Raised r.size r' ∧ BalancedSz (insertWith f x l).size r'
⊢ Raised (node sz l y r).size ((insertWith f x l).balanceL y r).size
-- Mathlib/RingTheory/Derivation/Basic.lean
lemma liftOfRightInverse_eq {f : F} {f_inv₁ f_inv₂ : M → A} (hf₁ : Function.RightInverse f_inv₁ f)
    (hf₂ : Function.RightInverse f_inv₂ f) :
    liftOfRightInverse hf₁ = liftOfRightInverse hf₂

Proof state:
case h.h.H.intro
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
f_inv₁ f_inv₂ : M → A
hf₁ : Function.RightInverse f_inv₁ ⇑f
hf₂ : Function.RightInverse f_inv₂ ⇑f
x✝¹ : Derivation R A A
x✝ : ∀ (x : A), f x = 0 → f (x✝¹ x) = 0
x : A
⊢ (liftOfRightInverse hf₁ x✝) (f x) = (liftOfRightInverse hf₂ x✝) (f x)

Tactic:
simp

Result:
no goals

Proof state:
case h.h.H
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
f_inv₁ f_inv₂ : M → A
hf₁ : Function.RightInverse f_inv₁ ⇑f
hf₂ : Function.RightInverse f_inv₂ ⇑f
x✝¹ : Derivation R A A
x✝ : ∀ (x : A), f x = 0 → f (x✝¹ x) = 0
x : M
⊢ (liftOfRightInverse hf₁ x✝) x = (liftOfRightInverse hf₂ x✝) x

Tactic:
obtain ⟨x, rfl⟩ := hf₁.surjective x

Result:
case h.h.H.intro
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
f_inv₁ f_inv₂ : M → A
hf₁ : Function.RightInverse f_inv₁ ⇑f
hf₂ : Function.RightInverse f_inv₂ ⇑f
x✝¹ : Derivation R A A
x✝ : ∀ (x : A), f x = 0 → f (x✝¹ x) = 0
x : A
⊢ (liftOfRightInverse hf₁ x✝) (f x) = (liftOfRightInverse hf₂ x✝) (f x)

Proof state:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
f_inv₁ f_inv₂ : M → A
hf₁ : Function.RightInverse f_inv₁ ⇑f
hf₂ : Function.RightInverse f_inv₂ ⇑f
⊢ liftOfRightInverse hf₁ = liftOfRightInverse hf₂

Tactic:
ext _ _ x

Result:
case h.h.H
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
f_inv₁ f_inv₂ : M → A
hf₁ : Function.RightInverse f_inv₁ ⇑f
hf₂ : Function.RightInverse f_inv₂ ⇑f
x✝¹ : Derivation R A A
x✝ : ∀ (x : A), f x = 0 → f (x✝¹ x) = 0
x : M
⊢ (liftOfRightInverse hf₁ x✝) x = (liftOfRightInverse hf₂ x✝) x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem sub_eq_max_sub (n m : Nat) : n - m = max n m - m

Proof state:
case inl
n m : Nat
h : m ≤ n
⊢ n - m = max n m - m

Tactic:
rw [Nat.max_eq_left h]

Result:
no goals

Proof state:
n m : Nat
⊢ n - m = max n m - m

Tactic:
cases Nat.le_total m n with
| inl h => rw [Nat.max_eq_left h]
| inr h => rw [Nat.max_eq_right h, Nat.sub_eq_zero_of_le h, Nat.sub_self]

Result:
no goals

Proof state:
case inr
n m : Nat
h : n ≤ m
⊢ n - m = max n m - m

Tactic:
rw [Nat.max_eq_right h, Nat.sub_eq_zero_of_le h, Nat.sub_self]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Intervals.lean
@[to_additive]
lemma prod_Ico_mul_eq_prod_Icc (h : a ≤ b) : (∏ x ∈ Ico a b, f x) * f b = ∏ x ∈ Icc a b, f x

Proof state:
α : Type u_1
M : Type u_2
inst✝² : PartialOrder α
inst✝¹ : CommMonoid M
f : α → M
a b : α
inst✝ : LocallyFiniteOrder α
h : a ≤ b
⊢ (∏ x ∈ Ico a b, f x) * f b = ∏ x ∈ Icc a b, f x

Tactic:
rw [mul_comm, mul_prod_Ico_eq_prod_Icc h]

Result:
no goals
-- Mathlib/Probability/Moments/Basic.lean
theorem mgf_smul_left (α : ℝ) : mgf (α • X) μ t = mgf X μ (α * t)

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
⊢ mgf (α • X) μ t = mgf X μ (α * t)

Tactic:
simp_rw [mgf, Pi.smul_apply, smul_eq_mul, mul_comm α t, mul_assoc]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Enum.lean
theorem enumOrd_le_of_forall_lt (ha : a ∈ s) (H : ∀ b < o, enumOrd s b < a) : enumOrd s o ≤ a

Proof state:
o a : Ordinal.{u}
s : Set Ordinal.{u}
ha : a ∈ s
H : ∀ b < o, enumOrd s b < a
⊢ enumOrd s o ≤ a

Tactic:
rw [enumOrd]

Result:
o a : Ordinal.{u}
s : Set Ordinal.{u}
ha : a ∈ s
H : ∀ b < o, enumOrd s b < a
⊢ sInf (s ∩ {b | ∀ c < o, enumOrd s c < b}) ≤ a

Proof state:
o a : Ordinal.{u}
s : Set Ordinal.{u}
ha : a ∈ s
H : ∀ b < o, enumOrd s b < a
⊢ sInf (s ∩ {b | ∀ c < o, enumOrd s c < b}) ≤ a

Tactic:
exact csInf_le' ⟨ha, H⟩

Result:
no goals
-- Mathlib/Data/Fintype/Pi.lean
lemma piDiag_subset_piFinset [DecidableEq ι] [Fintype ι] :
    s.piDiag ι ⊆ Fintype.piFinset fun _ ↦ s

Proof state:
α : Type u_1
ι : Type u_3
inst✝² : DecidableEq (ι → α)
s : Finset α
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ s.piDiag ι ⊆ Fintype.piFinset fun x => s

Tactic:
simp [← piFinset_filter_const]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem nf_repr_split {o o' m} [NF o] (h : split o = (o', m)) : NF o' ∧ repr o = repr o' + m

Proof state:
case mk.intro
o : ONote
m : ℕ
inst✝ : o.NF
a : ONote
s₁ : a.NF
e : o.split' = (a, m)
s₂ : o.repr = ω * a.repr + ↑m
⊢ (scale 1 a).NF ∧ o.repr = (scale 1 a).repr + ↑m

Tactic:
simp only [repr_scale, repr_one, Nat.cast_one, opow_one, ← s₂, and_true]

Result:
case mk.intro
o : ONote
m : ℕ
inst✝ : o.NF
a : ONote
s₁ : a.NF
e : o.split' = (a, m)
s₂ : o.repr = ω * a.repr + ↑m
⊢ (scale 1 a).NF

Proof state:
case mk.intro
o o' : ONote
m : ℕ
inst✝ : o.NF
a : ONote
n : ℕ
e : o.split' = (a, n)
s₁ : a.NF
s₂ : o.repr = ω * a.repr + ↑n
fst_eq✝ : scale 1 a = o'
snd_eq✝ : n = m
⊢ o'.NF ∧ o.repr = o'.repr + ↑m

Tactic:
substs o' n

Result:
case mk.intro
o : ONote
m : ℕ
inst✝ : o.NF
a : ONote
s₁ : a.NF
e : o.split' = (a, m)
s₂ : o.repr = ω * a.repr + ↑m
⊢ (scale 1 a).NF ∧ o.repr = (scale 1 a).repr + ↑m

Proof state:
case mk
o o' : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (o', m)
a : ONote
n : ℕ
e : o.split' = (a, n)
⊢ o'.NF ∧ o.repr = o'.repr + ↑m

Tactic:
obtain ⟨s₁, s₂⟩ := nf_repr_split' e

Result:
case mk.intro
o o' : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (o', m)
a : ONote
n : ℕ
e : o.split' = (a, n)
s₁ : a.NF
s₂ : o.repr = ω * a.repr + ↑n
⊢ o'.NF ∧ o.repr = o'.repr + ↑m

Proof state:
case mk.intro
o o' : ONote
m : ℕ
inst✝ : o.NF
a : ONote
n : ℕ
h : (scale 1 a, n) = (o', m)
e : o.split' = (a, n)
s₁ : a.NF
s₂ : o.repr = ω * a.repr + ↑n
⊢ o'.NF ∧ o.repr = o'.repr + ↑m

Tactic:
injection h

Result:
case mk.intro
o o' : ONote
m : ℕ
inst✝ : o.NF
a : ONote
n : ℕ
e : o.split' = (a, n)
s₁ : a.NF
s₂ : o.repr = ω * a.repr + ↑n
fst_eq✝ : scale 1 a = o'
snd_eq✝ : n = m
⊢ o'.NF ∧ o.repr = o'.repr + ↑m

Proof state:
case mk.intro
o o' : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (o', m)
a : ONote
n : ℕ
e : o.split' = (a, n)
s₁ : a.NF
s₂ : o.repr = ω * a.repr + ↑n
⊢ o'.NF ∧ o.repr = o'.repr + ↑m

Tactic:
rw [split_eq_scale_split' e] at h

Result:
case mk.intro
o o' : ONote
m : ℕ
inst✝ : o.NF
a : ONote
n : ℕ
h : (scale 1 a, n) = (o', m)
e : o.split' = (a, n)
s₁ : a.NF
s₂ : o.repr = ω * a.repr + ↑n
⊢ o'.NF ∧ o.repr = o'.repr + ↑m

Proof state:
case mk.intro
o : ONote
m : ℕ
inst✝ : o.NF
a : ONote
s₁ : a.NF
e : o.split' = (a, m)
s₂ : o.repr = ω * a.repr + ↑m
⊢ (scale 1 a).NF

Tactic:
infer_instance

Result:
no goals

Proof state:
o o' : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (o', m)
⊢ o'.NF ∧ o.repr = o'.repr + ↑m

Tactic:
rcases e : split' o with ⟨a, n⟩

Result:
case mk
o o' : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (o', m)
a : ONote
n : ℕ
e : o.split' = (a, n)
⊢ o'.NF ∧ o.repr = o'.repr + ↑m
-- Mathlib/LinearAlgebra/Matrix/DotProduct.lean
lemma self_mul_conjTranspose_mul_eq_zero {p} (A : Matrix m n R) (B : Matrix m p R) :
    (A * Aᴴ) * B = 0 ↔ Aᴴ * B = 0

Proof state:
m : Type u_1
n : Type u_2
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
p : Type u_5
A : Matrix m n R
B : Matrix m p R
⊢ A * Aᴴ * B = 0 ↔ Aᴴ * B = 0

Tactic:
simpa only [conjTranspose_conjTranspose] using conjTranspose_mul_self_mul_eq_zero Aᴴ _

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem norm_eq_norm (x : K) :
    mixedEmbedding.norm (mixedEmbedding K x) = |Algebra.norm ℚ x|

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ mixedEmbedding.norm ((mixedEmbedding K) x) = ↑|(Algebra.norm ℚ) x|

Tactic:
simp_rw [mixedEmbedding.norm_apply, normAtPlace_apply, prod_eq_abs_norm]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem mem_cyclicPermutations_iff : l ∈ cyclicPermutations l' ↔ l ~r l'

Proof state:
case mpr
α : Type u
l l' : List α
⊢ l ~r l' → l ∈ l'.cyclicPermutations

Tactic:
rintro ⟨k, rfl⟩

Result:
case mpr.intro
α : Type u
l : List α
k : ℕ
⊢ l ∈ (l.rotate k).cyclicPermutations

Proof state:
case mp.intro
α : Type u
l' : List α
k : Fin l'.cyclicPermutations.length
⊢ l'.rotate ↑k ~r l'

Tactic:
exact .forall _ _

Result:
no goals

Proof state:
case mpr.intro
α : Type u
l : List α
k : ℕ
⊢ l ∈ (l.rotate k).cyclicPermutations

Tactic:
rw [cyclicPermutations_rotate, mem_rotate]

Result:
case mpr.intro
α : Type u
l : List α
k : ℕ
⊢ l ∈ l.cyclicPermutations

Proof state:
case mp
α : Type u
l l' : List α
⊢ (∃ n, l'.rotate ↑n = l) → l ~r l'

Tactic:
rintro ⟨k, rfl⟩

Result:
case mp.intro
α : Type u
l' : List α
k : Fin l'.cyclicPermutations.length
⊢ l'.rotate ↑k ~r l'

Proof state:
case mpr.intro
α : Type u
l : List α
k : ℕ
⊢ l ∈ l.cyclicPermutations

Tactic:
apply mem_cyclicPermutations_self

Result:
no goals

Proof state:
case mp
α : Type u
l l' : List α
⊢ l ∈ l'.cyclicPermutations → l ~r l'

Tactic:
simp_rw [mem_iff_get, get_cyclicPermutations]

Result:
case mp
α : Type u
l l' : List α
⊢ (∃ n, l'.rotate ↑n = l) → l ~r l'

Proof state:
α : Type u
l l' : List α
⊢ l ∈ l'.cyclicPermutations ↔ l ~r l'

Tactic:
constructor

Result:
case mp
α : Type u
l l' : List α
⊢ l ∈ l'.cyclicPermutations → l ~r l'

case mpr
α : Type u
l l' : List α
⊢ l ~r l' → l ∈ l'.cyclicPermutations
-- Mathlib/MeasureTheory/OuterMeasure/Induced.lean
theorem extend_union {s₁ s₂ : Set α} (hd : Disjoint s₁ s₂) (h₁ : P s₁) (h₂ : P s₂) :
    extend m (s₁ ∪ s₂) = extend m s₁ + extend m s₂

Proof state:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s₁ s₂ : Set α
hd : Disjoint s₁ s₂
h₁ : P s₁
h₂ : P s₂
⊢ ∑ b : Bool, extend m (bif b then s₁ else s₂) = extend m s₁ + extend m s₂

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s₁ s₂ : Set α
hd : Disjoint s₁ s₂
h₁ : P s₁
h₂ : P s₂
⊢ extend m (s₁ ∪ s₂) = extend m s₁ + extend m s₂

Tactic:
rw [union_eq_iUnion,
  extend_iUnion P0 m0 PU mU (pairwise_disjoint_on_bool.2 hd) (Bool.forall_bool.2 ⟨h₂, h₁⟩),
  tsum_fintype]

Result:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s₁ s₂ : Set α
hd : Disjoint s₁ s₂
h₁ : P s₁
h₂ : P s₂
⊢ ∑ b : Bool, extend m (bif b then s₁ else s₂) = extend m s₁ + extend m s₂
-- Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean
@[to_additive le_sum_nonempty_of_subadditive_on_pred]
lemma le_prod_nonempty_of_submultiplicative_on_pred (f : α → β) (p : α → Prop)
    (h_mul : ∀ a b, p a → p b → f (a * b) ≤ f a * f b) (hp_mul : ∀ a b, p a → p b → p (a * b))
    (s : Multiset α) (hs_nonempty : s ≠ ∅) (hs : ∀ a, a ∈ s → p a) : f s.prod ≤ (s.map f).prod

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
⊢ ∀ (s : Multiset α), s ≠ ∅ → (∀ a ∈ s, p a) → f s.prod ≤ (map f s).prod

Tactic:
refine Multiset.induction ?_ ?_

Result:
case refine_1
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
⊢ 0 ≠ ∅ → (∀ a ∈ 0, p a) → f (prod 0) ≤ (map f 0).prod

case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
⊢ ∀ (a : α) (s : Multiset α),
    (s ≠ ∅ → (∀ a ∈ s, p a) → f s.prod ≤ (map f s).prod) →
      a ::ₘ s ≠ ∅ → (∀ a_2 ∈ a ::ₘ s, p a_2) → f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod

Proof state:
case refine_1
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
⊢ 0 ≠ ∅ → (∀ a ∈ 0, p a) → f (prod 0) ≤ (map f 0).prod

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/l2Space.lean
theorem summable_of_lp (f : lp G 2) :
    Summable fun i => V i (f i)

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
⊢ Summable fun i => (V i) (↑f i)

Tactic:
rw [hV.summable_iff_norm_sq_summable]

Result:
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
⊢ Summable fun i => ‖↑f i‖ ^ 2

Proof state:
case h.e'_5.h
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
x✝ : ι
⊢ ‖↑f x✝‖ ^ 2 = ‖↑f x✝‖ ^ ENNReal.toReal 2

Tactic:
norm_cast

Result:
no goals

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
⊢ Summable fun i => ‖↑f i‖ ^ 2

Tactic:
convert (lp.memℓp f).summable _

Result:
case h.e'_5.h
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
x✝ : ι
⊢ ‖↑f x✝‖ ^ 2 = ‖↑f x✝‖ ^ ENNReal.toReal 2

ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
⊢ 0 < ENNReal.toReal 2

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
⊢ 0 < ENNReal.toReal 2

Tactic:
norm_num

Result:
no goals