harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/CharP/MixedCharZero.lean
theorem split_equalCharZero_mixedCharZero [CharZero R] (h_equal : Algebra ℚ R → P)
    (h_mixed : ∀ p : ℕ, Nat.Prime p → MixedCharZero R p → P) : P

Proof state:
case pos
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : CharZero R
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
h : ∃ p > 0, MixedCharZero R p
⊢ P

Tactic:
rcases h with ⟨p, ⟨H, hp⟩⟩

Result:
case pos.intro.intro
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : CharZero R
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
H : p > 0
hp : MixedCharZero R p
⊢ P

Proof state:
case pos.intro.intro
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : CharZero R
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
H : p > 0
hp : MixedCharZero R p
⊢ P

Tactic:
rw [← MixedCharZero.reduce_to_p_prime] at h_mixed

Result:
case pos.intro.intro
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : CharZero R
h_equal : Algebra ℚ R → P
h_mixed : ∀ p > 0, MixedCharZero R p → P
p : ℕ
H : p > 0
hp : MixedCharZero R p
⊢ P

Proof state:
case neg
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : CharZero R
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
h : ¬∃ p > 0, MixedCharZero R p
⊢ P

Tactic:
apply h_equal

Result:
case neg
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : CharZero R
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
h : ¬∃ p > 0, MixedCharZero R p
⊢ Algebra ℚ R

Proof state:
case pos.intro.intro
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : CharZero R
h_equal : Algebra ℚ R → P
h_mixed : ∀ p > 0, MixedCharZero R p → P
p : ℕ
H : p > 0
hp : MixedCharZero R p
⊢ P

Tactic:
exact h_mixed p H hp

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : CharZero R
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
⊢ P

Tactic:
by_cases h : ∃ p > 0, MixedCharZero R p

Result:
case pos
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : CharZero R
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
h : ∃ p > 0, MixedCharZero R p
⊢ P

case neg
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : CharZero R
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
h : ¬∃ p > 0, MixedCharZero R p
⊢ P

Proof state:
case neg
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : CharZero R
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
h : Nonempty (Algebra ℚ R)
⊢ Algebra ℚ R

Tactic:
exact h.some

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : CharZero R
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
h : ¬∃ p > 0, MixedCharZero R p
⊢ Algebra ℚ R

Tactic:
rw [← isEmpty_algebraRat_iff_mixedCharZero, not_isEmpty_iff] at h

Result:
case neg
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : CharZero R
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
h : Nonempty (Algebra ℚ R)
⊢ Algebra ℚ R
-- Mathlib/Analysis/Analytic/Constructions.lean
lemma HasFPowerSeriesOnBall.pi
    (hf : ∀ i, HasFPowerSeriesOnBall (f i) (p i) e r) (hr : 0 < r) :
    HasFPowerSeriesOnBall (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) e r

Proof state:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
hf : ∀ (i : ι), HasFPowerSeriesOnBall (f i) (p i) e r
hr : 0 < r
⊢ HasFPowerSeriesOnBall (fun x x_1 => f x_1 x) (FormalMultilinearSeries.pi p) e r

Tactic:
simp_rw [← hasFPowerSeriesWithinOnBall_univ] at hf ⊢

Result:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
hr : 0 < r
hf : ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) Set.univ e r
⊢ HasFPowerSeriesWithinOnBall (fun x x_1 => f x_1 x) (FormalMultilinearSeries.pi p) Set.univ e r

Proof state:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
hr : 0 < r
hf : ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) Set.univ e r
⊢ HasFPowerSeriesWithinOnBall (fun x x_1 => f x_1 x) (FormalMultilinearSeries.pi p) Set.univ e r

Tactic:
exact HasFPowerSeriesWithinOnBall.pi hf hr

Result:
no goals
-- Mathlib/Logic/Equiv/Fin.lean
theorem coe_finRotate_of_ne_last {i : Fin n.succ} (h : i ≠ Fin.last n) :
    (finRotate (n + 1) i : ℕ) = i + 1

Proof state:
n : ℕ
i : Fin n.succ
h : i ≠ Fin.last n
this : ↑i < n
⊢ ↑(i + 1) = ↑i + 1

Tactic:
exact Fin.val_add_one_of_lt this

Result:
no goals

Proof state:
n : ℕ
i : Fin n.succ
h : i ≠ Fin.last n
⊢ ↑((finRotate (n + 1)) i) = ↑i + 1

Tactic:
rw [finRotate_succ_apply]

Result:
n : ℕ
i : Fin n.succ
h : i ≠ Fin.last n
⊢ ↑(i + 1) = ↑i + 1

Proof state:
n : ℕ
i : Fin n.succ
h : i ≠ Fin.last n
⊢ ↑(i + 1) = ↑i + 1

Tactic:
have : (i : ℕ) < n := Fin.val_lt_last h

Result:
n : ℕ
i : Fin n.succ
h : i ≠ Fin.last n
this : ↑i < n
⊢ ↑(i + 1) = ↑i + 1
-- Mathlib/Order/Interval/Set/OrdConnected.lean
theorem ordConnected_image {E : Type*} [EquivLike E α β] [OrderIsoClass E α β] (e : E) {s : Set α}
    [hs : OrdConnected s] : OrdConnected (e '' s)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
E : Type u_3
inst✝¹ : EquivLike E α β
inst✝ : OrderIsoClass E α β
e : E
s : Set α
hs : s.OrdConnected
⊢ (⇑(↑e).symm ⁻¹' s).OrdConnected

Tactic:
apply ordConnected_preimage (e : α ≃o β).symm

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
E : Type u_3
inst✝¹ : EquivLike E α β
inst✝ : OrderIsoClass E α β
e : E
s : Set α
hs : s.OrdConnected
⊢ (⇑e '' s).OrdConnected

Tactic:
erw [(e : α ≃o β).image_eq_preimage]

Result:
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
E : Type u_3
inst✝¹ : EquivLike E α β
inst✝ : OrderIsoClass E α β
e : E
s : Set α
hs : s.OrdConnected
⊢ (⇑(↑e).symm ⁻¹' s).OrdConnected
-- Mathlib/Algebra/Order/Invertible.lean
theorem invOf_nonneg [Invertible a] : 0 ≤ ⅟ a ↔ 0 ≤ a :=
  haveI : 0 < a * ⅟ a

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedSemiring α
a : α
inst✝ : Invertible a
⊢ 0 < a * ⅟a

Tactic:
simp only [mul_invOf_self, zero_lt_one]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Basic.lean
theorem shiftComm' (i j : A) :
    f⟦i⟧'⟦j⟧' = (shiftComm _ _ _).hom ≫ f⟦j⟧'⟦i⟧' ≫ (shiftComm _ _ _).hom

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
i j : A
⊢ (shiftFunctor C j).map ((shiftFunctor C i).map f) =
    (shiftComm X i j).hom ≫ (shiftFunctor C i).map ((shiftFunctor C j).map f) ≫ (shiftComm Y j i).hom

Tactic:
erw [← shiftComm_symm Y i j, ← ((shiftFunctorComm C i j).hom.naturality_assoc f)]

Result:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
i j : A
⊢ (shiftFunctor C j).map ((shiftFunctor C i).map f) =
    (shiftFunctor C i ⋙ shiftFunctor C j).map f ≫ (shiftFunctorComm C i j).hom.app Y ≫ (shiftComm Y i j).symm.hom

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
i j : A
⊢ (shiftFunctor C j).map ((shiftFunctor C i).map f) =
    (shiftFunctor C j).map ((shiftFunctor C i).map f) ≫
      (shiftFunctorComm C i j).hom.app Y ≫ (shiftFunctorComm C i j).inv.app Y

Tactic:
simp only [Iso.hom_inv_id_app, Functor.comp_obj, Category.comp_id]

Result:
no goals

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
i j : A
⊢ (shiftFunctor C j).map ((shiftFunctor C i).map f) =
    (shiftFunctor C i ⋙ shiftFunctor C j).map f ≫ (shiftFunctorComm C i j).hom.app Y ≫ (shiftComm Y i j).symm.hom

Tactic:
dsimp

Result:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
i j : A
⊢ (shiftFunctor C j).map ((shiftFunctor C i).map f) =
    (shiftFunctor C j).map ((shiftFunctor C i).map f) ≫
      (shiftFunctorComm C i j).hom.app Y ≫ (shiftFunctorComm C i j).inv.app Y
-- Mathlib/SetTheory/Game/Birthday.lean
theorem birthday_ordinalToGame (o : Ordinal) : birthday o.toGame = o

Proof state:
case a
o : Ordinal.{u_1}
x : PGame
hx₁ : x ≈ o.toPGame
hx₂ : x.birthday = (toGame o).birthday
⊢ o.toPGame ≤ x.birthday.toPGame

Tactic:
exact hx₁.2.trans (PGame.le_birthday x)

Result:
no goals

Proof state:
case a
o : Ordinal.{u_1}
⊢ (toGame o).birthday ≤ o

Tactic:
conv_rhs => rw [← PGame.birthday_ordinalToPGame o]

Result:
case a
o : Ordinal.{u_1}
⊢ (toGame o).birthday ≤ o.toPGame.birthday

Proof state:
case a
o : Ordinal.{u_1}
x : PGame
hx₁ : ⟦x⟧ = toGame o
hx₂ : x.birthday = (toGame o).birthday
⊢ o.toPGame ≤ x.birthday.toPGame

Tactic:
rw [← mk_toPGame, ← PGame.equiv_iff_game_eq] at hx₁

Result:
case a
o : Ordinal.{u_1}
x : PGame
hx₁ : x ≈ o.toPGame
hx₂ : x.birthday = (toGame o).birthday
⊢ o.toPGame ≤ x.birthday.toPGame

Proof state:
o : Ordinal.{u_1}
⊢ (toGame o).birthday = o

Tactic:
apply le_antisymm

Result:
case a
o : Ordinal.{u_1}
⊢ (toGame o).birthday ≤ o

case a
o : Ordinal.{u_1}
⊢ o ≤ (toGame o).birthday

Proof state:
case a
o : Ordinal.{u_1}
x : PGame
hx₁ : ⟦x⟧ = toGame o
hx₂ : x.birthday = (toGame o).birthday
⊢ o ≤ (toGame o).birthday

Tactic:
rw [← hx₂, ← toPGame_le_iff]

Result:
case a
o : Ordinal.{u_1}
x : PGame
hx₁ : ⟦x⟧ = toGame o
hx₂ : x.birthday = (toGame o).birthday
⊢ o.toPGame ≤ x.birthday.toPGame

Proof state:
case a
o : Ordinal.{u_1}
⊢ (toGame o).birthday ≤ o.toPGame.birthday

Tactic:
apply birthday_quot_le_pGameBirthday

Result:
no goals

Proof state:
case a
o : Ordinal.{u_1}
⊢ o ≤ (toGame o).birthday

Tactic:
let ⟨x, hx₁, hx₂⟩ := birthday_eq_pGameBirthday o.toGame

Result:
case a
o : Ordinal.{u_1}
x : PGame
hx₁ : ⟦x⟧ = toGame o
hx₂ : x.birthday = (toGame o).birthday
⊢ o ≤ (toGame o).birthday
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
@[simp] lemma binEntropy_two_inv : binEntropy 2⁻¹ = log 2

Proof state:
⊢ 1 / 2 * log 2 + 1 / 2 * log 2 = log 2

Tactic:
simp

Result:
⊢ 2⁻¹ * log 2 + 2⁻¹ * log 2 = log 2

Proof state:
⊢ binEntropy 2⁻¹ = log 2

Tactic:
norm_num [binEntropy]

Result:
⊢ 1 / 2 * log 2 + 1 / 2 * log 2 = log 2

Proof state:
⊢ 2⁻¹ * log 2 + 2⁻¹ * log 2 = log 2

Tactic:
ring

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Pi.lean
theorem measurePreserving_arrowCongr' {α₁ β₁ α₂ β₂ : Type*} [Fintype α₁] [Fintype α₂]
    [MeasurableSpace β₁] [MeasurableSpace β₂] (μ : α₁ → Measure β₁) (ν : α₂ → Measure β₂)
    [∀ i, SigmaFinite (ν i)] (eα : α₁ ≃ α₂) (eβ : β₁ ≃ᵐ β₂)
    (hm : ∀ i, MeasurePreserving eβ (μ i) (ν (eα i))) :
    MeasurePreserving (MeasurableEquiv.arrowCongr' eα eβ) (Measure.pi fun i ↦ μ i)
      (Measure.pi fun i ↦ ν i)

Proof state:
α₁ : Type u_4
β₁ : Type u_5
α₂ : Type u_6
β₂ : Type u_7
inst✝⁴ : Fintype α₁
inst✝³ : Fintype α₂
inst✝² : MeasurableSpace β₁
inst✝¹ : MeasurableSpace β₂
μ : α₁ → Measure β₁
ν : α₂ → Measure β₂
inst✝ : ∀ (i : α₂), SigmaFinite (ν i)
eα : α₁ ≃ α₂
eβ : β₁ ≃ᵐ β₂
hm : ∀ (i : α₁), MeasurePreserving (⇑eβ) (μ i) (ν (eα i))
⊢ MeasurePreserving (⇑(MeasurableEquiv.arrowCongr' eα eβ)) (Measure.pi fun i => μ i) (Measure.pi fun i => ν i)

Tactic:
classical
convert (measurePreserving_piCongrLeft (fun i : α₂ ↦ ν i) eα).comp
  (measurePreserving_pi μ (fun i : α₁ ↦ ν (eα i)) hm)
simp only [MeasurableEquiv.arrowCongr', Equiv.arrowCongr', Equiv.arrowCongr, EquivLike.coe_coe,
  comp_def, MeasurableEquiv.coe_mk, Equiv.coe_fn_mk, MeasurableEquiv.piCongrLeft,
  Equiv.piCongrLeft, Equiv.symm_symm, Equiv.piCongrLeft', eq_rec_constant, Equiv.coe_fn_symm_mk]

Result:
no goals

Proof state:
case h.e'_5
α₁ : Type u_4
β₁ : Type u_5
α₂ : Type u_6
β₂ : Type u_7
inst✝⁴ : Fintype α₁
inst✝³ : Fintype α₂
inst✝² : MeasurableSpace β₁
inst✝¹ : MeasurableSpace β₂
μ : α₁ → Measure β₁
ν : α₂ → Measure β₂
inst✝ : ∀ (i : α₂), SigmaFinite (ν i)
eα : α₁ ≃ α₂
eβ : β₁ ≃ᵐ β₂
hm : ∀ (i : α₁), MeasurePreserving (⇑eβ) (μ i) (ν (eα i))
⊢ ⇑(MeasurableEquiv.arrowCongr' eα eβ) = ⇑(MeasurableEquiv.piCongrLeft (fun i => β₂) eα) ∘ fun a i => eβ (a i)

Tactic:
simp only [MeasurableEquiv.arrowCongr', Equiv.arrowCongr', Equiv.arrowCongr, EquivLike.coe_coe,
  comp_def, MeasurableEquiv.coe_mk, Equiv.coe_fn_mk, MeasurableEquiv.piCongrLeft,
  Equiv.piCongrLeft, Equiv.symm_symm, Equiv.piCongrLeft', eq_rec_constant, Equiv.coe_fn_symm_mk]

Result:
no goals

Proof state:
α₁ : Type u_4
β₁ : Type u_5
α₂ : Type u_6
β₂ : Type u_7
inst✝⁴ : Fintype α₁
inst✝³ : Fintype α₂
inst✝² : MeasurableSpace β₁
inst✝¹ : MeasurableSpace β₂
μ : α₁ → Measure β₁
ν : α₂ → Measure β₂
inst✝ : ∀ (i : α₂), SigmaFinite (ν i)
eα : α₁ ≃ α₂
eβ : β₁ ≃ᵐ β₂
hm : ∀ (i : α₁), MeasurePreserving (⇑eβ) (μ i) (ν (eα i))
⊢ MeasurePreserving (⇑(MeasurableEquiv.arrowCongr' eα eβ)) (Measure.pi fun i => μ i) (Measure.pi fun i => ν i)

Tactic:
convert (measurePreserving_piCongrLeft (fun i : α₂ ↦ ν i) eα).comp
  (measurePreserving_pi μ (fun i : α₁ ↦ ν (eα i)) hm)

Result:
case h.e'_5
α₁ : Type u_4
β₁ : Type u_5
α₂ : Type u_6
β₂ : Type u_7
inst✝⁴ : Fintype α₁
inst✝³ : Fintype α₂
inst✝² : MeasurableSpace β₁
inst✝¹ : MeasurableSpace β₂
μ : α₁ → Measure β₁
ν : α₂ → Measure β₂
inst✝ : ∀ (i : α₂), SigmaFinite (ν i)
eα : α₁ ≃ α₂
eβ : β₁ ≃ᵐ β₂
hm : ∀ (i : α₁), MeasurePreserving (⇑eβ) (μ i) (ν (eα i))
⊢ ⇑(MeasurableEquiv.arrowCongr' eα eβ) = ⇑(MeasurableEquiv.piCongrLeft (fun i => β₂) eα) ∘ fun a i => eβ (a i)
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
theorem derivWithin_add (hf : DifferentiableWithinAt 𝕜 f s x)
    (hg : DifferentiableWithinAt 𝕜 g s x) :
    derivWithin (fun y => f y + g y) s x = derivWithin f s x + derivWithin g s x

Proof state:
case inl
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : 𝕜 → F
x : 𝕜
s : Set 𝕜
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y => f y + g y) s x = derivWithin f s x + derivWithin g s x

Tactic:
exact (hf.hasDerivWithinAt.add hg.hasDerivWithinAt).derivWithin hxs

Result:
no goals

Proof state:
case inr
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : 𝕜 → F
x : 𝕜
s : Set 𝕜
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun y => f y + g y) s x = derivWithin f s x + derivWithin g s x

Tactic:
simp [derivWithin_zero_of_isolated hxs]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : 𝕜 → F
x : 𝕜
s : Set 𝕜
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
⊢ derivWithin (fun y => f y + g y) s x = derivWithin f s x + derivWithin g s x

Tactic:
rcases uniqueDiffWithinAt_or_nhdsWithin_eq_bot s x with hxs | hxs

Result:
case inl
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : 𝕜 → F
x : 𝕜
s : Set 𝕜
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y => f y + g y) s x = derivWithin f s x + derivWithin g s x

case inr
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : 𝕜 → F
x : 𝕜
s : Set 𝕜
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun y => f y + g y) s x = derivWithin f s x + derivWithin g s x
-- Mathlib/Analysis/RCLike/Basic.lean
lemma nnnorm_nsmul [NormedAddCommGroup E] [NormedSpace K E] (n : ℕ) (x : E) :
    ‖n • x‖₊ = n • ‖x‖₊

Proof state:
K : Type u_1
E : Type u_2
inst✝² : RCLike K
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace K E
n : ℕ
x : E
⊢ ‖n • x‖₊ = n • ‖x‖₊

Tactic:
simpa [Nat.cast_smul_eq_nsmul] using nnnorm_smul (n : K) x

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem IsRestriction.subset (h : N ≤r M) : N.E ⊆ M.E

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).E ⊆ M.E

Tactic:
exact hR

Result:
no goals

Proof state:
α : Type u_1
M N : Matroid α
h : N ≤r M
⊢ N.E ⊆ M.E

Tactic:
obtain ⟨R, hR, rfl⟩ := h

Result:
case intro.intro
α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).E ⊆ M.E
-- Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
theorem LinearIndependent.comp (h : LinearIndependent R v) (f : ι' → ι) (hf : Injective f) :
    LinearIndependent R (v ∘ f)

Proof state:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : LinearIndependent R v
f : ι' → ι
hf : Injective f
⊢ LinearIndependent R (v ∘ f)

Tactic:
simpa [comp_def] using Injective.comp h (Finsupp.mapDomain_injective hf)

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma odd_iff : Odd n ↔ n % 2 = 1 :=
  ⟨fun ⟨m, hm⟩ ↦ by omega, fun h ↦ ⟨n / 2, (mod_add_div n 2).symm.trans (by rw [h, add_comm])⟩⟩

Proof state:
n : ℕ
x✝ : Odd n
m : ℕ
hm : n = 2 * m + 1
⊢ n % 2 = 1

Tactic:
omega

Result:
no goals

Proof state:
n : ℕ
h : n % 2 = 1
⊢ n % 2 + 2 * (n / 2) = 2 * (n / 2) + 1

Tactic:
rw [h, add_comm]

Result:
no goals
-- Mathlib/Order/Directed.lean
lemma prod {d₁ : Set α} {d₂ : Set β} (h₁ : DirectedOn (· ≼₁ ·) d₁) (h₂ : DirectedOn (· ≼₂ ·) d₂) :
    DirectedOn (fun p q ↦ p.1 ≼₁ q.1 ∧ p.2 ≼₂ q.2) (d₁ ×ˢ d₂) := fun _ hpd _ hqd => by
  obtain ⟨r₁, hdr₁, hpr₁, hqr₁⟩ := h₁ _ hpd.1 _ hqd.1
  obtain ⟨r₂, hdr₂, hpr₂, hqr₂⟩ := h₂ _ hpd.2 _ hqd.2
  exact ⟨⟨r₁, r₂⟩, ⟨hdr₁, hdr₂⟩, ⟨hpr₁, hpr₂⟩, ⟨hqr₁, hqr₂⟩⟩

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
r : α → α → Prop
r₂✝ : β → β → Prop
d₁ : Set α
d₂ : Set β
h₁ : DirectedOn (fun x1 x2 => r x1 x2) d₁
h₂ : DirectedOn (fun x1 x2 => r₂✝ x1 x2) d₂
x✝¹ : α × β
hpd : x✝¹ ∈ d₁ ×ˢ d₂
x✝ : α × β
hqd : x✝ ∈ d₁ ×ˢ d₂
r₁ : α
hdr₁ : r₁ ∈ d₁
hpr₁ : r x✝¹.1 r₁
hqr₁ : r x✝.1 r₁
r₂ : β
hdr₂ : r₂ ∈ d₂
hpr₂ : r₂✝ x✝¹.2 r₂
hqr₂ : r₂✝ x✝.2 r₂
⊢ ∃ z ∈ d₁ ×ˢ d₂, (fun p q => r p.1 q.1 ∧ r₂✝ p.2 q.2) x✝¹ z ∧ (fun p q => r p.1 q.1 ∧ r₂✝ p.2 q.2) x✝ z

Tactic:
exact ⟨⟨r₁, r₂⟩, ⟨hdr₁, hdr₂⟩, ⟨hpr₁, hpr₂⟩, ⟨hqr₁, hqr₂⟩⟩

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u
β : Type v
r : α → α → Prop
r₂ : β → β → Prop
d₁ : Set α
d₂ : Set β
h₁ : DirectedOn (fun x1 x2 => r x1 x2) d₁
h₂ : DirectedOn (fun x1 x2 => r₂ x1 x2) d₂
x✝¹ : α × β
hpd : x✝¹ ∈ d₁ ×ˢ d₂
x✝ : α × β
hqd : x✝ ∈ d₁ ×ˢ d₂
r₁ : α
hdr₁ : r₁ ∈ d₁
hpr₁ : r x✝¹.1 r₁
hqr₁ : r x✝.1 r₁
⊢ ∃ z ∈ d₁ ×ˢ d₂, (fun p q => r p.1 q.1 ∧ r₂ p.2 q.2) x✝¹ z ∧ (fun p q => r p.1 q.1 ∧ r₂ p.2 q.2) x✝ z

Tactic:
obtain ⟨r₂, hdr₂, hpr₂, hqr₂⟩ := h₂ _ hpd.2 _ hqd.2

Result:
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
r : α → α → Prop
r₂✝ : β → β → Prop
d₁ : Set α
d₂ : Set β
h₁ : DirectedOn (fun x1 x2 => r x1 x2) d₁
h₂ : DirectedOn (fun x1 x2 => r₂✝ x1 x2) d₂
x✝¹ : α × β
hpd : x✝¹ ∈ d₁ ×ˢ d₂
x✝ : α × β
hqd : x✝ ∈ d₁ ×ˢ d₂
r₁ : α
hdr₁ : r₁ ∈ d₁
hpr₁ : r x✝¹.1 r₁
hqr₁ : r x✝.1 r₁
r₂ : β
hdr₂ : r₂ ∈ d₂
hpr₂ : r₂✝ x✝¹.2 r₂
hqr₂ : r₂✝ x✝.2 r₂
⊢ ∃ z ∈ d₁ ×ˢ d₂, (fun p q => r p.1 q.1 ∧ r₂✝ p.2 q.2) x✝¹ z ∧ (fun p q => r p.1 q.1 ∧ r₂✝ p.2 q.2) x✝ z

Proof state:
α : Type u
β : Type v
r : α → α → Prop
r₂ : β → β → Prop
d₁ : Set α
d₂ : Set β
h₁ : DirectedOn (fun x1 x2 => r x1 x2) d₁
h₂ : DirectedOn (fun x1 x2 => r₂ x1 x2) d₂
x✝¹ : α × β
hpd : x✝¹ ∈ d₁ ×ˢ d₂
x✝ : α × β
hqd : x✝ ∈ d₁ ×ˢ d₂
⊢ ∃ z ∈ d₁ ×ˢ d₂, (fun p q => r p.1 q.1 ∧ r₂ p.2 q.2) x✝¹ z ∧ (fun p q => r p.1 q.1 ∧ r₂ p.2 q.2) x✝ z

Tactic:
obtain ⟨r₁, hdr₁, hpr₁, hqr₁⟩ := h₁ _ hpd.1 _ hqd.1

Result:
case intro.intro.intro
α : Type u
β : Type v
r : α → α → Prop
r₂ : β → β → Prop
d₁ : Set α
d₂ : Set β
h₁ : DirectedOn (fun x1 x2 => r x1 x2) d₁
h₂ : DirectedOn (fun x1 x2 => r₂ x1 x2) d₂
x✝¹ : α × β
hpd : x✝¹ ∈ d₁ ×ˢ d₂
x✝ : α × β
hqd : x✝ ∈ d₁ ×ˢ d₂
r₁ : α
hdr₁ : r₁ ∈ d₁
hpr₁ : r x✝¹.1 r₁
hqr₁ : r x✝.1 r₁
⊢ ∃ z ∈ d₁ ×ˢ d₂, (fun p q => r p.1 q.1 ∧ r₂ p.2 q.2) x✝¹ z ∧ (fun p q => r p.1 q.1 ∧ r₂ p.2 q.2) x✝ z
-- Mathlib/CategoryTheory/Limits/IsLimit.lean
theorem cone_fac (s : Cone F) : (limitCone h).extend (homOfCone h s) = s

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : yoneda.obj X ⋙ uliftFunctor.{u₁, v₃} ≅ F.cones
s : Cone F
⊢ (limitCone h).extend (homOfCone h (coneOfHom h (homOfCone h s))) = coneOfHom h (homOfCone h s)

Tactic:
conv_lhs => simp only [homOfCone_coneOfHom]

Result:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : yoneda.obj X ⋙ uliftFunctor.{u₁, v₃} ≅ F.cones
s : Cone F
⊢ (limitCone h).extend (homOfCone h s) = coneOfHom h (homOfCone h s)

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : yoneda.obj X ⋙ uliftFunctor.{u₁, v₃} ≅ F.cones
s : Cone F
⊢ (limitCone h).extend (homOfCone h s) = s

Tactic:
rw [← coneOfHom_homOfCone h s]

Result:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : yoneda.obj X ⋙ uliftFunctor.{u₁, v₃} ≅ F.cones
s : Cone F
⊢ (limitCone h).extend (homOfCone h (coneOfHom h (homOfCone h s))) = coneOfHom h (homOfCone h s)

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : yoneda.obj X ⋙ uliftFunctor.{u₁, v₃} ≅ F.cones
s : Cone F
⊢ (limitCone h).extend (homOfCone h s) = coneOfHom h (homOfCone h s)

Tactic:
apply (coneOfHom_fac _ _).symm

Result:
no goals