harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Interval/Finset/Nat.lean
lemma Icc_insert_succ_left (h : a ≤ b) : insert a (Icc (a + 1) b) = Icc a b

Proof state:
case h
a b : ℕ
h : a ≤ b
x : ℕ
⊢ x ∈ insert a (Icc (a + 1) b) ↔ x ∈ Icc a b

Tactic:
simp only [mem_insert, mem_Icc]

Result:
case h
a b : ℕ
h : a ≤ b
x : ℕ
⊢ x = a ∨ a + 1 ≤ x ∧ x ≤ b ↔ a ≤ x ∧ x ≤ b

Proof state:
case h
a b : ℕ
h : a ≤ b
x : ℕ
⊢ x = a ∨ a + 1 ≤ x ∧ x ≤ b ↔ a ≤ x ∧ x ≤ b

Tactic:
omega

Result:
no goals

Proof state:
a b : ℕ
h : a ≤ b
⊢ insert a (Icc (a + 1) b) = Icc a b

Tactic:
ext x

Result:
case h
a b : ℕ
h : a ≤ b
x : ℕ
⊢ x ∈ insert a (Icc (a + 1) b) ↔ x ∈ Icc a b
-- Mathlib/MeasureTheory/Covering/Differentiation.lean
theorem measure_limRatioMeas_zero : ρ {x | v.limRatioMeas hρ x = 0} = 0

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | v.limRatioMeas hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : μ o < ⊤
s : Set α := {x | v.limRatioMeas hρ x = 0} ∩ o
μs : μ s ≠ ⊤
q : ℝ≥0
hq : 0 < q
y : α
hy : y ∈ s
⊢ y ∈ {x | v.limRatioMeas hρ x < ↑q}

Tactic:
have : v.limRatioMeas hρ y = 0 := hy.1

Result:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | v.limRatioMeas hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : μ o < ⊤
s : Set α := {x | v.limRatioMeas hρ x = 0} ∩ o
μs : μ s ≠ ⊤
q : ℝ≥0
hq : 0 < q
y : α
hy : y ∈ s
this : v.limRatioMeas hρ y = 0
⊢ y ∈ {x | v.limRatioMeas hρ x < ↑q}

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | v.limRatioMeas hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : μ o < ⊤
s : Set α := {x | v.limRatioMeas hρ x = 0} ∩ o
μs : μ s ≠ ⊤
A : ∀ (q : ℝ≥0), 0 < q → ρ s ≤ ↑q * μ s
⊢ Tendsto (fun q => ↑q * μ s) (𝓝[>] 0) (𝓝 (↑0 * μ s))

Tactic:
apply ENNReal.Tendsto.mul_const _ (Or.inr μs)

Result:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | v.limRatioMeas hρ x = 0}
o : Set α
xo : x ∈ o
o_open : IsOpen o
μo : μ o < ⊤
s : Set α := {x | v.limRatioMeas hρ x = 0} ∩ o
μs : μ s ≠ ⊤
A : ∀ (q : ℝ≥0), 0 < q → ρ s ≤ ↑q * μ s
⊢ Tendsto ENNReal.ofNNReal (𝓝[>] 0) (𝓝 ↑0)
-- Mathlib/GroupTheory/Exponent.lean
theorem Monoid.exponent_pi_eq_zero {ι : Type*} {M : ι → Type*} [∀ i, Monoid (M i)] {j : ι}
    (hj : exponent (M j) = 0) : exponent ((i : ι) → M i) = 0

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
hj : exponent (M j) = 0
⊢ exponent ((i : ι) → M i) = 0

Tactic:
rw [@exponent_eq_zero_iff, ExponentExists] at hj ⊢

Result:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
hj : ¬∃ n, 0 < n ∧ ∀ (g : M j), g ^ n = 1
⊢ ¬∃ n, 0 < n ∧ ∀ (g : (i : ι) → M i), g ^ n = 1

Proof state:
case h.h.intro
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
hj : ∀ (n : ℕ), 0 < n → ∃ g, g ^ n ≠ 1
n : ℕ
hn : 0 < n
m : M j
hm : m ^ n ≠ 1
h : Pi.mulSingle j m ^ n = 1
⊢ m ^ n = 1

Tactic:
simpa using congr_fun h j

Result:
no goals

Proof state:
case h.h
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
hj : ∀ (n : ℕ), 0 < n → ∃ g, g ^ n ≠ 1
n : ℕ
hn : 0 < n
this : ∃ g, g ^ n ≠ 1
⊢ ∃ g, g ^ n ≠ 1

Tactic:
obtain ⟨m, hm⟩ := this

Result:
case h.h.intro
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
hj : ∀ (n : ℕ), 0 < n → ∃ g, g ^ n ≠ 1
n : ℕ
hn : 0 < n
m : M j
hm : m ^ n ≠ 1
⊢ ∃ g, g ^ n ≠ 1

Proof state:
case h.h.intro
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
hj : ∀ (n : ℕ), 0 < n → ∃ g, g ^ n ≠ 1
n : ℕ
hn : 0 < n
m : M j
hm : m ^ n ≠ 1
⊢ ∃ g, g ^ n ≠ 1

Tactic:
refine ⟨Pi.mulSingle j m, fun h ↦ hm ?_⟩

Result:
case h.h.intro
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
hj : ∀ (n : ℕ), 0 < n → ∃ g, g ^ n ≠ 1
n : ℕ
hn : 0 < n
m : M j
hm : m ^ n ≠ 1
h : Pi.mulSingle j m ^ n = 1
⊢ m ^ n = 1

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
hj : ¬∃ n, 0 < n ∧ ∀ (g : M j), g ^ n = 1
⊢ ¬∃ n, 0 < n ∧ ∀ (g : (i : ι) → M i), g ^ n = 1

Tactic:
push_neg at hj ⊢

Result:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
hj : ∀ (n : ℕ), 0 < n → ∃ g, g ^ n ≠ 1
⊢ ∀ (n : ℕ), 0 < n → ∃ g, g ^ n ≠ 1

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
hj : exponent (M j) = 0
⊢ exponent ((i : ι) → M i) = 0

Tactic:
classical
rw [@exponent_eq_zero_iff, ExponentExists] at hj ⊢
push_neg at hj ⊢
peel hj with n hn _
obtain ⟨m, hm⟩ := this
refine ⟨Pi.mulSingle j m, fun h ↦ hm ?_⟩
simpa using congr_fun h j

Result:
no goals

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
hj : ∀ (n : ℕ), 0 < n → ∃ g, g ^ n ≠ 1
⊢ ∀ (n : ℕ), 0 < n → ∃ g, g ^ n ≠ 1

Tactic:
peel hj with n hn _

Result:
case h.h
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
hj : ∀ (n : ℕ), 0 < n → ∃ g, g ^ n ≠ 1
n : ℕ
hn : 0 < n
this : ∃ g, g ^ n ≠ 1
⊢ ∃ g, g ^ n ≠ 1
-- Mathlib/Combinatorics/Enumerative/InclusionExclusion.lean
theorem inclusion_exclusion_card_biUnion (s : Finset ι) (S : ι → Finset α) :
    #(s.biUnion S) = ∑ t : s.powerset.filter (·.Nonempty),
      (-1 : ℤ) ^ (#t.1 + 1) * #(t.1.inf' (mem_filter.1 t.2).2 S)

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
⊢ ↑(#(s.biUnion S)) = ∑ t : { x // x ∈ filter (fun x => x.Nonempty) s.powerset }, (-1) ^ (#↑t + 1) * ↑(#((↑t).inf' ⋯ S))

Tactic:
simpa using inclusion_exclusion_sum_biUnion (G := ℤ) s S (f := 1)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Monadic.lean
theorem foldrM_map [Monad m] [LawfulMonad m] (f : β₁ → β₂) (g : β₂ → α → m α) (l : Vector β₁ n)
    (init : α) : (l.map f).foldrM g init = l.foldrM (fun x y => g (f x) y) init

Proof state:
case mk
m : Type u_1 → Type u_2
β₁ : Type u_3
β₂ : Type u_4
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β₁ → β₂
g : β₂ → α → m α
init : α
l : Array β₁
⊢ foldrM g init (map f { toArray := l, size_toArray := ⋯ }) =
    foldrM (fun x y => g (f x) y) init { toArray := l, size_toArray := ⋯ }

Tactic:
simp [Array.foldrM_map]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
β₁ : Type u_3
β₂ : Type u_4
α : Type u_1
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β₁ → β₂
g : β₂ → α → m α
l : Vector β₁ n
init : α
⊢ foldrM g init (map f l) = foldrM (fun x y => g (f x) y) init l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
m : Type u_1 → Type u_2
β₁ : Type u_3
β₂ : Type u_4
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β₁ → β₂
g : β₂ → α → m α
init : α
l : Array β₁
⊢ foldrM g init (map f { toArray := l, size_toArray := ⋯ }) =
    foldrM (fun x y => g (f x) y) init { toArray := l, size_toArray := ⋯ }
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
theorem σ_comp_σ {n} {i j : Fin (n + 1)} (H : i ≤ j) :
    X.σ j ≫ X.σ (Fin.castSucc i) = X.σ i ≫ X.σ j.succ

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

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

Result:
no goals

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

Tactic:
dsimp [δ, σ]

Result:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ X.map (SimplexCategory.σ j).op ≫ X.map (SimplexCategory.σ i.castSucc).op =
    X.map (SimplexCategory.σ i).op ≫ X.map (SimplexCategory.σ j.succ).op
-- Mathlib/Probability/StrongLaw.lean
theorem truncation_zero (f : α → ℝ) : truncation f 0 = 0

Proof state:
α : Type u_1
f : α → ℝ
⊢ (fun x => 0) ∘ f = 0

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
f : α → ℝ
⊢ truncation f 0 = 0

Tactic:
simp [truncation]

Result:
α : Type u_1
f : α → ℝ
⊢ (fun x => 0) ∘ f = 0
-- Mathlib/CategoryTheory/PathCategory/MorphismProperty.lean
/-- A reformulation of `CategoryTheory.Paths.induction'` in terms of `MorphismProperty`. -/
lemma morphismProperty_eq_top'
    (P : MorphismProperty (Paths V))
    (id : ∀ {v : V}, P (𝟙 (of.obj v)))
    (comp : ∀ {u v w : V} (p : u ⟶ v) (q : of.obj v ⟶ of.obj w), P q → P (of.map p ≫ q)) :
    P = ⊤

Proof state:
case h.mpr
V : Type u₁
inst✝ : Quiver V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 (of.obj v))
comp : ∀ {u v w : V} (p : u ⟶ v) (q : of.obj v ⟶ of.obj w), P q → P (of.map p ≫ q)
X✝ Y✝ : Paths V
f✝ : X✝ ⟶ Y✝
⊢ ⊤ f✝ → P f✝

Tactic:
exact fun _ ↦ induction' (fun f ↦ P f) id comp _

Result:
no goals

Proof state:
V : Type u₁
inst✝ : Quiver V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 (of.obj v))
comp : ∀ {u v w : V} (p : u ⟶ v) (q : of.obj v ⟶ of.obj w), P q → P (of.map p ≫ q)
⊢ P = ⊤

Tactic:
ext

Result:
case h
V : Type u₁
inst✝ : Quiver V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 (of.obj v))
comp : ∀ {u v w : V} (p : u ⟶ v) (q : of.obj v ⟶ of.obj w), P q → P (of.map p ≫ q)
X✝ Y✝ : Paths V
f✝ : X✝ ⟶ Y✝
⊢ P f✝ ↔ ⊤ f✝

Proof state:
case h
V : Type u₁
inst✝ : Quiver V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 (of.obj v))
comp : ∀ {u v w : V} (p : u ⟶ v) (q : of.obj v ⟶ of.obj w), P q → P (of.map p ≫ q)
X✝ Y✝ : Paths V
f✝ : X✝ ⟶ Y✝
⊢ P f✝ ↔ ⊤ f✝

Tactic:
constructor

Result:
case h.mp
V : Type u₁
inst✝ : Quiver V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 (of.obj v))
comp : ∀ {u v w : V} (p : u ⟶ v) (q : of.obj v ⟶ of.obj w), P q → P (of.map p ≫ q)
X✝ Y✝ : Paths V
f✝ : X✝ ⟶ Y✝
⊢ P f✝ → ⊤ f✝

case h.mpr
V : Type u₁
inst✝ : Quiver V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 (of.obj v))
comp : ∀ {u v w : V} (p : u ⟶ v) (q : of.obj v ⟶ of.obj w), P q → P (of.map p ≫ q)
X✝ Y✝ : Paths V
f✝ : X✝ ⟶ Y✝
⊢ ⊤ f✝ → P f✝

Proof state:
case h.mp
V : Type u₁
inst✝ : Quiver V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 (of.obj v))
comp : ∀ {u v w : V} (p : u ⟶ v) (q : of.obj v ⟶ of.obj w), P q → P (of.map p ≫ q)
X✝ Y✝ : Paths V
f✝ : X✝ ⟶ Y✝
⊢ P f✝ → ⊤ f✝

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem nil_eq_rotate_iff {l : List α} {n : ℕ} : [] = l.rotate n ↔ [] = l

Proof state:
α : Type u
l : List α
n : ℕ
⊢ [] = l.rotate n ↔ [] = l

Tactic:
rw [eq_comm, rotate_eq_nil_iff, eq_comm]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean
theorem pow_right_monotone (ha : 1 ≤ a) : Monotone fun n : ℕ ↦ a ^ n :=
  monotone_nat_of_le_succ fun n ↦ by rw [pow_succ]; exact le_mul_of_one_le_right' ha

Proof state:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
ha : 1 ≤ a
n : ℕ
⊢ a ^ n ≤ a ^ n * a

Tactic:
exact le_mul_of_one_le_right' ha

Result:
no goals

Proof state:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
ha : 1 ≤ a
n : ℕ
⊢ a ^ n ≤ a ^ (n + 1)

Tactic:
rw [pow_succ]

Result:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
ha : 1 ≤ a
n : ℕ
⊢ a ^ n ≤ a ^ n * a
-- Mathlib/Data/Matrix/Basic.lean
lemma zero_le_one_elem [Preorder α] [ZeroLEOneClass α] (i j : n) :
    0 ≤ (1 : Matrix n n α) i j

Proof state:
n : Type u_3
α : Type v
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Preorder α
inst✝ : ZeroLEOneClass α
i j : n
⊢ 0 ≤ 1 i j

Tactic:
by_cases hi : i = j

Result:
case pos
n : Type u_3
α : Type v
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Preorder α
inst✝ : ZeroLEOneClass α
i j : n
hi : i = j
⊢ 0 ≤ 1 i j

case neg
n : Type u_3
α : Type v
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Preorder α
inst✝ : ZeroLEOneClass α
i j : n
hi : ¬i = j
⊢ 0 ≤ 1 i j

Proof state:
case neg
n : Type u_3
α : Type v
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Preorder α
inst✝ : ZeroLEOneClass α
i j : n
hi : ¬i = j
⊢ 0 ≤ 1 i j

Tactic:
simp [hi]

Result:
no goals

Proof state:
case pos
n : Type u_3
α : Type v
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Preorder α
inst✝ : ZeroLEOneClass α
i j : n
hi : i = j
⊢ 0 ≤ 1 i j

Tactic:
subst hi

Result:
case pos
n : Type u_3
α : Type v
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Preorder α
inst✝ : ZeroLEOneClass α
i : n
⊢ 0 ≤ 1 i i

Proof state:
case pos
n : Type u_3
α : Type v
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Preorder α
inst✝ : ZeroLEOneClass α
i : n
⊢ 0 ≤ 1 i i

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem exists_square_le' [PosMulStrictMono α] (a0 : 0 < a) : ∃ b : α, b * b ≤ a

Proof state:
case inl
α : Type u_3
a : α
inst✝³ : MulOneClass α
inst✝² : Zero α
inst✝¹ : LinearOrder α
inst✝ : PosMulStrictMono α
a0 : 0 < a
ha : a < 1
⊢ ∃ b, b * b ≤ a

Tactic:
exact ⟨a, (mul_lt_of_lt_one_right a0 ha).le⟩

Result:
no goals

Proof state:
α : Type u_3
a : α
inst✝³ : MulOneClass α
inst✝² : Zero α
inst✝¹ : LinearOrder α
inst✝ : PosMulStrictMono α
a0 : 0 < a
ha : 1 ≤ a
⊢ 1 * 1 ≤ a

Tactic:
rwa [mul_one]

Result:
no goals

Proof state:
case inr
α : Type u_3
a : α
inst✝³ : MulOneClass α
inst✝² : Zero α
inst✝¹ : LinearOrder α
inst✝ : PosMulStrictMono α
a0 : 0 < a
ha : 1 ≤ a
⊢ ∃ b, b * b ≤ a

Tactic:
exact ⟨1, by rwa [mul_one]⟩

Result:
no goals

Proof state:
α : Type u_3
a : α
inst✝³ : MulOneClass α
inst✝² : Zero α
inst✝¹ : LinearOrder α
inst✝ : PosMulStrictMono α
a0 : 0 < a
⊢ ∃ b, b * b ≤ a

Tactic:
obtain ha | ha := lt_or_le a 1

Result:
case inl
α : Type u_3
a : α
inst✝³ : MulOneClass α
inst✝² : Zero α
inst✝¹ : LinearOrder α
inst✝ : PosMulStrictMono α
a0 : 0 < a
ha : a < 1
⊢ ∃ b, b * b ≤ a

case inr
α : Type u_3
a : α
inst✝³ : MulOneClass α
inst✝² : Zero α
inst✝¹ : LinearOrder α
inst✝ : PosMulStrictMono α
a0 : 0 < a
ha : 1 ≤ a
⊢ ∃ b, b * b ≤ a
-- Mathlib/Algebra/NoZeroSMulDivisors/Basic.lean
theorem two_nsmul_eq_zero
    (R) (M) [Semiring R] [CharZero R] [AddCommMonoid M] [Module R M] [NoZeroSMulDivisors R M]
    {v : M} : 2 • v = 0 ↔ v = 0

Proof state:
R : Type u_3
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : CharZero R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
v : M
this : NoZeroSMulDivisors ℕ M
⊢ 2 • v = 0 ↔ v = 0

Tactic:
simp [smul_eq_zero]

Result:
no goals

Proof state:
R : Type u_3
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : CharZero R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
v : M
⊢ 2 • v = 0 ↔ v = 0

Tactic:
haveI := Nat.noZeroSMulDivisors R M

Result:
R : Type u_3
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : CharZero R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
v : M
this : NoZeroSMulDivisors ℕ M
⊢ 2 • v = 0 ↔ v = 0
-- Mathlib/Data/Matroid/Closure.lean
lemma Indep.inter_isBasis_sInter {Xs : Set (Set α)} (hI : M.Indep I) (hXs : Xs.Nonempty)
    (h : ∀ X ∈ Xs, M.IsBasis (X ∩ I) X) : M.IsBasis (⋂₀ Xs ∩ I) (⋂₀ Xs)

Proof state:
α : Type u_2
M : Matroid α
I : Set α
Xs : Set (Set α)
hI : M.Indep I
hXs : Xs.Nonempty
h : ∀ X ∈ Xs, M.IsBasis (X ∩ I) X
⊢ M.IsBasis ((⋂ i ∈ Xs, i) ∩ I) (⋂ i ∈ Xs, i)

Tactic:
exact hI.inter_isBasis_biInter hXs h

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
I : Set α
Xs : Set (Set α)
hI : M.Indep I
hXs : Xs.Nonempty
h : ∀ X ∈ Xs, M.IsBasis (X ∩ I) X
⊢ M.IsBasis (⋂₀ Xs ∩ I) (⋂₀ Xs)

Tactic:
rw [sInter_eq_biInter]

Result:
α : Type u_2
M : Matroid α
I : Set α
Xs : Set (Set α)
hI : M.Indep I
hXs : Xs.Nonempty
h : ∀ X ∈ Xs, M.IsBasis (X ∩ I) X
⊢ M.IsBasis ((⋂ i ∈ Xs, i) ∩ I) (⋂ i ∈ Xs, i)
-- Mathlib/Order/OrderIsoNat.lean
theorem WellFoundedGT.iSup_eq_monotonicSequenceLimit [CompleteLattice α]
    [WellFoundedGT α] (a : ℕ →o α) : iSup a = monotonicSequenceLimit a

Proof state:
case inl
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
a : ℕ →o α
m : ℕ
hm : m ≤ monotonicSequenceLimitIndex a
⊢ a m ≤ monotonicSequenceLimit a

Tactic:
exact a.monotone hm

Result:
no goals

Proof state:
case inr.intro
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
a : ℕ →o α
m : ℕ
hm : monotonicSequenceLimitIndex a < m
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → ¬a n < a m
this : n ∈ {n | ∀ (m : ℕ), n ≤ m → a n = a m}
⊢ a m ≤ monotonicSequenceLimit a

Tactic:
exact (Nat.sInf_mem ⟨n, this⟩ m hm.le).ge

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
a : ℕ →o α
m : ℕ
⊢ a m ≤ monotonicSequenceLimit a

Tactic:
rcases le_or_lt m (monotonicSequenceLimitIndex a) with hm | hm

Result:
case inl
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
a : ℕ →o α
m : ℕ
hm : m ≤ monotonicSequenceLimitIndex a
⊢ a m ≤ monotonicSequenceLimit a

case inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
a : ℕ →o α
m : ℕ
hm : monotonicSequenceLimitIndex a < m
⊢ a m ≤ monotonicSequenceLimit a

Proof state:
case inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
a : ℕ →o α
m : ℕ
hm : monotonicSequenceLimitIndex a < m
⊢ a m ≤ monotonicSequenceLimit a

Tactic:
obtain ⟨n, hn⟩ := WellFoundedGT.monotone_chain_condition' a

Result:
case inr.intro
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
a : ℕ →o α
m : ℕ
hm : monotonicSequenceLimitIndex a < m
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → ¬a n < a m
⊢ a m ≤ monotonicSequenceLimit a

Proof state:
case inr.intro
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
a : ℕ →o α
m : ℕ
hm : monotonicSequenceLimitIndex a < m
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → ¬a n < a m
⊢ a m ≤ monotonicSequenceLimit a

Tactic:
have : n ∈ {n | ∀ m, n ≤ m → a n = a m} := fun k hk => (a.mono hk).eq_of_not_lt (hn k hk)

Result:
case inr.intro
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
a : ℕ →o α
m : ℕ
hm : monotonicSequenceLimitIndex a < m
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → ¬a n < a m
this : n ∈ {n | ∀ (m : ℕ), n ≤ m → a n = a m}
⊢ a m ≤ monotonicSequenceLimit a

Proof state:
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
a : ℕ →o α
⊢ iSup ⇑a = monotonicSequenceLimit a

Tactic:
refine (iSup_le fun m => ?_).antisymm (le_iSup a _)

Result:
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
a : ℕ →o α
m : ℕ
⊢ a m ≤ monotonicSequenceLimit a
-- Mathlib/Geometry/Manifold/VectorField.lean
lemma mlieBracket_add_left
    (hV : MDifferentiableAt I I.tangent (fun x ↦ (V x : TangentBundle I M)) x)
    (hV₁ : MDifferentiableAt I I.tangent (fun x ↦ (V₁ x : TangentBundle I M)) x) :
    mlieBracket I (V + V₁) W x =
      mlieBracket I V W x + mlieBracket I V₁ W x

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
x : M
V W V₁ : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := V x }) x
hV₁ : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := V₁ x }) x
⊢ mlieBracketWithin I (V + V₁) W univ x = mlieBracketWithin I V W univ x + mlieBracketWithin I V₁ W univ x

Tactic:
exact mlieBracketWithin_add_left hV hV₁ (uniqueMDiffWithinAt_univ _)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
x : M
V W V₁ : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := V x }) x
hV₁ : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := V₁ x }) x
⊢ mlieBracket I (V + V₁) W x = mlieBracket I V W x + mlieBracket I V₁ W x

Tactic:
simp only [← mlieBracketWithin_univ, ← contMDiffWithinAt_univ] at hV hV₁ ⊢

Result:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
x : M
V W V₁ : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := V x }) x
hV₁ : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := V₁ x }) x
⊢ mlieBracketWithin I (V + V₁) W univ x = mlieBracketWithin I V W univ x + mlieBracketWithin I V₁ W univ x
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
theorem condExpIndL1_of_measure_eq_top (hμs : μ s = ∞) (x : G) : condExpIndL1 hm μ s x = 0

Proof state:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hμs : μ s = ⊤
x : G
⊢ condExpIndL1 hm μ s x = 0

Tactic:
simp only [condExpIndL1, hμs, eq_self_iff_true, not_true, Ne, dif_neg, not_false_iff,
  and_false]

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem tail_inits (s : Stream' α) :
    tail (inits s) = initsCore [head s, head (tail s)] (tail (tail s))

Proof state:
α : Type u
s : Stream' α
⊢ s.inits.tail = initsCore [s.head, s.tail.head] s.tail.tail

Tactic:
unfold inits

Result:
α : Type u
s : Stream' α
⊢ (initsCore [s.head] s.tail).tail = initsCore [s.head, s.tail.head] s.tail.tail

Proof state:
α : Type u
s : Stream' α
⊢ (initsCore [s.head] s.tail).tail = initsCore [s.head, s.tail.head] s.tail.tail

Tactic:
rw [inits_core_eq]

Result:
α : Type u
s : Stream' α
⊢ ([s.head] :: initsCore ([s.head] ++ [s.tail.head]) s.tail.tail).tail = initsCore [s.head, s.tail.head] s.tail.tail

Proof state:
α : Type u
s : Stream' α
⊢ ([s.head] :: initsCore ([s.head] ++ [s.tail.head]) s.tail.tail).tail = initsCore [s.head, s.tail.head] s.tail.tail

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Finsupp/Order.lean
theorem disjoint_iff {f g : ι →₀ α} : Disjoint f g ↔ Disjoint f.support g.support

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : LinearOrder α
inst✝ : CanonicallyOrderedAdd α
f g : ι →₀ α
⊢ Disjoint f g ↔ Disjoint f.support g.support

Tactic:
classical
  rw [disjoint_iff, disjoint_iff, Finsupp.bot_eq_zero, ← Finsupp.support_eq_empty,
    Finsupp.support_inf]
  rfl

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : LinearOrder α
inst✝ : CanonicallyOrderedAdd α
f g : ι →₀ α
⊢ f.support ∩ g.support = ∅ ↔ f.support ⊓ g.support = ⊥

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : LinearOrder α
inst✝ : CanonicallyOrderedAdd α
f g : ι →₀ α
⊢ Disjoint f g ↔ Disjoint f.support g.support

Tactic:
rw [disjoint_iff, disjoint_iff, Finsupp.bot_eq_zero, ← Finsupp.support_eq_empty,
  Finsupp.support_inf]

Result:
ι : Type u_1
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : LinearOrder α
inst✝ : CanonicallyOrderedAdd α
f g : ι →₀ α
⊢ f.support ∩ g.support = ∅ ↔ f.support ⊓ g.support = ⊥
-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
theorem norm_toLp {f : 𝓢(E, F)} {p : ℝ≥0∞} {μ : Measure E} [hμ : μ.HasTemperateGrowth] :
    ‖f.toLp p μ‖ = ENNReal.toReal (eLpNorm f p μ)

Proof state:
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : SecondCountableTopologyEither E F
f : 𝓢(E, F)
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
⊢ ‖f.toLp p μ‖ = (eLpNorm (⇑f) p μ).toReal

Tactic:
rw [Lp.norm_def, eLpNorm_congr_ae (coeFn_toLp f p μ)]

Result:
no goals