harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem zero_trim (hle : m ≤ n) : (0 : VectorMeasure α M).trim hle = 0

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
n : MeasurableSpace α
hle : m ≤ n
i : Set α
hi : MeasurableSet i
⊢ ↑(trim 0 hle) i = ↑0 i

Tactic:
exact if_pos hi

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
n : MeasurableSpace α
hle : m ≤ n
⊢ trim 0 hle = 0

Tactic:
ext i hi

Result:
case h
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
n : MeasurableSpace α
hle : m ≤ n
i : Set α
hi : MeasurableSet i
⊢ ↑(trim 0 hle) i = ↑0 i
-- Mathlib/Data/List/SplitBy.lean
theorem nil_not_mem_splitByLoop {r : α → α → Bool} {l : List α} {a : α} {g : List α} :
    [] ∉ splitBy.loop r l a g []

Proof state:
case nil
α : Type u_1
r : α → α → Bool
a : α
g : List α
⊢ ¬[] ∈ splitBy.loop r [] a g []

Tactic:
simp [splitBy.loop]

Result:
no goals

Proof state:
case cons
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
⊢ ¬[] ∈
      match r a b with
      | true => splitBy.loop r l b (a :: g) []
      | false => splitBy.loop r l b [] [(a :: g).reverse]

Tactic:
split

Result:
case cons.h_1
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
x✝ : Bool
heq✝ : r a b = true
⊢ ¬[] ∈ splitBy.loop r l b (a :: g) []

case cons.h_2
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
x✝ : Bool
heq✝ : r a b = false
⊢ ¬[] ∈ splitBy.loop r l b [] [(a :: g).reverse]

Proof state:
case cons.h_2
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
x✝ : Bool
heq✝ : r a b = false
⊢ ¬([] ∈ [(a :: g).reverse].reverse ∨ [] ∈ splitBy.loop r l b [] [])

Tactic:
simpa using IH

Result:
no goals

Proof state:
case cons.h_2
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
x✝ : Bool
heq✝ : r a b = false
⊢ ¬[] ∈ splitBy.loop r l b [] [(a :: g).reverse]

Tactic:
rw [splitByLoop_eq_append, mem_append]

Result:
case cons.h_2
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
x✝ : Bool
heq✝ : r a b = false
⊢ ¬([] ∈ [(a :: g).reverse].reverse ∨ [] ∈ splitBy.loop r l b [] [])

Proof state:
case cons.h_1
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
x✝ : Bool
heq✝ : r a b = true
⊢ ¬[] ∈ splitBy.loop r l b (a :: g) []

Tactic:
exact IH

Result:
no goals

Proof state:
case cons
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
⊢ ¬[] ∈ splitBy.loop r (b :: l) a g []

Tactic:
rw [splitBy.loop]

Result:
case cons
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
⊢ ¬[] ∈
      match r a b with
      | true => splitBy.loop r l b (a :: g) []
      | false => splitBy.loop r l b [] [(a :: g).reverse]
-- Mathlib/Algebra/Category/Grp/EpiMono.lean
theorem h_apply_fromCoset (x : B) :
    (h x) (fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩) =
      fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩

Proof state:
A B : Grp
f : A ⟶ B
x : ↑B
⊢ (h x) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = fromCoset ⟨↑(Hom.hom f).range, ⋯⟩

Tactic:
change ((τ).symm.trans (g x)).trans τ _ = _

Result:
A B : Grp
f : A ⟶ B
x : ↑B
⊢ (((Equiv.symm τ).trans (g x)).trans τ) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = fromCoset ⟨↑(Hom.hom f).range, ⋯⟩

Proof state:
A B : Grp
f : A ⟶ B
x : ↑B
⊢ (((Equiv.symm τ).trans (g x)).trans τ) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = fromCoset ⟨↑(Hom.hom f).range, ⋯⟩

Tactic:
simp [-MonoidHom.coe_range, τ_symm_apply_fromCoset, g_apply_infinity, τ_apply_infinity]

Result:
no goals
-- Mathlib/Data/Int/Init.lean
lemma ofNat_add_negSucc_of_ge {m n : ℕ} (h : n.succ ≤ m) :
    ofNat m + -[n+1] = ofNat (m - n.succ)

Proof state:
m n : ℕ
h : n.succ ≤ m
⊢ ofNat m + -[n+1] = ofNat (m - n.succ)

Tactic:
rw [negSucc_eq, ofNat_eq_natCast, ofNat_eq_natCast, ← natCast_one, ← natCast_add,
  ← Int.sub_eq_add_neg, ← Int.natCast_sub h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Int.lean
theorem ofNat_sub_dichotomy {a b : Nat} :
    b ≤ a ∧ ((a - b : Nat) : Int) = a - b ∨ a < b ∧ ((a - b : Nat) : Int) = 0

Proof state:
case pos.h
a b : Nat
h : b ≤ a
t : ↑(a - b) = ↑a - ↑b
⊢ b ≤ a ∧ ↑(a - b) = ↑a - ↑b

Tactic:
exact ⟨h, t⟩

Result:
no goals

Proof state:
case pos
a b : Nat
h : b ≤ a
⊢ b ≤ a ∧ ↑(a - b) = ↑a - ↑b ∨ a < b ∧ ↑(a - b) = 0

Tactic:
left

Result:
case pos.h
a b : Nat
h : b ≤ a
⊢ b ≤ a ∧ ↑(a - b) = ↑a - ↑b

Proof state:
case neg.h
a b : Nat
h : ¬b ≤ a
⊢ a < b ∧ ↑(a - b) = 0

Tactic:
have t := Nat.not_le.mp h

Result:
case neg.h
a b : Nat
h : ¬b ≤ a
t : a < b
⊢ a < b ∧ ↑(a - b) = 0

Proof state:
case neg.h
a b : Nat
h : ¬b ≤ a
t : a < b
⊢ a < b

Tactic:
exact t

Result:
no goals

Proof state:
case neg.h
a b : Nat
h : ¬b ≤ a
t : a < b
⊢ a < b ∧ ↑(a - b) = 0

Tactic:
simp [Int.ofNat_sub_eq_zero h]

Result:
case neg.h
a b : Nat
h : ¬b ≤ a
t : a < b
⊢ a < b

Proof state:
case pos.h
a b : Nat
h : b ≤ a
⊢ b ≤ a ∧ ↑(a - b) = ↑a - ↑b

Tactic:
have t := Int.ofNat_sub h

Result:
case pos.h
a b : Nat
h : b ≤ a
t : ↑(a - b) = ↑a - ↑b
⊢ b ≤ a ∧ ↑(a - b) = ↑a - ↑b

Proof state:
a b : Nat
⊢ b ≤ a ∧ ↑(a - b) = ↑a - ↑b ∨ a < b ∧ ↑(a - b) = 0

Tactic:
by_cases h : b ≤ a

Result:
case pos
a b : Nat
h : b ≤ a
⊢ b ≤ a ∧ ↑(a - b) = ↑a - ↑b ∨ a < b ∧ ↑(a - b) = 0

case neg
a b : Nat
h : ¬b ≤ a
⊢ b ≤ a ∧ ↑(a - b) = ↑a - ↑b ∨ a < b ∧ ↑(a - b) = 0

Proof state:
case neg
a b : Nat
h : ¬b ≤ a
⊢ b ≤ a ∧ ↑(a - b) = ↑a - ↑b ∨ a < b ∧ ↑(a - b) = 0

Tactic:
right

Result:
case neg.h
a b : Nat
h : ¬b ≤ a
⊢ a < b ∧ ↑(a - b) = 0
-- Mathlib/Analysis/Asymptotics/TVS.lean
lemma isLittleOTVS_insert [TopologicalSpace α] {x : α} {s : Set α} (h : f x = 0) :
    f =o[𝕜;(𝓝[insert x s] x)] g ↔ f =o[𝕜;(𝓝[s] x)] g

Proof state:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : TopologicalSpace F
inst✝¹ : Module 𝕜 F
f : α → E
g : α → F
inst✝ : TopologicalSpace α
x : α
s : Set α
h : f x = 0
⊢ f =o[𝕜;𝓝[insert x s] x] g ↔ f =o[𝕜;𝓝[s] x] g

Tactic:
rw [nhdsWithin_insert, isLittleOTVS_sup, and_iff_right]

Result:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : TopologicalSpace F
inst✝¹ : Module 𝕜 F
f : α → E
g : α → F
inst✝ : TopologicalSpace α
x : α
s : Set α
h : f x = 0
⊢ f =o[𝕜;pure x] g

Proof state:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : TopologicalSpace F
inst✝¹ : Module 𝕜 F
f : α → E
g : α → F
inst✝ : TopologicalSpace α
x : α
s : Set α
h : f x = 0
⊢ f =o[𝕜;pure x] g

Tactic:
exact .congr' (.zero g _) h.symm .rfl

Result:
no goals
-- Mathlib/Data/Rat/Lemmas.lean
theorem intCast_div_self (n : ℤ) : ((n / n : ℤ) : ℚ) = n / n

Proof state:
case neg
n : ℤ
hn : ¬n = 0
⊢ ↑(n / n) = ↑n / ↑n

Tactic:
have : (n : ℚ) ≠ 0 := by rwa [← coe_int_inj] at hn

Result:
case neg
n : ℤ
hn : ¬n = 0
this : ↑n ≠ 0
⊢ ↑(n / n) = ↑n / ↑n

Proof state:
case neg
n : ℤ
hn : ¬n = 0
this : ↑n ≠ 0
⊢ ↑(n / n) = ↑n / ↑n

Tactic:
simp only [Int.ediv_self hn, Int.cast_one, Ne, not_false_iff, div_self this]

Result:
no goals

Proof state:
n : ℤ
hn : ¬n = 0
⊢ ↑n ≠ 0

Tactic:
rwa [← coe_int_inj] at hn

Result:
no goals

Proof state:
n : ℤ
⊢ ↑(n / n) = ↑n / ↑n

Tactic:
by_cases hn : n = 0

Result:
case pos
n : ℤ
hn : n = 0
⊢ ↑(n / n) = ↑n / ↑n

case neg
n : ℤ
hn : ¬n = 0
⊢ ↑(n / n) = ↑n / ↑n

Proof state:
case pos

⊢ ↑(0 / 0) = ↑0 / ↑0

Tactic:
simp only [Int.cast_zero, Int.zero_tdiv, zero_div, Int.ediv_zero]

Result:
no goals

Proof state:
case pos
n : ℤ
hn : n = 0
⊢ ↑(n / n) = ↑n / ↑n

Tactic:
subst hn

Result:
case pos

⊢ ↑(0 / 0) = ↑0 / ↑0
-- Mathlib/Data/Matrix/Block.lean
theorem blockDiagonal'_map (M : ∀ i, Matrix (m' i) (n' i) α) (f : α → β) (hf : f 0 = 0) :
    (blockDiagonal' M).map f = blockDiagonal' fun k => (M k).map f

Proof state:
case a
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : (i : o) → Matrix (m' i) (n' i) α
f : α → β
hf : f 0 = 0
i✝ : (i : o) × m' i
j✝ : (i : o) × n' i
⊢ (blockDiagonal' M).map f i✝ j✝ = blockDiagonal' (fun k => (M k).map f) i✝ j✝

Tactic:
simp only [map_apply, blockDiagonal'_apply, eq_comm]

Result:
case a
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : (i : o) → Matrix (m' i) (n' i) α
f : α → β
hf : f 0 = 0
i✝ : (i : o) × m' i
j✝ : (i : o) × n' i
⊢ f (if h : i✝.fst = j✝.fst then M i✝.fst i✝.snd (cast ⋯ j✝.snd) else 0) =
    if h : i✝.fst = j✝.fst then f (M i✝.fst i✝.snd (cast ⋯ j✝.snd)) else 0

Proof state:
case a
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : (i : o) → Matrix (m' i) (n' i) α
f : α → β
hf : f 0 = 0
i✝ : (i : o) × m' i
j✝ : (i : o) × n' i
⊢ f (if h : i✝.fst = j✝.fst then M i✝.fst i✝.snd (cast ⋯ j✝.snd) else 0) =
    if h : i✝.fst = j✝.fst then f (M i✝.fst i✝.snd (cast ⋯ j✝.snd)) else 0

Tactic:
rw [apply_dite f, hf]

Result:
no goals

Proof state:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : (i : o) → Matrix (m' i) (n' i) α
f : α → β
hf : f 0 = 0
⊢ (blockDiagonal' M).map f = blockDiagonal' fun k => (M k).map f

Tactic:
ext

Result:
case a
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : (i : o) → Matrix (m' i) (n' i) α
f : α → β
hf : f 0 = 0
i✝ : (i : o) × m' i
j✝ : (i : o) × n' i
⊢ (blockDiagonal' M).map f i✝ j✝ = blockDiagonal' (fun k => (M k).map f) i✝ j✝
-- Mathlib/Order/SuccPred/Archimedean.lean
theorem Succ.rec_iff {p : α → Prop} (hsucc : ∀ a, p a ↔ p (succ a)) {a b : α} (h : a ≤ b) :
    p a ↔ p b

Proof state:
case intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
p : α → Prop
hsucc : ∀ (a : α), p a ↔ p (succ a)
a : α
n : ℕ
h : a ≤ succ^[n] a
⊢ p a ↔ p (succ^[n] a)

Tactic:
exact Iterate.rec (fun b => p a ↔ p b) (fun c hc => hc.trans (hsucc _)) Iff.rfl n

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
p : α → Prop
hsucc : ∀ (a : α), p a ↔ p (succ a)
a b : α
h : a ≤ b
⊢ p a ↔ p b

Tactic:
obtain ⟨n, rfl⟩ := h.exists_succ_iterate

Result:
case intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
p : α → Prop
hsucc : ∀ (a : α), p a ↔ p (succ a)
a : α
n : ℕ
h : a ≤ succ^[n] a
⊢ p a ↔ p (succ^[n] a)
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem polar_add (f g : M → N) (x y : M) : polar (f + g) x y = polar f x y + polar g x y

Proof state:
M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f g : M → N
x y : M
⊢ polar (f + g) x y = polar f x y + polar g x y

Tactic:
simp only [polar, Pi.add_apply]

Result:
M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f g : M → N
x y : M
⊢ f (x + y) + g (x + y) - (f x + g x) - (f y + g y) = f (x + y) - f x - f y + (g (x + y) - g x - g y)

Proof state:
M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f g : M → N
x y : M
⊢ f (x + y) + g (x + y) - (f x + g x) - (f y + g y) = f (x + y) - f x - f y + (g (x + y) - g x - g y)

Tactic:
abel

Result:
no goals
-- Mathlib/Order/SuccPred/Archimedean.lean
lemma BddAbove.exists_isGreatest_of_nonempty {X : Type*} [LinearOrder X] [SuccOrder X]
    [IsSuccArchimedean X] {S : Set X} (hS : BddAbove S) (hS' : S.Nonempty) :
    ∃ x, IsGreatest S x

Proof state:
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
a✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x = succ m ∨ x ≤ m
⊢ ∀ x ∈ S, x ≤ m

Tactic:
intro x hx

Result:
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
a✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x = succ m ∨ x ≤ m
x : X
hx : x ∈ S
⊢ x ≤ m

Proof state:
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
hS : BddAbove S
hS' : S.Nonempty
⊢ ∃ x, IsGreatest S x

Tactic:
obtain ⟨m, hm⟩ := hS

Result:
case intro
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
hS' : S.Nonempty
m : X
hm : m ∈ upperBounds S
⊢ ∃ x, IsGreatest S x

Proof state:
case intro
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
hS' : S.Nonempty
m : X
hm : m ∈ upperBounds S
⊢ ∃ x, IsGreatest S x

Tactic:
obtain ⟨n, hn⟩ := hS'

Result:
case intro.intro
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m : X
hm : m ∈ upperBounds S
n : X
hn : n ∈ S
⊢ ∃ x, IsGreatest S x

Proof state:
case neg.refine_2
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
a✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hm : ∀ x ∈ S, x ≤ succ m
hn : n ∈ S
hm' : succ m ∉ S
⊢ ∃ x, IsGreatest S x

Tactic:
simp_rw [Order.le_succ_iff_eq_or_le] at hm

Result:
case neg.refine_2
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
a✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x = succ m ∨ x ≤ m
⊢ ∃ x, IsGreatest S x

Proof state:
case pos
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
a✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x ≤ m
hmS : m ∈ S
⊢ ∃ x, IsGreatest S x

Tactic:
exact ⟨m, hmS, hm⟩

Result:
no goals

Proof state:
case neg
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
a✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x ≤ m
hmS : m ∉ S
⊢ ∃ x, IsGreatest S x

Tactic:
exact IH hm hn hmS

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
lemma piFinset_image₂ (f : ∀ i, α i → β i → γ i) (s : ∀ i, Finset (α i)) (t : ∀ i, Finset (β i)) :
    piFinset (fun i ↦ image₂ (f i) (s i) (t i)) =
      image₂ (fun a b i ↦ f _ (a i) (b i)) (piFinset s) (piFinset t)

Proof state:
ι : Type u_14
α : ι → Type u_15
β : ι → Type u_16
γ : ι → Type u_17
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (γ i)
f : (i : ι) → α i → β i → γ i
s : (i : ι) → Finset (α i)
t : (i : ι) → Finset (β i)
⊢ (piFinset fun i => image₂ (f i) (s i) (t i)) = image₂ (fun a b i => f i (a i) (b i)) (piFinset s) (piFinset t)

Tactic:
ext

Result:
case h
ι : Type u_14
α : ι → Type u_15
β : ι → Type u_16
γ : ι → Type u_17
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (γ i)
f : (i : ι) → α i → β i → γ i
s : (i : ι) → Finset (α i)
t : (i : ι) → Finset (β i)
a✝ : (a : ι) → γ a
⊢ (a✝ ∈ piFinset fun i => image₂ (f i) (s i) (t i)) ↔
    a✝ ∈ image₂ (fun a b i => f i (a i) (b i)) (piFinset s) (piFinset t)

Proof state:
case h
ι : Type u_14
α : ι → Type u_15
β : ι → Type u_16
γ : ι → Type u_17
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (γ i)
f : (i : ι) → α i → β i → γ i
s : (i : ι) → Finset (α i)
t : (i : ι) → Finset (β i)
a✝ : (a : ι) → γ a
⊢ (a✝ ∈ piFinset fun i => image₂ (f i) (s i) (t i)) ↔
    a✝ ∈ image₂ (fun a b i => f i (a i) (b i)) (piFinset s) (piFinset t)

Tactic:
simp only [mem_piFinset, mem_image₂, Classical.skolem, forall_and, funext_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm'_eq_zero_of_ae_zero {f : α → F} (hq0_lt : 0 < q) (hf_zero : f =ᵐ[μ] 0) :
    eLpNorm' f q μ = 0

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hq0_lt : 0 < q
hf_zero : f =ᶠ[ae μ] 0
⊢ eLpNorm' f q μ = 0

Tactic:
rw [eLpNorm'_congr_ae hf_zero, eLpNorm'_zero hq0_lt]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem insertMany_empty_list_nil :
    (insertMany empty ([] : List (α × β))).1 = empty

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
⊢ (insertMany empty []).val = empty

Tactic:
simp only [insertMany_nil]

Result:
no goals
-- Mathlib/Combinatorics/Additive/VerySmallDoubling.lean
private lemma nonempty_of_doubling (h : #(A * A) < (3 / 2 : ℚ) * #A) : A.Nonempty

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
h : ↑(#(∅ * ∅)) < 3 / 2 * ↑(#∅)
⊢ False

Tactic:
simp at h

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
⊢ A.Nonempty

Tactic:
rw [nonempty_iff_ne_empty]

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
⊢ A ≠ ∅

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
⊢ A ≠ ∅

Tactic:
rintro rfl

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
h : ↑(#(∅ * ∅)) < 3 / 2 * ↑(#∅)
⊢ False
-- Mathlib/Algebra/Group/UniqueProds/Basic.lean
theorem iff_existsUnique (aA : a0 ∈ A) (bB : b0 ∈ B) :
    UniqueMul A B a0 b0 ↔ ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = a0 * b0 :=
  ⟨fun _ ↦ ⟨(a0, b0), ⟨Finset.mk_mem_product aA bB, rfl⟩, by simpa⟩,
    fun h ↦ h.elim
      (by
        rintro ⟨x1, x2⟩ _ J x y hx hy l
        rcases Prod.mk.inj_iff.mp (J (a0, b0) ⟨Finset.mk_mem_product aA bB, rfl⟩) with ⟨rfl, rfl⟩
        exact Prod.mk.inj_iff.mp (J (x, y) ⟨Finset.mk_mem_product hx hy, l⟩))⟩

Proof state:
G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
x✝ : UniqueMul A B a0 b0
⊢ ∀ (y : G × G), (fun ab => ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = a0 * b0) y → y = (a0, b0)

Tactic:
simpa

Result:
no goals

Proof state:
case mk
G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
h : ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = a0 * b0
x1 x2 : G
a✝ : (x1, x2) ∈ A ×ˢ B ∧ (x1, x2).1 * (x1, x2).2 = a0 * b0
J : ∀ (y : G × G), y ∈ A ×ˢ B ∧ y.1 * y.2 = a0 * b0 → y = (x1, x2)
x y : G
hx : x ∈ A
hy : y ∈ B
l : x * y = a0 * b0
⊢ x = a0 ∧ y = b0

Tactic:
rcases Prod.mk.inj_iff.mp (J (a0, b0) ⟨Finset.mk_mem_product aA bB, rfl⟩) with ⟨rfl, rfl⟩

Result:
case mk.intro
G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
h : ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = a0 * b0
x y : G
hx : x ∈ A
hy : y ∈ B
l : x * y = a0 * b0
a✝ : (a0, b0) ∈ A ×ˢ B ∧ (a0, b0).1 * (a0, b0).2 = a0 * b0
J : ∀ (y : G × G), y ∈ A ×ˢ B ∧ y.1 * y.2 = a0 * b0 → y = (a0, b0)
⊢ x = a0 ∧ y = b0

Proof state:
G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
h : ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = a0 * b0
⊢ ∀ (x : G × G),
    x ∈ A ×ˢ B ∧ x.1 * x.2 = a0 * b0 → (∀ (y : G × G), y ∈ A ×ˢ B ∧ y.1 * y.2 = a0 * b0 → y = x) → UniqueMul A B a0 b0

Tactic:
rintro ⟨x1, x2⟩ _ J x y hx hy l

Result:
case mk
G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
h : ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = a0 * b0
x1 x2 : G
a✝ : (x1, x2) ∈ A ×ˢ B ∧ (x1, x2).1 * (x1, x2).2 = a0 * b0
J : ∀ (y : G × G), y ∈ A ×ˢ B ∧ y.1 * y.2 = a0 * b0 → y = (x1, x2)
x y : G
hx : x ∈ A
hy : y ∈ B
l : x * y = a0 * b0
⊢ x = a0 ∧ y = b0

Proof state:
case mk.intro
G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
h : ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = a0 * b0
x y : G
hx : x ∈ A
hy : y ∈ B
l : x * y = a0 * b0
a✝ : (a0, b0) ∈ A ×ˢ B ∧ (a0, b0).1 * (a0, b0).2 = a0 * b0
J : ∀ (y : G × G), y ∈ A ×ˢ B ∧ y.1 * y.2 = a0 * b0 → y = (a0, b0)
⊢ x = a0 ∧ y = b0

Tactic:
exact Prod.mk.inj_iff.mp (J (x, y) ⟨Finset.mk_mem_product hx hy, l⟩)

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem lift_lt_aleph0 {c : Cardinal.{u}} : lift.{v} c < ℵ₀ ↔ c < ℵ₀

Proof state:
c : Cardinal.{u}
⊢ lift.{v, u} c < ℵ₀ ↔ c < ℵ₀

Tactic:
simpa using lift_lt (b := ℵ₀)

Result:
no goals
-- Mathlib/Data/Int/Bitwise.lean
theorem testBit_bit_succ (m b) : ∀ n, testBit (bit b n) (Nat.succ m) = testBit n m
  | (n : ℕ) => by rw [bit_coe_nat]; apply Nat.testBit_bit_succ
  | -[n+1] => by
    dsimp only [testBit]
    simp only [bit_negSucc]
    cases b <;> simp only [Bool.not_false, Bool.not_true, Nat.testBit_bit_succ]

Proof state:
m : ℕ
b : Bool
n : ℕ
⊢ (match bit b -[n+1], m.succ with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    !n.testBit m

Tactic:
simp only [bit_negSucc]

Result:
m : ℕ
b : Bool
n : ℕ
⊢ (!(Nat.bit (!b) n).testBit m.succ) = !n.testBit m

Proof state:
m : ℕ
b : Bool
n : ℕ
⊢ (bit b ↑n).testBit m.succ = (↑n).testBit m

Tactic:
rw [bit_coe_nat]

Result:
m : ℕ
b : Bool
n : ℕ
⊢ (↑(Nat.bit b n)).testBit m.succ = (↑n).testBit m

Proof state:
m : ℕ
b : Bool
n : ℕ
⊢ (!(Nat.bit (!b) n).testBit m.succ) = !n.testBit m

Tactic:
cases b <;> simp only [Bool.not_false, Bool.not_true, Nat.testBit_bit_succ]

Result:
no goals

Proof state:
m : ℕ
b : Bool
n : ℕ
⊢ (bit b -[n+1]).testBit m.succ = -[n+1].testBit m

Tactic:
dsimp only [testBit]

Result:
m : ℕ
b : Bool
n : ℕ
⊢ (match bit b -[n+1], m.succ with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    !n.testBit m

Proof state:
m : ℕ
b : Bool
n : ℕ
⊢ (↑(Nat.bit b n)).testBit m.succ = (↑n).testBit m

Tactic:
apply Nat.testBit_bit_succ

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_fract (a : α) : ⌊fract a⌋ = 0

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ ⌊fract a⌋ = 0

Tactic:
rw [floor_eq_iff, Int.cast_zero, zero_add]

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ 0 ≤ fract a ∧ fract a < 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ 0 ≤ fract a ∧ fract a < 1

Tactic:
exact ⟨fract_nonneg _, fract_lt_one _⟩

Result:
no goals
-- Mathlib/Algebra/Order/Group/Multiset.lean
@[simp]
lemma countP_nsmul (s) (n : ℕ) : countP p (n • s) = n * countP p s

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
⊢ countP p (n • s) = n * countP p s

Tactic:
induction n <;> simp [*, succ_nsmul, succ_mul, zero_nsmul]

Result:
no goals