harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Cover.lean
theorem wcovBy_iff : x ⩿ y ↔ x.1 ⩿ y.1 ∧ x.2 = y.2 ∨ x.2 ⩿ y.2 ∧ x.1 = y.1

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
fst✝¹ : α
snd✝¹ : β
fst✝ : α
snd✝ : β
⊢ (fst✝¹, snd✝¹) ⩿ (fst✝, snd✝) ↔
    (fst✝¹, snd✝¹).1 ⩿ (fst✝, snd✝).1 ∧ (fst✝¹, snd✝¹).2 = (fst✝, snd✝).2 ∨
      (fst✝¹, snd✝¹).2 ⩿ (fst✝, snd✝).2 ∧ (fst✝¹, snd✝¹).1 = (fst✝, snd✝).1

Tactic:
exact mk_wcovBy_mk_iff

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
x y : α × β
⊢ x ⩿ y ↔ x.1 ⩿ y.1 ∧ x.2 = y.2 ∨ x.2 ⩿ y.2 ∧ x.1 = y.1

Tactic:
cases x

Result:
case mk
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
y : α × β
fst✝ : α
snd✝ : β
⊢ (fst✝, snd✝) ⩿ y ↔ (fst✝, snd✝).1 ⩿ y.1 ∧ (fst✝, snd✝).2 = y.2 ∨ (fst✝, snd✝).2 ⩿ y.2 ∧ (fst✝, snd✝).1 = y.1

Proof state:
case mk
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
y : α × β
fst✝ : α
snd✝ : β
⊢ (fst✝, snd✝) ⩿ y ↔ (fst✝, snd✝).1 ⩿ y.1 ∧ (fst✝, snd✝).2 = y.2 ∨ (fst✝, snd✝).2 ⩿ y.2 ∧ (fst✝, snd✝).1 = y.1

Tactic:
cases y

Result:
case mk.mk
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
fst✝¹ : α
snd✝¹ : β
fst✝ : α
snd✝ : β
⊢ (fst✝¹, snd✝¹) ⩿ (fst✝, snd✝) ↔
    (fst✝¹, snd✝¹).1 ⩿ (fst✝, snd✝).1 ∧ (fst✝¹, snd✝¹).2 = (fst✝, snd✝).2 ∨
      (fst✝¹, snd✝¹).2 ⩿ (fst✝, snd✝).2 ∧ (fst✝¹, snd✝¹).1 = (fst✝, snd✝).1
-- Mathlib/Algebra/Group/Units/Defs.lean
theorem Units.isUnit_units_mul {M : Type*} [Monoid M] (u : Mˣ) (a : M) :
    IsUnit (↑u * a) ↔ IsUnit a :=
  Iff.intro
    (fun ⟨v, hv⟩ => by
      have : IsUnit (↑u⁻¹ * (↑u * a))

Proof state:
M : Type u_3
inst✝ : Monoid M
u : Mˣ
a : M
x✝ : IsUnit (↑u * a)
v : Mˣ
hv : ↑v = ↑u * a
⊢ IsUnit a

Tactic:
have : IsUnit (↑u⁻¹ * (↑u * a)) := by exists u⁻¹ * v; rw [← hv, Units.val_mul]

Result:
M : Type u_3
inst✝ : Monoid M
u : Mˣ
a : M
x✝ : IsUnit (↑u * a)
v : Mˣ
hv : ↑v = ↑u * a
this : IsUnit (↑u⁻¹ * (↑u * a))
⊢ IsUnit a

Proof state:
M : Type u_3
inst✝ : Monoid M
u : Mˣ
a : M
x✝ : IsUnit (↑u * a)
v : Mˣ
hv : ↑v = ↑u * a
this : IsUnit (↑u⁻¹ * (↑u * a))
⊢ IsUnit a

Tactic:
rwa [← mul_assoc, Units.inv_mul, one_mul] at this

Result:
no goals

Proof state:
M : Type u_3
inst✝ : Monoid M
u : Mˣ
a : M
x✝ : IsUnit (↑u * a)
v : Mˣ
hv : ↑v = ↑u * a
⊢ IsUnit (↑u⁻¹ * (↑u * a))

Tactic:
exists u⁻¹ * v

Result:
M : Type u_3
inst✝ : Monoid M
u : Mˣ
a : M
x✝ : IsUnit (↑u * a)
v : Mˣ
hv : ↑v = ↑u * a
⊢ ↑(u⁻¹ * v) = ↑u⁻¹ * (↑u * a)

Proof state:
M : Type u_3
inst✝ : Monoid M
u : Mˣ
a : M
x✝ : IsUnit (↑u * a)
v : Mˣ
hv : ↑v = ↑u * a
⊢ ↑(u⁻¹ * v) = ↑u⁻¹ * (↑u * a)

Tactic:
rw [← hv, Units.val_mul]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioc_eq_Ico_same_iff : Ioc a b = Ico a b ↔ ¬a < b where
  mp h

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
h : Ioc a b = Ico a b
⊢ ¬a < b

Tactic:
simpa using Set.ext_iff.mp h a

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
h : ¬a < b
⊢ Ioc a b = Ico a b

Tactic:
rw [Ioc_eq_empty h, Ico_eq_empty h]

Result:
no goals
-- Mathlib/Algebra/Colimit/Module.lean
theorem linearEquiv_of {i g} : linearEquiv _ _ (of _ _ G f i g) = ⟦⟨i, g⟩⟧

Proof state:
R : Type u_1
inst✝⁷ : Semiring R
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
inst✝⁵ : DecidableEq ι
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝² : Nonempty ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)
i : ι
g : G i
⊢ (linearEquiv G f) ((of R ι G f i) g) = ⟦⟨i, g⟩⟧

Tactic:
simp [linearEquiv]

Result:
R : Type u_1
inst✝⁷ : Semiring R
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
inst✝⁵ : DecidableEq ι
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝² : Nonempty ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)
i : ι
g : G i
⊢ (Module.of R ι G f i) g = ⟦⟨i, g⟩⟧

Proof state:
R : Type u_1
inst✝⁷ : Semiring R
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
inst✝⁵ : DecidableEq ι
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝² : Nonempty ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)
i : ι
g : G i
⊢ (Module.of R ι G f i) g = ⟦⟨i, g⟩⟧

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem ofBool_and_ofBool : ofBool b &&& ofBool b' = ofBool (b && b')

Proof state:
b b' : Bool
⊢ ofBool b &&& ofBool b' = ofBool (b && b')

Tactic:
cases b <;> cases b' <;> rfl

Result:
no goals
-- Mathlib/NumberTheory/SumFourSquares.lean
theorem lt_of_sum_four_squares_eq_mul {a b c d k m : ℕ}
    (h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = k * m)
    (ha : 2 * a < m) (hb : 2 * b < m) (hc : 2 * c < m) (hd : 2 * d < m) :
    k < m

Proof state:
a b c d k m : ℕ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = k * m
ha : 2 * a < m
hb : 2 * b < m
hc : 2 * c < m
hd : 2 * d < m
⊢ k < m

Tactic:
nlinarith

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
lemma eLpNorm_nnreal_eq_eLpNorm' {f : α → ε} {p : ℝ≥0} (hp : p ≠ 0) :
    eLpNorm f p μ = eLpNorm' f p μ :=
  eLpNorm_eq_eLpNorm' (by exact_mod_cast hp) ENNReal.coe_ne_top

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
f : α → ε
p : ℝ≥0
hp : p ≠ 0
⊢ ↑p ≠ 0

Tactic:
exact_mod_cast hp

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
theorem δ_comp_δ {n} {i j : Fin (n + 2)} (H : i ≤ j) :
    X.δ j.succ ≫ X.δ i = X.δ (Fin.castSucc i) ≫ X.δ j

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ X.δ j.succ ≫ X.δ i = X.δ i.castSucc ≫ X.δ j

Tactic:
dsimp [δ]

Result:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ X.map (SimplexCategory.δ j.succ).op ≫ X.map (SimplexCategory.δ i).op =
    X.map (SimplexCategory.δ i.castSucc).op ≫ X.map (SimplexCategory.δ j).op

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ X.map (SimplexCategory.δ j.succ).op ≫ X.map (SimplexCategory.δ i).op =
    X.map (SimplexCategory.δ i.castSucc).op ≫ X.map (SimplexCategory.δ j).op

Tactic:
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_δ H]

Result:
no goals
-- Mathlib/CategoryTheory/LiftingProperties/Basic.lean
lemma RetractArrow.rightLiftingProperty
    {X Y Z W X' Y' : C} {f : X ⟶ Y} {f' : X' ⟶ Y'}
    (h : RetractArrow f' f) (g : Z ⟶ W) [HasLiftingProperty g f] : HasLiftingProperty g f' where
  sq_hasLift := fun {u v} sq ↦
    have sq' : CommSq (u ≫ h.i.left) g f (v ≫ h.i.right) :=
      ⟨by rw [← Category.assoc, ← sq.w, Category.assoc, RetractArrow.i_w, Category.assoc]⟩
    ⟨⟨{ l := sq'.lift ≫ h.r.left}⟩⟩

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y Z W X' Y' : C
f : X ⟶ Y
f' : X' ⟶ Y'
h : RetractArrow f' f
g : Z ⟶ W
inst✝ : HasLiftingProperty g f
u : Z ⟶ X'
v : W ⟶ Y'
sq : CommSq u g f' v
⊢ (u ≫ h.i.left) ≫ f = g ≫ v ≫ h.i.right

Tactic:
rw [← Category.assoc, ← sq.w, Category.assoc, RetractArrow.i_w, Category.assoc]

Result:
no goals
-- Mathlib/Data/Sigma/Basic.lean
theorem Function.Surjective.sigma_map {f₁ : α₁ → α₂} {f₂ : ∀ a, β₁ a → β₂ (f₁ a)}
    (h₁ : Surjective f₁) (h₂ : ∀ a, Surjective (f₂ a)) : Surjective (Sigma.map f₁ f₂)

Proof state:
α₁ : Type u_2
α₂ : Type u_3
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Surjective f₁
h₂ : ∀ (a : α₁), Surjective (f₂ a)
⊢ Surjective (Sigma.map f₁ f₂)

Tactic:
simp only [Surjective, Sigma.forall, h₁.forall]

Result:
α₁ : Type u_2
α₂ : Type u_3
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Surjective f₁
h₂ : ∀ (a : α₁), Surjective (f₂ a)
⊢ ∀ (x : α₁) (b : β₂ (f₁ x)), ∃ a, Sigma.map f₁ f₂ a = ⟨f₁ x, b⟩

Proof state:
α₁ : Type u_2
α₂ : Type u_3
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Surjective f₁
h₂ : ∀ (a : α₁), Surjective (f₂ a)
⊢ ∀ (x : α₁) (b : β₂ (f₁ x)), ∃ a, Sigma.map f₁ f₂ a = ⟨f₁ x, b⟩

Tactic:
exact fun i ↦ (h₂ _).forall.2 fun x ↦ ⟨⟨i, x⟩, rfl⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem filterTR_loop_eq (p : α → Bool) (as bs : List α) :
    filterTR.loop p as bs = bs.reverse ++ filter p as

Proof state:
case nil
α : Type u
p : α → Bool
bs : List α
⊢ filterTR.loop p nil bs = bs.reverse ++ filter p nil

Tactic:
simp [filterTR.loop, filter]

Result:
no goals

Proof state:
case cons
α : Type u
p : α → Bool
a : α
as : List α
ih : ∀ (bs : List α), filterTR.loop p as bs = bs.reverse ++ filter p as
bs : List α
⊢ filterTR.loop p (a :: as) bs = bs.reverse ++ filter p (a :: as)

Tactic:
simp only [filterTR.loop, filter]

Result:
case cons
α : Type u
p : α → Bool
a : α
as : List α
ih : ∀ (bs : List α), filterTR.loop p as bs = bs.reverse ++ filter p as
bs : List α
⊢ (match p a with
    | true => filterTR.loop p as (a :: bs)
    | false => filterTR.loop p as bs) =
    bs.reverse ++
      match p a with
      | true => a :: filter p as
      | false => filter p as

Proof state:
case cons
α : Type u
p : α → Bool
a : α
as : List α
ih : ∀ (bs : List α), filterTR.loop p as bs = bs.reverse ++ filter p as
bs : List α
⊢ (match p a with
    | true => filterTR.loop p as (a :: bs)
    | false => filterTR.loop p as bs) =
    bs.reverse ++
      match p a with
      | true => a :: filter p as
      | false => filter p as

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
α : Type u
p : α → Bool
as bs : List α
⊢ filterTR.loop p as bs = bs.reverse ++ filter p as

Tactic:
induction as generalizing bs with
| nil => simp [filterTR.loop, filter]
| cons a as ih =>
  simp only [filterTR.loop, filter]
  split <;> simp_all

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem div_div : a / b / c = a / (b * c)

Proof state:
α : Type u_1
inst✝ : DivisionCommMonoid α
a b c : α
⊢ a / b / c = a / (b * c)

Tactic:
simp

Result:
no goals
-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem WellFoundedGT.finite_ne_bot_of_iSupIndep [WellFoundedGT α]
    {ι : Type*} {t : ι → α} (ht : iSupIndep t) : Set.Finite {i | t i ≠ ⊥}

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
ι : Type u_3
t : ι → α
ht : iSupIndep t
⊢ {i | t i ≠ ⊥}.Finite

Tactic:
refine Finite.of_finite_image (Finite.subset ?_ (image_subset_range t _)) ht.injOn

Result:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
ι : Type u_3
t : ι → α
ht : iSupIndep t
⊢ (range t).Finite

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
ι : Type u_3
t : ι → α
ht : iSupIndep t
⊢ (range t).Finite

Tactic:
exact WellFoundedGT.finite_of_sSupIndep ht.sSupIndep_range

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem nnnorm_zero : ‖(0 : Lp E p μ)‖₊ = 0

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

Tactic:
rw [nnnorm_def]

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
⊢ (eLpNorm (↑↑0) p μ).toNNReal = 0

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
⊢ (eLpNorm (↑↑0) p μ).toNNReal = 0

Tactic:
change (eLpNorm (⇑(0 : α →ₘ[μ] E)) p μ).toNNReal = 0

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
⊢ (eLpNorm (↑0) p μ).toNNReal = 0

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
⊢ (eLpNorm (↑0) p μ).toNNReal = 0

Tactic:
simp [eLpNorm_congr_ae AEEqFun.coeFn_zero, eLpNorm_zero]

Result:
no goals
-- Mathlib/Analysis/Complex/Liouville.lean
theorem deriv_eq_smul_circleIntegral [CompleteSpace F] {R : ℝ} {c : ℂ} {f : ℂ → F} (hR : 0 < R)
    (hf : DiffContOnCl ℂ f (ball c R)) :
    deriv f c = (2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - c) ^ (-2 : ℤ) • f z

Proof state:
case intro
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
f : ℂ → F
R : ℝ≥0
hR : 0 < ↑R
hf : DiffContOnCl ℂ f (ball c ↑R)
⊢ deriv f c = (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑R), (z - c) ^ (-2) • f z

Tactic:
refine (hf.hasFPowerSeriesOnBall hR).hasFPowerSeriesAt.deriv.trans ?_

Result:
case intro
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
f : ℂ → F
R : ℝ≥0
hR : 0 < ↑R
hf : DiffContOnCl ℂ f (ball c ↑R)
⊢ ((cauchyPowerSeries f c (↑R) 1) fun x => 1) = (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑R), (z - c) ^ (-2) • f z

Proof state:
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
R : ℝ
c : ℂ
f : ℂ → F
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
⊢ deriv f c = (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c) ^ (-2) • f z

Tactic:
lift R to ℝ≥0 using hR.le

Result:
case intro
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
f : ℂ → F
R : ℝ≥0
hR : 0 < ↑R
hf : DiffContOnCl ℂ f (ball c ↑R)
⊢ deriv f c = (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑R), (z - c) ^ (-2) • f z

Proof state:
case intro
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
f : ℂ → F
R : ℝ≥0
hR : 0 < ↑R
hf : DiffContOnCl ℂ f (ball c ↑R)
⊢ ((cauchyPowerSeries f c (↑R) 1) fun x => 1) = (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑R), (z - c) ^ (-2) • f z

Tactic:
simp only [cauchyPowerSeries_apply, one_div, zpow_neg, pow_one, smul_smul, zpow_two, mul_inv]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/WithLp.lean
theorem differentiableAt_piLp :
    DifferentiableAt 𝕜 f y ↔ ∀ i, DifferentiableAt 𝕜 (fun x => f x i) y

Proof state:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
y : H
⊢ (∀ (i : ι), DifferentiableAt 𝕜 (fun x => (⇑(PiLp.continuousLinearEquiv p 𝕜 E) ∘ f) x i) y) ↔
    ∀ (i : ι), DifferentiableAt 𝕜 (fun x => f x i) y

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
y : H
⊢ DifferentiableAt 𝕜 f y ↔ ∀ (i : ι), DifferentiableAt 𝕜 (fun x => f x i) y

Tactic:
rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_differentiableAt_iff, differentiableAt_pi]

Result:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
y : H
⊢ (∀ (i : ι), DifferentiableAt 𝕜 (fun x => (⇑(PiLp.continuousLinearEquiv p 𝕜 E) ∘ f) x i) y) ↔
    ∀ (i : ι), DifferentiableAt 𝕜 (fun x => f x i) y
-- Mathlib/Computability/Halting.lean
theorem cons {n m} {f : List.Vector ℕ n → ℕ} {g} (hf : @Partrec' n f)
    (hg : @Vec n m g) : Vec fun v => f v ::ᵥ g v := fun i =>
  Fin.cases (by simpa using hf) (fun i => by simp only [hg i, get_cons_succ]) i

Proof state:
n m : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ n → List.Vector ℕ m
hf : Partrec' ↑f
hg : Vec g
i✝ : Fin m.succ
i : Fin m
⊢ Partrec' fun v => ↑(some (((fun v => f v ::ᵥ g v) v).get i.succ))

Tactic:
simp only [hg i, get_cons_succ]

Result:
no goals

Proof state:
n m : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ n → List.Vector ℕ m
hf : Partrec' ↑f
hg : Vec g
i : Fin m.succ
⊢ Partrec' fun v => ↑(some (((fun v => f v ::ᵥ g v) v).get 0))

Tactic:
simpa using hf

Result:
no goals
-- Mathlib/Data/Real/GoldenRatio.lean
theorem geom_goldConj_isSol_fibRec : fibRec.IsSolution (ψ ^ ·)

Proof state:
⊢ fibRec.IsSolution fun x => ψ ^ x

Tactic:
rw [fibRec.geom_sol_iff_root_charPoly, fibRec_charPoly_eq]

Result:
⊢ (X ^ 2 - (X + 1)).IsRoot ψ

Proof state:
⊢ (X ^ 2 - (X + 1)).IsRoot ψ

Tactic:
simp [sub_eq_zero]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/Prod.lean
@[simp] lemma snd_prod (κ : Kernel α β) [IsMarkovKernel κ] (η : Kernel α γ) [IsSFiniteKernel η] :
    snd (κ ×ₖ η) = η

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsMarkovKernel κ
η : Kernel α γ
inst✝ : IsSFiniteKernel η
⊢ (κ ×ₖ η).snd = η

Tactic:
ext x

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsMarkovKernel κ
η : Kernel α γ
inst✝ : IsSFiniteKernel η
x : α
s✝ : Set γ
a✝ : MeasurableSet s✝
⊢ ((κ ×ₖ η).snd x) s✝ = (η x) s✝

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsMarkovKernel κ
η : Kernel α γ
inst✝ : IsSFiniteKernel η
x : α
s✝ : Set γ
a✝ : MeasurableSet s✝
⊢ ((κ ×ₖ η).snd x) s✝ = (η x) s✝

Tactic:
simp [snd_apply, prod_apply]

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
theorem tangentBundleCore_coordChange_model_space (x x' z : H) :
    (tangentBundleCore I H).coordChange (achart H x) (achart H x') z =
    ContinuousLinearMap.id 𝕜 E

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
x x' z : H
⊢ (tangentBundleCore I H).coordChange (achart H x) (achart H x') z = ContinuousLinearMap.id 𝕜 E

Tactic:
ext v

Result:
case h
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
x x' z : H
v : E
⊢ ((tangentBundleCore I H).coordChange (achart H x) (achart H x') z) v = (ContinuousLinearMap.id 𝕜 E) v

Proof state:
case h
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
x x' z : H
v : E
⊢ ((tangentBundleCore I H).coordChange (achart H x) (achart H x') z) v = (ContinuousLinearMap.id 𝕜 E) v

Tactic:
exact (tangentBundleCore I H).coordChange_self (achart _ z) z (mem_univ _) v

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem isLocalHom_iff_comap_closedPoint {S : Type v} [CommSemiring S] [IsLocalRing S]
    (f : R →+* S) : IsLocalHom f ↔ PrimeSpectrum.comap f (closedPoint S) = closedPoint R

Proof state:
R : Type u
inst✝³ : CommSemiring R
inst✝² : IsLocalRing R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : IsLocalRing S
f : R →+* S
this : IsLocalHom f ↔ Ideal.comap f (maximalIdeal S) = maximalIdeal R
⊢ IsLocalHom f ↔ (PrimeSpectrum.comap f) (closedPoint S) = closedPoint R

Tactic:
rw [this, PrimeSpectrum.ext_iff]

Result:
R : Type u
inst✝³ : CommSemiring R
inst✝² : IsLocalRing R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : IsLocalRing S
f : R →+* S
this : IsLocalHom f ↔ Ideal.comap f (maximalIdeal S) = maximalIdeal R
⊢ Ideal.comap f (maximalIdeal S) = maximalIdeal R ↔
    ((PrimeSpectrum.comap f) (closedPoint S)).asIdeal = (closedPoint R).asIdeal

Proof state:
R : Type u
inst✝³ : CommSemiring R
inst✝² : IsLocalRing R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : IsLocalRing S
f : R →+* S
⊢ IsLocalHom f ↔ (PrimeSpectrum.comap f) (closedPoint S) = closedPoint R

Tactic:
have := (local_hom_TFAE f).out 0 4

Result:
R : Type u
inst✝³ : CommSemiring R
inst✝² : IsLocalRing R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : IsLocalRing S
f : R →+* S
this : IsLocalHom f ↔ Ideal.comap f (maximalIdeal S) = maximalIdeal R
⊢ IsLocalHom f ↔ (PrimeSpectrum.comap f) (closedPoint S) = closedPoint R

Proof state:
R : Type u
inst✝³ : CommSemiring R
inst✝² : IsLocalRing R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : IsLocalRing S
f : R →+* S
this : IsLocalHom f ↔ Ideal.comap f (maximalIdeal S) = maximalIdeal R
⊢ Ideal.comap f (maximalIdeal S) = maximalIdeal R ↔
    ((PrimeSpectrum.comap f) (closedPoint S)).asIdeal = (closedPoint R).asIdeal

Tactic:
rfl

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem scale_eq_mul (x) [NF x] : ∀ (o) [NF o], scale x o = oadd x 1 0 * o
  | 0, _ => rfl
  | oadd e n a, h => by
    simp only [HMul.hMul]; simp only [scale]
    haveI := h.snd
    by_cases e0 : e = 0
    · simp_rw [scale_eq_mul]
      simp [Mul.mul, mul, scale_eq_mul, e0, h.zero_of_zero,
        show x + 0 = x from repr_inj.1 (by simp)]
    · simp [e0, Mul.mul, mul, scale_eq_mul, (· * ·)]

Proof state:
case pos
x : ONote
inst✝ : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
this : a.NF
e0 : e = 0
⊢ (x + e).oadd n (x.scale a) = Mul.mul (x.oadd 1 0) (e.oadd n a)

Tactic:
simp_rw [scale_eq_mul]

Result:
case pos
x : ONote
inst✝ : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
this : a.NF
e0 : e = 0
⊢ (x + e).oadd n (x.oadd 1 0 * a) = Mul.mul (x.oadd 1 0) (e.oadd n a)

Proof state:
x : ONote
inst✝ : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
⊢ (x + e).oadd n (x.scale a) = Mul.mul (x.oadd 1 0) (e.oadd n a)

Tactic:
haveI := h.snd

Result:
x : ONote
inst✝ : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
this : a.NF
⊢ (x + e).oadd n (x.scale a) = Mul.mul (x.oadd 1 0) (e.oadd n a)

Proof state:
x : ONote
inst✝ : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
this : a.NF
e0 : e = 0
⊢ (x + 0).repr = x.repr

Tactic:
simp

Result:
no goals

Proof state:
case pos
x : ONote
inst✝ : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
this : a.NF
e0 : e = 0
⊢ (x + e).oadd n (x.oadd 1 0 * a) = Mul.mul (x.oadd 1 0) (e.oadd n a)

Tactic:
simp [Mul.mul, mul, scale_eq_mul, e0, h.zero_of_zero,
  show x + 0 = x from repr_inj.1 (by simp)]

Result:
no goals

Proof state:
x : ONote
inst✝ : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
this : a.NF
⊢ (x + e).oadd n (x.scale a) = Mul.mul (x.oadd 1 0) (e.oadd n a)

Tactic:
by_cases e0 : e = 0

Result:
case pos
x : ONote
inst✝ : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
this : a.NF
e0 : e = 0
⊢ (x + e).oadd n (x.scale a) = Mul.mul (x.oadd 1 0) (e.oadd n a)

case neg
x : ONote
inst✝ : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
this : a.NF
e0 : ¬e = 0
⊢ (x + e).oadd n (x.scale a) = Mul.mul (x.oadd 1 0) (e.oadd n a)

Proof state:
x : ONote
inst✝ : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
⊢ x.scale (e.oadd n a) = Mul.mul (x.oadd 1 0) (e.oadd n a)

Tactic:
simp only [scale]

Result:
x : ONote
inst✝ : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
⊢ (x + e).oadd n (x.scale a) = Mul.mul (x.oadd 1 0) (e.oadd n a)

Proof state:
x : ONote
inst✝ : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
⊢ x.scale (e.oadd n a) = x.oadd 1 0 * e.oadd n a

Tactic:
simp only [HMul.hMul]

Result:
x : ONote
inst✝ : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
⊢ x.scale (e.oadd n a) = Mul.mul (x.oadd 1 0) (e.oadd n a)