harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Moments/IntegrableExpMul.lean
lemma sub_half_inf_sub_mem_Ioo {l u v : ℝ} (hv : v ∈ Set.Ioo l u) :
    v - ((v - l) ⊓ (u - v)) / 2 ∈ Set.Ioo l u

Proof state:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ v - (v - l) ⊓ (u - v) < v - ((v - l) ⊓ (u - v)) / 2

Tactic:
gcongr

Result:
case h
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ ((v - l) ⊓ (u - v)) / 2 < (v - l) ⊓ (u - v)

Proof state:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ v - ((v - l) ⊓ (u - v)) / 2 ≤ v

Tactic:
rw [sub_le_iff_le_add]

Result:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ v ≤ v + ((v - l) ⊓ (u - v)) / 2

Proof state:
case h
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ ((v - l) ⊓ (u - v)) / 2 < (v - l) ⊓ (u - v)

Tactic:
exact half_lt_self (by positivity)

Result:
no goals

Proof state:
l u v : ℝ
hv : v ∈ Set.Ioo l u
⊢ 0 < (v - l) ⊓ (u - v)

Tactic:
simp [hv.1, hv.2]

Result:
no goals

Proof state:
case left
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ l < v - ((v - l) ⊓ (u - v)) / 2

Tactic:
calc l = v - (v - l) := by abel
_ ≤ v - ((v - l) ⊓ (u - v)) := by gcongr; exact inf_le_left
_ < v - ((v - l) ⊓ (u - v)) / 2 := by gcongr; exact half_lt_self (by positivity)

Result:
no goals

Proof state:
case right
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ v - ((v - l) ⊓ (u - v)) / 2 < u

Tactic:
calc v - ((v - l) ⊓ (u - v)) / 2
_ ≤ v := by
  rw [sub_le_iff_le_add]
  exact le_add_of_nonneg_right (by positivity)
_ < u := hv.2

Result:
no goals

Proof state:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ 0 ≤ ((v - l) ⊓ (u - v)) / 2

Tactic:
positivity

Result:
no goals

Proof state:
case h
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ (v - l) ⊓ (u - v) ≤ v - l

Tactic:
exact inf_le_left

Result:
no goals

Proof state:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ 0 < (v - l) ⊓ (u - v)

Tactic:
positivity

Result:
no goals

Proof state:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ v ≤ v + ((v - l) ⊓ (u - v)) / 2

Tactic:
exact le_add_of_nonneg_right (by positivity)

Result:
no goals

Proof state:
l u v : ℝ
hv : v ∈ Set.Ioo l u
⊢ v - ((v - l) ⊓ (u - v)) / 2 ∈ Set.Ioo l u

Tactic:
have h_pos : 0 < (v - l) ⊓ (u - v) := by simp [hv.1, hv.2]

Result:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ v - ((v - l) ⊓ (u - v)) / 2 ∈ Set.Ioo l u

Proof state:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ v - (v - l) ≤ v - (v - l) ⊓ (u - v)

Tactic:
gcongr

Result:
case h
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ (v - l) ⊓ (u - v) ≤ v - l

Proof state:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ v - ((v - l) ⊓ (u - v)) / 2 ∈ Set.Ioo l u

Tactic:
constructor

Result:
case left
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ l < v - ((v - l) ⊓ (u - v)) / 2

case right
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ v - ((v - l) ⊓ (u - v)) / 2 < u

Proof state:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ l = v - (v - l)

Tactic:
abel

Result:
no goals
-- Mathlib/Data/Matroid/Map.lean
@[simp] lemma comap_isBasis_iff {I X : Set α} :
    (N.comap f).IsBasis I X ↔ N.IsBasis (f '' I) (f '' X) ∧ I.InjOn f ∧ I ⊆ X

Proof state:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X
e : α
x✝ : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
hIE : insert e I ⊆ (N.comap f).E
this : N.Indep (insert (f e) (f '' I)) → ∃ x ∈ I, f x = f e
⊢ (N.comap f).Dep (insert e I)

Tactic:
simpa [← not_indep_iff hIE, injOn_insert heI, h.2.1, image_insert_eq]

Result:
no goals

Proof state:
case refine_1
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : (N.comap f).IsBasis I X
⊢ N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X

Tactic:
obtain ⟨hI, hinj⟩ := comap_indep_iff.1 h.indep

Result:
case refine_1.intro
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : (N.comap f).IsBasis I X
hI : N.Indep (f '' I)
hinj : InjOn f I
⊢ N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_finset_product (s : Finset (α × β)) (f : α × β → M) :
    (∏ᶠ (ab) (_ : ab ∈ s), f ab) = ∏ᶠ (a) (b) (_ : (a, b) ∈ s), f (a, b)

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset (α × β)
f : α × β → M
⊢ ∏ᶠ (ab : α × β) (_ : ab ∈ s), f ab = ∏ᶠ (a : α) (b : β) (_ : (a, b) ∈ s), f (a, b)

Tactic:
classical
  rw [finprod_mem_finset_product']
  simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset (α × β)
f : α × β → M
⊢ ∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.1 = a) s)), f (a, b) =
    ∏ᶠ (a : α) (b : β) (_ : (a, b) ∈ s), f (a, b)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset (α × β)
f : α × β → M
⊢ ∏ᶠ (ab : α × β) (_ : ab ∈ s), f ab = ∏ᶠ (a : α) (b : β) (_ : (a, b) ∈ s), f (a, b)

Tactic:
rw [finprod_mem_finset_product']

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset (α × β)
f : α × β → M
⊢ ∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.1 = a) s)), f (a, b) =
    ∏ᶠ (a : α) (b : β) (_ : (a, b) ∈ s), f (a, b)
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem mkRat_mul_mkRat (n₁ n₂ : Int) (d₁ d₂) :
    mkRat n₁ d₁ * mkRat n₂ d₂ = mkRat (n₁ * n₂) (d₁ * d₂)

Proof state:
n₁ n₂ : Int
d₁ d₂ : Nat
z₁ : ¬d₁ = 0
z₂ : ¬d₂ = 0
⊢ mkRat n₁ d₁ * mkRat n₂ d₂ = mkRat (n₁ * n₂) (d₁ * d₂)

Tactic:
rw [← normalize_eq_mkRat z₁, ← normalize_eq_mkRat z₂, normalize_mul_normalize, normalize_eq_mkRat]

Result:
no goals

Proof state:
n₁ n₂ : Int
d₁ d₂ : Nat
z₁ : d₁ = 0
⊢ mkRat n₁ d₁ * mkRat n₂ d₂ = mkRat (n₁ * n₂) (d₁ * d₂)

Tactic:
simp [z₁]

Result:
no goals

Proof state:
n₁ n₂ : Int
d₁ d₂ : Nat
z₁ : ¬d₁ = 0
⊢ mkRat n₁ d₁ * mkRat n₂ d₂ = mkRat (n₁ * n₂) (d₁ * d₂)

Tactic:
if z₂ : d₂ = 0 then simp [z₂] else
rw [← normalize_eq_mkRat z₁, ← normalize_eq_mkRat z₂, normalize_mul_normalize, normalize_eq_mkRat]

Result:
no goals

Proof state:
n₁ n₂ : Int
d₁ d₂ : Nat
z₁ : ¬d₁ = 0
z₂ : d₂ = 0
⊢ mkRat n₁ d₁ * mkRat n₂ d₂ = mkRat (n₁ * n₂) (d₁ * d₂)

Tactic:
simp [z₂]

Result:
no goals

Proof state:
n₁ n₂ : Int
d₁ d₂ : Nat
⊢ mkRat n₁ d₁ * mkRat n₂ d₂ = mkRat (n₁ * n₂) (d₁ * d₂)

Tactic:
if z₁ : d₁ = 0 then simp [z₁] else if z₂ : d₂ = 0 then simp [z₂] else
rw [← normalize_eq_mkRat z₁, ← normalize_eq_mkRat z₂, normalize_mul_normalize, normalize_eq_mkRat]

Result:
no goals
-- Mathlib/Algebra/Group/Indicator.lean
theorem mulIndicator_congr (h : EqOn f g s) : mulIndicator s f = mulIndicator s g :=
  funext fun x => by
    simp only [mulIndicator]
    split_ifs with h_1
    · exact h h_1
    rfl

Proof state:
case pos
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f g : α → M
h : EqOn f g s
x : α
h_1 : x ∈ s
⊢ f x = g x

Tactic:
exact h h_1

Result:
no goals

Proof state:
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f g : α → M
h : EqOn f g s
x : α
⊢ s.mulIndicator f x = s.mulIndicator g x

Tactic:
simp only [mulIndicator]

Result:
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f g : α → M
h : EqOn f g s
x : α
⊢ (if x ∈ s then f x else 1) = if x ∈ s then g x else 1

Proof state:
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f g : α → M
h : EqOn f g s
x : α
⊢ (if x ∈ s then f x else 1) = if x ∈ s then g x else 1

Tactic:
split_ifs with h_1

Result:
case pos
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f g : α → M
h : EqOn f g s
x : α
h_1 : x ∈ s
⊢ f x = g x

case neg
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f g : α → M
h : EqOn f g s
x : α
h_1 : x ∉ s
⊢ 1 = 1

Proof state:
case neg
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f g : α → M
h : EqOn f g s
x : α
h_1 : x ∉ s
⊢ 1 = 1

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Zero.lean
lemma finrank_maxGenEigenspace (φ : Module.End K M) :
    finrank K (φ.maxGenEigenspace 0) = natTrailingDegree (φ.charpoly)

Proof state:
K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
⊢ finrank K ↥V = (charpoly φ).natTrailingDegree

Tactic:
have hφV : ∀ x ∈ V, φ x ∈ V := by
  simp only [V, Module.End.mem_maxGenEigenspace, zero_smul, sub_zero,
    forall_exists_index]
  intro x n hx
  use n
  rw [← LinearMap.mul_apply, ← pow_succ, pow_succ', LinearMap.mul_apply, hx, map_zero]

Result:
K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
⊢ finrank K ↥V = (charpoly φ).natTrailingDegree

Proof state:
case h.a
K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
hφW : ∀ x ∈ W, φ x ∈ W
F : ↥V →ₗ[K] ↥V := restrict φ hφV
G : ↥W →ₗ[K] ↥W := restrict φ hφW
ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G
e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW
bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ : ψ = e.symm.conj φ
x : ↥W
hx : G x = 0
⊢ ↑x ∈ V

Tactic:
simp only [Module.End.mem_maxGenEigenspace, zero_smul, sub_zero, V]

Result:
case h.a
K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
hφW : ∀ x ∈ W, φ x ∈ W
F : ↥V →ₗ[K] ↥V := restrict φ hφV
G : ↥W →ₗ[K] ↥W := restrict φ hφW
ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G
e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW
bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ : ψ = e.symm.conj φ
x : ↥W
hx : G x = 0
⊢ ∃ k, (φ ^ k) ↑x = 0

Proof state:
K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
⊢ IsCompl (⨆ n, ker (φ ^ n)) W

Tactic:
exact LinearMap.isCompl_iSup_ker_pow_iInf_range_pow φ

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/BorelCantelli.lean
theorem limsup_ae_eq_of_forall_ae_eq (s : ℕ → Set α) {t : Set α}
    (h : ∀ n, s n =ᵐ[μ] t) : limsup (α := Set α) s atTop =ᵐ[μ] t

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s : ℕ → Set α
t : Set α
h : ∀ᵐ (x : α) ∂μ, ∀ (i : ℕ), x ∈ s i ↔ x ∈ t
x : α
hx : ∀ (i : ℕ), x ∈ s i ↔ x ∈ t
⊢ x ∈ limsup s atTop ↔ x ∈ t

Tactic:
simp [mem_limsup_iff_frequently_mem, hx]

Result:
no goals

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s : ℕ → Set α
t : Set α
h : ∀ᵐ (x : α) ∂μ, ∀ (i : ℕ), x ∈ s i ↔ x ∈ t
⊢ limsup s atTop =ᶠ[ae μ] t

Tactic:
refine eventuallyEq_set.2 <| h.mono fun x hx ↦ ?_

Result:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s : ℕ → Set α
t : Set α
h : ∀ᵐ (x : α) ∂μ, ∀ (i : ℕ), x ∈ s i ↔ x ∈ t
x : α
hx : ∀ (i : ℕ), x ∈ s i ↔ x ∈ t
⊢ x ∈ limsup s atTop ↔ x ∈ t

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s : ℕ → Set α
t : Set α
h : ∀ (n : ℕ), s n =ᶠ[ae μ] t
⊢ limsup s atTop =ᶠ[ae μ] t

Tactic:
simp only [eventuallyEq_set, ← eventually_countable_forall] at h

Result:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s : ℕ → Set α
t : Set α
h : ∀ᵐ (x : α) ∂μ, ∀ (i : ℕ), x ∈ s i ↔ x ∈ t
⊢ limsup s atTop =ᶠ[ae μ] t
-- Mathlib/Order/PrimeIdeal.lean
theorem IsPrime.of_mem_or_mem [IsProper I] (hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I) :
    IsPrime I

Proof state:
P : Type u_1
inst✝¹ : SemilatticeInf P
I : Ideal P
inst✝ : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ I.IsPrime

Tactic:
rw [isPrime_iff]

Result:
P : Type u_1
inst✝¹ : SemilatticeInf P
I : Ideal P
inst✝ : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ I.IsProper ∧ IsPFilter (↑I)ᶜ

Proof state:
case right.refine_3
P : Type u_1
inst✝¹ : SemilatticeInf P
I : Ideal P
inst✝ : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ ∀ {x y : P}, x ≤ y → x ∈ (↑I)ᶜ → y ∈ (↑I)ᶜ

Tactic:
exact @mem_compl_of_ge _ _ _

Result:
no goals

Proof state:
case right
P : Type u_1
inst✝¹ : SemilatticeInf P
I : Ideal P
inst✝ : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ IsPFilter (↑I)ᶜ

Tactic:
refine .of_def ?_ ?_ ?_

Result:
case right.refine_1
P : Type u_1
inst✝¹ : SemilatticeInf P
I : Ideal P
inst✝ : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ (↑I)ᶜ.Nonempty

case right.refine_2
P : Type u_1
inst✝¹ : SemilatticeInf P
I : Ideal P
inst✝ : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ DirectedOn (fun x1 x2 => x1 ≥ x2) (↑I)ᶜ

case right.refine_3
P : Type u_1
inst✝¹ : SemilatticeInf P
I : Ideal P
inst✝ : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ ∀ {x y : P}, x ≤ y → x ∈ (↑I)ᶜ → y ∈ (↑I)ᶜ

Proof state:
case right.refine_2
P : Type u_1
inst✝¹ : SemilatticeInf P
I : Ideal P
inst✝ : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
x : P
hx : x ∈ (↑I)ᶜ
y : P
hy : y ∈ (↑I)ᶜ
⊢ ∃ z ∈ (↑I)ᶜ, (fun x1 x2 => x1 ≥ x2) x z ∧ (fun x1 x2 => x1 ≥ x2) y z

Tactic:
exact ⟨x ⊓ y, fun h => (hI h).elim hx hy, inf_le_left, inf_le_right⟩

Result:
no goals

Proof state:
P : Type u_1
inst✝¹ : SemilatticeInf P
I : Ideal P
inst✝ : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ I.IsProper ∧ IsPFilter (↑I)ᶜ

Tactic:
use ‹_›

Result:
case right
P : Type u_1
inst✝¹ : SemilatticeInf P
I : Ideal P
inst✝ : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ IsPFilter (↑I)ᶜ

Proof state:
case right.refine_2
P : Type u_1
inst✝¹ : SemilatticeInf P
I : Ideal P
inst✝ : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ DirectedOn (fun x1 x2 => x1 ≥ x2) (↑I)ᶜ

Tactic:
intro x hx y hy

Result:
case right.refine_2
P : Type u_1
inst✝¹ : SemilatticeInf P
I : Ideal P
inst✝ : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
x : P
hx : x ∈ (↑I)ᶜ
y : P
hy : y ∈ (↑I)ᶜ
⊢ ∃ z ∈ (↑I)ᶜ, (fun x1 x2 => x1 ≥ x2) x z ∧ (fun x1 x2 => x1 ≥ x2) y z

Proof state:
case right.refine_1
P : Type u_1
inst✝¹ : SemilatticeInf P
I : Ideal P
inst✝ : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ (↑I)ᶜ.Nonempty

Tactic:
exact Set.nonempty_compl.2 (I.isProper_iff.1 ‹_›)

Result:
no goals
-- Mathlib/Algebra/Order/Group/Indicator.lean
lemma indicator_le_indicator_nonneg (s : Set α) (f : α → M) :
    s.indicator f ≤ {a | 0 ≤ f a}.indicator f

Proof state:
case pos
α : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : LinearOrder M
s : Set α
f : α → M
a : α
h✝¹ : a ∈ s
h✝ : a ∈ {a | 0 ≤ f a}
⊢ f a ≤ f a

case neg
α : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : LinearOrder M
s : Set α
f : α → M
a : α
h✝¹ : a ∈ s
h✝ : a ∉ {a | 0 ≤ f a}
⊢ f a ≤ 0

case pos
α : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : LinearOrder M
s : Set α
f : α → M
a : α
h✝¹ : a ∉ s
h✝ : a ∈ {a | 0 ≤ f a}
⊢ 0 ≤ f a

case neg
α : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : LinearOrder M
s : Set α
f : α → M
a : α
h✝¹ : a ∉ s
h✝ : a ∉ {a | 0 ≤ f a}
⊢ 0 ≤ 0

Tactic:
exacts [le_rfl, (not_le.1 ‹_›).le, ‹_›, le_rfl]

Result:
no goals

Proof state:
α : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : LinearOrder M
s : Set α
f : α → M
a : α
⊢ s.indicator f a ≤ {a | 0 ≤ f a}.indicator f a

Tactic:
classical
simp_rw [indicator_apply]
split_ifs
exacts [le_rfl, (not_le.1 ‹_›).le, ‹_›, le_rfl]

Result:
no goals

Proof state:
α : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : LinearOrder M
s : Set α
f : α → M
⊢ s.indicator f ≤ {a | 0 ≤ f a}.indicator f

Tactic:
intro a

Result:
α : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : LinearOrder M
s : Set α
f : α → M
a : α
⊢ s.indicator f a ≤ {a | 0 ≤ f a}.indicator f a

Proof state:
α : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : LinearOrder M
s : Set α
f : α → M
a : α
⊢ (if a ∈ s then f a else 0) ≤ if a ∈ {a | 0 ≤ f a} then f a else 0

Tactic:
split_ifs

Result:
case pos
α : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : LinearOrder M
s : Set α
f : α → M
a : α
h✝¹ : a ∈ s
h✝ : a ∈ {a | 0 ≤ f a}
⊢ f a ≤ f a

case neg
α : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : LinearOrder M
s : Set α
f : α → M
a : α
h✝¹ : a ∈ s
h✝ : a ∉ {a | 0 ≤ f a}
⊢ f a ≤ 0

case pos
α : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : LinearOrder M
s : Set α
f : α → M
a : α
h✝¹ : a ∉ s
h✝ : a ∈ {a | 0 ≤ f a}
⊢ 0 ≤ f a

case neg
α : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : LinearOrder M
s : Set α
f : α → M
a : α
h✝¹ : a ∉ s
h✝ : a ∉ {a | 0 ≤ f a}
⊢ 0 ≤ 0

Proof state:
α : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : LinearOrder M
s : Set α
f : α → M
a : α
⊢ s.indicator f a ≤ {a | 0 ≤ f a}.indicator f a

Tactic:
simp_rw [indicator_apply]

Result:
α : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : LinearOrder M
s : Set α
f : α → M
a : α
⊢ (if a ∈ s then f a else 0) ≤ if a ∈ {a | 0 ≤ f a} then f a else 0
-- Mathlib/Algebra/Order/AbsoluteValue/Basic.lean
lemma IsNontrivial.exists_abv_lt_one {F S : Type*} [Field F] [LinearOrderedField S]
    {v : AbsoluteValue F S} (h : v.IsNontrivial) :
    ∃ x ≠ 0, v x < 1

Proof state:
case intro
F : Type u_7
S : Type u_8
inst✝¹ : Field F
inst✝ : LinearOrderedField S
v : AbsoluteValue F S
h : v.IsNontrivial
y : F
hy : 1 < v y
hy₀ : y ≠ 0
⊢ (v y)⁻¹ < 1

Tactic:
exact (inv_lt_one₀ <| v.pos hy₀).mpr hy

Result:
no goals

Proof state:
case intro
F : Type u_7
S : Type u_8
inst✝¹ : Field F
inst✝ : LinearOrderedField S
v : AbsoluteValue F S
h : v.IsNontrivial
y : F
hy : 1 < v y
hy₀ : y ≠ 0
⊢ v y⁻¹ < 1

Tactic:
rw [map_inv₀]

Result:
case intro
F : Type u_7
S : Type u_8
inst✝¹ : Field F
inst✝ : LinearOrderedField S
v : AbsoluteValue F S
h : v.IsNontrivial
y : F
hy : 1 < v y
hy₀ : y ≠ 0
⊢ (v y)⁻¹ < 1

Proof state:
case intro
F : Type u_7
S : Type u_8
inst✝¹ : Field F
inst✝ : LinearOrderedField S
v : AbsoluteValue F S
h : v.IsNontrivial
y : F
hy : 1 < v y
hy₀ : y ≠ 0
⊢ ∃ x, x ≠ 0 ∧ v x < 1

Tactic:
refine ⟨y⁻¹, inv_ne_zero hy₀, ?_⟩

Result:
case intro
F : Type u_7
S : Type u_8
inst✝¹ : Field F
inst✝ : LinearOrderedField S
v : AbsoluteValue F S
h : v.IsNontrivial
y : F
hy : 1 < v y
hy₀ : y ≠ 0
⊢ v y⁻¹ < 1

Proof state:
case intro
F : Type u_7
S : Type u_8
inst✝¹ : Field F
inst✝ : LinearOrderedField S
v : AbsoluteValue F S
h : v.IsNontrivial
y : F
hy : 1 < v y
⊢ ∃ x, x ≠ 0 ∧ v x < 1

Tactic:
have hy₀ := v.ne_zero_iff.mp <| (zero_lt_one.trans hy).ne'

Result:
case intro
F : Type u_7
S : Type u_8
inst✝¹ : Field F
inst✝ : LinearOrderedField S
v : AbsoluteValue F S
h : v.IsNontrivial
y : F
hy : 1 < v y
hy₀ : y ≠ 0
⊢ ∃ x, x ≠ 0 ∧ v x < 1

Proof state:
F : Type u_7
S : Type u_8
inst✝¹ : Field F
inst✝ : LinearOrderedField S
v : AbsoluteValue F S
h : v.IsNontrivial
⊢ ∃ x, x ≠ 0 ∧ v x < 1

Tactic:
obtain ⟨y, hy⟩ := h.exists_abv_gt_one

Result:
case intro
F : Type u_7
S : Type u_8
inst✝¹ : Field F
inst✝ : LinearOrderedField S
v : AbsoluteValue F S
h : v.IsNontrivial
y : F
hy : 1 < v y
⊢ ∃ x, x ≠ 0 ∧ v x < 1
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem tan_nonpos_of_nonpos_of_neg_pi_div_two_le {x : ℝ} (hx0 : x ≤ 0) (hpx : -(π / 2) ≤ x) :
    tan x ≤ 0 :=
  neg_nonneg.1 (tan_neg x ▸ tan_nonneg_of_nonneg_of_le_pi_div_two (by linarith) (by linarith))

Proof state:
x : ℝ
hx0 : x ≤ 0
hpx : -(π / 2) ≤ x
⊢ -x ≤ π / 2

Tactic:
linarith

Result:
no goals

Proof state:
x : ℝ
hx0 : x ≤ 0
hpx : -(π / 2) ≤ x
⊢ 0 ≤ -x

Tactic:
linarith

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/Defs.lean
theorem comp (f : ι' → ι) (hf : Function.Injective f) : AlgebraicIndependent R (x ∘ f)

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
f : ι' → ι
hf : Injective f
⊢ AlgebraicIndependent R (x ∘ f)

Tactic:
intro p q

Result:
ι : Type u_1
ι' : Type u_2
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
f : ι' → ι
hf : Injective f
p q : MvPolynomial ι' R
⊢ (aeval (x ∘ f)) p = (aeval (x ∘ f)) q → p = q

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
f : ι' → ι
hf : Injective f
p q : MvPolynomial ι' R
⊢ (aeval (x ∘ f)) p = (aeval (x ∘ f)) q → p = q

Tactic:
simpa [aeval_rename, (rename_injective f hf).eq_iff] using @hx (rename f p) (rename f q)

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem coe_real_ereal_eq_coe_toNNReal_sub_coe_toNNReal (x : ℝ) :
    (x : EReal) = Real.toNNReal x - Real.toNNReal (-x)

Proof state:
x : ℝ
⊢ ↑x = ↑↑x.toNNReal - ↑↑(-x).toNNReal

Tactic:
rcases le_total 0 x with (h | h)

Result:
case inl
x : ℝ
h : 0 ≤ x
⊢ ↑x = ↑↑x.toNNReal - ↑↑(-x).toNNReal

case inr
x : ℝ
h : x ≤ 0
⊢ ↑x = ↑↑x.toNNReal - ↑↑(-x).toNNReal

Proof state:
case inr
x : ℝ
h : x ≤ 0
⊢ ↑x = ↑↑x.toNNReal - ↑↑(-x).toNNReal

Tactic:
rw [Real.toNNReal_of_nonpos h, ENNReal.coe_zero, coe_ennreal_zero, coe_nnreal_eq_coe_real,
  Real.coe_toNNReal, zero_sub, coe_neg, neg_neg]

Result:
case inr.hr
x : ℝ
h : x ≤ 0
⊢ 0 ≤ -x

Proof state:
case inr.hr
x : ℝ
h : x ≤ 0
⊢ 0 ≤ -x

Tactic:
exact neg_nonneg.2 h

Result:
no goals

Proof state:
case inl.intro
x : ℝ≥0
⊢ ↑↑x = ↑↑(↑x).toNNReal - ↑↑(-↑x).toNNReal

Tactic:
rw [Real.toNNReal_of_nonpos (neg_nonpos.mpr x.coe_nonneg), Real.toNNReal_coe, ENNReal.coe_zero,
  coe_ennreal_zero, sub_zero]

Result:
case inl.intro
x : ℝ≥0
⊢ ↑↑x = ↑↑x

Proof state:
case inl.intro
x : ℝ≥0
⊢ ↑↑x = ↑↑x

Tactic:
rfl

Result:
no goals

Proof state:
case inl
x : ℝ
h : 0 ≤ x
⊢ ↑x = ↑↑x.toNNReal - ↑↑(-x).toNNReal

Tactic:
lift x to ℝ≥0 using h

Result:
case inl.intro
x : ℝ≥0
⊢ ↑↑x = ↑↑(↑x).toNNReal - ↑↑(-↑x).toNNReal
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem shiftRight_add {w : Nat} (x : BitVec w) (n m : Nat) :
    x >>> (n + m) = (x >>> n) >>> m

Proof state:
case pred
w : Nat
x : BitVec w
n m i : Nat
a✝ : i < w
⊢ (x >>> (n + m)).getLsbD i = (x >>> n >>> m).getLsbD i

Tactic:
simp [Nat.add_assoc n m i]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
n m : Nat
⊢ x >>> (n + m) = x >>> n >>> m

Tactic:
ext i

Result:
case pred
w : Nat
x : BitVec w
n m i : Nat
a✝ : i < w
⊢ (x >>> (n + m)).getLsbD i = (x >>> n >>> m).getLsbD i
-- Mathlib/Algebra/Group/Pointwise/Set/BigOperators.lean
theorem multiset_prod_subset_multiset_prod (t : Multiset ι) (f₁ f₂ : ι → Set α)
    (hf : ∀ i ∈ t, f₁ i ⊆ f₂ i) : (t.map f₁).prod ⊆ (t.map f₂).prod

Proof state:
case h
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f₁ f₂ : ι → Set α
a✝ : List ι
hf : ∀ i ∈ ⟦a✝⟧, f₁ i ⊆ f₂ i
⊢ (List.map f₁ a✝).prod ⊆ (List.map f₂ a✝).prod

Tactic:
exact list_prod_subset_list_prod _ _ _ hf

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
t : Multiset ι
f₁ f₂ : ι → Set α
hf : ∀ i ∈ t, f₁ i ⊆ f₂ i
⊢ (Multiset.map f₁ t).prod ⊆ (Multiset.map f₂ t).prod

Tactic:
induction t using Quotient.inductionOn

Result:
case h
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f₁ f₂ : ι → Set α
a✝ : List ι
hf : ∀ i ∈ ⟦a✝⟧, f₁ i ⊆ f₂ i
⊢ (Multiset.map f₁ ⟦a✝⟧).prod ⊆ (Multiset.map f₂ ⟦a✝⟧).prod

Proof state:
case h
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f₁ f₂ : ι → Set α
a✝ : List ι
hf : ∀ i ∈ ⟦a✝⟧, f₁ i ⊆ f₂ i
⊢ (Multiset.map f₁ ⟦a✝⟧).prod ⊆ (Multiset.map f₂ ⟦a✝⟧).prod

Tactic:
simp_rw [Multiset.quot_mk_to_coe, Multiset.map_coe, Multiset.prod_coe]

Result:
case h
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f₁ f₂ : ι → Set α
a✝ : List ι
hf : ∀ i ∈ ⟦a✝⟧, f₁ i ⊆ f₂ i
⊢ (List.map f₁ a✝).prod ⊆ (List.map f₂ a✝).prod