harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Pell.lean
theorem mul_inv_x_pos {a₁ : Solution₁ d} (h : IsFundamental a₁) {a : Solution₁ d} (hax : 1 < a.x)
    (hay : 0 < a.y) : 0 < (a * a₁⁻¹).x

Proof state:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ d * a.y * (a.x * a₁.y) < a.x * (a.x * a₁.x)

Tactic:
refine ((mul_le_mul_left <| mul_pos h.d_pos hay).mpr <| x_mul_y_le_y_mul_x h hax hay).trans_lt ?_

Result:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ d * a.y * (a.y * a₁.x) < a.x * (a.x * a₁.x)

Proof state:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ 0 < a₁.x

Tactic:
exact zero_lt_one.trans h.1

Result:
no goals

Proof state:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ 0 < (a * a₁⁻¹).x

Tactic:
simp only [x_mul, x_inv, y_inv, mul_neg, lt_add_neg_iff_add_lt, zero_add]

Result:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ d * (a.y * a₁.y) < a.x * a₁.x

Proof state:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ d * (a.y * a₁.y) < a.x * a₁.x

Tactic:
refine (mul_lt_mul_left <| zero_lt_one.trans hax).mp ?_

Result:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ a.x * (d * (a.y * a₁.y)) < a.x * (a.x * a₁.x)

Proof state:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ a.x * (d * (a.y * a₁.y)) = d * a.y * (a.x * a₁.y)

Tactic:
ring

Result:
no goals

Proof state:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ d * a.y * (a.y * a₁.x) < a.x * (a.x * a₁.x)

Tactic:
rw [← mul_assoc, mul_assoc d, ← sq, a.prop_y, ← sub_pos]

Result:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ 0 < a.x * (a.x * a₁.x) - (a.x ^ 2 - 1) * a₁.x

Proof state:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ 0 < a.x * (a.x * a₁.x) - (a.x ^ 2 - 1) * a₁.x

Tactic:
ring_nf

Result:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ 0 < a₁.x

Proof state:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ a.x * (d * (a.y * a₁.y)) < a.x * (a.x * a₁.x)

Tactic:
rw [(by ring : a.x * (d * (a.y * a₁.y)) = d * a.y * (a.x * a₁.y))]

Result:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ d * a.y * (a.x * a₁.y) < a.x * (a.x * a₁.x)
-- Mathlib/Algebra/Lie/Weights/Chain.lean
lemma exists₂_genWeightSpace_smul_add_eq_bot :
    ∃ᵉ (p < (0 : ℤ)) (q > (0 : ℤ)),
      genWeightSpace M (p • χ₁ + χ₂) = ⊥ ∧
      genWeightSpace M (q • χ₁ + χ₂) = ⊥

Proof state:
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
q : ℕ
hq₀ : q > 0
hq : genWeightSpace M (q • χ₁ + χ₂) = ⊥
p : ℕ
hp₀ : p > 0
hp : genWeightSpace M (p • -χ₁ + χ₂) = ⊥
⊢ ↑q > 0

Tactic:
simpa

Result:
no goals

Proof state:
case intro.intro.intro.intro.refine_1
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
q : ℕ
hq₀ : q > 0
hq : genWeightSpace M (q • χ₁ + χ₂) = ⊥
p : ℕ
hp₀ : p > 0
hp : genWeightSpace M (p • -χ₁ + χ₂) = ⊥
⊢ genWeightSpace M (p • -χ₁ + χ₂) = ⊥

Tactic:
exact hp

Result:
no goals
-- Mathlib/Order/Atoms.lean
theorem isAtom_iff [OrderBot A] {K : A} :
    IsAtom K ↔ K ≠ ⊥ ∧ ∀ H g, H ≤ K → g ∉ H → g ∈ K → H = ⊥

Proof state:
A : Type u_4
B : Type u_5
inst✝¹ : SetLike A B
inst✝ : OrderBot A
K : A
⊢ IsAtom K ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥

Tactic:
simp_rw [IsAtom, lt_iff_le_not_le, SetLike.not_le_iff_exists,
  and_comm (a := _ ≤ _), and_imp, exists_imp, ← and_imp, and_comm]

Result:
no goals
-- Mathlib/Data/List/Dedup.lean
theorem dedup_eq_nil (l : List α) : l.dedup = [] ↔ l = []

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : l.dedup = [] ↔ l = []
h : a ∈ l
⊢ (a :: l).dedup = [] ↔ a :: l = []

Tactic:
simp only [List.dedup_cons_of_mem h, hl, List.ne_nil_of_mem h, reduceCtorEq]

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : l.dedup = [] ↔ l = []
⊢ (a :: l).dedup = [] ↔ a :: l = []

Tactic:
by_cases h : a ∈ l

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : l.dedup = [] ↔ l = []
h : a ∈ l
⊢ (a :: l).dedup = [] ↔ a :: l = []

case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : l.dedup = [] ↔ l = []
h : a ∉ l
⊢ (a :: l).dedup = [] ↔ a :: l = []

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : l.dedup = [] ↔ l = []
h : a ∉ l
⊢ (a :: l).dedup = [] ↔ a :: l = []

Tactic:
simp only [List.dedup_cons_of_not_mem h, List.cons_ne_nil]

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
⊢ [].dedup = [] ↔ [] = []

Tactic:
exact Iff.rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ l.dedup = [] ↔ l = []

Tactic:
induction' l with a l hl

Result:
case nil
α : Type u_1
inst✝ : DecidableEq α
⊢ [].dedup = [] ↔ [] = []

case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : l.dedup = [] ↔ l = []
⊢ (a :: l).dedup = [] ↔ a :: l = []
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem div_le_iff_le_mul' : a / b ≤ c ↔ a ≤ b * c

Proof state:
α : Type u
inst✝² : CommGroup α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b c : α
⊢ a / b ≤ c ↔ a ≤ b * c

Tactic:
rw [div_le_iff_le_mul, mul_comm]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem neighborSet_fst_subgraphOfAdj {v w : V} (hvw : G.Adj v w) :
    (G.subgraphOfAdj hvw).neighborSet v = {w}

Proof state:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
u : V
this : w = u ↔ u = w
⊢ u ∈ (G.subgraphOfAdj hvw).neighborSet v ↔ u ∈ {w}

Tactic:
simpa [hvw.ne.symm] using this

Result:
no goals

Proof state:
case h
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
u : V
⊢ w = u ↔ u = w

Tactic:
rw [eq_comm]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ (G.subgraphOfAdj hvw).neighborSet v = {w}

Tactic:
ext u

Result:
case h
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
u : V
⊢ u ∈ (G.subgraphOfAdj hvw).neighborSet v ↔ u ∈ {w}

Proof state:
case h
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
u : V
⊢ u ∈ (G.subgraphOfAdj hvw).neighborSet v ↔ u ∈ {w}

Tactic:
suffices w = u ↔ u = w by simpa [hvw.ne.symm] using this

Result:
case h
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
u : V
⊢ w = u ↔ u = w
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapFinIdx_eq_append_iff {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
    l.mapFinIdx f = l₁ ++ l₂ ↔
      ∃ (l₁' : List α) (l₂' : List α) (w : l = l₁' ++ l₂'),
        l₁'.mapFinIdx (fun i a h => f i a (by simp [w]; omega)) = l₁ ∧
        l₂'.mapFinIdx (fun i a h => f (i + l₁'.length) a (by simp [w]; omega)) = l₂

Proof state:
case mp
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
h : (l₁ ++ l₂).length = l.length
w : ∀ (i : Nat) (h_1 : i < l.length), (l₁ ++ l₂)[i] = f i l[i] h_1
⊢ ∃ l₁' l₂' w, (l₁'.mapFinIdx fun i a h => f i a ⋯) = l₁ ∧ (l₂'.mapFinIdx fun i a h => f (i + l₁'.length) a ⋯) = l₂

Tactic:
simp only [length_append] at h

Result:
case mp
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
h✝ : (l₁ ++ l₂).length = l.length
w : ∀ (i : Nat) (h : i < l.length), (l₁ ++ l₂)[i] = f i l[i] h
h : l₁.length + l₂.length = l.length
⊢ ∃ l₁' l₂' w, (l₁'.mapFinIdx fun i a h => f i a ⋯) = l₁ ∧ (l₂'.mapFinIdx fun i a h => f (i + l₁'.length) a ⋯) = l₂
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem sum_centroidWeightsIndicator_eq_one_of_card_ne_zero [CharZero k] [Fintype ι]
    (h : #s ≠ 0) : ∑ i, s.centroidWeightsIndicator k i = 1

Proof state:
k : Type u_1
inst✝² : DivisionRing k
ι : Type u_4
s : Finset ι
inst✝¹ : CharZero k
inst✝ : Fintype ι
h : #s ≠ 0
⊢ ∑ i : ι, centroidWeightsIndicator k s i = 1

Tactic:
rw [sum_centroidWeightsIndicator]

Result:
k : Type u_1
inst✝² : DivisionRing k
ι : Type u_4
s : Finset ι
inst✝¹ : CharZero k
inst✝ : Fintype ι
h : #s ≠ 0
⊢ ∑ i ∈ s, centroidWeights k s i = 1

Proof state:
k : Type u_1
inst✝² : DivisionRing k
ι : Type u_4
s : Finset ι
inst✝¹ : CharZero k
inst✝ : Fintype ι
h : #s ≠ 0
⊢ ∑ i ∈ s, centroidWeights k s i = 1

Tactic:
exact s.sum_centroidWeights_eq_one_of_card_ne_zero k h

Result:
no goals
-- Mathlib/Order/SupIndep.lean
theorem iSupIndep_def' : iSupIndep t ↔ ∀ i, Disjoint (t i) (sSup (t '' { j | j ≠ i }))

Proof state:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
⊢ iSupIndep t ↔ ∀ (i : ι), Disjoint (t i) (⨆ a ∈ {j | j ≠ i}, t a)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
⊢ iSupIndep t ↔ ∀ (i : ι), Disjoint (t i) (sSup (t '' {j | j ≠ i}))

Tactic:
simp_rw [sSup_image]

Result:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
⊢ iSupIndep t ↔ ∀ (i : ι), Disjoint (t i) (⨆ a ∈ {j | j ≠ i}, t a)
-- Mathlib/Data/Multiset/Powerset.lean
theorem powersetCardAux_cons (n : ℕ) (a : α) (l : List α) :
    powersetCardAux (n + 1) (a :: l) =
      powersetCardAux (n + 1) l ++ List.map (cons a) (powersetCardAux n l)

Proof state:
α : Type u_1
n : ℕ
a : α
l : List α
⊢ powersetCardAux (n + 1) (a :: l) = powersetCardAux (n + 1) l ++ List.map (cons a) (powersetCardAux n l)

Tactic:
simp [powersetCardAux_eq_map_coe]

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem le_zero_lf {x : PGame} : x ≤ 0 ↔ ∀ i, x.moveLeft i ⧏ 0

Proof state:
x : PGame
⊢ ((∀ (i : x.LeftMoves), x.moveLeft i ⧏ 0) ∧ ∀ (j : RightMoves 0), x ⧏ moveRight 0 j) ↔
    ∀ (i : x.LeftMoves), x.moveLeft i ⧏ 0

Tactic:
simp

Result:
no goals

Proof state:
x : PGame
⊢ x ≤ 0 ↔ ∀ (i : x.LeftMoves), x.moveLeft i ⧏ 0

Tactic:
rw [le_iff_forall_lf]

Result:
x : PGame
⊢ ((∀ (i : x.LeftMoves), x.moveLeft i ⧏ 0) ∧ ∀ (j : RightMoves 0), x ⧏ moveRight 0 j) ↔
    ∀ (i : x.LeftMoves), x.moveLeft i ⧏ 0
-- Mathlib/RingTheory/Ideal/Height.lean
lemma Ideal.finiteHeight_iff_lt {I : Ideal R} :
    Ideal.FiniteHeight I ↔ I = ⊤ ∨ I.height < ⊤

Proof state:
case mpr.eq_top_or_height_ne_top.inr
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.height < ⊤
⊢ I = ⊤ ∨ I.height ≠ ⊤

Tactic:
exact Or.inr (ne_top_of_lt h)

Result:
no goals

Proof state:
case mp
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.FiniteHeight
⊢ I = ⊤ ∨ I.height < ⊤

Tactic:
cases h.eq_top_or_height_ne_top with
| inl h => exact Or.inl h
| inr h => exact Or.inr (lt_of_le_of_ne le_top h)

Result:
no goals

Proof state:
case mpr
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I = ⊤ ∨ I.height < ⊤
⊢ I.FiniteHeight

Tactic:
constructor

Result:
case mpr.eq_top_or_height_ne_top
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I = ⊤ ∨ I.height < ⊤
⊢ I = ⊤ ∨ I.height ≠ ⊤

Proof state:
case mpr
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ I = ⊤ ∨ I.height < ⊤ → I.FiniteHeight

Tactic:
intro h

Result:
case mpr
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I = ⊤ ∨ I.height < ⊤
⊢ I.FiniteHeight

Proof state:
case mpr.eq_top_or_height_ne_top.inl
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I = ⊤
⊢ I = ⊤ ∨ I.height ≠ ⊤

Tactic:
exact Or.inl h

Result:
no goals

Proof state:
case mpr.eq_top_or_height_ne_top
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I = ⊤ ∨ I.height < ⊤
⊢ I = ⊤ ∨ I.height ≠ ⊤

Tactic:
cases h with
| inl h => exact Or.inl h
| inr h => exact Or.inr (ne_top_of_lt h)

Result:
no goals

Proof state:
case mp
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ I.FiniteHeight → I = ⊤ ∨ I.height < ⊤

Tactic:
intro h

Result:
case mp
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.FiniteHeight
⊢ I = ⊤ ∨ I.height < ⊤

Proof state:
case mp.inl
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I.FiniteHeight
h : I = ⊤
⊢ I = ⊤ ∨ I.height < ⊤

Tactic:
exact Or.inl h

Result:
no goals

Proof state:
case mp.inr
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I.FiniteHeight
h : I.height ≠ ⊤
⊢ I = ⊤ ∨ I.height < ⊤

Tactic:
exact Or.inr (lt_of_le_of_ne le_top h)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ I.FiniteHeight ↔ I = ⊤ ∨ I.height < ⊤

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ I.FiniteHeight → I = ⊤ ∨ I.height < ⊤

case mpr
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ I = ⊤ ∨ I.height < ⊤ → I.FiniteHeight
-- Mathlib/NumberTheory/MulChar/Basic.lean
theorem pow_apply' (χ : MulChar R R') {n : ℕ} (hn : n ≠ 0) (a : R) : (χ ^ n) a = χ a ^ n

Proof state:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
hn : n ≠ 0
a : R
⊢ (χ ^ n) a = χ a ^ n

Tactic:
by_cases ha : IsUnit a

Result:
case pos
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
hn : n ≠ 0
a : R
ha : IsUnit a
⊢ (χ ^ n) a = χ a ^ n

case neg
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
hn : n ≠ 0
a : R
ha : ¬IsUnit a
⊢ (χ ^ n) a = χ a ^ n

Proof state:
case pos
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
hn : n ≠ 0
a : R
ha : IsUnit a
⊢ (χ ^ n) a = χ a ^ n

Tactic:
exact pow_apply_coe χ n ha.unit

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
hn : n ≠ 0
a : R
ha : ¬IsUnit a
⊢ (χ ^ n) a = χ a ^ n

Tactic:
rw [map_nonunit (χ ^ n) ha, map_nonunit χ ha, zero_pow hn]

Result:
no goals
-- Mathlib/Data/Finset/Max.lean
theorem min'_mem : s.min' H ∈ s :=
  mem_of_min <| by simp only [Finset.min, min', id_eq, coe_inf', Function.comp_def]

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
H : s.Nonempty
⊢ s.min = ↑(s.min' H)

Tactic:
simp only [Finset.min, min', id_eq, coe_inf', Function.comp_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem lt_of_sub_neg {a b : Int} (h : a - b < 0) : a < b

Proof state:
a b : Int
h : a - b < 0
⊢ a < b

Tactic:
have h := Int.add_lt_add_right h b

Result:
a b : Int
h✝ : a - b < 0
h : a - b + b < 0 + b
⊢ a < b

Proof state:
a b : Int
h✝ : a - b < 0
h : a - b + b < 0 + b
⊢ a < b

Tactic:
rwa [Int.sub_add_cancel, Int.zero_add] at h

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Portmanteau.lean
theorem tendsto_of_forall_isOpen_le_liminf {μ : ProbabilityMeasure Ω}
    {μs : ℕ → ProbabilityMeasure Ω}
    (h_opens : ∀ G, IsOpen G → μ G ≤ atTop.liminf (fun i ↦ μs i G)) :
    atTop.Tendsto (fun i ↦ μs i) (𝓝 μ)

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
G : Set Ω
G_open : IsOpen G
h_opens : μ G ≤ liminf (fun i => (μs i) G) atTop
⊢ ∀ᶠ (x : ℝ≥0) in map (fun x => (μs x) G) atTop, (fun x1 x2 => x1 ≤ x2) x 1

Tactic:
simp

Result:
no goals

Proof state:
case refine_3
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
G : Set Ω
G_open : IsOpen G
h_opens : μ G ≤ liminf (fun i => (μs i) G) atTop
⊢ IsBoundedUnder (fun x1 x2 => x1 ≥ x2) atTop fun x => (μs x) G

Tactic:
exact ⟨0, by simp⟩

Result:
no goals

Proof state:
case h
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) atTop
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
⊢ ∫ (x : Ω), f x ∂↑μ ≤ liminf (fun i => ∫ (x : Ω), f x ∂↑(μs i)) atTop

Tactic:
apply integral_le_liminf_integral_of_forall_isOpen_measure_le_liminf_measure (f := f) f_nn

Result:
case h
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) atTop
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
⊢ ∀ (G : Set Ω), IsOpen G → ↑μ G ≤ liminf (fun i => ↑(μs i) G) atTop

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
G : Set Ω
G_open : IsOpen G
h_opens : μ G ≤ liminf (fun i => (μs i) G) atTop
⊢ ∀ᶠ (x : ℝ≥0) in map (fun x => (μs x) G) atTop, (fun x1 x2 => x1 ≥ x2) x 0

Tactic:
simp

Result:
no goals

Proof state:
case refine_2
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
G : Set Ω
G_open : IsOpen G
h_opens : μ G ≤ liminf (fun i => (μs i) G) atTop
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) atTop fun x => (μs x) G

Tactic:
exact IsBoundedUnder.isCoboundedUnder_ge ⟨1, by simp⟩

Result:
no goals
-- Mathlib/Data/Set/Card/Arithmetic.lean
theorem exists_union_disjoint_cardinal_eq_of_even (he : Even s.ncard) :
    ∃ (t u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #t = #u

Proof state:
case inr
α : Type u_1
s : Set α
hs : s.Finite
he : Even #hs.toFinset
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u

Tactic:
obtain ⟨t, u, hutu, hdtu, hctu⟩ := Finset.exists_disjoint_union_of_even_card he

Result:
case inr.intro.intro.intro.intro
α : Type u_1
s : Set α
hs : s.Finite
he : Even #hs.toFinset
t u : Finset α
hutu : t ∪ u = hs.toFinset
hdtu : Disjoint t u
hctu : #t = #u
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u

Proof state:
case inl
α : Type u_1
s : Set α
he : Even s.ncard
hs : s.Infinite
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u

Tactic:
exact hs.exists_union_disjoint_cardinal_eq_of_infinite

Result:
no goals

Proof state:
case h
α : Type u_1
s : Set α
hs : s.Finite
he : Even #hs.toFinset
t u : Finset α
hutu : t ∪ u = hs.toFinset
hdtu : Disjoint t u
hctu : #t = #u
⊢ ↑t ∪ ↑u = s ∧ Disjoint ↑t ↑u ∧ #↑↑t = #↑↑u

Tactic:
simp [← Finset.coe_union, *]

Result:
no goals

Proof state:
case inr.intro.intro.intro.intro
α : Type u_1
s : Set α
hs : s.Finite
he : Even #hs.toFinset
t u : Finset α
hutu : t ∪ u = hs.toFinset
hdtu : Disjoint t u
hctu : #t = #u
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u

Tactic:
use t.toSet, u.toSet

Result:
case h
α : Type u_1
s : Set α
hs : s.Finite
he : Even #hs.toFinset
t u : Finset α
hutu : t ∪ u = hs.toFinset
hdtu : Disjoint t u
hctu : #t = #u
⊢ ↑t ∪ ↑u = s ∧ Disjoint ↑t ↑u ∧ #↑↑t = #↑↑u

Proof state:
case inr
α : Type u_1
s : Set α
he : Even s.ncard
hs : s.Finite
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u

Tactic:
rw [ncard_eq_toFinset_card s hs] at he

Result:
case inr
α : Type u_1
s : Set α
hs : s.Finite
he : Even #hs.toFinset
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u

Proof state:
case inr
α : Type u_1
s : Set α
he : Even s.ncard
hs : s.Finite
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u

Tactic:
classical
rw [ncard_eq_toFinset_card s hs] at he
obtain ⟨t, u, hutu, hdtu, hctu⟩ := Finset.exists_disjoint_union_of_even_card he
use t.toSet, u.toSet
simp [← Finset.coe_union, *]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
he : Even s.ncard
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u

Tactic:
obtain hs | hs := s.infinite_or_finite

Result:
case inl
α : Type u_1
s : Set α
he : Even s.ncard
hs : s.Infinite
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u

case inr
α : Type u_1
s : Set α
he : Even s.ncard
hs : s.Finite
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u
-- Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean
theorem order_eq_zero_iff (hp : p ≠ 0) : p.order = 0 ↔ p 0 ≠ 0

Proof state:
𝕜 : Type u
E : Type v
F : Type w
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : ContinuousAdd E
inst✝⁵ : ContinuousConstSMul 𝕜 E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
hp : p ≠ 0
⊢ p.order = 0 ↔ p 0 ≠ 0

Tactic:
simp [order_eq_zero_iff', hp]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem Expr.eq_of_toNormPoly (ctx : Context) (a b : Expr) (h : a.toNormPoly = b.toNormPoly) : a.denote ctx = b.denote ctx

Proof state:
ctx : Context
a b : Expr
h✝ : Poly.norm.go a.toPoly [] = Poly.norm.go b.toPoly []
h : denote ctx a = denote ctx b
⊢ denote ctx a = denote ctx b

Tactic:
assumption

Result:
no goals

Proof state:
ctx : Context
a b : Expr
h : a.toNormPoly = b.toNormPoly
⊢ denote ctx a = denote ctx b

Tactic:
simp [toNormPoly, Poly.norm] at h

Result:
ctx : Context
a b : Expr
h : Poly.norm.go a.toPoly [] = Poly.norm.go b.toPoly []
⊢ denote ctx a = denote ctx b

Proof state:
ctx : Context
a b : Expr
h : Poly.norm.go a.toPoly [] = Poly.norm.go b.toPoly []
⊢ denote ctx a = denote ctx b

Tactic:
have h := congrArg (Poly.denote ctx) h

Result:
ctx : Context
a b : Expr
h✝ : Poly.norm.go a.toPoly [] = Poly.norm.go b.toPoly []
h : Poly.denote ctx (Poly.norm.go a.toPoly []) = Poly.denote ctx (Poly.norm.go b.toPoly [])
⊢ denote ctx a = denote ctx b

Proof state:
ctx : Context
a b : Expr
h✝ : Poly.norm.go a.toPoly [] = Poly.norm.go b.toPoly []
h : Poly.denote ctx (Poly.norm.go a.toPoly []) = Poly.denote ctx (Poly.norm.go b.toPoly [])
⊢ denote ctx a = denote ctx b

Tactic:
simp at h

Result:
ctx : Context
a b : Expr
h✝ : Poly.norm.go a.toPoly [] = Poly.norm.go b.toPoly []
h : denote ctx a = denote ctx b
⊢ denote ctx a = denote ctx b
-- Mathlib/CategoryTheory/Sites/Sieves.lean
theorem functorPullback_comp (R : Sieve ((F ⋙ G).obj X)) :
    R.functorPullback (F ⋙ G) = (R.functorPullback G).functorPullback F

Proof state:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve ((F ⋙ G).obj X)
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ (functorPullback (F ⋙ G) R).arrows f✝ ↔ (functorPullback F (functorPullback G R)).arrows f✝

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve ((F ⋙ G).obj X)
⊢ functorPullback (F ⋙ G) R = functorPullback F (functorPullback G R)

Tactic:
ext

Result:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve ((F ⋙ G).obj X)
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ (functorPullback (F ⋙ G) R).arrows f✝ ↔ (functorPullback F (functorPullback G R)).arrows f✝
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
/-- Binary entropy is strictly decreasing in interval [1/2, 1]. -/
lemma binEntropy_strictAntiOn : StrictAntiOn binEntropy (Icc 2⁻¹ 1)

Proof state:
⊢ StrictAntiOn (qaryEntropy 2) (Icc (1 / 2) 1)

Tactic:
convert qaryEntropy_strictAntiOn (by rfl) using 1

Result:
case h.e'_6

⊢ Icc (1 / 2) 1 = Icc (1 - 1 / ↑2) 1

Proof state:
⊢ Icc 2⁻¹ 1 = Icc (1 / 2) 1

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ 2 ≤ ?m.172555

Tactic:
rfl

Result:
no goals

Proof state:
⊢ StrictAntiOn binEntropy (Icc 2⁻¹ 1)

Tactic:
rw [show (Icc (2⁻¹ : ℝ) 1) = Icc (1/2) 1 by norm_num, ← qaryEntropy_two]

Result:
⊢ StrictAntiOn (qaryEntropy 2) (Icc (1 / 2) 1)

Proof state:
case h.e'_6

⊢ Icc (1 / 2) 1 = Icc (1 - 1 / ↑2) 1

Tactic:
norm_num

Result:
no goals