harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Nimber/Field.lean
theorem one_mul (a : Nimber) : 1 * a = a

Proof state:
case a
a : Nimber
⊢ a ≤ 1 * a

Tactic:
by_contra! h

Result:
case a
a : Nimber
h : 1 * a < a
⊢ False

Proof state:
a : Nimber
⊢ 1 * a = a

Tactic:
apply le_antisymm

Result:
case a
a : Nimber
⊢ 1 * a ≤ a

case a
a : Nimber
⊢ a ≤ 1 * a

Proof state:
case a
a x : Nimber
hx : x < 1
y : Nimber
hy : y < a
⊢ x * a + 1 * y + x * y ≠ a

Tactic:
rw [Nimber.lt_one_iff_zero] at hx

Result:
case a
a x : Nimber
hx : x = 0
y : Nimber
hy : y < a
⊢ x * a + 1 * y + x * y ≠ a

Proof state:
case a
a x : Nimber
hx : x = 0
y : Nimber
hy : y < a
⊢ x * a + 1 * y + x * y ≠ a

Tactic:
rw [hx, Nimber.one_mul, zero_mul, zero_mul, add_zero, zero_add]

Result:
case a
a x : Nimber
hx : x = 0
y : Nimber
hy : y < a
⊢ y ≠ a

Proof state:
case a
a : Nimber
⊢ 1 * a ≤ a

Tactic:
refine mul_le_of_forall_ne fun x hx y hy ↦ ?_

Result:
case a
a x : Nimber
hx : x < 1
y : Nimber
hy : y < a
⊢ x * a + 1 * y + x * y ≠ a

Proof state:
case a
a : Nimber
h : 1 * a < a
⊢ False

Tactic:
exact (mul_left_cancel₀ one_ne_zero <| Nimber.one_mul _).not_lt h

Result:
no goals

Proof state:
case a
a x : Nimber
hx : x = 0
y : Nimber
hy : y < a
⊢ y ≠ a

Tactic:
exact hy.ne

Result:
no goals
-- Mathlib/Topology/MetricSpace/DilationEquiv.lean
theorem coe_pow (e : X ≃ᵈ X) (n : ℕ) : ⇑(e ^ n) = e^[n]

Proof state:
X : Type u_1
inst✝ : PseudoEMetricSpace X
e : X ≃ᵈ X
n : ℕ
⊢ (⇑(toPerm e))^[n] = (⇑e)^[n]

Tactic:
rfl

Result:
no goals

Proof state:
X : Type u_1
inst✝ : PseudoEMetricSpace X
e : X ≃ᵈ X
n : ℕ
⊢ ⇑(e ^ n) = (⇑e)^[n]

Tactic:
rw [← coe_toEquiv, ← toPerm_apply, map_pow, Equiv.Perm.coe_pow]

Result:
X : Type u_1
inst✝ : PseudoEMetricSpace X
e : X ≃ᵈ X
n : ℕ
⊢ (⇑(toPerm e))^[n] = (⇑e)^[n]
-- Mathlib/Logic/Equiv/Basic.lean
theorem Perm.subtypeCongr.refl :
    Perm.subtypeCongr (Equiv.refl { a // p a }) (Equiv.refl { a // ¬p a }) = Equiv.refl ε

Proof state:
case H
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
x : ε
⊢ (subtypeCongr (Equiv.refl { a // p a }) (Equiv.refl { a // ¬p a })) x = (Equiv.refl ε) x

Tactic:
by_cases h : p x <;> simp [h]

Result:
no goals

Proof state:
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
⊢ subtypeCongr (Equiv.refl { a // p a }) (Equiv.refl { a // ¬p a }) = Equiv.refl ε

Tactic:
ext x

Result:
case H
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
x : ε
⊢ (subtypeCongr (Equiv.refl { a // p a }) (Equiv.refl { a // ¬p a })) x = (Equiv.refl ε) x
-- Mathlib/Analysis/Convex/Exposed.lean
theorem convex (hAB : IsExposed 𝕜 A B) (hA : Convex 𝕜 A) : Convex 𝕜 B

Proof state:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
hA : Convex 𝕜 A
hAB : IsExposed 𝕜 A ∅
⊢ Convex 𝕜 ∅

Tactic:
exact convex_empty

Result:
no goals

Proof state:
case inr.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
hA : Convex 𝕜 A
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
hB : {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}.Nonempty
⊢ Convex 𝕜 {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}

Tactic:
exact fun x₁ hx₁ x₂ hx₂ a b ha hb hab =>
  ⟨hA hx₁.1 hx₂.1 ha hb hab, fun y hy =>
    ((l.toLinearMap.concaveOn convex_univ).convex_ge _ ⟨mem_univ _, hx₁.2 y hy⟩
        ⟨mem_univ _, hx₂.2 y hy⟩ ha hb hab).2⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B : Set E
hAB : IsExposed 𝕜 A B
hA : Convex 𝕜 A
⊢ Convex 𝕜 B

Tactic:
obtain rfl | hB := B.eq_empty_or_nonempty

Result:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
hA : Convex 𝕜 A
hAB : IsExposed 𝕜 A ∅
⊢ Convex 𝕜 ∅

case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B : Set E
hAB : IsExposed 𝕜 A B
hA : Convex 𝕜 A
hB : B.Nonempty
⊢ Convex 𝕜 B

Proof state:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B : Set E
hAB : IsExposed 𝕜 A B
hA : Convex 𝕜 A
hB : B.Nonempty
⊢ Convex 𝕜 B

Tactic:
obtain ⟨l, rfl⟩ := hAB hB

Result:
case inr.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
hA : Convex 𝕜 A
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
hB : {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}.Nonempty
⊢ Convex 𝕜 {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
-- Mathlib/Data/ZMod/ValMinAbs.lean
lemma natCast_natAbs_valMinAbs [NeZero n] (a : ZMod n) :
    (a.valMinAbs.natAbs : ZMod n) = if a.val ≤ (n : ℕ) / 2 then a else -a

Proof state:
case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑a.val - ↑n ≤ 0
h✝ : ¬a.val ≤ n / 2
⊢ ↑(↑a.val - ↑n).natAbs = -a

Tactic:
rw [← Int.cast_natCast, Int.ofNat_natAbs_of_nonpos this, Int.cast_neg, Int.cast_sub,
  Int.cast_natCast, Int.cast_natCast, natCast_self, sub_zero, natCast_zmod_val]

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ ↑a.val - ↑n ≤ 0

Tactic:
rw [sub_nonpos, Int.ofNat_le]

Result:
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ a.val ≤ n

Proof state:
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ ↑a.valMinAbs.natAbs = if a.val ≤ n / 2 then a else -a

Tactic:
have : (a.val : ℤ) - n ≤ 0 := by
  rw [sub_nonpos, Int.ofNat_le]
  exact a.val_le

Result:
n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑a.val - ↑n ≤ 0
⊢ ↑a.valMinAbs.natAbs = if a.val ≤ n / 2 then a else -a

Proof state:
n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑a.val - ↑n ≤ 0
⊢ ↑a.valMinAbs.natAbs = if a.val ≤ n / 2 then a else -a

Tactic:
rw [valMinAbs_def_pos]

Result:
n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑a.val - ↑n ≤ 0
⊢ ↑(if a.val ≤ n / 2 then ↑a.val else ↑a.val - ↑n).natAbs = if a.val ≤ n / 2 then a else -a

Proof state:
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ a.val ≤ n

Tactic:
exact a.val_le

Result:
no goals

Proof state:
case pos
n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑a.val - ↑n ≤ 0
h✝ : a.val ≤ n / 2
⊢ ↑(↑a.val).natAbs = a

Tactic:
rw [Int.natAbs_ofNat, natCast_zmod_val]

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑a.val - ↑n ≤ 0
⊢ ↑(if a.val ≤ n / 2 then ↑a.val else ↑a.val - ↑n).natAbs = if a.val ≤ n / 2 then a else -a

Tactic:
split_ifs

Result:
case pos
n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑a.val - ↑n ≤ 0
h✝ : a.val ≤ n / 2
⊢ ↑(↑a.val).natAbs = a

case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑a.val - ↑n ≤ 0
h✝ : ¬a.val ≤ n / 2
⊢ ↑(↑a.val - ↑n).natAbs = -a
-- Mathlib/NumberTheory/Harmonic/EulerMascheroni.lean
lemma strictMono_eulerMascheroniSeq : StrictMono eulerMascheroniSeq

Proof state:
n : ℕ
⊢ ↑(n + 1) + 1 ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
n : ℕ
⊢ log (1 + (↑n + 1)⁻¹) < (↑n + 1)⁻¹

Tactic:
refine (log_lt_sub_one_of_pos ?_ (ne_of_gt <| lt_add_of_pos_right _ ?_)).trans_le (le_of_eq ?_)

Result:
case refine_1
n : ℕ
⊢ 0 < 1 + (↑n + 1)⁻¹

case refine_2
n : ℕ
⊢ 0 < (↑n + 1)⁻¹

case refine_3
n : ℕ
⊢ 1 + (↑n + 1)⁻¹ - 1 = (↑n + 1)⁻¹

Proof state:
case refine_2
n : ℕ
⊢ 0 < (↑n + 1)⁻¹

Tactic:
positivity

Result:
no goals

Proof state:
case refine_3
n : ℕ
⊢ 1 + (↑n + 1)⁻¹ - 1 = (↑n + 1)⁻¹

Tactic:
simp only [add_sub_cancel_left]

Result:
no goals

Proof state:
⊢ StrictMono eulerMascheroniSeq

Tactic:
refine strictMono_nat_of_lt_succ (fun n ↦ ?_)

Result:
n : ℕ
⊢ eulerMascheroniSeq n < eulerMascheroniSeq (n + 1)

Proof state:
case refine_1
n : ℕ
⊢ 0 < 1 + (↑n + 1)⁻¹

Tactic:
positivity

Result:
no goals

Proof state:
n : ℕ
⊢ eulerMascheroniSeq n < eulerMascheroniSeq (n + 1)

Tactic:
rw [eulerMascheroniSeq, eulerMascheroniSeq, ← sub_pos, sub_sub_sub_comm,
  harmonic_succ, add_comm, Rat.cast_add, add_sub_cancel_right,
  ← log_div (by positivity) (by positivity), add_div, Nat.cast_add_one,
  Nat.cast_add_one, div_self (by positivity), sub_pos, one_div, Rat.cast_inv, Rat.cast_add,
  Rat.cast_one, Rat.cast_natCast]

Result:
n : ℕ
⊢ log (1 + (↑n + 1)⁻¹) < (↑n + 1)⁻¹

Proof state:
n : ℕ
⊢ ↑n + 1 ≠ 0

Tactic:
positivity

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/Comp.lean
theorem comp_restrict {s : Set γ} (hs : MeasurableSet s) :
    η.restrict hs ∘ₖ κ = (η ∘ₖ κ).restrict hs

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
s : Set γ
hs : MeasurableSet s
a : α
t : Set γ
ht : MeasurableSet t
⊢ ((η.restrict hs ∘ₖ κ) a) t = (((η ∘ₖ κ).restrict hs) a) t

Tactic:
simp_rw [comp_apply' _ _ _ ht, restrict_apply' _ _ _ ht, comp_apply' _ _ _ (ht.inter hs)]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
s : Set γ
hs : MeasurableSet s
⊢ η.restrict hs ∘ₖ κ = (η ∘ₖ κ).restrict hs

Tactic:
ext a t ht

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
s : Set γ
hs : MeasurableSet s
a : α
t : Set γ
ht : MeasurableSet t
⊢ ((η.restrict hs ∘ₖ κ) a) t = (((η ∘ₖ κ).restrict hs) a) t
-- Mathlib/Algebra/Group/Basic.lean
theorem mul_right_comm (a b c : G) : a * b * c = a * c * b

Proof state:
G : Type u_3
inst✝ : CommSemigroup G
a b c : G
⊢ a * b * c = a * c * b

Tactic:
rw [mul_assoc, mul_comm b, mul_assoc]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
theorem GammaIntegral_ofReal (s : ℝ) :
    GammaIntegral ↑s = ↑(∫ x : ℝ in Ioi 0, Real.exp (-x) * x ^ (s - 1))

Proof state:
s : ℝ
this : ∀ (r : ℝ), ↑r = ↑r
⊢ ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (↑s - 1) = ↑(∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1))

Tactic:
conv_rhs => rw [this, ← _root_.integral_ofReal]

Result:
s : ℝ
this : ∀ (r : ℝ), ↑r = ↑r
⊢ ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (↑s - 1) = ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x) * x ^ (s - 1))

Proof state:
s : ℝ
this : ∀ (r : ℝ), ↑r = ↑r
⊢ (↑s).GammaIntegral = ↑(∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1))

Tactic:
rw [GammaIntegral]

Result:
s : ℝ
this : ∀ (r : ℝ), ↑r = ↑r
⊢ ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (↑s - 1) = ↑(∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1))

Proof state:
s : ℝ
this : ∀ (r : ℝ), ↑r = ↑r
x : ℝ
hx : x ∈ Ioi 0
⊢ ↑(rexp (-x)) * ↑x ^ (↑s - 1) = ↑(rexp (-x) * x ^ (s - 1))

Tactic:
rw [ofReal_mul, ofReal_cpow (mem_Ioi.mp hx).le]

Result:
s : ℝ
this : ∀ (r : ℝ), ↑r = ↑r
x : ℝ
hx : x ∈ Ioi 0
⊢ ↑(rexp (-x)) * ↑x ^ (↑s - 1) = ↑(rexp (-x)) * ↑x ^ ↑(s - 1)

Proof state:
s : ℝ
this : ∀ (r : ℝ), ↑r = ↑r
x : ℝ
hx : x ∈ Ioi 0
⊢ (fun x => ↑(rexp (-x)) * ↑x ^ (↑s - 1)) x = (fun x => ↑(rexp (-x) * x ^ (s - 1))) x

Tactic:
dsimp only

Result:
s : ℝ
this : ∀ (r : ℝ), ↑r = ↑r
x : ℝ
hx : x ∈ Ioi 0
⊢ ↑(rexp (-x)) * ↑x ^ (↑s - 1) = ↑(rexp (-x) * x ^ (s - 1))

Proof state:
s : ℝ
⊢ (↑s).GammaIntegral = ↑(∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1))

Tactic:
have : ∀ r : ℝ, Complex.ofReal r = @RCLike.ofReal ℂ _ r := fun r => rfl

Result:
s : ℝ
this : ∀ (r : ℝ), ↑r = ↑r
⊢ (↑s).GammaIntegral = ↑(∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1))

Proof state:
s : ℝ
this : ∀ (r : ℝ), ↑r = ↑r
⊢ ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (↑s - 1) = ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x) * x ^ (s - 1))

Tactic:
refine setIntegral_congr_fun measurableSet_Ioi ?_

Result:
s : ℝ
this : ∀ (r : ℝ), ↑r = ↑r
⊢ EqOn (fun x => ↑(rexp (-x)) * ↑x ^ (↑s - 1)) (fun x => ↑(rexp (-x) * x ^ (s - 1))) (Ioi 0)

Proof state:
s : ℝ
this : ∀ (r : ℝ), ↑r = ↑r
x : ℝ
hx : x ∈ Ioi 0
⊢ ↑(rexp (-x)) * ↑x ^ (↑s - 1) = ↑(rexp (-x)) * ↑x ^ ↑(s - 1)

Tactic:
simp

Result:
no goals

Proof state:
s : ℝ
this : ∀ (r : ℝ), ↑r = ↑r
⊢ EqOn (fun x => ↑(rexp (-x)) * ↑x ^ (↑s - 1)) (fun x => ↑(rexp (-x) * x ^ (s - 1))) (Ioi 0)

Tactic:
intro x hx

Result:
s : ℝ
this : ∀ (r : ℝ), ↑r = ↑r
x : ℝ
hx : x ∈ Ioi 0
⊢ (fun x => ↑(rexp (-x)) * ↑x ^ (↑s - 1)) x = (fun x => ↑(rexp (-x) * x ^ (s - 1))) x
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem ContinuousInv.of_nhds_one {G : Type*} [Group G] [TopologicalSpace G]
    (hinv : Tendsto (fun x : G => x⁻¹) (𝓝 1) (𝓝 1))
    (hleft : ∀ x₀ : G, 𝓝 x₀ = map (fun x : G => x₀ * x) (𝓝 1))
    (hconj : ∀ x₀ : G, Tendsto (fun x : G => x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)) : ContinuousInv G

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hinv : Tendsto (fun x => x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hconj : ∀ (x₀ : G), Tendsto (fun x => x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
x₀ : G
this : Tendsto (fun x => x₀⁻¹ * (x₀ * x⁻¹ * x₀⁻¹)) (𝓝 1) (map (fun x => x₀⁻¹ * x) (𝓝 1))
⊢ ContinuousAt (fun a => a⁻¹) x₀

Tactic:
simpa only [ContinuousAt, hleft x₀, hleft x₀⁻¹, tendsto_map'_iff, Function.comp_def, mul_assoc,
  mul_inv_rev, inv_mul_cancel_left] using this

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hinv : Tendsto (fun x => x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hconj : ∀ (x₀ : G), Tendsto (fun x => x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
⊢ ContinuousInv G

Tactic:
refine ⟨continuous_iff_continuousAt.2 fun x₀ => ?_⟩

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hinv : Tendsto (fun x => x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hconj : ∀ (x₀ : G), Tendsto (fun x => x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
x₀ : G
⊢ ContinuousAt (fun a => a⁻¹) x₀
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem _root_.IsOpen.is_const_of_deriv_eq_zero
    (hs : IsOpen s) (hs' : IsPreconnected s) (hf : DifferentiableOn 𝕜 f s)
    (hf' : s.EqOn (deriv f) 0) {x y : 𝕜} (hx : x ∈ s) (hy : y ∈ s) : f x = f y :=
  hs.is_const_of_fderiv_eq_zero hs' hf (fun a ha ↦ by ext; simp [← deriv_fderiv, hf' ha]) hx hy

Proof state:
𝕜 : Type u_3
G : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : 𝕜 → G
s : Set 𝕜
hs : IsOpen s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (deriv f) 0 s
x y : 𝕜
hx : x ∈ s
hy : y ∈ s
a : 𝕜
ha : a ∈ s
⊢ fderiv 𝕜 f a = 0 a

Tactic:
ext

Result:
case h
𝕜 : Type u_3
G : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : 𝕜 → G
s : Set 𝕜
hs : IsOpen s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (deriv f) 0 s
x y : 𝕜
hx : x ∈ s
hy : y ∈ s
a : 𝕜
ha : a ∈ s
⊢ (fderiv 𝕜 f a) 1 = (0 a) 1

Proof state:
case h
𝕜 : Type u_3
G : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : 𝕜 → G
s : Set 𝕜
hs : IsOpen s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (deriv f) 0 s
x y : 𝕜
hx : x ∈ s
hy : y ∈ s
a : 𝕜
ha : a ∈ s
⊢ (fderiv 𝕜 f a) 1 = (0 a) 1

Tactic:
simp [← deriv_fderiv, hf' ha]

Result:
no goals
-- Mathlib/Algebra/Homology/Homotopy.lean
theorem nullHomotopicMap'_f_of_not_rel_right {k₁ k₀ : ι} (r₁₀ : c.Rel k₁ k₀)
    (hk₁ : ∀ l : ι, ¬c.Rel l k₁) (h : ∀ i j, c.Rel j i → (C.X i ⟶ D.X j)) :
    (nullHomotopicMap' h).f k₁ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (nullHomotopicMap fun i j => dite (c.Rel j i) (h i j) fun x => 0).f k₁ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀

Tactic:
rw [nullHomotopicMap_f_of_not_rel_right r₁₀ hk₁]

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (C.d k₁ k₀ ≫ dite (c.Rel k₁ k₀) (h k₀ k₁) fun x => 0) = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (C.d k₁ k₀ ≫ dite (c.Rel k₁ k₀) (h k₀ k₁) fun x => 0) = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀

Tactic:
split_ifs

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (nullHomotopicMap' h).f k₁ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀

Tactic:
simp only [nullHomotopicMap']

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (nullHomotopicMap fun i j => dite (c.Rel j i) (h i j) fun x => 0).f k₁ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
lemma memLp_indicator_const (p : ℝ≥0∞) (hs : MeasurableSet s) (c : E) (hμsc : c = 0 ∨ μ s ≠ ∞) :
    MemLp (s.indicator fun _ => c) p μ

Proof state:
case inl
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
p : ℝ≥0∞
hs : MeasurableSet s
⊢ MemLp (fun x => 0) p (μ.restrict s)

Tactic:
exact MemLp.zero

Result:
no goals

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
p : ℝ≥0∞
hs : MeasurableSet s
c : E
hμsc : c = 0 ∨ μ s ≠ ⊤
⊢ MemLp (fun x => c) p (μ.restrict s)

Tactic:
obtain rfl | hμ := hμsc

Result:
case inl
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
p : ℝ≥0∞
hs : MeasurableSet s
⊢ MemLp (fun x => 0) p (μ.restrict s)

case inr
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
p : ℝ≥0∞
hs : MeasurableSet s
c : E
hμ : μ s ≠ ⊤
⊢ MemLp (fun x => c) p (μ.restrict s)

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
p : ℝ≥0∞
hs : MeasurableSet s
c : E
hμsc : c = 0 ∨ μ s ≠ ⊤
⊢ MemLp (s.indicator fun x => c) p μ

Tactic:
rw [memLp_indicator_iff_restrict hs]

Result:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
p : ℝ≥0∞
hs : MeasurableSet s
c : E
hμsc : c = 0 ∨ μ s ≠ ⊤
⊢ MemLp (fun x => c) p (μ.restrict s)

Proof state:
case inr
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
p : ℝ≥0∞
hs : MeasurableSet s
c : E
hμ : μ s ≠ ⊤
⊢ MemLp (fun x => c) p (μ.restrict s)

Tactic:
have := Fact.mk hμ.lt_top

Result:
case inr
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
p : ℝ≥0∞
hs : MeasurableSet s
c : E
hμ : μ s ≠ ⊤
this : Fact (μ s < ⊤)
⊢ MemLp (fun x => c) p (μ.restrict s)

Proof state:
case inr
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
p : ℝ≥0∞
hs : MeasurableSet s
c : E
hμ : μ s ≠ ⊤
this : Fact (μ s < ⊤)
⊢ MemLp (fun x => c) p (μ.restrict s)

Tactic:
apply memLp_const

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem degree_mul_comm (hp : p.Monic) (q : R[X]) : (p * q).degree = (q * p).degree

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : q = 0
⊢ (p * q).degree = (q * p).degree

Tactic:
simp [h]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
⊢ (p * q).degree = (q * p).degree

Tactic:
by_cases h : q = 0

Result:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : q = 0
⊢ (p * q).degree = (q * p).degree

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ (p * q).degree = (q * p).degree

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ p.degree + q.degree = q.degree + p.degree

Tactic:
exact add_comm _ _

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
rwa [hp.leadingCoeff, one_mul, leadingCoeff_ne_zero]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ (p * q).degree = (q * p).degree

Tactic:
rw [degree_mul', hp.degree_mul]

Result:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ p.degree + q.degree = q.degree + p.degree

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0
-- Mathlib/Analysis/InnerProductSpace/Symmetric.lean
theorem IsSymmetric.smul {c : 𝕜} (hc : conj c = c) {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) :
    c • T |>.IsSymmetric

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
c : 𝕜
hc : (starRingEnd 𝕜) c = c
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
⊢ inner ((c • T) x) y = inner x ((c • T) y)

Tactic:
simp only [smul_apply, inner_smul_left, hc, hT x y, inner_smul_right]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
c : 𝕜
hc : (starRingEnd 𝕜) c = c
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
⊢ (c • T).IsSymmetric

Tactic:
intro x y

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
c : 𝕜
hc : (starRingEnd 𝕜) c = c
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
⊢ inner ((c • T) x) y = inner x ((c • T) y)
-- Mathlib/Analysis/Analytic/IsolatedZeros.lean
/-- For a function `f` on `𝕜`, and `z₀ ∈ 𝕜`, there exists at most one `n` such that on a
neighbourhood of `z₀` we have `f z = (z - z₀) ^ n • g z`, with `g` analytic and nonvanishing at
`z₀`. -/
lemma unique_eventuallyEq_pow_smul_nonzero {m n : ℕ}
    (hm : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ z in 𝓝 z₀, f z = (z - z₀) ^ m • g z)
    (hn : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ z in 𝓝 z₀, f z = (z - z₀) ^ n • g z) :
    m = n

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
m n : ℕ
hm : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ ↑m • g z
hn : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ ↑n • g z
⊢ m = n

Tactic:
exact Int.ofNat_inj.mp <| unique_eventuallyEq_zpow_smul_nonzero
  (let ⟨g, h₁, h₂, h₃⟩ := hm; ⟨g, h₁, h₂, h₃.filter_mono nhdsWithin_le_nhds⟩)
  (let ⟨g, h₁, h₂, h₃⟩ := hn; ⟨g, h₁, h₂, h₃.filter_mono nhdsWithin_le_nhds⟩)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
m n : ℕ
hm : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ m • g z
hn : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
⊢ m = n

Tactic:
simp_rw [← zpow_natCast] at hm hn

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
m n : ℕ
hm : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ ↑m • g z
hn : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ ↑n • g z
⊢ m = n