harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Convex/Body.lean
theorem zero_mem_of_symmetric (K : ConvexBody V) (h_symm : ∀ x ∈ K, - x ∈ K) : 0 ∈ K

Proof state:
V : Type u_1
inst✝² : TopologicalSpace V
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
K : ConvexBody V
h_symm : ∀ x ∈ K, -x ∈ K
⊢ 0 ∈ K

Tactic:
obtain ⟨x, hx⟩ := K.nonempty

Result:
case intro
V : Type u_1
inst✝² : TopologicalSpace V
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
K : ConvexBody V
h_symm : ∀ x ∈ K, -x ∈ K
x : V
hx : x ∈ ↑K
⊢ 0 ∈ K

Proof state:
case intro.a
V : Type u_1
inst✝² : TopologicalSpace V
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
K : ConvexBody V
h_symm : ∀ x ∈ K, -x ∈ K
x : V
hx : x ∈ ↑K
⊢ 0 < 1 / 2

case intro.a
V : Type u_1
inst✝² : TopologicalSpace V
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
K : ConvexBody V
h_symm : ∀ x ∈ K, -x ∈ K
x : V
hx : x ∈ ↑K
⊢ 0 < 1 / 2

case intro.a
V : Type u_1
inst✝² : TopologicalSpace V
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
K : ConvexBody V
h_symm : ∀ x ∈ K, -x ∈ K
x : V
hx : x ∈ ↑K
⊢ 1 / 2 + 1 / 2 = 1

Tactic:
all_goals linarith

Result:
no goals

Proof state:
case intro
V : Type u_1
inst✝² : TopologicalSpace V
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
K : ConvexBody V
h_symm : ∀ x ∈ K, -x ∈ K
x : V
hx : x ∈ ↑K
⊢ 0 ∈ K

Tactic:
rw [show 0 = (1/2 : ℝ) • x + (1/2 : ℝ) • (- x) by field_simp]

Result:
case intro
V : Type u_1
inst✝² : TopologicalSpace V
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
K : ConvexBody V
h_symm : ∀ x ∈ K, -x ∈ K
x : V
hx : x ∈ ↑K
⊢ (1 / 2) • x + (1 / 2) • -x ∈ K

Proof state:
V : Type u_1
inst✝² : TopologicalSpace V
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
K : ConvexBody V
h_symm : ∀ x ∈ K, -x ∈ K
x : V
hx : x ∈ ↑K
⊢ 0 = (1 / 2) • x + (1 / 2) • -x

Tactic:
field_simp

Result:
no goals

Proof state:
case intro
V : Type u_1
inst✝² : TopologicalSpace V
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
K : ConvexBody V
h_symm : ∀ x ∈ K, -x ∈ K
x : V
hx : x ∈ ↑K
⊢ (1 / 2) • x + (1 / 2) • -x ∈ K

Tactic:
apply convex_iff_forall_pos.mp K.convex hx (h_symm x hx)

Result:
case intro.a
V : Type u_1
inst✝² : TopologicalSpace V
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
K : ConvexBody V
h_symm : ∀ x ∈ K, -x ∈ K
x : V
hx : x ∈ ↑K
⊢ 0 < 1 / 2

case intro.a
V : Type u_1
inst✝² : TopologicalSpace V
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
K : ConvexBody V
h_symm : ∀ x ∈ K, -x ∈ K
x : V
hx : x ∈ ↑K
⊢ 0 < 1 / 2

case intro.a
V : Type u_1
inst✝² : TopologicalSpace V
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
K : ConvexBody V
h_symm : ∀ x ∈ K, -x ∈ K
x : V
hx : x ∈ ↑K
⊢ 1 / 2 + 1 / 2 = 1

Proof state:
case intro.a
V : Type u_1
inst✝² : TopologicalSpace V
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
K : ConvexBody V
h_symm : ∀ x ∈ K, -x ∈ K
x : V
hx : x ∈ ↑K
⊢ 1 / 2 + 1 / 2 = 1

Tactic:
linarith

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem succ_inj {a b : Fin n} : a.succ = b.succ ↔ a = b

Proof state:
n : Nat
a b : Fin n
h : a.succ = b.succ
⊢ ↑a = ↑b

Tactic:
apply Nat.le_antisymm <;> exact succ_le_succ_iff.1 (h ▸ Nat.le_refl _)

Result:
no goals

Proof state:
n : Nat
a b : Fin n
⊢ a.succ = b.succ ↔ a = b

Tactic:
refine ⟨fun h => Fin.ext ?_, congrArg _⟩

Result:
n : Nat
a b : Fin n
h : a.succ = b.succ
⊢ ↑a = ↑b
-- Mathlib/Combinatorics/SetFamily/Shadow.lean
lemma mem_shadow_iterate_iff_exists_card :
    t ∈ ∂^[k] 𝒜 ↔ ∃ u : Finset α, #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ t ∈ ∂ ^[k] 𝒜 ↔ ∃ u, #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜

Tactic:
induction k generalizing t with
| zero => simp
| succ k ih =>
  simp only [mem_shadow_iff_insert_mem, ih, Function.iterate_succ_apply', card_eq_succ]
  aesop

Result:
no goals

Proof state:
case zero
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ ∂ ^[0] 𝒜 ↔ ∃ u, #u = 0 ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜

Tactic:
simp

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
k : ℕ
ih : ∀ {t : Finset α}, t ∈ ∂ ^[k] 𝒜 ↔ ∃ u, #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜
t : Finset α
⊢ (∃ a ∉ t, ∃ u, #u = k ∧ Disjoint (insert a t) u ∧ insert a t ∪ u ∈ 𝒜) ↔
    ∃ u, (∃ a t, a ∉ t ∧ insert a t = u ∧ #t = k) ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜

Tactic:
aesop

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
k : ℕ
ih : ∀ {t : Finset α}, t ∈ ∂ ^[k] 𝒜 ↔ ∃ u, #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜
t : Finset α
⊢ t ∈ ∂ ^[k + 1] 𝒜 ↔ ∃ u, #u = k + 1 ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜

Tactic:
simp only [mem_shadow_iff_insert_mem, ih, Function.iterate_succ_apply', card_eq_succ]

Result:
case succ
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
k : ℕ
ih : ∀ {t : Finset α}, t ∈ ∂ ^[k] 𝒜 ↔ ∃ u, #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜
t : Finset α
⊢ (∃ a ∉ t, ∃ u, #u = k ∧ Disjoint (insert a t) u ∧ insert a t ∪ u ∈ 𝒜) ↔
    ∃ u, (∃ a t, a ∉ t ∧ insert a t = u ∧ #t = k) ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜
-- Mathlib/Algebra/Lie/CartanSubalgebra.lean
theorem ucs_eq_self_of_isCartanSubalgebra (H : LieSubalgebra R L) [H.IsCartanSubalgebra] (k : ℕ) :
    H.toLieSubmodule.ucs k = H.toLieSubmodule

Proof state:
case zero
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
⊢ LieSubmodule.ucs 0 H.toLieSubmodule = H.toLieSubmodule

Tactic:
simp

Result:
no goals

Proof state:
case succ
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
k : ℕ
ih : LieSubmodule.ucs k H.toLieSubmodule = H.toLieSubmodule
⊢ LieSubmodule.ucs (k + 1) H.toLieSubmodule = H.toLieSubmodule

Tactic:
simp [ih]

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
k : ℕ
⊢ LieSubmodule.ucs k H.toLieSubmodule = H.toLieSubmodule

Tactic:
induction k with
| zero => simp
| succ k ih => simp [ih]

Result:
no goals
-- Mathlib/Order/Lattice.lean
theorem sup_eq_left : a ⊔ b = a ↔ b ≤ a :=
  le_antisymm_iff.trans <| by simp [le_rfl]

Proof state:
α : Type u
inst✝ : SemilatticeSup α
a b : α
⊢ a ⊔ b ≤ a ∧ a ≤ a ⊔ b ↔ b ≤ a

Tactic:
simp [le_rfl]

Result:
no goals
-- Mathlib/Order/Cover.lean
theorem CovBy.Ico_eq (h : a ⋖ b) : Ico a b = {a}

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⋖ b
⊢ Ico a b = {a}

Tactic:
rw [← Ioo_union_left h.lt, h.Ioo_eq, empty_union]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCofiber.lean
lemma nullHomotopicMap_eq : nullHomotopicMap K = π K ≫ ι₀ K - 𝟙 _

Proof state:
case pos
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))
hc : ∀ (j : ι), ∃ i, c.Rel i j
i : ι
hi : c.Rel i (c.next i)
⊢ (nullHomotopicMap K).f i = (π K ≫ ι₀ K - 𝟙 K.cylinder).f i

Tactic:
exact homotopyCofiber.ext_from_X (biprod.lift (𝟙 K) (-𝟙 K)) (c.next i) i hi
  (inlX_nullHomotopy_f _ _ _ _) (inrX_nullHomotopy_f _ hc _)

Result:
no goals

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))
hc : ∀ (j : ι), ∃ i, c.Rel i j
⊢ nullHomotopicMap K = π K ≫ ι₀ K - 𝟙 K.cylinder

Tactic:
ext i

Result:
case h
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))
hc : ∀ (j : ι), ∃ i, c.Rel i j
i : ι
⊢ (nullHomotopicMap K).f i = (π K ≫ ι₀ K - 𝟙 K.cylinder).f i

Proof state:
case neg
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))
hc : ∀ (j : ι), ∃ i, c.Rel i j
i : ι
hi : ¬c.Rel i (c.next i)
⊢ (nullHomotopicMap K).f i = (π K ≫ ι₀ K - 𝟙 K.cylinder).f i

Tactic:
exact homotopyCofiber.ext_from_X' (biprod.lift (𝟙 K) (-𝟙 K)) _ hi (inrX_nullHomotopy_f _ hc _)

Result:
no goals

Proof state:
case h
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))
hc : ∀ (j : ι), ∃ i, c.Rel i j
i : ι
⊢ (nullHomotopicMap K).f i = (π K ≫ ι₀ K - 𝟙 K.cylinder).f i

Tactic:
by_cases hi : c.Rel i (c.next i)

Result:
case pos
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))
hc : ∀ (j : ι), ∃ i, c.Rel i j
i : ι
hi : c.Rel i (c.next i)
⊢ (nullHomotopicMap K).f i = (π K ≫ ι₀ K - 𝟙 K.cylinder).f i

case neg
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))
hc : ∀ (j : ι), ∃ i, c.Rel i j
i : ι
hi : ¬c.Rel i (c.next i)
⊢ (nullHomotopicMap K).f i = (π K ≫ ι₀ K - 𝟙 K.cylinder).f i
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Norm.lean
theorem Int.lt_eq (a b : Int) : (a < b) = (a + 1 ≤ b)

Proof state:
a b : Int
⊢ (a < b) = (a + 1 ≤ b)

Tactic:
simp [Int.lt, LT.lt]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem hasMFDerivWithinAt_univ :
    HasMFDerivWithinAt I I' f univ x f' ↔ HasMFDerivAt I I' f x f'

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
⊢ HasMFDerivWithinAt I I' f univ x f' ↔ HasMFDerivAt I I' f x f'

Tactic:
simp only [HasMFDerivWithinAt, HasMFDerivAt, continuousWithinAt_univ, mfld_simps]

Result:
no goals
-- Mathlib/MeasureTheory/PiSystem.lean
theorem generateHas_compl {C : Set (Set α)} {s : Set α} : GenerateHas C sᶜ ↔ GenerateHas C s

Proof state:
case h.e'_3
α : Type u_3
C : Set (Set α)
s : Set α
h : GenerateHas C sᶜ
⊢ s = sᶜᶜ

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_3
C : Set (Set α)
s : Set α
⊢ GenerateHas C sᶜ → GenerateHas C s

Tactic:
intro h

Result:
α : Type u_3
C : Set (Set α)
s : Set α
h : GenerateHas C sᶜ
⊢ GenerateHas C s

Proof state:
α : Type u_3
C : Set (Set α)
s : Set α
h : GenerateHas C sᶜ
⊢ GenerateHas C s

Tactic:
convert GenerateHas.compl h

Result:
case h.e'_3
α : Type u_3
C : Set (Set α)
s : Set α
h : GenerateHas C sᶜ
⊢ s = sᶜᶜ

Proof state:
α : Type u_3
C : Set (Set α)
s : Set α
⊢ GenerateHas C sᶜ ↔ GenerateHas C s

Tactic:
refine ⟨?_, GenerateHas.compl⟩

Result:
α : Type u_3
C : Set (Set α)
s : Set α
⊢ GenerateHas C sᶜ → GenerateHas C s
-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
@[simp]
lemma compProd_of_not_sfinite (μ : Measure α) (κ : Kernel α β) (h : ¬ SFinite μ) :
    μ ⊗ₘ κ = 0

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
h : ¬SFinite μ
⊢ μ ⊗ₘ κ = 0

Tactic:
rw [compProd, Kernel.compProd_of_not_isSFiniteKernel_left, Kernel.zero_apply]

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
h : ¬SFinite μ
⊢ ¬IsSFiniteKernel (Kernel.const Unit μ)

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
h : ¬SFinite μ
⊢ ¬IsSFiniteKernel (Kernel.const Unit μ)

Tactic:
rwa [Kernel.isSFiniteKernel_const]

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
lemma ext_of_single_vecMul [DecidableEq m] [Fintype m] {M N : Matrix m n α}
    (h : ∀ i, Pi.single i 1 ᵥ* M = Pi.single i 1 ᵥ* N) :
    M = N

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
M N : Matrix m n α
h : ∀ (i : m), Pi.single i 1 ᵥ* M = Pi.single i 1 ᵥ* N
⊢ M = N

Tactic:
ext i j

Result:
case a
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
M N : Matrix m n α
h : ∀ (i : m), Pi.single i 1 ᵥ* M = Pi.single i 1 ᵥ* N
i : m
j : n
⊢ M i j = N i j

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
M N : Matrix m n α
i : m
j : n
h : ∀ (i : m), M i = N i
⊢ M i j = N i j

Tactic:
exact congrFun (h i) j

Result:
no goals

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
M N : Matrix m n α
h : ∀ (i : m), Pi.single i 1 ᵥ* M = Pi.single i 1 ᵥ* N
i : m
j : n
⊢ M i j = N i j

Tactic:
simp_rw [single_one_vecMul] at h

Result:
case a
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
M N : Matrix m n α
i : m
j : n
h : ∀ (i : m), M i = N i
⊢ M i j = N i j
-- Mathlib/Data/List/InsertIdx.lean
theorem eraseIdx_map (f : α → β) (l : List α) (n : ℕ) :
    (map f l).eraseIdx n = (l.eraseIdx n).map f

Proof state:
α : Type u
β : Type v
f : α → β
l : List α
n : ℕ
⊢ (map f l).eraseIdx n = map f (l.eraseIdx n)

Tactic:
simpa only [pmap_eq_map] using eraseIdx_pmap (fun a _ ↦ f a) (fun _ _ ↦ trivial) n

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean
theorem dotProduct_mulVec_degMatrix [CommRing R] (x : V → R) :
    x ⬝ᵥ (G.degMatrix R *ᵥ x) = ∑ i : V, G.degree i * x i * x i

Proof state:
V : Type u_1
R : Type u_2
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : CommRing R
x : V → R
⊢ x ⬝ᵥ degMatrix R G *ᵥ x = ∑ i : V, ↑(G.degree i) * x i * x i

Tactic:
simp only [dotProduct, degMatrix, mulVec_diagonal, ← mul_assoc, mul_comm]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem contDiffOn_infty_iff_derivWithin (hs : UniqueDiffOn 𝕜 s₂) :
    ContDiffOn 𝕜 ∞ f₂ s₂ ↔ DifferentiableOn 𝕜 f₂ s₂ ∧ ContDiffOn 𝕜 ∞ (derivWithin f₂ s₂) s₂

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f₂ : 𝕜 → F
s₂ : Set 𝕜
hs : UniqueDiffOn 𝕜 s₂
⊢ ContDiffOn 𝕜 ∞ f₂ s₂ ↔ DifferentiableOn 𝕜 f₂ s₂ ∧ ContDiffOn 𝕜 ∞ (derivWithin f₂ s₂) s₂

Tactic:
rw [show ∞ = ∞ + 1 by rfl, contDiffOn_succ_iff_derivWithin hs]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f₂ : 𝕜 → F
s₂ : Set 𝕜
hs : UniqueDiffOn 𝕜 s₂
⊢ DifferentiableOn 𝕜 f₂ s₂ ∧ (∞ = ω → AnalyticOn 𝕜 f₂ s₂) ∧ ContDiffOn 𝕜 ∞ (derivWithin f₂ s₂) s₂ ↔
    DifferentiableOn 𝕜 f₂ s₂ ∧ ContDiffOn 𝕜 (∞ + 1) (derivWithin f₂ s₂) s₂

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f₂ : 𝕜 → F
s₂ : Set 𝕜
hs : UniqueDiffOn 𝕜 s₂
⊢ DifferentiableOn 𝕜 f₂ s₂ ∧ (∞ = ω → AnalyticOn 𝕜 f₂ s₂) ∧ ContDiffOn 𝕜 ∞ (derivWithin f₂ s₂) s₂ ↔
    DifferentiableOn 𝕜 f₂ s₂ ∧ ContDiffOn 𝕜 (∞ + 1) (derivWithin f₂ s₂) s₂

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f₂ : 𝕜 → F
s₂ : Set 𝕜
hs : UniqueDiffOn 𝕜 s₂
⊢ ∞ = ∞ + 1

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Matrix/Basis.lean
theorem induction_on
    [AddCommMonoid α] [Finite m] [Finite n] [Nonempty m] [Nonempty n]
    {P : Matrix m n α → Prop} (M : Matrix m n α) (h_add : ∀ p q, P p → P q → P (p + q))
    (h_std_basis : ∀ i j x, P (stdBasisMatrix i j x)) : P M :=
  Matrix.induction_on' M
    (by
      inhabit m
      inhabit n
      simpa using h_std_basis default default 0)
    h_add h_std_basis

Proof state:
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : AddCommMonoid α
inst✝³ : Finite m
inst✝² : Finite n
inst✝¹ : Nonempty m
inst✝ : Nonempty n
P : Matrix m n α → Prop
M : Matrix m n α
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
inhabited_h✝ : Inhabited m
inhabited_h : Inhabited n
⊢ P 0

Tactic:
simpa using h_std_basis default default 0

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : AddCommMonoid α
inst✝³ : Finite m
inst✝² : Finite n
inst✝¹ : Nonempty m
inst✝ : Nonempty n
P : Matrix m n α → Prop
M : Matrix m n α
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
inhabited_h : Inhabited m
⊢ P 0

Tactic:
inhabit n

Result:
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : AddCommMonoid α
inst✝³ : Finite m
inst✝² : Finite n
inst✝¹ : Nonempty m
inst✝ : Nonempty n
P : Matrix m n α → Prop
M : Matrix m n α
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
inhabited_h✝ : Inhabited m
inhabited_h : Inhabited n
⊢ P 0

Proof state:
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : AddCommMonoid α
inst✝³ : Finite m
inst✝² : Finite n
inst✝¹ : Nonempty m
inst✝ : Nonempty n
P : Matrix m n α → Prop
M : Matrix m n α
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
⊢ P 0

Tactic:
inhabit m

Result:
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : AddCommMonoid α
inst✝³ : Finite m
inst✝² : Finite n
inst✝¹ : Nonempty m
inst✝ : Nonempty n
P : Matrix m n α → Prop
M : Matrix m n α
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
inhabited_h : Inhabited m
⊢ P 0
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem nndist_one_right (a : E) : nndist a 1 = ‖a‖₊

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ nndist a 1 = ‖a‖₊

Tactic:
simp [nndist_eq_nnnorm_div]

Result:
no goals
-- Mathlib/Data/ENat/Basic.lean
theorem nat_induction {P : ℕ∞ → Prop} (a : ℕ∞) (h0 : P 0) (hsuc : ∀ n : ℕ, P n → P n.succ)
    (htop : (∀ n : ℕ, P n) → P ⊤) : P a

Proof state:
case top
P : ℕ∞ → Prop
h0 : P 0
hsuc : ∀ (n : ℕ), P ↑n → P ↑n.succ
htop : (∀ (n : ℕ), P ↑n) → P ⊤
A : ∀ (n : ℕ), P ↑n
⊢ P ⊤

Tactic:
exact htop A

Result:
no goals

Proof state:
case coe
P : ℕ∞ → Prop
h0 : P 0
hsuc : ∀ (n : ℕ), P ↑n → P ↑n.succ
htop : (∀ (n : ℕ), P ↑n) → P ⊤
A : ∀ (n : ℕ), P ↑n
a✝ : ℕ
⊢ P ↑a✝

Tactic:
exact A _

Result:
no goals

Proof state:
P : ℕ∞ → Prop
a : ℕ∞
h0 : P 0
hsuc : ∀ (n : ℕ), P ↑n → P ↑n.succ
htop : (∀ (n : ℕ), P ↑n) → P ⊤
A : ∀ (n : ℕ), P ↑n
⊢ P a

Tactic:
cases a

Result:
case top
P : ℕ∞ → Prop
h0 : P 0
hsuc : ∀ (n : ℕ), P ↑n → P ↑n.succ
htop : (∀ (n : ℕ), P ↑n) → P ⊤
A : ∀ (n : ℕ), P ↑n
⊢ P ⊤

case coe
P : ℕ∞ → Prop
h0 : P 0
hsuc : ∀ (n : ℕ), P ↑n → P ↑n.succ
htop : (∀ (n : ℕ), P ↑n) → P ⊤
A : ∀ (n : ℕ), P ↑n
a✝ : ℕ
⊢ P ↑a✝

Proof state:
P : ℕ∞ → Prop
a : ℕ∞
h0 : P 0
hsuc : ∀ (n : ℕ), P ↑n → P ↑n.succ
htop : (∀ (n : ℕ), P ↑n) → P ⊤
⊢ P a

Tactic:
have A : ∀ n : ℕ, P n := fun n => Nat.recOn n h0 hsuc

Result:
P : ℕ∞ → Prop
a : ℕ∞
h0 : P 0
hsuc : ∀ (n : ℕ), P ↑n → P ↑n.succ
htop : (∀ (n : ℕ), P ↑n) → P ⊤
A : ∀ (n : ℕ), P ↑n
⊢ P a
-- Mathlib/RingTheory/Unramified/Basic.lean
theorem lift_unique_of_ringHom [FormallyUnramified R A] {C : Type*} [CommRing C]
    (f : B →+* C) (hf : IsNilpotent <| RingHom.ker f) (g₁ g₂ : A →ₐ[R] B)
    (h : f.comp ↑g₁ = f.comp (g₂ : A →+* B)) : g₁ = g₂ :=
  FormallyUnramified.lift_unique _ hf _ _
    (by
      ext x
      have := RingHom.congr_fun h x
      simpa only [Ideal.Quotient.eq, Function.comp_apply, AlgHom.coe_comp, Ideal.Quotient.mkₐ_eq_mk,
        RingHom.mem_ker, map_sub, sub_eq_zero])

Proof state:
case H
R : Type v
inst✝⁶ : CommRing R
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B : Type w
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : FormallyUnramified R A
C : Type u_1
inst✝ : CommRing C
f : B →+* C
hf : IsNilpotent (RingHom.ker f)
g₁ g₂ : A →ₐ[R] B
h : f.comp ↑g₁ = f.comp ↑g₂
x : A
⊢ ((Ideal.Quotient.mkₐ R (RingHom.ker f)).comp g₁) x = ((Ideal.Quotient.mkₐ R (RingHom.ker f)).comp g₂) x

Tactic:
have := RingHom.congr_fun h x

Result:
case H
R : Type v
inst✝⁶ : CommRing R
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B : Type w
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : FormallyUnramified R A
C : Type u_1
inst✝ : CommRing C
f : B →+* C
hf : IsNilpotent (RingHom.ker f)
g₁ g₂ : A →ₐ[R] B
h : f.comp ↑g₁ = f.comp ↑g₂
x : A
this : (f.comp ↑g₁) x = (f.comp ↑g₂) x
⊢ ((Ideal.Quotient.mkₐ R (RingHom.ker f)).comp g₁) x = ((Ideal.Quotient.mkₐ R (RingHom.ker f)).comp g₂) x

Proof state:
case H
R : Type v
inst✝⁶ : CommRing R
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B : Type w
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : FormallyUnramified R A
C : Type u_1
inst✝ : CommRing C
f : B →+* C
hf : IsNilpotent (RingHom.ker f)
g₁ g₂ : A →ₐ[R] B
h : f.comp ↑g₁ = f.comp ↑g₂
x : A
this : (f.comp ↑g₁) x = (f.comp ↑g₂) x
⊢ ((Ideal.Quotient.mkₐ R (RingHom.ker f)).comp g₁) x = ((Ideal.Quotient.mkₐ R (RingHom.ker f)).comp g₂) x

Tactic:
simpa only [Ideal.Quotient.eq, Function.comp_apply, AlgHom.coe_comp, Ideal.Quotient.mkₐ_eq_mk,
  RingHom.mem_ker, map_sub, sub_eq_zero]

Result:
no goals

Proof state:
R : Type v
inst✝⁶ : CommRing R
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B : Type w
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : FormallyUnramified R A
C : Type u_1
inst✝ : CommRing C
f : B →+* C
hf : IsNilpotent (RingHom.ker f)
g₁ g₂ : A →ₐ[R] B
h : f.comp ↑g₁ = f.comp ↑g₂
⊢ (Ideal.Quotient.mkₐ R (RingHom.ker f)).comp g₁ = (Ideal.Quotient.mkₐ R (RingHom.ker f)).comp g₂

Tactic:
ext x

Result:
case H
R : Type v
inst✝⁶ : CommRing R
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B : Type w
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : FormallyUnramified R A
C : Type u_1
inst✝ : CommRing C
f : B →+* C
hf : IsNilpotent (RingHom.ker f)
g₁ g₂ : A →ₐ[R] B
h : f.comp ↑g₁ = f.comp ↑g₂
x : A
⊢ ((Ideal.Quotient.mkₐ R (RingHom.ker f)).comp g₁) x = ((Ideal.Quotient.mkₐ R (RingHom.ker f)).comp g₂) x
-- Mathlib/Data/ZMod/QuotientGroup.lean
theorem orbitZPowersEquiv_symm_apply' (k : ℤ) :
    (orbitZPowersEquiv a b).symm k =
      (⟨a, mem_zpowers a⟩ : zpowers a) ^ k • ⟨b, mem_orbit_self b⟩

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : Group α
a : α
inst✝ : MulAction α β
b : β
k : ℤ
⊢ (orbitZPowersEquiv a b).symm ↑k = ⟨a, ⋯⟩ ^ k • ⟨b, ⋯⟩

Tactic:
rw [orbitZPowersEquiv_symm_apply, ZMod.coe_intCast]

Result:
α : Type u_3
β : Type u_4
inst✝¹ : Group α
a : α
inst✝ : MulAction α β
b : β
k : ℤ
⊢ ⟨a, ⋯⟩ ^ (k % ↑(minimalPeriod (fun x => a • x) b)) • ⟨b, ⋯⟩ = ⟨a, ⋯⟩ ^ k • ⟨b, ⋯⟩

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : Group α
a : α
inst✝ : MulAction α β
b : β
k : ℤ
⊢ ⟨a, ⋯⟩ ^ (k % ↑(minimalPeriod (fun x => a • x) b)) • ⟨b, ⋯⟩ = ⟨a, ⋯⟩ ^ k • ⟨b, ⋯⟩

Tactic:
exact Subtype.ext (zpow_smul_mod_minimalPeriod _ _ k)

Result:
no goals