harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem Ordered.upperBound?_exists [@TransCmp α cmp] [IsCut cmp cut] (h : Ordered cmp t) :
    (∃ x, t.upperBound? cut = some x) ↔ ∃ x ∈ t, cut x ≠ .gt

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
h : Ordered cmp t
H : ∃ x, x ∈ t ∧ cut x ≠ Ordering.gt
⊢ ∃ x, upperBound? cut t = some x

Tactic:
obtain ⟨x, hx, e⟩ := H

Result:
case intro.intro
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
h : Ordered cmp t
x : α
hx : x ∈ t
e : cut x ≠ Ordering.gt
⊢ ∃ x, upperBound? cut t = some x

Proof state:
case intro.intro.node.h_3
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : Ordered cmp l✝ → ∀ (x : α), x ∈ l✝ → cut x ≠ Ordering.gt → ∃ x, upperBound? cut l✝ = some x
ihr : Ordered cmp r✝ → ∀ (x : α), x ∈ r✝ → cut x ≠ Ordering.gt → ∃ x, upperBound? cut r✝ = some x
h : Ordered cmp (node c✝ l✝ v✝ r✝)
x : α
hx : x ∈ node c✝ l✝ v✝ r✝
e : cut x ≠ Ordering.gt
x✝ : Ordering
heq✝ : cut v✝ = Ordering.eq
⊢ ∃ x, some v✝ = some x

Tactic:
exact ⟨_, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : Ordered cmp l✝ → ∀ (x : α), x ∈ l✝ → cut x ≠ Ordering.gt → ∃ x, upperBound? cut l✝ = some x
ihr : Ordered cmp r✝ → ∀ (x : α), x ∈ r✝ → cut x ≠ Ordering.gt → ∃ x, upperBound? cut r✝ = some x
h : Ordered cmp (node c✝ l✝ v✝ r✝)
x : α
e : cut x ≠ Ordering.gt
x✝ : Ordering
hv : cut v✝ = Ordering.gt
hx : Any (fun x_1 => x = x_1) l✝
⊢ ∃ x, upperBound? cut r✝ = some x

Tactic:
cases e <| IsCut.gt_trans (All_def.1 h.1 _ hx).1 hv

Result:
no goals

Proof state:
case intro.intro.node
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : Ordered cmp l✝ → ∀ (x : α), x ∈ l✝ → cut x ≠ Ordering.gt → ∃ x, upperBound? cut l✝ = some x
ihr : Ordered cmp r✝ → ∀ (x : α), x ∈ r✝ → cut x ≠ Ordering.gt → ∃ x, upperBound? cut r✝ = some x
h : Ordered cmp (node c✝ l✝ v✝ r✝)
x : α
hx : x ∈ node c✝ l✝ v✝ r✝
e : cut x ≠ Ordering.gt
⊢ ∃ x, upperBound? cut (node c✝ l✝ v✝ r✝) = some x

Tactic:
simp [upperBound?]

Result:
case intro.intro.node
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : Ordered cmp l✝ → ∀ (x : α), x ∈ l✝ → cut x ≠ Ordering.gt → ∃ x, upperBound? cut l✝ = some x
ihr : Ordered cmp r✝ → ∀ (x : α), x ∈ r✝ → cut x ≠ Ordering.gt → ∃ x, upperBound? cut r✝ = some x
h : Ordered cmp (node c✝ l✝ v✝ r✝)
x : α
hx : x ∈ node c✝ l✝ v✝ r✝
e : cut x ≠ Ordering.gt
⊢ ∃ x,
    (match cut v✝ with
      | Ordering.lt => upperBound? cut l✝ (some v✝)
      | Ordering.gt => upperBound? cut r✝
      | Ordering.eq => some v✝) =
      some x
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
lemma IsMatching.induce_connectedComponent (h : M.IsMatching) (c : ConnectedComponent G) :
    (M.induce (M.verts ∩ c.supp)).IsMatching

Proof state:
case intro.intro.intro
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v✝ : V
hv : v✝ ∈ M.verts
w : V
hvw : M.Adj v✝ w
hw : ∀ (y : V), (fun w => M.Adj v✝ w) y → y = w
⊢ ∃! w, (M.induce (M.verts ∩ (G.connectedComponentMk v✝).supp)).Adj v✝ w

Tactic:
use w

Result:
case h
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v✝ : V
hv : v✝ ∈ M.verts
w : V
hvw : M.Adj v✝ w
hw : ∀ (y : V), (fun w => M.Adj v✝ w) y → y = w
⊢ (fun w => (M.induce (M.verts ∩ (G.connectedComponentMk v✝).supp)).Adj v✝ w) w ∧
    ∀ (y : V), (fun w => (M.induce (M.verts ∩ (G.connectedComponentMk v✝).supp)).Adj v✝ w) y → y = w

Proof state:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
c : G.ConnectedComponent
⊢ (M.induce (M.verts ∩ c.supp)).IsMatching

Tactic:
intro _ hv

Result:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
c : G.ConnectedComponent
v✝ : V
hv : v✝ ∈ (M.induce (M.verts ∩ c.supp)).verts
⊢ ∃! w, (M.induce (M.verts ∩ c.supp)).Adj v✝ w

Proof state:
case h
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v✝ : V
hv : v✝ ∈ M.verts
w : V
hvw : M.Adj v✝ w
hw : ∀ (y : V), (fun w => M.Adj v✝ w) y → y = w
⊢ (fun w => (M.induce (M.verts ∩ (G.connectedComponentMk v✝).supp)).Adj v✝ w) w ∧
    ∀ (y : V), (fun w => (M.induce (M.verts ∩ (G.connectedComponentMk v✝).supp)).Adj v✝ w) y → y = w

Tactic:
simpa [hv, hvw, M.edge_vert hvw.symm, (M.adj_sub hvw).symm.reachable] using fun _ _ _ ↦ hw _

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
c : G.ConnectedComponent
v✝ : V
hv : v✝ ∈ (M.induce (M.verts ∩ c.supp)).verts
⊢ ∃! w, (M.induce (M.verts ∩ c.supp)).Adj v✝ w

Tactic:
obtain ⟨hv, rfl⟩ := hv

Result:
case intro
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v✝ : V
hv : v✝ ∈ M.verts
⊢ ∃! w, (M.induce (M.verts ∩ (G.connectedComponentMk v✝).supp)).Adj v✝ w

Proof state:
case intro
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v✝ : V
hv : v✝ ∈ M.verts
⊢ ∃! w, (M.induce (M.verts ∩ (G.connectedComponentMk v✝).supp)).Adj v✝ w

Tactic:
obtain ⟨w, hvw, hw⟩ := h hv

Result:
case intro.intro.intro
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v✝ : V
hv : v✝ ∈ M.verts
w : V
hvw : M.Adj v✝ w
hw : ∀ (y : V), (fun w => M.Adj v✝ w) y → y = w
⊢ ∃! w, (M.induce (M.verts ∩ (G.connectedComponentMk v✝).supp)).Adj v✝ w
-- Mathlib/Probability/Independence/Kernel.lean
@[to_additive]
lemma iIndepFun.indepFun_mul_left (hf_indep : iIndepFun (fun _ ↦ m) f κ μ)
    (hf_meas : ∀ i, Measurable (f i)) (i j k : ι) (hik : i ≠ k) (hjk : j ≠ k) :
    IndepFun (f i * f j) (f k) κ μ

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst✝¹ : Mul β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_indep : iIndepFun (fun x => m) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
this : IndepFun (fun ω => (f i ω, f j ω)) (f k) κ μ
⊢ IndepFun (f i * f j) (f k) κ μ

Tactic:
simpa using this.comp (measurable_fst.mul measurable_snd) measurable_id

Result:
no goals

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst✝¹ : Mul β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_indep : iIndepFun (fun x => m) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
⊢ IndepFun (f i * f j) (f k) κ μ

Tactic:
have : IndepFun (fun ω => (f i ω, f j ω)) (f k) κ μ :=
  hf_indep.indepFun_prod_mk hf_meas i j k hik hjk

Result:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst✝¹ : Mul β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_indep : iIndepFun (fun x => m) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
this : IndepFun (fun ω => (f i ω, f j ω)) (f k) κ μ
⊢ IndepFun (f i * f j) (f k) κ μ
-- Mathlib/Analysis/Normed/Group/Quotient.lean
theorem lift_unique {N : Type*} [SeminormedAddCommGroup N] (S : AddSubgroup M)
    (f : NormedAddGroupHom M N) (hf : ∀ s ∈ S, f s = 0) (g : NormedAddGroupHom (M ⧸ S) N)
    (h : g.comp S.normedMk = f) : g = lift S f hf

Proof state:
M : Type u_1
inst✝¹ : SeminormedAddCommGroup M
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ s ∈ S, f s = 0
g : NormedAddGroupHom (M ⧸ S) N
h : g.comp S.normedMk = f
⊢ g = lift S f hf

Tactic:
ext x

Result:
case H
M : Type u_1
inst✝¹ : SeminormedAddCommGroup M
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ s ∈ S, f s = 0
g : NormedAddGroupHom (M ⧸ S) N
h : g.comp S.normedMk = f
x : M ⧸ S
⊢ g x = (lift S f hf) x

Proof state:
case H.intro
M : Type u_1
inst✝¹ : SeminormedAddCommGroup M
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ s ∈ S, f s = 0
g : NormedAddGroupHom (M ⧸ S) N
h : g.comp S.normedMk = f
x : M
⊢ f x = (lift S f hf) (S.normedMk x)

Tactic:
rfl

Result:
no goals

Proof state:
case H.intro
M : Type u_1
inst✝¹ : SeminormedAddCommGroup M
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ s ∈ S, f s = 0
g : NormedAddGroupHom (M ⧸ S) N
h : g.comp S.normedMk = f
x : M
⊢ (g.comp S.normedMk) x = (lift S f hf) (S.normedMk x)

Tactic:
simp only [h]

Result:
case H.intro
M : Type u_1
inst✝¹ : SeminormedAddCommGroup M
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ s ∈ S, f s = 0
g : NormedAddGroupHom (M ⧸ S) N
h : g.comp S.normedMk = f
x : M
⊢ f x = (lift S f hf) (S.normedMk x)

Proof state:
case H.intro
M : Type u_1
inst✝¹ : SeminormedAddCommGroup M
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ s ∈ S, f s = 0
g : NormedAddGroupHom (M ⧸ S) N
h : g.comp S.normedMk = f
x : M
⊢ g (S.normedMk x) = (lift S f hf) (S.normedMk x)

Tactic:
change g.comp S.normedMk x = _

Result:
case H.intro
M : Type u_1
inst✝¹ : SeminormedAddCommGroup M
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ s ∈ S, f s = 0
g : NormedAddGroupHom (M ⧸ S) N
h : g.comp S.normedMk = f
x : M
⊢ (g.comp S.normedMk) x = (lift S f hf) (S.normedMk x)

Proof state:
case H
M : Type u_1
inst✝¹ : SeminormedAddCommGroup M
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ s ∈ S, f s = 0
g : NormedAddGroupHom (M ⧸ S) N
h : g.comp S.normedMk = f
x : M ⧸ S
⊢ g x = (lift S f hf) x

Tactic:
rcases AddSubgroup.surjective_normedMk _ x with ⟨x, rfl⟩

Result:
case H.intro
M : Type u_1
inst✝¹ : SeminormedAddCommGroup M
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ s ∈ S, f s = 0
g : NormedAddGroupHom (M ⧸ S) N
h : g.comp S.normedMk = f
x : M
⊢ g (S.normedMk x) = (lift S f hf) (S.normedMk x)
-- Mathlib/Algebra/Homology/HomotopyCofiber.lean
@[reassoc (attr := simp)]
lemma inrX_sndX (i : ι) : inrX φ i ≫ sndX φ i = 𝟙 _

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i : ι
⊢ inrX φ i ≫ sndX φ i = 𝟙 (G.X i)

Tactic:
dsimp [sndX, inrX]

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i : ι
⊢ ((if hi : c.Rel i (c.next i) then biprod.inr ≫ (XIsoBiprod φ i (c.next i) hi).inv else (XIso φ i hi).inv) ≫
      if hi : c.Rel i (c.next i) then (XIsoBiprod φ i (c.next i) hi).hom ≫ biprod.snd else (XIso φ i hi).hom) =
    𝟙 (G.X i)

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i : ι
⊢ ((if hi : c.Rel i (c.next i) then biprod.inr ≫ (XIsoBiprod φ i (c.next i) hi).inv else (XIso φ i hi).inv) ≫
      if hi : c.Rel i (c.next i) then (XIsoBiprod φ i (c.next i) hi).hom ≫ biprod.snd else (XIso φ i hi).hom) =
    𝟙 (G.X i)

Tactic:
split_ifs with hi <;> simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
@[simp]
lemma leadingCoeff_Ψ₂Sq (h : (4 : R) ≠ 0) : W.Ψ₂Sq.leadingCoeff = 4

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
h : 4 ≠ 0
⊢ W.Ψ₂Sq.leadingCoeff = 4

Tactic:
rw [leadingCoeff, W.natDegree_Ψ₂Sq h, coeff_Ψ₂Sq]

Result:
no goals
-- Mathlib/Probability/Martingale/Centering.lean
theorem predictablePart_bdd_difference {R : ℝ≥0} {f : ℕ → Ω → ℝ} (ℱ : Filtration ℕ m0)
    (hbdd : ∀ᵐ ω ∂μ, ∀ i, |f (i + 1) ω - f i ω| ≤ R) :
    ∀ᵐ ω ∂μ, ∀ i, |predictablePart f ℱ μ (i + 1) ω - predictablePart f ℱ μ i ω| ≤ R

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
R : ℝ≥0
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(μ[f (i + 1) - f i|↑ℱ i]) ω| ≤ ↑R

Tactic:
exact ae_all_iff.2 fun i => ae_bdd_condExp_of_ae_bdd <| ae_all_iff.1 hbdd i

Result:
no goals

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
R : ℝ≥0
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |predictablePart f ℱ μ (i + 1) ω - predictablePart f ℱ μ i ω| ≤ ↑R

Tactic:
simp_rw [predictablePart, Finset.sum_apply, Finset.sum_range_succ_sub_sum]

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
R : ℝ≥0
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(μ[f (i + 1) - f i|↑ℱ i]) ω| ≤ ↑R
-- Mathlib/Analysis/Normed/Group/Int.lean
theorem nnnorm_zpow_le_mul_norm (n : ℤ) (a : α) : ‖a ^ n‖₊ ≤ ‖n‖₊ * ‖a‖₊

Proof state:
α : Type u_1
inst✝ : SeminormedCommGroup α
n : ℤ
a : α
⊢ ‖a ^ n‖₊ ≤ ‖n‖₊ * ‖a‖₊

Tactic:
simpa only [← NNReal.coe_le_coe, NNReal.coe_mul] using norm_zpow_le_mul_norm n a

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem normSq_eq_zero : normSq a = 0 ↔ a = 0

Proof state:
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
⊢ normSq a = 0 ↔ a = 0

Tactic:
refine ⟨fun h => ?_, fun h => h.symm ▸ normSq.map_zero⟩

Result:
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : normSq a = 0
⊢ a = 0

Proof state:
case ha
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : (a.re ^ 2 + a.imI ^ 2 = 0 ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.re ^ 2

case hb
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : (a.re ^ 2 + a.imI ^ 2 = 0 ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.imI ^ 2

case ha
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 = 0 ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.re ^ 2 + a.imI ^ 2

case hb
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 = 0 ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.imJ ^ 2

case ha
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2 = 0
⊢ 0 ≤ a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2

case hb
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2 = 0
⊢ 0 ≤ a.imK ^ 2

Tactic:
all_goals apply_rules [sq_nonneg, add_nonneg]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : ((a.re ^ 2 = 0 ∧ a.imI ^ 2 = 0) ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0
⊢ a = 0

Tactic:
exact ext a 0 (pow_eq_zero h.1.1.1) (pow_eq_zero h.1.1.2) (pow_eq_zero h.1.2) (pow_eq_zero h.2)

Result:
no goals

Proof state:
case hb
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2 = 0
⊢ 0 ≤ a.imK ^ 2

Tactic:
apply_rules [sq_nonneg, add_nonneg]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : normSq a = 0
⊢ a = 0

Tactic:
rw [normSq_def', add_eq_zero_iff_of_nonneg, add_eq_zero_iff_of_nonneg, add_eq_zero_iff_of_nonneg]
  at h

Result:
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : ((a.re ^ 2 = 0 ∧ a.imI ^ 2 = 0) ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0
⊢ a = 0

case ha
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : (a.re ^ 2 + a.imI ^ 2 = 0 ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.re ^ 2

case hb
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : (a.re ^ 2 + a.imI ^ 2 = 0 ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.imI ^ 2

case ha
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 = 0 ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.re ^ 2 + a.imI ^ 2

case hb
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 = 0 ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.imJ ^ 2

case ha
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2 = 0
⊢ 0 ≤ a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2

case hb
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2 = 0
⊢ 0 ≤ a.imK ^ 2
-- Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean
theorem sumIDeriv_apply (p : R[X]) :
    sumIDeriv p = ∑ i ∈ range (p.natDegree + 1), derivative^[i] p

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ((derivativeFinsupp p).sum fun i => id) = ∑ i ∈ range (p.natDegree + 1), (⇑derivative)^[i] p

Tactic:
exact Finsupp.sum_of_support_subset _ (by simp) _ (by simp)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ i ∈ range (p.natDegree + 1), id 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ sumIDeriv p = ∑ i ∈ range (p.natDegree + 1), (⇑derivative)^[i] p

Tactic:
dsimp [sumIDeriv]

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ((derivativeFinsupp p).sum fun i => id) = ∑ i ∈ range (p.natDegree + 1), (⇑derivative)^[i] p

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ (derivativeFinsupp p).support ⊆ range (p.natDegree + 1)

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Nilpotent.lean
@[simp] lemma isNilpotent_X_mul_iff :
    IsNilpotent (X * P) ↔ IsNilpotent P

Proof state:
case refine_1
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : IsNilpotent (X * P)
⊢ IsNilpotent P

Tactic:
rwa [Commute.isNilpotent_mul_right_iff (commute_X P) (by simp)] at h

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : IsNilpotent (X * P)
⊢ X ∈ nonZeroDivisorsRight R[X]

Tactic:
simp

Result:
no goals

Proof state:
case refine_2
R : Type u_1
inst✝ : Semiring R
P : R[X]
⊢ IsNilpotent P → IsNilpotent (X * P)

Tactic:
rintro ⟨k, hk⟩

Result:
case refine_2.intro
R : Type u_1
inst✝ : Semiring R
P : R[X]
k : ℕ
hk : P ^ k = 0
⊢ IsNilpotent (X * P)

Proof state:
case refine_2.intro
R : Type u_1
inst✝ : Semiring R
P : R[X]
k : ℕ
hk : P ^ k = 0
⊢ IsNilpotent (X * P)

Tactic:
exact ⟨k, by simp [(commute_X P).mul_pow, hk]⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
P : R[X]
⊢ IsNilpotent (X * P) ↔ IsNilpotent P

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

Result:
case refine_1
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : IsNilpotent (X * P)
⊢ IsNilpotent P

case refine_2
R : Type u_1
inst✝ : Semiring R
P : R[X]
⊢ IsNilpotent P → IsNilpotent (X * P)

Proof state:
R : Type u_1
inst✝ : Semiring R
P : R[X]
k : ℕ
hk : P ^ k = 0
⊢ (X * P) ^ k = 0

Tactic:
simp [(commute_X P).mul_pow, hk]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem DistinctKeys.insertListIfNewUnit [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × Unit)}
    {toInsert : List α} (distinct: DistinctKeys l):
    DistinctKeys (insertListIfNewUnit l toInsert)

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
distinct : DistinctKeys l
⊢ DistinctKeys (List.insertListIfNewUnit l toInsert)

Tactic:
induction toInsert generalizing l with
| nil => simp [List.insertListIfNewUnit, distinct]
| cons hd tl ih =>
  simp only [List.insertListIfNewUnit]
  apply ih (insertEntryIfNew distinct)

Result:
no goals

Proof state:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
hd : α
tl : List α
ih : ∀ {l : List ((_ : α) × Unit)}, DistinctKeys l → DistinctKeys (List.insertListIfNewUnit l tl)
l : List ((_ : α) × Unit)
distinct : DistinctKeys l
⊢ DistinctKeys (List.insertListIfNewUnit l (hd :: tl))

Tactic:
simp only [List.insertListIfNewUnit]

Result:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
hd : α
tl : List α
ih : ∀ {l : List ((_ : α) × Unit)}, DistinctKeys l → DistinctKeys (List.insertListIfNewUnit l tl)
l : List ((_ : α) × Unit)
distinct : DistinctKeys l
⊢ DistinctKeys (List.insertListIfNewUnit (List.insertEntryIfNew hd () l) tl)

Proof state:
case nil
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × Unit)
distinct : DistinctKeys l
⊢ DistinctKeys (List.insertListIfNewUnit l [])

Tactic:
simp [List.insertListIfNewUnit, distinct]

Result:
no goals

Proof state:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
hd : α
tl : List α
ih : ∀ {l : List ((_ : α) × Unit)}, DistinctKeys l → DistinctKeys (List.insertListIfNewUnit l tl)
l : List ((_ : α) × Unit)
distinct : DistinctKeys l
⊢ DistinctKeys (List.insertListIfNewUnit (List.insertEntryIfNew hd () l) tl)

Tactic:
apply ih (insertEntryIfNew distinct)

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm_zero : eLpNorm (0 : α → F) p μ = 0

Proof state:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
h0 : ¬p = 0
h_top : p = ⊤
⊢ eLpNorm 0 p μ = 0

Tactic:
simp only [h_top, eLpNorm_exponent_top, eLpNormEssSup_zero]

Result:
no goals

Proof state:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
h0 : p ≠ 0
h_top : ¬p = ⊤
⊢ eLpNorm 0 p μ = 0

Tactic:
simp [eLpNorm_eq_eLpNorm' h0 h_top, ENNReal.toReal_pos h0 h_top]

Result:
no goals

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
⊢ eLpNorm 0 p μ = 0

Tactic:
by_cases h0 : p = 0

Result:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
h0 : p = 0
⊢ eLpNorm 0 p μ = 0

case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
h0 : ¬p = 0
⊢ eLpNorm 0 p μ = 0

Proof state:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
h0 : p = 0
⊢ eLpNorm 0 p μ = 0

Tactic:
simp [h0]

Result:
no goals

Proof state:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
h0 : ¬p = 0
h_top : ¬p = ⊤
⊢ eLpNorm 0 p μ = 0

Tactic:
rw [← Ne] at h0

Result:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
h0 : p ≠ 0
h_top : ¬p = ⊤
⊢ eLpNorm 0 p μ = 0

Proof state:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
h0 : ¬p = 0
⊢ eLpNorm 0 p μ = 0

Tactic:
by_cases h_top : p = ∞

Result:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
h0 : ¬p = 0
h_top : p = ⊤
⊢ eLpNorm 0 p μ = 0

case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
h0 : ¬p = 0
h_top : ¬p = ⊤
⊢ eLpNorm 0 p μ = 0
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem AnalyticOn.contDiff (hf : AnalyticOn 𝕜 f univ) : ContDiff 𝕜 n f

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
hf : AnalyticOn 𝕜 f univ
⊢ ContDiff 𝕜 n f

Tactic:
rw [← contDiffOn_univ]

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
hf : AnalyticOn 𝕜 f univ
⊢ ContDiffOn 𝕜 n f univ

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
hf : AnalyticOn 𝕜 f univ
⊢ ContDiffOn 𝕜 n f univ

Tactic:
exact hf.contDiffOn (n := n) uniqueDiffOn_univ

Result:
no goals