harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/RelabelFin.lean
theorem of_maxLiteral_eq_some' (f : CNF Nat) (h : f.maxLiteral = some maxLit) :
    ∀ clause, clause ∈ f → clause.maxLiteral = some localMax → localMax ≤ maxLit

Proof state:
maxLit localMax : Nat
f : CNF Nat
h : f.maxLiteral = some maxLit
⊢ ∀ (clause : Clause Nat), clause ∈ f → clause.maxLiteral = some localMax → localMax ≤ maxLit

Tactic:
intro clause hclause1 hclause2

Result:
maxLit localMax : Nat
f : CNF Nat
h : f.maxLiteral = some maxLit
clause : Clause Nat
hclause1 : clause ∈ f
hclause2 : clause.maxLiteral = some localMax
⊢ localMax ≤ maxLit

Proof state:
maxLit localMax : Nat
f : CNF Nat
clause : Clause Nat
hclause1 : clause ∈ f
hclause2 : clause.maxLiteral = some localMax
h : (∃ a, a ∈ f ∧ a.maxLiteral = some maxLit) ∧ ∀ (b : Nat) (x : Clause Nat), x ∈ f → x.maxLiteral = some b → b ≤ maxLit
⊢ localMax ≤ maxLit

Tactic:
rcases h with ⟨_, hclause3⟩

Result:
case intro
maxLit localMax : Nat
f : CNF Nat
clause : Clause Nat
hclause1 : clause ∈ f
hclause2 : clause.maxLiteral = some localMax
left✝ : ∃ a, a ∈ f ∧ a.maxLiteral = some maxLit
hclause3 : ∀ (b : Nat) (x : Clause Nat), x ∈ f → x.maxLiteral = some b → b ≤ maxLit
⊢ localMax ≤ maxLit

Proof state:
maxLit localMax : Nat
f : CNF Nat
h : f.maxLiteral = some maxLit
clause : Clause Nat
hclause1 : clause ∈ f
hclause2 : clause.maxLiteral = some localMax
⊢ localMax ≤ maxLit

Tactic:
simp [maxLiteral, List.max?_eq_some_iff'] at h

Result:
maxLit localMax : Nat
f : CNF Nat
clause : Clause Nat
hclause1 : clause ∈ f
hclause2 : clause.maxLiteral = some localMax
h : (∃ a, a ∈ f ∧ a.maxLiteral = some maxLit) ∧ ∀ (b : Nat) (x : Clause Nat), x ∈ f → x.maxLiteral = some b → b ≤ maxLit
⊢ localMax ≤ maxLit

Proof state:
case intro
maxLit localMax : Nat
f : CNF Nat
clause : Clause Nat
hclause1 : clause ∈ f
hclause2 : clause.maxLiteral = some localMax
left✝ : ∃ a, a ∈ f ∧ a.maxLiteral = some maxLit
hclause3 : ∀ (b : Nat) (x : Clause Nat), x ∈ f → x.maxLiteral = some b → b ≤ maxLit
⊢ localMax ≤ maxLit

Tactic:
apply hclause3 localMax clause hclause1 hclause2

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Relabel.lean
theorem relabel_const {decls : Array (Decl α)} {r : α → β} {hidx : idx < decls.size}
    (h : relabel r decls[idx] = .const b) :
    decls[idx] = (.const b)

Proof state:
α β : Type
idx : Nat
b : Bool
decls : Array (Decl α)
r : α → β
hidx : idx < decls.size
h :
  (match decls[idx] with
    | const b => const b
    | atom a => atom (r a)
    | gate lhs rhs linv rinv => gate lhs rhs linv rinv) =
    const b
⊢ decls[idx] = const b

Tactic:
split at h <;> simp_all

Result:
no goals

Proof state:
α β : Type
idx : Nat
b : Bool
decls : Array (Decl α)
r : α → β
hidx : idx < decls.size
h : relabel r decls[idx] = const b
⊢ decls[idx] = const b

Tactic:
unfold relabel at h

Result:
α β : Type
idx : Nat
b : Bool
decls : Array (Decl α)
r : α → β
hidx : idx < decls.size
h :
  (match decls[idx] with
    | const b => const b
    | atom a => atom (r a)
    | gate lhs rhs linv rinv => gate lhs rhs linv rinv) =
    const b
⊢ decls[idx] = const b
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
theorem carrier.asIdeal.homogeneous : (carrier.asIdeal f_deg hm q).IsHomogeneous 𝒜 :=
  fun i a ha j =>
  (em (i = j)).elim (fun h => h ▸ by simpa only [proj_apply, decompose_coe, of_eq_same] using ha _)
    fun h => by
    simpa only [proj_apply, decompose_of_mem_ne 𝒜 (Submodule.coe_mem (decompose 𝒜 a i)) h,
      zero_pow hm.ne', map_zero] using carrier.zero_mem f_deg hm q j

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
i : ℕ
a : A
ha : a ∈ asIdeal f_deg hm q
j : ℕ
h : i = j
⊢ HomogeneousLocalization.mk
      { deg := m * i, num := ⟨(proj 𝒜 i) ↑(((decompose 𝒜) a) i) ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } ∈
    q.asIdeal

Tactic:
simpa only [proj_apply, decompose_coe, of_eq_same] using ha _

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
i : ℕ
a : A
ha : a ∈ asIdeal f_deg hm q
j : ℕ
h : ¬i = j
⊢ HomogeneousLocalization.mk
      { deg := m * j, num := ⟨(proj 𝒜 j) ↑(((decompose 𝒜) a) i) ^ m, ⋯⟩, den := ⟨f ^ j, ⋯⟩, den_mem := ⋯ } ∈
    q.asIdeal

Tactic:
simpa only [proj_apply, decompose_of_mem_ne 𝒜 (Submodule.coe_mem (decompose 𝒜 a i)) h,
  zero_pow hm.ne', map_zero] using carrier.zero_mem f_deg hm q j

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
theorem Commute.geom_sum₂_comm {α : Type u} [Semiring α] {x y : α} (n : ℕ)
    (h : Commute x y) :
    ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = ∑ i ∈ range n, y ^ i * x ^ (n - 1 - i)

Proof state:
case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n✝ : ℕ
⊢ ∑ r ∈ range (n✝ + 1), x ^ (n✝ - r) * y ^ (n✝ - (n✝ - r)) = ∑ x_1 ∈ range (n✝ + 1), y ^ x_1 * x ^ (n✝ - x_1)

Tactic:
refine Finset.sum_congr rfl fun i hi => ?_

Result:
case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n✝ i : ℕ
hi : i ∈ range (n✝ + 1)
⊢ x ^ (n✝ - i) * y ^ (n✝ - (n✝ - i)) = y ^ i * x ^ (n✝ - i)

Proof state:
case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n✝ : ℕ
⊢ ∑ i ∈ range (n✝ + 1), x ^ i * y ^ (n✝ + 1 - 1 - i) = ∑ i ∈ range (n✝ + 1), y ^ i * x ^ (n✝ + 1 - 1 - i)

Tactic:
simp only [Nat.succ_eq_add_one, Nat.add_sub_cancel]

Result:
case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n✝ : ℕ
⊢ ∑ x_1 ∈ range (n✝ + 1), x ^ x_1 * y ^ (n✝ - x_1) = ∑ x_1 ∈ range (n✝ + 1), y ^ x_1 * x ^ (n✝ - x_1)

Proof state:
α : Type u
inst✝ : Semiring α
x y : α
n : ℕ
h : Commute x y
⊢ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = ∑ i ∈ range n, y ^ i * x ^ (n - 1 - i)

Tactic:
cases n

Result:
case zero
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
⊢ ∑ i ∈ range 0, x ^ i * y ^ (0 - 1 - i) = ∑ i ∈ range 0, y ^ i * x ^ (0 - 1 - i)

case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n✝ : ℕ
⊢ ∑ i ∈ range (n✝ + 1), x ^ i * y ^ (n✝ + 1 - 1 - i) = ∑ i ∈ range (n✝ + 1), y ^ i * x ^ (n✝ + 1 - 1 - i)

Proof state:
case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n✝ : ℕ
⊢ ∑ x_1 ∈ range (n✝ + 1), x ^ x_1 * y ^ (n✝ - x_1) = ∑ x_1 ∈ range (n✝ + 1), y ^ x_1 * x ^ (n✝ - x_1)

Tactic:
rw [← Finset.sum_flip]

Result:
case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n✝ : ℕ
⊢ ∑ r ∈ range (n✝ + 1), x ^ (n✝ - r) * y ^ (n✝ - (n✝ - r)) = ∑ x_1 ∈ range (n✝ + 1), y ^ x_1 * x ^ (n✝ - x_1)

Proof state:
case zero
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
⊢ ∑ i ∈ range 0, x ^ i * y ^ (0 - 1 - i) = ∑ i ∈ range 0, y ^ i * x ^ (0 - 1 - i)

Tactic:
simp

Result:
no goals

Proof state:
case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n✝ i : ℕ
hi : i ∈ range (n✝ + 1)
⊢ x ^ (n✝ - i) * y ^ (n✝ - (n✝ - i)) = y ^ i * x ^ (n✝ - i)

Tactic:
simpa [Nat.sub_sub_self (Nat.succ_le_succ_iff.mp (Finset.mem_range.mp hi))] using h.pow_pow _ _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/OfFn.lean
theorem mem_ofFn {n} (f : Fin n → α) (a : α) : a ∈ ofFn f ↔ ∃ i, f i = a

Proof state:
case mp.intro.intro
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
h : i < (ofFn f).length
w : (ofFn f)[i] ∈ ofFn f
⊢ ∃ i_1, f i_1 = (ofFn f)[i]

Tactic:
exact ⟨⟨i, by simpa using h⟩, by simp⟩

Result:
no goals

Proof state:
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
h : i < (ofFn f).length
w : (ofFn f)[i] ∈ ofFn f
⊢ i < n

Tactic:
simpa using h

Result:
no goals

Proof state:
case mp
α : Type u_1
n : Nat
f : Fin n → α
a : α
w : a ∈ ofFn f
⊢ ∃ i, f i = a

Tactic:
obtain ⟨i, h, rfl⟩ := getElem_of_mem w

Result:
case mp.intro.intro
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
h : i < (ofFn f).length
w : (ofFn f)[i] ∈ ofFn f
⊢ ∃ i_1, f i_1 = (ofFn f)[i]

Proof state:
case mp
α : Type u_1
n : Nat
f : Fin n → α
a : α
⊢ a ∈ ofFn f → ∃ i, f i = a

Tactic:
intro w

Result:
case mp
α : Type u_1
n : Nat
f : Fin n → α
a : α
w : a ∈ ofFn f
⊢ ∃ i, f i = a

Proof state:
case mpr
α : Type u_1
n : Nat
f : Fin n → α
a : α
⊢ (∃ i, f i = a) → a ∈ ofFn f

Tactic:
rintro ⟨i, rfl⟩

Result:
case mpr.intro
α : Type u_1
n : Nat
f : Fin n → α
i : Fin n
⊢ f i ∈ ofFn f

Proof state:
α : Type u_1
n : Nat
f : Fin n → α
i : Nat
h : i < (ofFn f).length
w : (ofFn f)[i] ∈ ofFn f
⊢ f ⟨i, ⋯⟩ = (ofFn f)[i]

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
f : Fin n → α
a : α
⊢ a ∈ ofFn f ↔ ∃ i, f i = a

Tactic:
constructor

Result:
case mp
α : Type u_1
n : Nat
f : Fin n → α
a : α
⊢ a ∈ ofFn f → ∃ i, f i = a

case mpr
α : Type u_1
n : Nat
f : Fin n → α
a : α
⊢ (∃ i, f i = a) → a ∈ ofFn f

Proof state:
case mpr.intro
α : Type u_1
n : Nat
f : Fin n → α
i : Fin n
⊢ f i ∈ ofFn f

Tactic:
apply mem_of_getElem (i := i) <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx?_eq_none_of_findIdx?_eq_none {xs : List α} {p q : α → Bool} (w : ∀ x ∈ xs, p x → q x) :
    xs.findIdx? q = none → xs.findIdx? p = none

Proof state:
α : Type u_1
xs : List α
p q : α → Bool
w : ∀ (x : α), x ∈ xs → p x = true → q x = true
h : ∀ (x : α), x ∈ xs → q x = false
x : α
m : x ∈ xs
⊢ p x = false

Tactic:
cases z : p x

Result:
case false
α : Type u_1
xs : List α
p q : α → Bool
w : ∀ (x : α), x ∈ xs → p x = true → q x = true
h : ∀ (x : α), x ∈ xs → q x = false
x : α
m : x ∈ xs
z : p x = false
⊢ false = false

case true
α : Type u_1
xs : List α
p q : α → Bool
w : ∀ (x : α), x ∈ xs → p x = true → q x = true
h : ∀ (x : α), x ∈ xs → q x = false
x : α
m : x ∈ xs
z : p x = true
⊢ true = false

Proof state:
α : Type u_1
xs : List α
p q : α → Bool
w : ∀ (x : α), x ∈ xs → p x = true → q x = true
⊢ findIdx? q xs = none → findIdx? p xs = none

Tactic:
simp only [findIdx?_eq_none_iff]

Result:
α : Type u_1
xs : List α
p q : α → Bool
w : ∀ (x : α), x ∈ xs → p x = true → q x = true
⊢ (∀ (x : α), x ∈ xs → q x = false) → ∀ (x : α), x ∈ xs → p x = false

Proof state:
case true
α : Type u_1
xs : List α
p q : α → Bool
w : ∀ (x : α), x ∈ xs → p x = true → q x = true
h : ∀ (x : α), x ∈ xs → q x = false
x : α
m : x ∈ xs
z : p x = true
⊢ true = false

Tactic:
exfalso

Result:
case true
α : Type u_1
xs : List α
p q : α → Bool
w : ∀ (x : α), x ∈ xs → p x = true → q x = true
h : ∀ (x : α), x ∈ xs → q x = false
x : α
m : x ∈ xs
z : p x = true
⊢ False

Proof state:
case false
α : Type u_1
xs : List α
p q : α → Bool
w : ∀ (x : α), x ∈ xs → p x = true → q x = true
h : ∀ (x : α), x ∈ xs → q x = false
x : α
m : x ∈ xs
z : p x = false
⊢ false = false

Tactic:
rfl

Result:
no goals

Proof state:
case true
α : Type u_1
xs : List α
p q : α → Bool
x : α
m : x ∈ xs
z : p x = true
w : q x = true
h : q x = false
⊢ False

Tactic:
simp_all

Result:
no goals

Proof state:
case true
α : Type u_1
xs : List α
p q : α → Bool
h : ∀ (x : α), x ∈ xs → q x = false
x : α
m : x ∈ xs
z : p x = true
w : q x = true
⊢ False

Tactic:
specialize h x m

Result:
case true
α : Type u_1
xs : List α
p q : α → Bool
x : α
m : x ∈ xs
z : p x = true
w : q x = true
h : q x = false
⊢ False

Proof state:
α : Type u_1
xs : List α
p q : α → Bool
w : ∀ (x : α), x ∈ xs → p x = true → q x = true
⊢ (∀ (x : α), x ∈ xs → q x = false) → ∀ (x : α), x ∈ xs → p x = false

Tactic:
intro h x m

Result:
α : Type u_1
xs : List α
p q : α → Bool
w : ∀ (x : α), x ∈ xs → p x = true → q x = true
h : ∀ (x : α), x ∈ xs → q x = false
x : α
m : x ∈ xs
⊢ p x = false

Proof state:
case true
α : Type u_1
xs : List α
p q : α → Bool
w : ∀ (x : α), x ∈ xs → p x = true → q x = true
h : ∀ (x : α), x ∈ xs → q x = false
x : α
m : x ∈ xs
z : p x = true
⊢ False

Tactic:
specialize w x m z

Result:
case true
α : Type u_1
xs : List α
p q : α → Bool
h : ∀ (x : α), x ∈ xs → q x = false
x : α
m : x ∈ xs
z : p x = true
w : q x = true
⊢ False
-- Mathlib/Order/Disjoint.lean
theorem Disjoint.left_le_of_le_sup_left (h : a ≤ c ⊔ b) (hd : Disjoint a c) : a ≤ b :=
  hd.left_le_of_le_sup_right <| by rwa [sup_comm]

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b c : α
h : a ≤ c ⊔ b
hd : Disjoint a c
⊢ a ≤ b ⊔ c

Tactic:
rwa [sup_comm]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Perm.lean
theorem subperm_append_diff_self_of_count_le {l₁ l₂ : List α}
    (h : ∀ x ∈ l₁, count x l₁ ≤ count x l₂) : l₁ ++ l₂.diff l₁ ~ l₂

Proof state:
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
IH : ∀ {l₂ : List α}, (∀ (x : α), x ∈ tl → count x tl ≤ count x l₂) → tl ++ l₂.diff tl ~ l₂
l₂ : List α
h : ∀ (x : α), x ∈ hd :: tl → count x (hd :: tl) ≤ count x l₂
⊢ hd ∈ l₂

Tactic:
rw [← count_pos_iff]

Result:
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
IH : ∀ {l₂ : List α}, (∀ (x : α), x ∈ tl → count x tl ≤ count x l₂) → tl ++ l₂.diff tl ~ l₂
l₂ : List α
h : ∀ (x : α), x ∈ hd :: tl → count x (hd :: tl) ≤ count x l₂
⊢ 0 < count hd l₂

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
h : ∀ (x : α), x ∈ [] → count x [] ≤ count x l₂
⊢ [] ++ l₂.diff [] ~ l₂

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem isNoetherian_zero : IsNoetherian R₁ (0 : FractionalIdeal R₁⁰ K) :=
  isNoetherian_submodule.mpr fun I (hI : I ≤ (0 : FractionalIdeal R₁⁰ K)) => by
    rw [coe_zero, le_bot_iff] at hI
    rw [hI]
    exact fg_bot

Proof state:
R₁ : Type u_3
inst✝² : CommRing R₁
K : Type u_4
inst✝¹ : Field K
inst✝ : Algebra R₁ K
I : Submodule R₁ K
hI : I = ⊥
⊢ ⊥.FG

Tactic:
exact fg_bot

Result:
no goals

Proof state:
R₁ : Type u_3
inst✝² : CommRing R₁
K : Type u_4
inst✝¹ : Field K
inst✝ : Algebra R₁ K
I : Submodule R₁ K
hI : I ≤ ↑0
⊢ I.FG

Tactic:
rw [coe_zero, le_bot_iff] at hI

Result:
R₁ : Type u_3
inst✝² : CommRing R₁
K : Type u_4
inst✝¹ : Field K
inst✝ : Algebra R₁ K
I : Submodule R₁ K
hI : I = ⊥
⊢ I.FG

Proof state:
R₁ : Type u_3
inst✝² : CommRing R₁
K : Type u_4
inst✝¹ : Field K
inst✝ : Algebra R₁ K
I : Submodule R₁ K
hI : I = ⊥
⊢ I.FG

Tactic:
rw [hI]

Result:
R₁ : Type u_3
inst✝² : CommRing R₁
K : Type u_4
inst✝¹ : Field K
inst✝ : Algebra R₁ K
I : Submodule R₁ K
hI : I = ⊥
⊢ ⊥.FG
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
lemma absolutelyContinuous_withDensity_rnDeriv [HaveLebesgueDecomposition ν μ] (hμν : μ ≪ ν) :
    μ ≪ μ.withDensity (ν.rnDeriv μ)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
x✝ : MeasurableSet s
hνs : (μ.withDensity (ν.rnDeriv μ)) s = 0
⊢ μ s = 0

Tactic:
obtain ⟨t, _, ht1, ht2⟩ := mutuallySingular_singularPart ν μ

Result:
case intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
x✝ : MeasurableSet s
hνs : (μ.withDensity (ν.rnDeriv μ)) s = 0
t : Set α
left✝ : MeasurableSet t
ht1 : (ν.singularPart μ) t = 0
ht2 : μ tᶜ = 0
⊢ μ s = 0

Proof state:
case intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
x✝ : MeasurableSet s
hνs : (μ.withDensity (ν.rnDeriv μ)) s = 0
t : Set α
left✝ : MeasurableSet t
ht1 : (ν.singularPart μ) t = 0
ht2 : μ tᶜ = 0
⊢ μ (s ∩ t) + μ (s ∩ tᶜ) ≤ 0

Tactic:
simp only [nonpos_iff_eq_zero, add_eq_zero]

Result:
case intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
x✝ : MeasurableSet s
hνs : (μ.withDensity (ν.rnDeriv μ)) s = 0
t : Set α
left✝ : MeasurableSet t
ht1 : (ν.singularPart μ) t = 0
ht2 : μ tᶜ = 0
⊢ μ (s ∩ t) = 0 ∧ μ (s ∩ tᶜ) = 0

Proof state:
case intro.intro.intro.left
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
x✝ : MeasurableSet s
hνs : (μ.withDensity (ν.rnDeriv μ)) s = 0
t : Set α
left✝ : MeasurableSet t
ht1 : (ν.singularPart μ) t = 0
ht2 : μ tᶜ = 0
⊢ (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) (s ∩ t) = 0

Tactic:
simp only [coe_add, Pi.add_apply, add_eq_zero]

Result:
case intro.intro.intro.left
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
x✝ : MeasurableSet s
hνs : (μ.withDensity (ν.rnDeriv μ)) s = 0
t : Set α
left✝ : MeasurableSet t
ht1 : (ν.singularPart μ) t = 0
ht2 : μ tᶜ = 0
⊢ (ν.singularPart μ) (s ∩ t) = 0 ∧ (μ.withDensity (ν.rnDeriv μ)) (s ∩ t) = 0
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
@[reassoc (attr := simp)]
lemma whiskerRight_μ_δ (X Y : C) (T : D) : μ F X Y ▷ T ≫ δ F X Y ▷ T = 𝟙 _

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
X Y : C
T : D
⊢ μ F X Y ▷ T ≫ δ F X Y ▷ T = 𝟙 ((F.obj X ⊗ F.obj Y) ⊗ T)

Tactic:
rw [← MonoidalCategory.comp_whiskerRight, μ_δ, id_whiskerRight]

Result:
no goals
-- Mathlib/Topology/Instances/ZMultiples.lean
theorem tendsto_zmultiplesHom_cofinite {a : ℝ} (ha : a ≠ 0) :
    Tendsto (zmultiplesHom ℝ a) cofinite (cocompact ℝ)

Proof state:
a : ℝ
ha : a ≠ 0
⊢ DiscreteTopology ↥((zmultiplesHom ℝ) a).range

Tactic:
rw [AddSubgroup.range_zmultiplesHom]

Result:
a : ℝ
ha : a ≠ 0
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples a)

Proof state:
a : ℝ
ha : a ≠ 0
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples a)

Tactic:
infer_instance

Result:
no goals

Proof state:
a : ℝ
ha : a ≠ 0
⊢ Tendsto (⇑((zmultiplesHom ℝ) a)) Filter.cofinite (cocompact ℝ)

Tactic:
apply (zmultiplesHom ℝ a).tendsto_coe_cofinite_of_discrete <| smul_left_injective ℤ ha

Result:
a : ℝ
ha : a ≠ 0
⊢ DiscreteTopology ↥((zmultiplesHom ℝ) a).range
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem max_assoc : ∀ (a b c : Nat), max (max a b) c = max a (max b c)
  | 0, _, _ => by rw [Nat.zero_max, Nat.zero_max]
  | _, 0, _ => by rw [Nat.zero_max, Nat.max_zero]
  | _, _, 0 => by rw [Nat.max_zero, Nat.max_zero]
  | _+1, _+1, _+1 => by simp only [Nat.succ_max_succ]; exact congrArg succ <| Nat.max_assoc ..

Proof state:
x✝¹ x✝ : Nat
⊢ max (max x✝¹ 0) x✝ = max x✝¹ (max 0 x✝)

Tactic:
rw [Nat.zero_max, Nat.max_zero]

Result:
no goals

Proof state:
x✝¹ x✝ : Nat
⊢ max (max x✝¹ x✝) 0 = max x✝¹ (max x✝ 0)

Tactic:
rw [Nat.max_zero, Nat.max_zero]

Result:
no goals

Proof state:
n✝² n✝¹ n✝ : Nat
⊢ (max (max n✝² n✝¹) n✝).succ = (max n✝² (max n✝¹ n✝)).succ

Tactic:
exact congrArg succ <| Nat.max_assoc ..

Result:
no goals

Proof state:
x✝¹ x✝ : Nat
⊢ max (max 0 x✝¹) x✝ = max 0 (max x✝¹ x✝)

Tactic:
rw [Nat.zero_max, Nat.zero_max]

Result:
no goals

Proof state:
n✝² n✝¹ n✝ : Nat
⊢ max (max (n✝² + 1) (n✝¹ + 1)) (n✝ + 1) = max (n✝² + 1) (max (n✝¹ + 1) (n✝ + 1))

Tactic:
simp only [Nat.succ_max_succ]

Result:
n✝² n✝¹ n✝ : Nat
⊢ (max (max n✝² n✝¹) n✝).succ = (max n✝² (max n✝¹ n✝)).succ
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma cpow_inv_two_re (x : ℂ) : (x ^ (2⁻¹ : ℂ)).re = sqrt ((‖x‖ + x.re) / 2)

Proof state:
case hx
x : ℂ
⊢ 0 ≤ ‖x‖

case hl
x : ℂ
⊢ -π ≤ x.arg

case hr
x : ℂ
⊢ x.arg ≤ π

Tactic:
exacts [norm_nonneg _, (neg_pi_lt_arg _).le, arg_le_pi _]

Result:
no goals

Proof state:
x : ℂ
⊢ (x ^ 2⁻¹).re = √((‖x‖ + x.re) / 2)

Tactic:
rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_re, ← div_eq_mul_inv, ← one_div,
  ← Real.sqrt_eq_rpow, cos_half, ← sqrt_mul, ← mul_div_assoc, mul_add, mul_one, norm_mul_cos_arg]

Result:
case hx
x : ℂ
⊢ 0 ≤ ‖x‖

case hl
x : ℂ
⊢ -π ≤ x.arg

case hr
x : ℂ
⊢ x.arg ≤ π
-- Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean
lemma iff_flat_and_proper_ideal :
    FaithfullyFlat R M ↔
    (Flat R M ∧ ∀ (I : Ideal R), I ≠ ⊤ → I • (⊤ : Submodule R M) ≠ ⊤)

Proof state:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : Flat R M ∧ ∀ ⦃m : Ideal R⦄, m.IsMaximal → m • ⊤ ≠ ⊤
flat : Flat R M
h : ∀ ⦃m : Ideal R⦄, m.IsMaximal → m • ⊤ ≠ ⊤
I : Ideal R
hI : I ≠ ⊤
r : I • ⊤ = ⊤
m : Ideal R
hm : m.IsMaximal
le : I ≤ m
⊢ ⊤ ≤ I • ⊤

Tactic:
simp [r]

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (Flat R M ∧ ∀ ⦃m : Ideal R⦄, m.IsMaximal → m • ⊤ ≠ ⊤) ↔ Flat R M ∧ ∀ (I : Ideal R), I ≠ ⊤ → I • ⊤ ≠ ⊤

Tactic:
refine ⟨fun ⟨flat, h⟩ => ⟨flat, fun I hI r => ?_⟩, fun h => ⟨h.1, fun m hm => h.2 _ hm.ne_top⟩⟩

Result:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : Flat R M ∧ ∀ ⦃m : Ideal R⦄, m.IsMaximal → m • ⊤ ≠ ⊤
flat : Flat R M
h : ∀ ⦃m : Ideal R⦄, m.IsMaximal → m • ⊤ ≠ ⊤
I : Ideal R
hI : I ≠ ⊤
r : I • ⊤ = ⊤
⊢ False

Proof state:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ FaithfullyFlat R M ↔ Flat R M ∧ ∀ (I : Ideal R), I ≠ ⊤ → I • ⊤ ≠ ⊤

Tactic:
rw [faithfullyFlat_iff]

Result:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (Flat R M ∧ ∀ ⦃m : Ideal R⦄, m.IsMaximal → m • ⊤ ≠ ⊤) ↔ Flat R M ∧ ∀ (I : Ideal R), I ≠ ⊤ → I • ⊤ ≠ ⊤

Proof state:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : Flat R M ∧ ∀ ⦃m : Ideal R⦄, m.IsMaximal → m • ⊤ ≠ ⊤
flat : Flat R M
h : ∀ ⦃m : Ideal R⦄, m.IsMaximal → m • ⊤ ≠ ⊤
I : Ideal R
hI : I ≠ ⊤
r : I • ⊤ = ⊤
⊢ False

Tactic:
obtain ⟨m, hm, le⟩ := I.exists_le_maximal hI

Result:
case intro.intro
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : Flat R M ∧ ∀ ⦃m : Ideal R⦄, m.IsMaximal → m • ⊤ ≠ ⊤
flat : Flat R M
h : ∀ ⦃m : Ideal R⦄, m.IsMaximal → m • ⊤ ≠ ⊤
I : Ideal R
hI : I ≠ ⊤
r : I • ⊤ = ⊤
m : Ideal R
hm : m.IsMaximal
le : I ≤ m
⊢ False

Proof state:
case intro.intro
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : Flat R M ∧ ∀ ⦃m : Ideal R⦄, m.IsMaximal → m • ⊤ ≠ ⊤
flat : Flat R M
h : ∀ ⦃m : Ideal R⦄, m.IsMaximal → m • ⊤ ≠ ⊤
I : Ideal R
hI : I ≠ ⊤
r : I • ⊤ = ⊤
m : Ideal R
hm : m.IsMaximal
le : I ≤ m
⊢ False

Tactic:
exact h hm <| eq_top_iff.2 <| show ⊤ ≤ m • ⊤ from r ▸ Submodule.smul_mono le (by simp [r])

Result:
no goals
-- Mathlib/Probability/Independence/Basic.lean
lemma iIndepSet_iff (s : ι → Set Ω) (μ : Measure Ω) :
    iIndepSet s μ ↔ ∀ (s' : Finset ι) {f : ι → Set Ω}
      (_H : ∀ i, i ∈ s' → MeasurableSet[generateFrom {s i}] (f i)),
      μ (⋂ i ∈ s', f i) = ∏ i ∈ s', μ (f i)

Proof state:
Ω : Type u_1
ι : Type u_2
x✝ : MeasurableSpace Ω
s : ι → Set Ω
μ : Measure Ω
⊢ iIndepSet s μ ↔
    ∀ (s' : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s', MeasurableSet (f i)) → μ (⋂ i ∈ s', f i) = ∏ i ∈ s', μ (f i)

Tactic:
simp only [iIndepSet_iff_iIndep, iIndep_iff]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Defs.lean
theorem top_mem_insertTop {s : Finset α} : ⊤ ∈ insertTop s

Proof state:
α : Type u_1
s : Finset α
⊢ ⊤ ∈ insertTop s

Tactic:
simp [insertTop]

Result:
no goals