harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem zipWithAux_toArray_succ (as : List α) (bs : List β) (f : α → β → γ) (i : Nat) (cs : Array γ) :
    zipWithAux as.toArray bs.toArray f (i + 1) cs = zipWithAux as.tail.toArray bs.tail.toArray f i cs

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : α → β → γ
i : Nat
cs : Array γ
⊢ (if h : i + 1 < as.toArray.size then
      let a := as.toArray[i + 1];
      if h : i + 1 < bs.toArray.size then
        let b := bs.toArray[i + 1];
        as.toArray.zipWithAux bs.toArray f (i + 1 + 1) (cs.push (f a b))
      else cs
    else cs) =
    as.tail.toArray.zipWithAux bs.tail.toArray f i cs

Tactic:
conv => rhs; rw [zipWithAux]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : α → β → γ
i : Nat
cs : Array γ
⊢ (if h : i + 1 < as.toArray.size then
      let a := as.toArray[i + 1];
      if h : i + 1 < bs.toArray.size then
        let b := bs.toArray[i + 1];
        as.toArray.zipWithAux bs.toArray f (i + 1 + 1) (cs.push (f a b))
      else cs
    else cs) =
    if h : i < as.tail.toArray.size then
      let a := as.tail.toArray[i];
      if h : i < bs.tail.toArray.size then
        let b := bs.tail.toArray[i];
        as.tail.toArray.zipWithAux bs.tail.toArray f (i + 1) (cs.push (f a b))
      else cs
    else cs
-- Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean
theorem arrow_ι (j : J) : arrows j ≫ ι arrows j = head arrows

Proof state:
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
j : J
⊢ arrows j ≫ ι arrows j = head arrows

Tactic:
apply colimit.w (WidePushoutShape.wideSpan _ _ _) (WidePushoutShape.Hom.init j)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem isEmpty_eq_false {l : List α} : l.isEmpty = false ↔ l ≠ []

Proof state:
α : Type u_1
l : List α
⊢ l.isEmpty = false ↔ l ≠ []

Tactic:
cases l <;> simp

Result:
no goals
-- Mathlib/Topology/Order/LeftRightLim.lean
theorem continuousAt_iff_leftLim_eq_rightLim : ContinuousAt f x ↔ leftLim f x = rightLim f x

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : leftLim f x = rightLim f x
⊢ f x ≤ leftLim f x

Tactic:
rw [h]

Result:
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : leftLim f x = rightLim f x
⊢ f x ≤ rightLim f x
-- Mathlib/RingTheory/WittVector/Basic.lean
private lemma ghostFun_nsmul (m : ℕ) (x : WittVector p R) : ghostFun (m • x) = m • ghostFun x

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
m : ℕ
x : 𝕎 R
⊢ WittVector.ghostFun (m • x) = m • WittVector.ghostFun x

Tactic:
ghost_fun_tac m • (X 0), ![x.coeff]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
@[simp]
lemma monomial_mul_mem_coeffsIn : monomial i 1 * p ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M

Proof state:
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
p : MvPolynomial σ S
i : σ →₀ ℕ
⊢ (monomial i) 1 * p ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M

Tactic:
simp [mul_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem sublist_or_mem_of_sublist (h : l <+ l₁ ++ a :: l₂) : l <+ l₁ ++ l₂ ∨ a ∈ l

Proof state:
α✝ : Type u_1
a : α✝
l₂ : List α✝
b : α✝
l₁ : List α✝
IH : ∀ {l : List α✝}, l <+ l₁ ++ a :: l₂ → l <+ l₁ ++ l₂ ∨ a ∈ l
l : List α✝
h✝ : l <+ b :: l₁ ++ a :: l₂
l₁✝ : List α✝
h : l₁✝ <+ l₁.append (a :: l₂)
⊢ b :: l₁✝ <+ b :: l₁ ++ l₂ ∨ a ∈ b :: l₁✝

Tactic:
exact (IH h).imp (Sublist.cons₂ _) (.tail _)

Result:
no goals

Proof state:
α✝ : Type u_1
a : α✝
l₂ l : List α✝
h✝ : l <+ [] ++ a :: l₂
l₁✝ : List α✝
h : l₁✝ <+ l₂
⊢ a :: l₁✝ <+ [] ++ l₂ ∨ a ∈ a :: l₁✝

Tactic:
exact .inr (.head ..)

Result:
no goals

Proof state:
case nil
α✝ : Type u_1
a : α✝
l₂ l : List α✝
h : l <+ [] ++ a :: l₂
⊢ l <+ [] ++ l₂ ∨ a ∈ l

Tactic:
match h with
| .cons _ h => exact .inl h
| .cons₂ _ h => exact .inr (.head ..)

Result:
no goals

Proof state:
α✝ : Type u_1
a : α✝
l₂ l✝ : List α✝
h✝ : l✝ <+ [] ++ a :: l₂
l : List α✝
h : l <+ l₂
⊢ l <+ [] ++ l₂ ∨ a ∈ l

Tactic:
exact .inl h

Result:
no goals

Proof state:
α✝ : Type u_1
a : α✝
l₂ : List α✝
b : α✝
l₁ : List α✝
IH : ∀ {l : List α✝}, l <+ l₁ ++ a :: l₂ → l <+ l₁ ++ l₂ ∨ a ∈ l
l✝ : List α✝
h✝ : l✝ <+ b :: l₁ ++ a :: l₂
l : List α✝
h : l <+ l₁.append (a :: l₂)
⊢ l <+ b :: l₁ ++ l₂ ∨ a ∈ l

Tactic:
exact (IH h).imp_left (Sublist.cons _)

Result:
no goals

Proof state:
case cons
α✝ : Type u_1
a : α✝
l₂ : List α✝
b : α✝
l₁ : List α✝
IH : ∀ {l : List α✝}, l <+ l₁ ++ a :: l₂ → l <+ l₁ ++ l₂ ∨ a ∈ l
l : List α✝
h : l <+ b :: l₁ ++ a :: l₂
⊢ l <+ b :: l₁ ++ l₂ ∨ a ∈ l

Tactic:
match h with
| .cons _ h => exact (IH h).imp_left (Sublist.cons _)
| .cons₂ _ h => exact (IH h).imp (Sublist.cons₂ _) (.tail _)

Result:
no goals

Proof state:
α✝ : Type u_1
l l₁ : List α✝
a : α✝
l₂ : List α✝
h : l <+ l₁ ++ a :: l₂
⊢ l <+ l₁ ++ l₂ ∨ a ∈ l

Tactic:
induction l₁ generalizing l with
| nil => match h with
  | .cons _ h => exact .inl h
  | .cons₂ _ h => exact .inr (.head ..)
| cons b l₁ IH =>
  match h with
  | .cons _ h => exact (IH h).imp_left (Sublist.cons _)
  | .cons₂ _ h => exact (IH h).imp (Sublist.cons₂ _) (.tail _)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldlM_append [Monad m] [LawfulMonad m] (f : β → α → m β) (b) (l l' : Array α) :
    (l ++ l').foldlM f b = l.foldlM f b >>= l'.foldlM f

Proof state:
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
l l' : Array α
⊢ foldlM f b (l ++ l') = do
    let init ← foldlM f b l
    foldlM f init l'

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RefVecOperator/Map.lean
theorem go_denote_mem_prefix {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len)
    (s : RefVec aig curr) (input : RefVec aig len)
    (f : (aig : AIG α) → Ref aig → Entrypoint α) [LawfulOperator α Ref f] [LawfulMapOperator α f]
    (start : Nat) (hstart) :
    ⟦
      (go aig curr hcurr s input f).aig,
      ⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
      assign
    ⟧
      =
    ⟦aig, ⟨start, hstart⟩, assign⟧

Proof state:
case a
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
input : aig.RefVec len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
start : Nat
hstart : start < aig.decls.size
⊢ start < ?m

case a
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
input : aig.RefVec len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
start : Nat
hstart : start < aig.decls.size
⊢ ?m ≤ (go aig curr hcurr s input f).aig.decls.size

case m
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
input : aig.RefVec len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
start : Nat
hstart : start < aig.decls.size
⊢ Nat

Tactic:
exact hstart

Result:
case a
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
input : aig.RefVec len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
start : Nat
hstart : start < aig.decls.size
⊢ aig.decls.size ≤ (go aig curr hcurr s input f).aig.decls.size
-- Mathlib/Topology/Algebra/GroupWithZero.lean
theorem map_mul_right_nhds_one₀ (ha : a ≠ 0) : map (· * a) (𝓝 1) = 𝓝 (a)

Proof state:
G₀ : Type u_3
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : ContinuousMul G₀
a : G₀
ha : a ≠ 0
⊢ map (fun x => x * a) (𝓝 1) = 𝓝 a

Tactic:
rw [map_mul_right_nhds₀ ha, one_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem length_dropLast_cons (a : α) (as : List α) : (a :: as).dropLast.length = as.length

Proof state:
α : Type u
a : α
as : List α
b : α
bs : List α
ih : (b :: bs).dropLast.length = bs.length
⊢ (a :: b :: bs).dropLast.length = (b :: bs).length

Tactic:
simp [dropLast, ih]

Result:
no goals

Proof state:
α : Type u
a : α
as : List α
⊢ (a :: nil).dropLast.length = nil.length

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
a : α
as : List α
b : α
bs : List α
⊢ (a :: b :: bs).dropLast.length = (b :: bs).length

Tactic:
have ih := length_dropLast_cons b bs

Result:
α : Type u
a : α
as : List α
b : α
bs : List α
ih : (b :: bs).dropLast.length = bs.length
⊢ (a :: b :: bs).dropLast.length = (b :: bs).length

Proof state:
α : Type u
a : α
as : List α
⊢ (a :: as).dropLast.length = as.length

Tactic:
match as with
| []       => rfl
| b::bs =>
  have ih := length_dropLast_cons b bs
  simp [dropLast, ih]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
lemma length_le : c.length ≤ n

Proof state:
n : ℕ
c : OrderedFinpartition n
⊢ c.length ≤ n

Tactic:
simpa only [Fintype.card_fin] using Fintype.card_le_of_injective _ c.parts_strictMono.injective

Result:
no goals
-- Mathlib/Algebra/Lie/OfAssociative.lean
theorem toEnd_comp_subtype_mem (m : M) (hm : m ∈ (N : Submodule R M)) :
    (toEnd R L M x).comp (N : Submodule R M).subtype ⟨m, hm⟩ ∈ (N : Submodule R M)

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
x : L
m : M
hm : m ∈ ↑N
⊢ ((toEnd R L M) x ∘ₗ (↑N).subtype) ⟨m, hm⟩ ∈ ↑N

Tactic:
simpa using N.lie_mem hm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem wfImp_modify [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α]
    (h : Raw.WFImp m.1) {a : α} {f : β → β} : Raw.WFImp (Const.modify m a f).1

Proof state:
α : Type u
β : Type v
m : Raw₀ α fun x => β
inst✝³ : BEq α
inst✝² : EquivBEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
h : Raw.WFImp m.val
a : α
f : β → β
⊢ Raw.WFImp (modify m a f).val

Tactic:
rw [Const.modify_eq_modifyₘ]

Result:
α : Type u
β : Type v
m : Raw₀ α fun x => β
inst✝³ : BEq α
inst✝² : EquivBEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
h : Raw.WFImp m.val
a : α
f : β → β
⊢ Raw.WFImp (modifyₘ m a f).val

Proof state:
α : Type u
β : Type v
m : Raw₀ α fun x => β
inst✝³ : BEq α
inst✝² : EquivBEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
h : Raw.WFImp m.val
a : α
f : β → β
⊢ Raw.WFImp (modifyₘ m a f).val

Tactic:
exact wfImp_alterₘ h

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
lemma Nat.log_ne_padicValNat_succ {n : ℕ} (hn : n ≠ 0) : log 2 n ≠ padicValNat 2 (n + 1)

Proof state:
n : ℕ
hn : n ≠ 0
⊢ padicValNat 2 (n + 1) ≠ 0 ∨ 1 < 2 ∧ n ≠ 0

Tactic:
simp [hn]

Result:
no goals

Proof state:
case intro
n : ℕ
hn : n ≠ 0
h1 : 2 ^ padicValNat 2 (n + 1) * 1 < n + 1
h2 : n + 1 ≤ 2 ^ padicValNat 2 (n + 1) * 2
⊢ 2 ^ padicValNat 2 (n + 1) * (1 + 1) ≠ n + 1

Tactic:
exact pow_succ_padicValNat_not_dvd (p := 2) n.succ_ne_zero ∘ dvd_of_eq

Result:
no goals

Proof state:
n : ℕ
hn : n ≠ 0
⊢ ¬(2 ^ padicValNat 2 (n + 1) ≤ n ∧ n < 2 ^ (padicValNat 2 (n + 1) + 1))

Tactic:
rintro ⟨h1, h2⟩

Result:
case intro
n : ℕ
hn : n ≠ 0
h1 : 2 ^ padicValNat 2 (n + 1) ≤ n
h2 : n < 2 ^ (padicValNat 2 (n + 1) + 1)
⊢ False

Proof state:
n : ℕ
hn : n ≠ 0
⊢ log 2 n ≠ padicValNat 2 (n + 1)

Tactic:
rw [Ne, log_eq_iff (by simp [hn])]

Result:
n : ℕ
hn : n ≠ 0
⊢ ¬(2 ^ padicValNat 2 (n + 1) ≤ n ∧ n < 2 ^ (padicValNat 2 (n + 1) + 1))

Proof state:
case intro
n : ℕ
hn : n ≠ 0
h1 : 2 ^ padicValNat 2 (n + 1) ≤ n
h2 : n < 2 ^ (padicValNat 2 (n + 1) + 1)
⊢ False

Tactic:
rw [← Nat.lt_add_one_iff, ← mul_one (2 ^ _)] at h1

Result:
case intro
n : ℕ
hn : n ≠ 0
h1 : 2 ^ padicValNat 2 (n + 1) * 1 < n + 1
h2 : n < 2 ^ (padicValNat 2 (n + 1) + 1)
⊢ False

Proof state:
case intro
n : ℕ
hn : n ≠ 0
h1 : 2 ^ padicValNat 2 (n + 1) * 1 < n + 1
h2 : n < 2 ^ (padicValNat 2 (n + 1) + 1)
⊢ False

Tactic:
rw [← add_one_le_iff, Nat.pow_succ] at h2

Result:
case intro
n : ℕ
hn : n ≠ 0
h1 : 2 ^ padicValNat 2 (n + 1) * 1 < n + 1
h2 : n + 1 ≤ 2 ^ padicValNat 2 (n + 1) * 2
⊢ False

Proof state:
case intro
n : ℕ
hn : n ≠ 0
h1 : 2 ^ padicValNat 2 (n + 1) * 1 < n + 1
h2 : n + 1 ≤ 2 ^ padicValNat 2 (n + 1) * 2
⊢ False

Tactic:
refine not_dvd_of_between_consec_multiples h1 (lt_of_le_of_ne' h2 ?_) pow_padicValNat_dvd

Result:
case intro
n : ℕ
hn : n ≠ 0
h1 : 2 ^ padicValNat 2 (n + 1) * 1 < n + 1
h2 : n + 1 ≤ 2 ^ padicValNat 2 (n + 1) * 2
⊢ 2 ^ padicValNat 2 (n + 1) * (1 + 1) ≠ n + 1
-- Mathlib/Probability/Kernel/Condexp.lean
theorem aestronglyMeasurable_integral_condExpKernel [NormedSpace ℝ F]
    (hf : AEStronglyMeasurable f μ) :
    AEStronglyMeasurable[m] (fun ω => ∫ y, f y ∂condExpKernel μ m ω) μ

Proof state:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (fun ω => ∫ (y : Ω), f y ∂(condExpKernel μ m) ω) μ

Tactic:
nontriviality Ω

Result:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf : AEStronglyMeasurable f μ
a✝ : Nontrivial Ω
⊢ AEStronglyMeasurable (fun ω => ∫ (y : Ω), f y ∂(condExpKernel μ m) ω) μ

Proof state:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf : AEStronglyMeasurable f μ
a✝ : Nontrivial Ω
h : AEStronglyMeasurable (fun a => ∫ (y : Ω), f (id a, y).2 ∂(condDistrib id id μ) (id a)) μ
⊢ AEStronglyMeasurable (fun ω => ∫ (y : Ω), f y ∂((condDistrib id id μ).comap id ⋯) ω) μ

Tactic:
exact h.mono inf_le_left

Result:
no goals

Proof state:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf : AEStronglyMeasurable f μ
a✝ : Nontrivial Ω
⊢ AEStronglyMeasurable (fun ω => ∫ (y : Ω), f y ∂((condDistrib id id μ).comap id ⋯) ω) μ

Tactic:
have h := aestronglyMeasurable_integral_condDistrib
  (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
  (hf.comp_snd_map_prod_id (inf_le_right : m ⊓ mΩ ≤ mΩ))

Result:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf : AEStronglyMeasurable f μ
a✝ : Nontrivial Ω
h : AEStronglyMeasurable (fun a => ∫ (y : Ω), f (id a, y).2 ∂(condDistrib id id μ) (id a)) μ
⊢ AEStronglyMeasurable (fun ω => ∫ (y : Ω), f y ∂((condDistrib id id μ).comap id ⋯) ω) μ

Proof state:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf : AEStronglyMeasurable f μ
a✝ : Nontrivial Ω
⊢ AEStronglyMeasurable (fun ω => ∫ (y : Ω), f y ∂(condExpKernel μ m) ω) μ

Tactic:
rw [condExpKernel_eq]

Result:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf : AEStronglyMeasurable f μ
a✝ : Nontrivial Ω
⊢ AEStronglyMeasurable (fun ω => ∫ (y : Ω), f y ∂((condDistrib id id μ).comap id ⋯) ω) μ
-- Mathlib/Algebra/Group/Subgroup/Defs.lean
theorem inclusion_right (h : H ≤ K) (x : K) (hx : (x : G) ∈ H) : inclusion h ⟨x, hx⟩ = x

Proof state:
case mk
G : Type u_1
inst✝² : Group G
S : Type u_4
H K : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
h : H ≤ K
val✝ : G
property✝ : val✝ ∈ K
hx : ↑⟨val✝, property✝⟩ ∈ H
⊢ (inclusion h) ⟨↑⟨val✝, property✝⟩, hx⟩ = ⟨val✝, property✝⟩

Tactic:
rfl

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
S : Type u_4
H K : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
h : H ≤ K
x : ↥K
hx : ↑x ∈ H
⊢ (inclusion h) ⟨↑x, hx⟩ = x

Tactic:
cases x

Result:
case mk
G : Type u_1
inst✝² : Group G
S : Type u_4
H K : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
h : H ≤ K
val✝ : G
property✝ : val✝ ∈ K
hx : ↑⟨val✝, property✝⟩ ∈ H
⊢ (inclusion h) ⟨↑⟨val✝, property✝⟩, hx⟩ = ⟨val✝, property✝⟩
-- Mathlib/Data/Nat/Nth.lean
theorem range_nth_of_infinite (hf : (setOf p).Infinite) : Set.range (nth p) = setOf p

Proof state:
p : ℕ → Prop
hf : (setOf p).Infinite
this : Infinite ↑(setOf p)
⊢ Set.range (Subtype.val ∘ ⇑(Subtype.orderIsoOfNat (setOf p))) = setOf p

Tactic:
classical exact Nat.Subtype.coe_comp_ofNat_range

Result:
no goals

Proof state:
p : ℕ → Prop
hf : (setOf p).Infinite
this : Infinite ↑(setOf p)
⊢ Set.range (Subtype.val ∘ ⇑(Subtype.orderIsoOfNat (setOf p))) = setOf p

Tactic:
exact Nat.Subtype.coe_comp_ofNat_range

Result:
no goals

Proof state:
p : ℕ → Prop
hf : (setOf p).Infinite
⊢ Set.range (Subtype.val ∘ ⇑(Subtype.orderIsoOfNat (setOf p))) = setOf p

Tactic:
haveI := hf.to_subtype

Result:
p : ℕ → Prop
hf : (setOf p).Infinite
this : Infinite ↑(setOf p)
⊢ Set.range (Subtype.val ∘ ⇑(Subtype.orderIsoOfNat (setOf p))) = setOf p

Proof state:
p : ℕ → Prop
hf : (setOf p).Infinite
⊢ Set.range (nth p) = setOf p

Tactic:
rw [nth_eq_orderIsoOfNat hf]

Result:
p : ℕ → Prop
hf : (setOf p).Infinite
⊢ Set.range (Subtype.val ∘ ⇑(Subtype.orderIsoOfNat (setOf p))) = setOf p
-- Mathlib/LinearAlgebra/Dual.lean
theorem dualAnnihilator_top : (⊤ : Submodule R M).dualAnnihilator = ⊥

Proof state:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : Dual R M
⊢ (∀ (w : M), v w = 0) → v = 0

Tactic:
exact fun h => LinearMap.ext h

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ⊤.dualAnnihilator = ⊥

Tactic:
rw [eq_bot_iff]

Result:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ⊤.dualAnnihilator ≤ ⊥

Proof state:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : Dual R M
⊢ v ∈ ⊤.dualAnnihilator → v ∈ ⊥

Tactic:
simp_rw [mem_dualAnnihilator, mem_bot, mem_top, forall_true_left]

Result:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : Dual R M
⊢ (∀ (w : M), v w = 0) → v = 0

Proof state:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ⊤.dualAnnihilator ≤ ⊥

Tactic:
intro v

Result:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : Dual R M
⊢ v ∈ ⊤.dualAnnihilator → v ∈ ⊥
-- Mathlib/Order/Filter/Basic.lean
theorem exists_mem_and_iff {P : Set α → Prop} {Q : Set α → Prop} (hP : Antitone P)
    (hQ : Antitone Q) : ((∃ u ∈ f, P u) ∧ ∃ u ∈ f, Q u) ↔ ∃ u ∈ f, P u ∧ Q u

Proof state:
case mp
α : Type u
f : Filter α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
⊢ ((∃ u ∈ f, P u) ∧ ∃ u ∈ f, Q u) → ∃ u ∈ f, P u ∧ Q u

Tactic:
rintro ⟨⟨u, huf, hPu⟩, v, hvf, hQv⟩

Result:
case mp.intro.intro.intro.intro.intro
α : Type u
f : Filter α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
u : Set α
huf : u ∈ f
hPu : P u
v : Set α
hvf : v ∈ f
hQv : Q v
⊢ ∃ u ∈ f, P u ∧ Q u

Proof state:
α : Type u
f : Filter α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
⊢ ((∃ u ∈ f, P u) ∧ ∃ u ∈ f, Q u) ↔ ∃ u ∈ f, P u ∧ Q u

Tactic:
constructor

Result:
case mp
α : Type u
f : Filter α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
⊢ ((∃ u ∈ f, P u) ∧ ∃ u ∈ f, Q u) → ∃ u ∈ f, P u ∧ Q u

case mpr
α : Type u
f : Filter α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
⊢ (∃ u ∈ f, P u ∧ Q u) → (∃ u ∈ f, P u) ∧ ∃ u ∈ f, Q u

Proof state:
case mp.intro.intro.intro.intro.intro
α : Type u
f : Filter α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
u : Set α
huf : u ∈ f
hPu : P u
v : Set α
hvf : v ∈ f
hQv : Q v
⊢ ∃ u ∈ f, P u ∧ Q u

Tactic:
exact
  ⟨u ∩ v, inter_mem huf hvf, hP inter_subset_left hPu, hQ inter_subset_right hQv⟩

Result:
no goals

Proof state:
case mpr
α : Type u
f : Filter α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
⊢ (∃ u ∈ f, P u ∧ Q u) → (∃ u ∈ f, P u) ∧ ∃ u ∈ f, Q u

Tactic:
rintro ⟨u, huf, hPu, hQu⟩

Result:
case mpr.intro.intro.intro
α : Type u
f : Filter α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
u : Set α
huf : u ∈ f
hPu : P u
hQu : Q u
⊢ (∃ u ∈ f, P u) ∧ ∃ u ∈ f, Q u

Proof state:
case mpr.intro.intro.intro
α : Type u
f : Filter α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
u : Set α
huf : u ∈ f
hPu : P u
hQu : Q u
⊢ (∃ u ∈ f, P u) ∧ ∃ u ∈ f, Q u

Tactic:
exact ⟨⟨u, huf, hPu⟩, u, huf, hQu⟩

Result:
no goals
-- Mathlib/Algebra/Lie/Semisimple/Basic.lean
theorem hasTrivialRadical_iff_no_abelian_ideals :
    HasTrivialRadical R L ↔ ∀ I : LieIdeal R L, IsLieAbelian I → I = ⊥

Proof state:
case mpr
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h₁ : ∀ (I : LieIdeal R L), IsLieAbelian ↥I → I = ⊥
I : LieIdeal R L
h₂ : IsSolvable ↥I
⊢ I = ⊥

Tactic:
rw [← abelian_of_solvable_ideal_eq_bot_iff]

Result:
case mpr
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h₁ : ∀ (I : LieIdeal R L), IsLieAbelian ↥I → I = ⊥
I : LieIdeal R L
h₂ : IsSolvable ↥I
⊢ derivedAbelianOfIdeal I = ⊥

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ HasTrivialRadical R L ↔ ∀ (I : LieIdeal R L), IsLieAbelian ↥I → I = ⊥

Tactic:
rw [hasTrivialRadical_iff_no_solvable_ideals]

Result:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ (∀ (I : LieIdeal R L), IsSolvable ↥I → I = ⊥) ↔ ∀ (I : LieIdeal R L), IsLieAbelian ↥I → I = ⊥

Proof state:
case mpr
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h₁ : ∀ (I : LieIdeal R L), IsLieAbelian ↥I → I = ⊥
I : LieIdeal R L
h₂ : IsSolvable ↥I
⊢ derivedAbelianOfIdeal I = ⊥

Tactic:
exact h₁ _ <| abelian_derivedAbelianOfIdeal I

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ (∀ (I : LieIdeal R L), IsSolvable ↥I → I = ⊥) ↔ ∀ (I : LieIdeal R L), IsLieAbelian ↥I → I = ⊥

Tactic:
constructor <;> intro h₁ I h₂

Result:
case mp
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h₁ : ∀ (I : LieIdeal R L), IsSolvable ↥I → I = ⊥
I : LieIdeal R L
h₂ : IsLieAbelian ↥I
⊢ I = ⊥

case mpr
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h₁ : ∀ (I : LieIdeal R L), IsLieAbelian ↥I → I = ⊥
I : LieIdeal R L
h₂ : IsSolvable ↥I
⊢ I = ⊥

Proof state:
case mp
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h₁ : ∀ (I : LieIdeal R L), IsSolvable ↥I → I = ⊥
I : LieIdeal R L
h₂ : IsLieAbelian ↥I
⊢ I = ⊥

Tactic:
exact h₁ _ <| LieAlgebra.ofAbelianIsSolvable I

Result:
no goals
-- Mathlib/Order/Birkhoff.lean
lemma supIrredLowerSet_surjective : Surjective (supIrredLowerSet (α := α))

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : Finite α
⊢ Surjective ⇑supIrredLowerSet

Tactic:
aesop (add simp Surjective)

Result:
no goals