harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem HasDerivAt.smul (hc : HasDerivAt c c' x) (hf : HasDerivAt f f' x) :
    HasDerivAt (fun y => c y • f y) (c x • f' + c' • f x) x

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
𝕜' : Type u_2
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivWithinAt c c' univ x
hf : HasDerivWithinAt f f' univ x
⊢ HasDerivWithinAt (fun y => c y • f y) (c x • f' + c' • f x) univ x

Tactic:
exact hc.smul hf

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
𝕜' : Type u_2
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivAt c c' x
hf : HasDerivAt f f' x
⊢ HasDerivAt (fun y => c y • f y) (c x • f' + c' • f x) x

Tactic:
rw [← hasDerivWithinAt_univ] at *

Result:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
𝕜' : Type u_2
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivWithinAt c c' univ x
hf : HasDerivWithinAt f f' univ x
⊢ HasDerivWithinAt (fun y => c y • f y) (c x • f' + c' • f x) univ x
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem _root_.IsOpen.is_const_of_fderiv_eq_zero
    (hs : IsOpen s) (hs' : IsPreconnected s) (hf : DifferentiableOn 𝕜 f s)
    (hf' : s.EqOn (fderiv 𝕜 f) 0) {x y : E} (hx : x ∈ s) (hy : y ∈ s) : f x = f y

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
x y : E
hx : x ∈ s
hy : y ∈ s
⊢ f x = f y

Tactic:
obtain ⟨a, ha⟩ := hs.exists_is_const_of_fderiv_eq_zero hs' hf hf'

Result:
case intro
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
x y : E
hx : x ∈ s
hy : y ∈ s
a : G
ha : ∀ x ∈ s, f x = a
⊢ f x = f y

Proof state:
case intro
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
x y : E
hx : x ∈ s
hy : y ∈ s
a : G
ha : ∀ x ∈ s, f x = a
⊢ f x = f y

Tactic:
rw [ha x hx, ha y hy]

Result:
no goals
-- Mathlib/RingTheory/Coprime/Lemmas.lean
theorem pow_right (H : IsRelPrime x y) : IsRelPrime x (y ^ n)

Proof state:
α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x y : α
n : ℕ
H : IsRelPrime x y
⊢ IsRelPrime x (∏ _x ∈ Finset.range n, y)

Tactic:
exact IsRelPrime.prod_right fun _ _ ↦ H

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x y : α
n : ℕ
H : IsRelPrime x y
⊢ IsRelPrime x (y ^ n)

Tactic:
rw [← Finset.card_range n, ← Finset.prod_const]

Result:
α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x y : α
n : ℕ
H : IsRelPrime x y
⊢ IsRelPrime x (∏ _x ∈ Finset.range n, y)
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Monadic.lean
theorem mapFinIdxM_toArray [Monad m] [LawfulMonad m] (l : List α)
    (f : (i : Nat) → α → (h : i < l.length) → m β) :
    l.toArray.mapFinIdxM f = toArray <$> l.mapFinIdxM f

Proof state:
case e_a.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : (i : Nat) → α → i < l.length → m β
i : Nat
acc : Array β
k : Nat
inv : k + 1 + acc.size = l.length
x : β
⊢ Array.mapFinIdxM.map l.toArray f k (acc.size + 1) ⋯ (acc.push x) =
    toArray <$> mapFinIdxM.go l f (drop (acc.size + 1) l) (acc.push x) ⋯

Tactic:
conv => enter [1, 4]; rw [← Array.size_push _ x]

Result:
case e_a.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : (i : Nat) → α → i < l.length → m β
i : Nat
acc : Array β
k : Nat
inv : k + 1 + acc.size = l.length
x : β
⊢ Array.mapFinIdxM.map l.toArray f k (acc.push x).size ⋯ (acc.push x) =
    toArray <$> mapFinIdxM.go l f (drop (acc.size + 1) l) (acc.push x) ⋯

Proof state:
case e_a
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : (i : Nat) → α → i < l.length → m β
i : Nat
acc : Array β
k : Nat
inv : k + 1 + acc.size = l.length
⊢ (fun __do_lift => Array.mapFinIdxM.map l.toArray f k (acc.size + 1) ⋯ (acc.push __do_lift)) = fun a =>
    toArray <$> mapFinIdxM.go l f (drop (acc.size + 1) l) (acc.push a) ⋯

Tactic:
funext x

Result:
case e_a.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : (i : Nat) → α → i < l.length → m β
i : Nat
acc : Array β
k : Nat
inv : k + 1 + acc.size = l.length
x : β
⊢ Array.mapFinIdxM.map l.toArray f k (acc.size + 1) ⋯ (acc.push x) =
    toArray <$> mapFinIdxM.go l f (drop (acc.size + 1) l) (acc.push x) ⋯
-- Mathlib/Topology/Connected/LocPathConnected.lean
/-- A space is locally path-connected iff all path components of open subsets are neighbourhoods. -/
lemma locPathConnectedSpace_iff_pathComponentIn_mem_nhds {X : Type*} [TopologicalSpace X] :
    LocPathConnectedSpace X ↔
    ∀ x : X, ∀ u : Set X, IsOpen u → x ∈ u → pathComponentIn x u ∈ nhds x

Proof state:
X : Type u_4
inst✝ : TopologicalSpace X
⊢ (∀ (x : X) (u : Set X), IsOpen u → IsOpen (pathComponentIn x u)) ↔
    ∀ (x : X) (u : Set X), IsOpen u → x ∈ u → pathComponentIn x u ∈ 𝓝 x

Tactic:
simp_rw [forall_comm (β := Set X), ← imp_forall_iff]

Result:
X : Type u_4
inst✝ : TopologicalSpace X
⊢ (∀ (b : Set X), IsOpen b → ∀ (x : X), IsOpen (pathComponentIn x b)) ↔
    ∀ (b : Set X), IsOpen b → ∀ x ∈ b, pathComponentIn x b ∈ 𝓝 x

Proof state:
X : Type u_4
inst✝ : TopologicalSpace X
u : Set X
x✝ : IsOpen u
⊢ (∀ (x : X), IsOpen (pathComponentIn x u)) ↔ ∀ x ∈ u, pathComponentIn x u ∈ 𝓝 x

Tactic:
exact ⟨fun h x hxu ↦ (h x).mem_nhds (mem_pathComponentIn_self hxu),
  fun h x ↦ isOpen_iff_mem_nhds.mpr fun y hy ↦
    pathComponentIn_congr hy ▸ h y <| pathComponentIn_subset hy⟩

Result:
no goals

Proof state:
X : Type u_4
inst✝ : TopologicalSpace X
⊢ LocPathConnectedSpace X ↔ ∀ (x : X) (u : Set X), IsOpen u → x ∈ u → pathComponentIn x u ∈ 𝓝 x

Tactic:
rw [locPathConnectedSpace_iff_isOpen_pathComponentIn]

Result:
X : Type u_4
inst✝ : TopologicalSpace X
⊢ (∀ (x : X) (u : Set X), IsOpen u → IsOpen (pathComponentIn x u)) ↔
    ∀ (x : X) (u : Set X), IsOpen u → x ∈ u → pathComponentIn x u ∈ 𝓝 x

Proof state:
X : Type u_4
inst✝ : TopologicalSpace X
⊢ (∀ (b : Set X), IsOpen b → ∀ (x : X), IsOpen (pathComponentIn x b)) ↔
    ∀ (b : Set X), IsOpen b → ∀ x ∈ b, pathComponentIn x b ∈ 𝓝 x

Tactic:
refine forall_congr' fun u ↦ imp_congr_right fun _ ↦ ?_

Result:
X : Type u_4
inst✝ : TopologicalSpace X
u : Set X
x✝ : IsOpen u
⊢ (∀ (x : X), IsOpen (pathComponentIn x u)) ↔ ∀ x ∈ u, pathComponentIn x u ∈ 𝓝 x
-- Mathlib/Probability/Kernel/Composition/CompProd.lean
@[simp]
lemma compProd_zero_left (κ : Kernel (α × β) γ) :
    (0 : Kernel α β) ⊗ₖ κ = 0

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel (α × β) γ
⊢ 0 ⊗ₖ κ = 0

Tactic:
by_cases h : IsSFiniteKernel κ

Result:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel (α × β) γ
h : IsSFiniteKernel κ
⊢ 0 ⊗ₖ κ = 0

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel (α × β) γ
h : ¬IsSFiniteKernel κ
⊢ 0 ⊗ₖ κ = 0

Proof state:
case pos.h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel (α × β) γ
h : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (κ (a, b)) {c | (b, c) ∈ s} ∂0 a = (0 a) s

Tactic:
simp

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel (α × β) γ
h : ¬IsSFiniteKernel κ
⊢ 0 ⊗ₖ κ = 0

Tactic:
rw [Kernel.compProd_of_not_isSFiniteKernel_right _ _ h]

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel (α × β) γ
h : IsSFiniteKernel κ
⊢ 0 ⊗ₖ κ = 0

Tactic:
ext a s hs

Result:
case pos.h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel (α × β) γ
h : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ((0 ⊗ₖ κ) a) s = (0 a) s

Proof state:
case pos.h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel (α × β) γ
h : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ((0 ⊗ₖ κ) a) s = (0 a) s

Tactic:
rw [Kernel.compProd_apply hs]

Result:
case pos.h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel (α × β) γ
h : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (κ (a, b)) {c | (b, c) ∈ s} ∂0 a = (0 a) s
-- Mathlib/Data/List/ReduceOption.lean
theorem reduceOption_concat (l : List (Option α)) (x : Option α) :
    (l.concat x).reduceOption = l.reduceOption ++ x.toList

Proof state:
case cons
α : Type u_1
hd : Option α
tl : List (Option α)
x : Option α
hl : ∀ (x : Option α), tl.reduceOption ++ [x].reduceOption = tl.reduceOption ++ x.toList
⊢ ((hd :: tl).concat x).reduceOption = (hd :: tl).reduceOption ++ x.toList

Tactic:
cases hd <;> simp [hl, reduceOption_append]

Result:
no goals

Proof state:
case nil
α : Type u_1
x : Option α
⊢ ([].concat x).reduceOption = [].reduceOption ++ x.toList

Tactic:
cases x <;> simp [Option.toList]

Result:
no goals

Proof state:
α : Type u_1
l : List (Option α)
x : Option α
⊢ (l.concat x).reduceOption = l.reduceOption ++ x.toList

Tactic:
induction' l with hd tl hl generalizing x

Result:
case nil
α : Type u_1
x : Option α
⊢ ([].concat x).reduceOption = [].reduceOption ++ x.toList

case cons
α : Type u_1
hd : Option α
tl : List (Option α)
hl : ∀ (x : Option α), (tl.concat x).reduceOption = tl.reduceOption ++ x.toList
x : Option α
⊢ ((hd :: tl).concat x).reduceOption = (hd :: tl).reduceOption ++ x.toList

Proof state:
case cons
α : Type u_1
hd : Option α
tl : List (Option α)
hl : ∀ (x : Option α), (tl.concat x).reduceOption = tl.reduceOption ++ x.toList
x : Option α
⊢ ((hd :: tl).concat x).reduceOption = (hd :: tl).reduceOption ++ x.toList

Tactic:
simp only [concat_eq_append, reduceOption_append] at hl

Result:
case cons
α : Type u_1
hd : Option α
tl : List (Option α)
x : Option α
hl : ∀ (x : Option α), tl.reduceOption ++ [x].reduceOption = tl.reduceOption ++ x.toList
⊢ ((hd :: tl).concat x).reduceOption = (hd :: tl).reduceOption ++ x.toList
-- Mathlib/Data/Finset/Card.lean
theorem card_sdiff (h : s ⊆ t) : #(t \ s) = #t - #s

Proof state:
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
h : s ⊆ t
⊢ #(t \ s) = #t - #s

Tactic:
suffices #(t \ s) = #(t \ s ∪ s) - #s by rwa [sdiff_union_of_subset h] at this

Result:
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
h : s ⊆ t
⊢ #(t \ s) = #(t \ s ∪ s) - #s

Proof state:
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
h : s ⊆ t
⊢ #(t \ s) = #(t \ s ∪ s) - #s

Tactic:
rw [card_union_of_disjoint sdiff_disjoint, Nat.add_sub_cancel_right]

Result:
no goals

Proof state:
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
h : s ⊆ t
this : #(t \ s) = #(t \ s ∪ s) - #s
⊢ #(t \ s) = #t - #s

Tactic:
rwa [sdiff_union_of_subset h] at this

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Lipschitz.lean
theorem list_prod (f : ι → Function.End α) (K : ι → ℝ≥0)
    (h : ∀ i, LipschitzWith (K i) (f i)) : ∀ l : List ι, LipschitzWith (l.map K).prod (l.map f).prod
  | [] => by simpa using LipschitzWith.id
  | i::l => by
    simp only [List.map_cons, List.prod_cons]
    exact (h i).mul_end (LipschitzWith.list_prod f K h l)

Proof state:
α : Type u
ι : Type x
inst✝ : PseudoEMetricSpace α
f : ι → Function.End α
K : ι → ℝ≥0
h : ∀ (i : ι), LipschitzWith (K i) (f i)
i : ι
l : List ι
⊢ LipschitzWith (List.map K (i :: l)).prod (List.map f (i :: l)).prod

Tactic:
simp only [List.map_cons, List.prod_cons]

Result:
α : Type u
ι : Type x
inst✝ : PseudoEMetricSpace α
f : ι → Function.End α
K : ι → ℝ≥0
h : ∀ (i : ι), LipschitzWith (K i) (f i)
i : ι
l : List ι
⊢ LipschitzWith (K i * (List.map K l).prod) (f i * (List.map f l).prod)

Proof state:
α : Type u
ι : Type x
inst✝ : PseudoEMetricSpace α
f : ι → Function.End α
K : ι → ℝ≥0
h : ∀ (i : ι), LipschitzWith (K i) (f i)
i : ι
l : List ι
⊢ LipschitzWith (K i * (List.map K l).prod) (f i * (List.map f l).prod)

Tactic:
exact (h i).mul_end (LipschitzWith.list_prod f K h l)

Result:
no goals

Proof state:
α : Type u
ι : Type x
inst✝ : PseudoEMetricSpace α
f : ι → Function.End α
K : ι → ℝ≥0
h : ∀ (i : ι), LipschitzWith (K i) (f i)
⊢ LipschitzWith (List.map K []).prod (List.map f []).prod

Tactic:
simpa using LipschitzWith.id

Result:
no goals
-- Mathlib/Order/Interval/Finset/Nat.lean
theorem Nat.cauchy_induction' (seed : ℕ) (h : ∀ n, P (n + 1) → P n) (hs : P seed)
    (hi : ∀ x, seed ≤ x → P x → ∃ y, x < y ∧ P y) (n : ℕ) : P n

Proof state:
case intro.intro.intro.intro
P : ℕ → Prop
seed : ℕ
h : ∀ (n : ℕ), P (n + 1) → P n
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
hf : {x | P x}.Finite
m : ℕ
hP : m ∈ {x | P x}
hm : ∀ a' ∈ {x | P x}, id m ≤ id a' → id m = id a'
y : ℕ
hl : m < y
hy : P y
⊢ False

Tactic:
exact hl.ne (hm y hy hl.le)

Result:
no goals

Proof state:
P : ℕ → Prop
seed : ℕ
h : ∀ (n : ℕ), P (n + 1) → P n
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
⊢ P n

Tactic:
apply Nat.decreasing_induction_of_infinite h fun hf => _

Result:
P : ℕ → Prop
seed : ℕ
h : ∀ (n : ℕ), P (n + 1) → P n
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
⊢ {x | P x}.Finite → False

Proof state:
P : ℕ → Prop
seed : ℕ
h : ∀ (n : ℕ), P (n + 1) → P n
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
hf : {x | P x}.Finite
⊢ False

Tactic:
obtain ⟨m, hP, hm⟩ := hf.exists_maximal_wrt id _ ⟨seed, hs⟩

Result:
case intro.intro
P : ℕ → Prop
seed : ℕ
h : ∀ (n : ℕ), P (n + 1) → P n
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
hf : {x | P x}.Finite
m : ℕ
hP : m ∈ {x | P x}
hm : ∀ a' ∈ {x | P x}, id m ≤ id a' → id m = id a'
⊢ False

Proof state:
case intro.intro
P : ℕ → Prop
seed : ℕ
h : ∀ (n : ℕ), P (n + 1) → P n
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
hf : {x | P x}.Finite
m : ℕ
hP : m ∈ {x | P x}
hm : ∀ a' ∈ {x | P x}, id m ≤ id a' → id m = id a'
⊢ False

Tactic:
obtain ⟨y, hl, hy⟩ := hi m (le_of_not_lt fun hl => hl.ne <| hm seed hs hl.le) hP

Result:
case intro.intro.intro.intro
P : ℕ → Prop
seed : ℕ
h : ∀ (n : ℕ), P (n + 1) → P n
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
hf : {x | P x}.Finite
m : ℕ
hP : m ∈ {x | P x}
hm : ∀ a' ∈ {x | P x}, id m ≤ id a' → id m = id a'
y : ℕ
hl : m < y
hy : P y
⊢ False

Proof state:
P : ℕ → Prop
seed : ℕ
h : ∀ (n : ℕ), P (n + 1) → P n
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
⊢ {x | P x}.Finite → False

Tactic:
intro hf

Result:
P : ℕ → Prop
seed : ℕ
h : ∀ (n : ℕ), P (n + 1) → P n
hs : P seed
hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ y, x < y ∧ P y
n : ℕ
hf : {x | P x}.Finite
⊢ False
-- Mathlib/.lake/packages/batteries/Batteries/Classes/Order.lean
theorem compareOfLessAndEq_eq_lt {x y : α} [LT α] [Decidable (x < y)] [DecidableEq α] :
    compareOfLessAndEq x y = .lt ↔ x < y

Proof state:
α : Type u_1
x y : α
inst✝² : LT α
inst✝¹ : Decidable (x < y)
inst✝ : DecidableEq α
⊢ ¬x < y → (if x = y then Ordering.eq else Ordering.gt) = Ordering.lt ↔ x < y

Tactic:
split <;> simp

Result:
no goals

Proof state:
α : Type u_1
x y : α
inst✝² : LT α
inst✝¹ : Decidable (x < y)
inst✝ : DecidableEq α
⊢ compareOfLessAndEq x y = Ordering.lt ↔ x < y

Tactic:
simp [compareOfLessAndEq]

Result:
α : Type u_1
x y : α
inst✝² : LT α
inst✝¹ : Decidable (x < y)
inst✝ : DecidableEq α
⊢ ¬x < y → (if x = y then Ordering.eq else Ordering.gt) = Ordering.lt ↔ x < y
-- Mathlib/GroupTheory/FixedPointFree.lean
theorem orderOf_ne_two_of_involutive (hφ : FixedPointFree φ) (h2 : Function.Involutive φ) (g : G) :
    orderOf g ≠ 2

Proof state:
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
g : G
hg : orderOf g = 2
key : φ g = g
⊢ False

Tactic:
rw [hφ g key, orderOf_one] at hg

Result:
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
g : G
hg : 1 = 2
key : φ g = g
⊢ False

Proof state:
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
g : G
hg : orderOf g = 2
⊢ False

Tactic:
have key : φ g = g := by
  rw [hφ.coe_eq_inv_of_involutive h2, inv_eq_iff_mul_eq_one, ← sq, ← hg, pow_orderOf_eq_one]

Result:
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
g : G
hg : orderOf g = 2
key : φ g = g
⊢ False

Proof state:
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
g : G
hg : 1 = 2
key : φ g = g
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
g : G
⊢ orderOf g ≠ 2

Tactic:
intro hg

Result:
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
g : G
hg : orderOf g = 2
⊢ False

Proof state:
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
g : G
hg : orderOf g = 2
⊢ φ g = g

Tactic:
rw [hφ.coe_eq_inv_of_involutive h2, inv_eq_iff_mul_eq_one, ← sq, ← hg, pow_orderOf_eq_one]

Result:
no goals
-- Mathlib/Algebra/EuclideanDomain/Basic.lean
theorem mod_eq_sub_mul_div {R : Type*} [EuclideanDomain R] (a b : R) : a % b = a - b * (a / b) :=
  calc
    a % b = b * (a / b) + a % b - b * (a / b) := (add_sub_cancel_left _ _).symm
    _ = a - b * (a / b)

Proof state:
R : Type u_1
inst✝ : EuclideanDomain R
a b : R
⊢ b * (a / b) + a % b - b * (a / b) = a - b * (a / b)

Tactic:
rw [div_add_mod]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
@[simp] lemma zpow_lt_one_iff_right_of_lt_one₀ (ha₀ : 0 < a) (ha₁ : a < 1) : a ^ n < 1 ↔ 0 < n

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulStrictMono G₀
n : ℤ
ha₀ : 0 < a
ha₁ : a < 1
⊢ a ^ n < 1 ↔ 0 < n

Tactic:
simp [← zpow_lt_zpow_iff_right_of_lt_one₀ ha₀ ha₁]

Result:
no goals
-- Mathlib/Order/CompleteLatticeIntervals.lean
theorem subset_sSup_of_not_bddAbove [Inhabited s] {t : Set s} (ht : ¬BddAbove t) :
    sSup t = default

Proof state:
α : Type u_2
s : Set α
inst✝² : Preorder α
inst✝¹ : SupSet α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
⊢ sSup t = default

Tactic:
simp [sSup, ht]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem count_erase_of_ne (ab : a ≠ b) (l : List α) : count a (l.erase b) = count a l

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
ab : a ≠ b
l : List α
⊢ count a (l.erase b) = count a l

Tactic:
rw [count_erase, if_neg (by simpa using ab.symm), Nat.sub_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
ab : a ≠ b
l : List α
⊢ ¬(b == a) = true

Tactic:
simpa using ab.symm

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Vanishing.lean
theorem sum_tmul_eq_zero_of_vanishesTrivially (hmn : VanishesTrivially R m n) :
    ∑ i, m i ⊗ₜ n i = (0 : M ⊗[R] N)

Proof state:
case intro.intro.intro.intro
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
k : ℕ
a : ι → Fin k → R
y : Fin k → N
h₁ : ∀ (i : ι), n i = ∑ j : Fin k, a i j • y j
h₂ : ∀ (j : Fin k), ∑ i : ι, a i j • m i = 0
⊢ ∑ y_1 : Fin k, ∑ x : ι, a x y_1 • m x ⊗ₜ[R] y y_1 = 0

Tactic:
simp_rw [← tmul_smul, ← smul_tmul, ← sum_tmul, h₂, zero_tmul, Finset.sum_const_zero]

Result:
no goals

Proof state:
case intro.intro.intro.intro
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
k : ℕ
a : ι → Fin k → R
y : Fin k → N
h₁ : ∀ (i : ι), n i = ∑ j : Fin k, a i j • y j
h₂ : ∀ (j : Fin k), ∑ i : ι, a i j • m i = 0
⊢ ∑ i : ι, m i ⊗ₜ[R] n i = 0

Tactic:
simp_rw [h₁, tmul_sum, tmul_smul]

Result:
case intro.intro.intro.intro
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
k : ℕ
a : ι → Fin k → R
y : Fin k → N
h₁ : ∀ (i : ι), n i = ∑ j : Fin k, a i j • y j
h₂ : ∀ (j : Fin k), ∑ i : ι, a i j • m i = 0
⊢ ∑ x : ι, ∑ x_1 : Fin k, a x x_1 • m x ⊗ₜ[R] y x_1 = 0

Proof state:
case intro.intro.intro.intro
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
k : ℕ
a : ι → Fin k → R
y : Fin k → N
h₁ : ∀ (i : ι), n i = ∑ j : Fin k, a i j • y j
h₂ : ∀ (j : Fin k), ∑ i : ι, a i j • m i = 0
⊢ ∑ x : ι, ∑ x_1 : Fin k, a x x_1 • m x ⊗ₜ[R] y x_1 = 0

Tactic:
rw [Finset.sum_comm]

Result:
case intro.intro.intro.intro
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
k : ℕ
a : ι → Fin k → R
y : Fin k → N
h₁ : ∀ (i : ι), n i = ∑ j : Fin k, a i j • y j
h₂ : ∀ (j : Fin k), ∑ i : ι, a i j • m i = 0
⊢ ∑ y_1 : Fin k, ∑ x : ι, a x y_1 • m x ⊗ₜ[R] y y_1 = 0

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hmn : VanishesTrivially R m n
⊢ ∑ i : ι, m i ⊗ₜ[R] n i = 0

Tactic:
obtain ⟨k, a, y, h₁, h₂⟩ := hmn

Result:
case intro.intro.intro.intro
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
k : ℕ
a : ι → Fin k → R
y : Fin k → N
h₁ : ∀ (i : ι), n i = ∑ j : Fin k, a i j • y j
h₂ : ∀ (j : Fin k), ∑ i : ι, a i j • m i = 0
⊢ ∑ i : ι, m i ⊗ₜ[R] n i = 0