harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/Turan.lean
lemma not_adj_iff_part_eq [DecidableEq V] :
    ¬G.Adj s t ↔ h.finpartition.part s = h.finpartition.part t

Proof state:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s t : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
⊢ t ∈ fp.part s ↔ fp.part s = fp.part t

Tactic:
rw [fp.mem_part_iff_part_eq_part (mem_univ t) (mem_univ s), eq_comm]

Result:
no goals

Proof state:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s t : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
⊢ ¬G.Adj s t ↔ h.finpartition.part s = h.finpartition.part t

Tactic:
change h.setoid.r s t ↔ _

Result:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s t : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
⊢ h.setoid s t ↔ h.finpartition.part s = h.finpartition.part t

Proof state:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s t : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
⊢ t ∈ (Finpartition.ofSetoid h.setoid).part s ↔ h.finpartition.part s = h.finpartition.part t

Tactic:
let fp := h.finpartition

Result:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s t : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
⊢ t ∈ (Finpartition.ofSetoid h.setoid).part s ↔ h.finpartition.part s = h.finpartition.part t

Proof state:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s t : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
⊢ h.setoid s t ↔ h.finpartition.part s = h.finpartition.part t

Tactic:
rw [← Finpartition.mem_part_ofSetoid_iff_rel]

Result:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s t : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
⊢ t ∈ (Finpartition.ofSetoid h.setoid).part s ↔ h.finpartition.part s = h.finpartition.part t

Proof state:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s t : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
⊢ t ∈ (Finpartition.ofSetoid h.setoid).part s ↔ h.finpartition.part s = h.finpartition.part t

Tactic:
change t ∈ fp.part s ↔ fp.part s = fp.part t

Result:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s t : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
⊢ t ∈ fp.part s ↔ fp.part s = fp.part t
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem length_reverse (as : List α) : (as.reverse).length = as.length

Proof state:
case cons
α : Type u_1
a : α
as : List α
ih : as.reverse.length = as.length
⊢ (a :: as).reverse.length = (a :: as).length

Tactic:
simp [ih]

Result:
no goals

Proof state:
case nil
α : Type u_1
⊢ [].reverse.length = [].length

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
as : List α
⊢ as.reverse.length = as.length

Tactic:
induction as with
| nil => rfl
| cons a as ih => simp [ih]

Result:
no goals
-- Mathlib/Topology/Separation/Regular.lean
theorem IsCompact.exists_isOpen_closure_subset {K U : Set X} (hK : IsCompact K) (hU : U ∈ 𝓝ˢ K) :
    ∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U

Proof state:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
K U : Set X
hK : IsCompact K
hU : U ∈ 𝓝ˢ K
hd : Disjoint (𝓝ˢ K) (𝓝ˢ Uᶜ)
V : Set X
hVo : IsOpen V
hKV : K ⊆ V
W : Set X
hVW : Disjoint V W
hW : IsOpen W
hUW : Uᶜ ⊆ W
⊢ closure V ⊆ Wᶜ

Tactic:
exact closure_minimal hVW.subset_compl_right hW.isClosed_compl

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
K U : Set X
hK : IsCompact K
hU : U ∈ 𝓝ˢ K
⊢ ∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U

Tactic:
have hd : Disjoint (𝓝ˢ K) (𝓝ˢ Uᶜ) := by
  simpa [hK.disjoint_nhdsSet_left, disjoint_nhds_nhdsSet,
    ← subset_interior_iff_mem_nhdsSet] using hU

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
K U : Set X
hK : IsCompact K
hU : U ∈ 𝓝ˢ K
hd : Disjoint (𝓝ˢ K) (𝓝ˢ Uᶜ)
⊢ ∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U

Proof state:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
K U : Set X
hK : IsCompact K
hU : U ∈ 𝓝ˢ K
hd : Disjoint (𝓝ˢ K) (𝓝ˢ Uᶜ)
V : Set X
hVo : IsOpen V
hKV : K ⊆ V
W : Set X
hVW : Disjoint V W
hW : IsOpen W
hUW : Uᶜ ⊆ W
⊢ ∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U

Tactic:
refine ⟨V, hVo, hKV, Subset.trans ?_ (compl_subset_comm.1 hUW)⟩

Result:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
K U : Set X
hK : IsCompact K
hU : U ∈ 𝓝ˢ K
hd : Disjoint (𝓝ˢ K) (𝓝ˢ Uᶜ)
V : Set X
hVo : IsOpen V
hKV : K ⊆ V
W : Set X
hVW : Disjoint V W
hW : IsOpen W
hUW : Uᶜ ⊆ W
⊢ closure V ⊆ Wᶜ

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
K U : Set X
hK : IsCompact K
hU : U ∈ 𝓝ˢ K
hd : Disjoint (𝓝ˢ K) (𝓝ˢ Uᶜ)
⊢ ∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U

Tactic:
rcases ((hasBasis_nhdsSet _).disjoint_iff (hasBasis_nhdsSet _)).1 hd
  with ⟨V, ⟨hVo, hKV⟩, W, ⟨hW, hUW⟩, hVW⟩

Result:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
K U : Set X
hK : IsCompact K
hU : U ∈ 𝓝ˢ K
hd : Disjoint (𝓝ˢ K) (𝓝ˢ Uᶜ)
V : Set X
hVo : IsOpen V
hKV : K ⊆ V
W : Set X
hVW : Disjoint V W
hW : IsOpen W
hUW : Uᶜ ⊆ W
⊢ ∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
K U : Set X
hK : IsCompact K
hU : U ∈ 𝓝ˢ K
⊢ Disjoint (𝓝ˢ K) (𝓝ˢ Uᶜ)

Tactic:
simpa [hK.disjoint_nhdsSet_left, disjoint_nhds_nhdsSet,
  ← subset_interior_iff_mem_nhdsSet] using hU

Result:
no goals
-- Mathlib/Data/Matrix/ConjTranspose.lean
theorem diagonal_conjTranspose [AddMonoid α] [StarAddMonoid α] (v : n → α) :
    (diagonal v)ᴴ = diagonal (star v)

Proof state:
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
v : n → α
⊢ (diagonal v)ᴴ = diagonal (star v)

Tactic:
rw [conjTranspose, diagonal_transpose, diagonal_map (star_zero _)]

Result:
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
v : n → α
⊢ (diagonal fun m => star (v m)) = diagonal (star v)

Proof state:
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
v : n → α
⊢ (diagonal fun m => star (v m)) = diagonal (star v)

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem _root_.IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal {α : Type*}
    [MeasurableSpace α] (μ : Measure α) [μ_fin : IsFiniteMeasure μ] {f : α → ℝ≥0∞}
    (f_bdd : ∃ c : ℝ≥0, ∀ x, f x ≤ c) : ∫⁻ x, f x ∂μ < ∞

Proof state:
α : Type u_5
inst✝ : MeasurableSpace α
μ : Measure α
μ_fin : IsFiniteMeasure μ
f : α → ℝ≥0∞
f_bdd : ∃ c, ∀ (x : α), f x ≤ ↑c
⊢ ∫⁻ (x : α) in univ, f x ∂μ < ⊤

Tactic:
refine setLIntegral_lt_top_of_le_nnreal (measure_ne_top _ _) ?_

Result:
α : Type u_5
inst✝ : MeasurableSpace α
μ : Measure α
μ_fin : IsFiniteMeasure μ
f : α → ℝ≥0∞
f_bdd : ∃ c, ∀ (x : α), f x ≤ ↑c
⊢ ∃ y, ∀ x ∈ univ, f x ≤ ↑y

Proof state:
α : Type u_5
inst✝ : MeasurableSpace α
μ : Measure α
μ_fin : IsFiniteMeasure μ
f : α → ℝ≥0∞
f_bdd : ∃ c, ∀ (x : α), f x ≤ ↑c
⊢ ∃ y, ∀ x ∈ univ, f x ≤ ↑y

Tactic:
simpa using f_bdd

Result:
no goals

Proof state:
α : Type u_5
inst✝ : MeasurableSpace α
μ : Measure α
μ_fin : IsFiniteMeasure μ
f : α → ℝ≥0∞
f_bdd : ∃ c, ∀ (x : α), f x ≤ ↑c
⊢ ∫⁻ (x : α), f x ∂μ < ⊤

Tactic:
rw [← μ.restrict_univ]

Result:
α : Type u_5
inst✝ : MeasurableSpace α
μ : Measure α
μ_fin : IsFiniteMeasure μ
f : α → ℝ≥0∞
f_bdd : ∃ c, ∀ (x : α), f x ≤ ↑c
⊢ ∫⁻ (x : α) in univ, f x ∂μ < ⊤
-- Mathlib/Topology/Homotopy/Basic.lean
theorem symm_trans {f₀ f₁ f₂ : C(X, Y)} (F : Homotopy f₀ f₁) (G : Homotopy f₁ f₂) :
    (F.trans G).symm = G.symm.trans F.symm

Proof state:
case h.mk
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : ↑I
snd✝ : X
⊢ (if h : 1 - ↑t ≤ 1 / 2 then F (⟨2 * (1 - ↑t), ⋯⟩, snd✝) else G (⟨2 * (1 - ↑t) - 1, ⋯⟩, snd✝)) =
    if h : ↑t ≤ 1 / 2 then G (σ ⟨2 * ↑t, ⋯⟩, snd✝) else F (σ ⟨2 * ↑t - 1, ⋯⟩, snd✝)

Tactic:
split_ifs with h₁ h₂ h₂

Result:
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : ↑I
snd✝ : X
h₁ : 1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ F (⟨2 * (1 - ↑t), ⋯⟩, snd✝) = G (σ ⟨2 * ↑t, ⋯⟩, snd✝)

case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : ↑I
snd✝ : X
h₁ : 1 - ↑t ≤ 1 / 2
h₂ : ¬↑t ≤ 1 / 2
⊢ F (⟨2 * (1 - ↑t), ⋯⟩, snd✝) = F (σ ⟨2 * ↑t - 1, ⋯⟩, snd✝)

case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : ↑I
snd✝ : X
h₁ : ¬1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ G (⟨2 * (1 - ↑t) - 1, ⋯⟩, snd✝) = G (σ ⟨2 * ↑t, ⋯⟩, snd✝)

case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : ↑I
snd✝ : X
h₁ : ¬1 - ↑t ≤ 1 / 2
h₂ : ¬↑t ≤ 1 / 2
⊢ G (⟨2 * (1 - ↑t) - 1, ⋯⟩, snd✝) = F (σ ⟨2 * ↑t - 1, ⋯⟩, snd✝)

Proof state:
case pos.h.e_6.h.e_fst
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : ↑I
snd✝ : X
h₁ : ¬1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ ⟨2 * (1 - ↑t) - 1, ⋯⟩ = σ ⟨2 * ↑t, ⋯⟩

Tactic:
apply Subtype.ext

Result:
case pos.h.e_6.h.e_fst.a
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : ↑I
snd✝ : X
h₁ : ¬1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ ↑⟨2 * (1 - ↑t) - 1, ⋯⟩ = ↑(σ ⟨2 * ↑t, ⋯⟩)

Proof state:
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : ↑I
snd✝ : X
h₁ : 1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
ht : ↑t = 1 / 2
⊢ F (⟨2 * (1 - ↑t), ⋯⟩, snd✝) = G (σ ⟨2 * ↑t, ⋯⟩, snd✝)

Tactic:
norm_num [ht]

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem sub_iInf : (a - ⨅ i, f i) = ⨆ i, a - f i

Proof state:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ a - ⨅ i, f i = ⨆ i, a - f i

Tactic:
refine eq_of_forall_ge_iff fun c => ?_

Result:
ι : Sort u_1
f : ι → ℝ≥0∞
a c : ℝ≥0∞
⊢ a - ⨅ i, f i ≤ c ↔ ⨆ i, a - f i ≤ c

Proof state:
ι : Sort u_1
f : ι → ℝ≥0∞
a c : ℝ≥0∞
⊢ a - ⨅ i, f i ≤ c ↔ ⨆ i, a - f i ≤ c

Tactic:
rw [tsub_le_iff_right, add_comm, iInf_add]

Result:
ι : Sort u_1
f : ι → ℝ≥0∞
a c : ℝ≥0∞
⊢ a ≤ ⨅ i, f i + c ↔ ⨆ i, a - f i ≤ c

Proof state:
ι : Sort u_1
f : ι → ℝ≥0∞
a c : ℝ≥0∞
⊢ a ≤ ⨅ i, f i + c ↔ ⨆ i, a - f i ≤ c

Tactic:
simp [tsub_le_iff_right, sub_eq_add_neg, add_comm]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem log_nat_eq_sum_factorization (n : ℕ) :
    log n = n.factorization.sum fun p t => t * log p

Proof state:
n : ℕ
⊢ log ↑n = n.factorization.sum fun p t => ↑t * log ↑p

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Result:
case inl

⊢ log ↑0 = (Nat.factorization 0).sum fun p t => ↑t * log ↑p

case inr
n : ℕ
hn : n ≠ 0
⊢ log ↑n = n.factorization.sum fun p t => ↑t * log ↑p

Proof state:
case inr.hg
n : ℕ
hn : n ≠ 0
⊢ ∀ (a : ℕ), ↑(a ^ n.factorization a) = 0 → n.factorization a = 0

Tactic:
intro p hp

Result:
case inr.hg
n : ℕ
hn : n ≠ 0
p : ℕ
hp : ↑(p ^ n.factorization p) = 0
⊢ n.factorization p = 0

Proof state:
case inr
n : ℕ
hn : n ≠ 0
⊢ log ↑n = n.factorization.sum fun p t => log ↑(p ^ t)

Tactic:
rw [← Finsupp.log_prod, ← Nat.cast_finsupp_prod, Nat.factorization_prod_pow_eq_self hn]

Result:
case inr.hg
n : ℕ
hn : n ≠ 0
⊢ ∀ (a : ℕ), ↑(a ^ n.factorization a) = 0 → n.factorization a = 0

Proof state:
case inr.hg
n : ℕ
hn : n ≠ 0
p : ℕ
hp : ↑(p ^ n.factorization p) = 0
⊢ n.factorization p = 0

Tactic:
rw [pow_eq_zero (Nat.cast_eq_zero.1 hp), Nat.factorization_zero_right]

Result:
no goals

Proof state:
case inl

⊢ log ↑0 = (Nat.factorization 0).sum fun p t => ↑t * log ↑p

Tactic:
simp

Result:
no goals

Proof state:
case inr
n : ℕ
hn : n ≠ 0
⊢ log ↑n = n.factorization.sum fun p t => ↑t * log ↑p

Tactic:
simp only [← log_pow, ← Nat.cast_pow]

Result:
case inr
n : ℕ
hn : n ≠ 0
⊢ log ↑n = n.factorization.sum fun p t => log ↑(p ^ t)
-- Mathlib/Probability/Independence/Basic.lean
theorem iIndepFun_iff_measure_inter_preimage_eq_mul {ι : Type*} {β : ι → Type*}
    {m : ∀ x, MeasurableSpace (β x)} {f : ∀ i, Ω → β i} :
    iIndepFun m f μ ↔
      ∀ (S : Finset ι) {sets : ∀ i : ι, Set (β i)} (_H : ∀ i, i ∈ S → MeasurableSet[m i] (sets i)),
        μ (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, μ (f i ⁻¹' sets i)

Proof state:
Ω : Type u_1
_mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_10
β : ι → Type u_11
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
⊢ iIndepFun m f μ ↔
    ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
      (∀ i ∈ S, MeasurableSet (sets i)) → μ (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, μ (f i ⁻¹' sets i)

Tactic:
simp only [iIndepFun, Kernel.iIndepFun_iff_measure_inter_preimage_eq_mul, ae_dirac_eq,
  Filter.eventually_pure, Kernel.const_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean
theorem denote_go_eq_divRec_q (aig : AIG α) (assign : α → Bool) (curr : Nat) (lhs rhs rbv qbv : BitVec w)
    (falseRef trueRef : AIG.Ref aig) (n d q r : AIG.RefVec aig w) (wn wr : Nat)
    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, n.get idx hidx, assign⟧ = lhs.getLsbD idx)
    (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, d.get idx hidx, assign⟧ = rhs.getLsbD idx)
    (hq : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, q.get idx hidx, assign⟧ = qbv.getLsbD idx)
    (hr : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, r.get idx hidx, assign⟧ = rbv.getLsbD idx)
    (hfalse : ⟦aig, falseRef, assign⟧ = false)
    (htrue : ⟦aig, trueRef, assign⟧ = true)
      :
    ∀ (idx : Nat) (hidx : idx < w),
      ⟦
        (go aig curr falseRef trueRef n d wn wr q r).aig,
        (go aig curr falseRef trueRef n d wn wr q r).q.get idx hidx,
        assign
      ⟧
        =
      (BitVec.divRec curr { n := lhs, d := rhs} { wn, wr, q := qbv, r := rbv }).q.getLsbD idx

Proof state:
case htrue.hstart
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
lhs rhs : BitVec w
curr : Nat
ih :
  ∀ (aig : AIG α) (rbv qbv : BitVec w) (falseRef trueRef : aig.Ref) (n d q r : aig.RefVec w) (wn wr : Nat),
    (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := n.get idx hidx }⟧ = lhs.getLsbD idx) →
      (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := d.get idx hidx }⟧ = rhs.getLsbD idx) →
        (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := q.get idx hidx }⟧ = qbv.getLsbD idx) →
          (∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = rbv.getLsbD idx) →
            ⟦assign, { aig := aig, ref := falseRef }⟧ = false →
              ⟦assign, { aig := aig, ref := trueRef }⟧ = true →
                ∀ (idx : Nat) (hidx : idx < w),
                  ⟦assign,
                      { aig := (go aig curr falseRef trueRef n d wn wr q r).aig,
                        ref := (go aig curr falseRef trueRef n d wn wr q r).q.get idx hidx }⟧ =
                    (BitVec.divRec curr { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).q.getLsbD idx
aig : AIG α
rbv qbv : BitVec w
falseRef trueRef : aig.Ref
n d q r : aig.RefVec w
wn wr : Nat
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := n.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := d.get idx hidx }⟧ = rhs.getLsbD idx
hq : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := q.get idx hidx }⟧ = qbv.getLsbD idx
hr : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = rbv.getLsbD idx
hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false
htrue : ⟦assign, { aig := aig, ref := trueRef }⟧ = true
idx : Nat
hidx : idx < w
hdiscr :
  ¬{ wn := wn, wr := wr, q := qbv, r := rbv }.r.shiftConcat
        (lhs.getLsbD ({ wn := wn, wr := wr, q := qbv, r := rbv }.wn - 1)) <
      rhs
⊢ (trueRef.cast ⋯).gate < aig.decls.size

Tactic:
simp [Ref.hgate]

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
lemma Indep.insert_isCircuit_of_forall (hI : M.Indep I) (heI : e ∉ I) (he : e ∈ M.closure I)
    (h : ∀ f ∈ I, e ∉ M.closure (I \ {f})) : M.IsCircuit (insert e I)

Proof state:
case inr
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
f : α
hfI : f ∈ I
⊢ M.Indep (insert e I \ {f})

Tactic:
rw [← insert_diff_singleton_comm (by rintro rfl; contradiction),
  (hI.diff _).insert_indep_iff_of_not_mem (by simp [heI])]

Result:
case inr
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
f : α
hfI : f ∈ I
⊢ e ∈ M.E \ M.closure (I \ {f})

Proof state:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
⊢ ∀ e_1 ∈ insert e I, M.Indep (insert e I \ {e_1})

Tactic:
rintro f (rfl | hfI)

Result:
case inl
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
f : α
heI : f ∉ I
he : f ∈ M.closure I
h : ∀ f_1 ∈ I, f ∉ M.closure (I \ {f_1})
⊢ M.Indep (insert f I \ {f})

case inr
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
f : α
hfI : f ∈ I
⊢ M.Indep (insert e I \ {f})

Proof state:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
f : α
hfI : f ∈ I
⊢ e ∉ I \ {f}

Tactic:
simp [heI]

Result:
no goals

Proof state:
case inr
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
f : α
hfI : f ∈ I
⊢ e ∈ M.E \ M.closure (I \ {f})

Tactic:
exact ⟨mem_ground_of_mem_closure he, h f hfI⟩

Result:
no goals

Proof state:
case inl
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
f : α
heI : f ∉ I
he : f ∈ M.closure I
h : ∀ f_1 ∈ I, f ∉ M.closure (I \ {f_1})
⊢ M.Indep (insert f I \ {f})

Tactic:
simpa [heI]

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
f : α
hfI : f ∈ I
⊢ e ≠ f

Tactic:
rintro rfl

Result:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
hfI : e ∈ I
⊢ False

Proof state:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
hfI : e ∈ I
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
⊢ M.IsCircuit (insert e I)

Tactic:
rw [isCircuit_iff_dep_forall_diff_singleton_indep, hI.insert_dep_iff, and_iff_right ⟨he, heI⟩]

Result:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
⊢ ∀ e_1 ∈ insert e I, M.Indep (insert e I \ {e_1})
-- Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean
lemma hf_modif_int :
    LocallyIntegrableOn P.f_modif (Ioi 0)

Proof state:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
this : LocallyIntegrableOn (fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) (Ioi 0) volume
x : ℝ
hx : x ∈ Ioi 0
⊢ IntegrableAtFilter ((Ioo 0 1).indicator fun x => P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) (𝓝[Ioi 0] x) volume

Tactic:
obtain ⟨s, hs, hs'⟩ := P.hf_int.sub this x hx

Result:
case refine_2.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
this : LocallyIntegrableOn (fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) (Ioi 0) volume
x : ℝ
hx : x ∈ Ioi 0
s : Set ℝ
hs : s ∈ 𝓝[Ioi 0] x
hs' : IntegrableOn (P.f - fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) s volume
⊢ IntegrableAtFilter ((Ioo 0 1).indicator fun x => P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) (𝓝[Ioi 0] x) volume

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ LocallyIntegrableOn P.f_modif (Ioi 0) volume

Tactic:
have : LocallyIntegrableOn (fun x : ℝ ↦ (P.ε * ↑(x ^ (-P.k))) • P.g₀) (Ioi 0) := by
  refine ContinuousOn.locallyIntegrableOn ?_ measurableSet_Ioi
  refine continuousOn_of_forall_continuousAt (fun x (hx : 0 < x) ↦ ?_)
  refine (continuousAt_const.mul ?_).smul continuousAt_const
  exact continuous_ofReal.continuousAt.comp (continuousAt_rpow_const _ _ (Or.inl hx.ne'))

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
this : LocallyIntegrableOn (fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) (Ioi 0) volume
⊢ LocallyIntegrableOn P.f_modif (Ioi 0) volume

Proof state:
case refine_1.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
this : LocallyIntegrableOn (fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) (Ioi 0) volume
x : ℝ
hx : x ∈ Ioi 0
s : Set ℝ
hs : s ∈ 𝓝[Ioi 0] x
hs' : IntegrableOn (P.f - fun x => ?m.84581) s volume
⊢ IntegrableOn (fun x => P.f x - P.f₀) (Ioi 1 ∩ s) volume

Tactic:
exact hs'.mono_set Set.inter_subset_right

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Archimedean.lean
theorem tendsto_ratCast_atBot_iff [LinearOrderedField R] [Archimedean R] {f : α → ℚ}
    {l : Filter α} : Tendsto (fun n => (f n : R)) l atBot ↔ Tendsto f l atBot

Proof state:
α : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
f : α → ℚ
l : Filter α
⊢ Tendsto (fun n => ↑(f n)) l atBot ↔ Tendsto (Rat.cast ∘ f) l atBot

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
f : α → ℚ
l : Filter α
⊢ Tendsto (fun n => ↑(f n)) l atBot ↔ Tendsto f l atBot

Tactic:
rw [← @Rat.comap_cast_atBot R, tendsto_comap_iff]

Result:
α : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
f : α → ℚ
l : Filter α
⊢ Tendsto (fun n => ↑(f n)) l atBot ↔ Tendsto (Rat.cast ∘ f) l atBot