harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem extract_cons_addChar (c : Char) (cs : List Char) (b e : Pos) :
    extract ⟨c :: cs⟩ (b + c) (e + c) = extract ⟨cs⟩ b e

Proof state:
c : Char
cs : List Char
b e : Pos
⊢ { data := c :: cs }.extract (b + c) (e + c) = { data := cs }.extract b e

Tactic:
simp only [extract, pos_add_char, ge_iff_le, Nat.add_le_add_iff_right]

Result:
c : Char
cs : List Char
b e : Pos
⊢ (if e.byteIdx ≤ b.byteIdx then "" else { data := extract.go₁ (c :: cs) 0 (b + c) (e + c) }) =
    if e.byteIdx ≤ b.byteIdx then "" else { data := extract.go₁ cs 0 b e }

Proof state:
c : Char
cs : List Char
b e : Pos
⊢ (if e.byteIdx ≤ b.byteIdx then "" else { data := extract.go₁ (c :: cs) 0 (b + c) (e + c) }) =
    if e.byteIdx ≤ b.byteIdx then "" else { data := extract.go₁ cs 0 b e }

Tactic:
split <;> [rfl; rw [extract.go₁_cons_addChar]]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem findRev?_push_of_pos (l : Vector α n) (h : p a) :
    findRev? p (l.push a) = some a

Proof state:
case mk
α : Type
n : Nat
p : α → Bool
a : α
h : p a = true
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ findRev? p ({ toArray := toArray✝, size_toArray := size_toArray✝ }.push a) = some a

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type
n : Nat
p : α → Bool
a : α
l : Vector α n
h : p a = true
⊢ findRev? p (l.push a) = some a

Tactic:
cases l

Result:
case mk
α : Type
n : Nat
p : α → Bool
a : α
h : p a = true
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ findRev? p ({ toArray := toArray✝, size_toArray := size_toArray✝ }.push a) = some a
-- Mathlib/Data/Nat/Log.lean
theorem log_eq_of_pow_le_of_lt_pow {b m n : ℕ} (h₁ : b ^ m ≤ n) (h₂ : n < b ^ (m + 1)) :
    log b n = m

Proof state:
case inl
b n : ℕ
h₁ : b ^ 0 ≤ n
h₂ : n < b
⊢ log b n = 0

Tactic:
exact log_of_lt h₂

Result:
no goals

Proof state:
case inl
b n : ℕ
h₁ : b ^ 0 ≤ n
h₂ : n < b ^ (0 + 1)
⊢ log b n = 0

Tactic:
rw [Nat.pow_one] at h₂

Result:
case inl
b n : ℕ
h₁ : b ^ 0 ≤ n
h₂ : n < b
⊢ log b n = 0

Proof state:
b m n : ℕ
h₁ : b ^ m ≤ n
h₂ : n < b ^ (m + 1)
⊢ log b n = m

Tactic:
rcases eq_or_ne m 0 with (rfl | hm)

Result:
case inl
b n : ℕ
h₁ : b ^ 0 ≤ n
h₂ : n < b ^ (0 + 1)
⊢ log b n = 0

case inr
b m n : ℕ
h₁ : b ^ m ≤ n
h₂ : n < b ^ (m + 1)
hm : m ≠ 0
⊢ log b n = m

Proof state:
case inr
b m n : ℕ
h₁ : b ^ m ≤ n
h₂ : n < b ^ (m + 1)
hm : m ≠ 0
⊢ log b n = m

Tactic:
exact (log_eq_iff (Or.inl hm)).2 ⟨h₁, h₂⟩

Result:
no goals
-- Mathlib/RingTheory/SimpleModule/Basic.lean
theorem surjective_or_eq_zero [IsSimpleModule R N] (f : M →ₗ[R] N) :
    Function.Surjective f ∨ f = 0

Proof state:
R : Type u_2
inst✝⁵ : Ring R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
⊢ range f = ⊥ ∨ range f = ⊤

Tactic:
apply eq_bot_or_eq_top

Result:
no goals

Proof state:
R : Type u_2
inst✝⁵ : Ring R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
⊢ Function.Surjective ⇑f ∨ f = 0

Tactic:
rw [← range_eq_top, ← range_eq_bot, or_comm]

Result:
R : Type u_2
inst✝⁵ : Ring R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
⊢ range f = ⊥ ∨ range f = ⊤
-- Mathlib/Algebra/Order/CompleteField.lean
theorem cutMap_bddAbove (a : α) : BddAbove (cutMap β a)

Proof state:
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean α
a : α
⊢ BddAbove (cutMap β a)

Tactic:
obtain ⟨q, hq⟩ := exists_rat_gt a

Result:
case intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean α
a : α
q : ℚ
hq : a < ↑q
⊢ BddAbove (cutMap β a)

Proof state:
case intro
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : LinearOrderedField β
inst✝ : Archimedean α
a : α
q : ℚ
hq : a < ↑q
⊢ BddAbove (cutMap β a)

Tactic:
exact ⟨q, forall_mem_image.2 fun r hr => mod_cast (hq.trans' hr).le⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem and_eq_false_iff : ∀ {x y : Bool}, (x && y) = false ↔ x = false ∨ y = false

Proof state:
⊢ ∀ {x y : Bool}, (x && y) = false ↔ x = false ∨ y = false

Tactic:
decide

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem span_induction {p : (x : M) → x ∈ span R s → Prop}
    (mem : ∀ (x) (h : x ∈ s), p x (subset_span h))
    (zero : p 0 (Submodule.zero_mem _))
    (add : ∀ x y hx hy, p x hx → p y hy → p (x + y) (Submodule.add_mem _ ‹_› ‹_›))
    (smul : ∀ (a : R) (x hx), p x hx → p (a • x) (Submodule.smul_mem _ _ ‹_›)) {x}
    (hx : x ∈ span R s) : p x hx

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
p : (x : M) → x ∈ span R s → Prop
mem : ∀ (x : M) (h : x ∈ s), p x ⋯
zero : p 0 ⋯
add : ∀ (x y : M) (hx : x ∈ span R s) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) ⋯
smul : ∀ (a : R) (x : M) (hx : x ∈ span R s), p x hx → p (a • x) ⋯
x : M
hx : x ∈ span R s
⊢ p x hx

Tactic:
let p : Submodule R M :=
  { carrier := { x | ∃ hx, p x hx }
    add_mem' := fun ⟨_, hpx⟩ ⟨_, hpy⟩ ↦ ⟨_, add _ _ _ _ hpx hpy⟩
    zero_mem' := ⟨_, zero⟩
    smul_mem' := fun r ↦ fun ⟨_, hpx⟩ ↦ ⟨_, smul r _ _ hpx⟩ }

Result:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
p✝ : (x : M) → x ∈ span R s → Prop
mem : ∀ (x : M) (h : x ∈ s), p✝ x ⋯
zero : p✝ 0 ⋯
add : ∀ (x y : M) (hx : x ∈ span R s) (hy : y ∈ span R s), p✝ x hx → p✝ y hy → p✝ (x + y) ⋯
smul : ∀ (a : R) (x : M) (hx : x ∈ span R s), p✝ x hx → p✝ (a • x) ⋯
x : M
hx : x ∈ span R s
p : Submodule R M := { carrier := {x | ∃ (hx : x ∈ span R s), p✝ x hx}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ p✝ x hx

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
p✝ : (x : M) → x ∈ span R s → Prop
mem : ∀ (x : M) (h : x ∈ s), p✝ x ⋯
zero : p✝ 0 ⋯
add : ∀ (x y : M) (hx : x ∈ span R s) (hy : y ∈ span R s), p✝ x hx → p✝ y hy → p✝ (x + y) ⋯
smul : ∀ (a : R) (x : M) (hx : x ∈ span R s), p✝ x hx → p✝ (a • x) ⋯
x : M
hx : x ∈ span R s
p : Submodule R M := { carrier := {x | ∃ (hx : x ∈ span R s), p✝ x hx}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ p✝ x hx

Tactic:
exact span_le (p := p) |>.mpr (fun y hy ↦ ⟨subset_span hy, mem y hy⟩) hx |>.elim fun _ ↦ id

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem nontrivial_span_singleton {x : M} (h : x ≠ 0) : Nontrivial (R ∙ x) :=
  ⟨by
    use 0, ⟨x, Submodule.mem_span_singleton_self x⟩
    intro H
    rw [eq_comm, Submodule.mk_eq_zero] at H
    exact h H⟩

Proof state:
case h
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
h : x ≠ 0
⊢ 0 ≠ ⟨x, ⋯⟩

Tactic:
intro H

Result:
case h
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
h : x ≠ 0
H : 0 = ⟨x, ⋯⟩
⊢ False

Proof state:
case h
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
h : x ≠ 0
H : x = 0
⊢ False

Tactic:
exact h H

Result:
no goals

Proof state:
case h
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
h : x ≠ 0
H : 0 = ⟨x, ⋯⟩
⊢ False

Tactic:
rw [eq_comm, Submodule.mk_eq_zero] at H

Result:
case h
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
h : x ≠ 0
H : x = 0
⊢ False

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
h : x ≠ 0
⊢ ∃ x_1 y, x_1 ≠ y

Tactic:
use 0, ⟨x, Submodule.mem_span_singleton_self x⟩

Result:
case h
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
h : x ≠ 0
⊢ 0 ≠ ⟨x, ⋯⟩
-- Mathlib/FieldTheory/IsPerfectClosure.lean
theorem injective_comp_of_pNilradical_eq_bot [IsPRadical i p] (h : pNilradical M p = ⊥) :
    Function.Injective fun f : L →+* M ↦ f.comp i := fun f g heq ↦ by
  ext x
  obtain ⟨n, y, hx⟩ := IsPRadical.pow_mem i p x
  apply_fun _ using pow_expChar_pow_inj_of_pNilradical_eq_bot M p h n
  simpa only [← map_pow, ← hx] using congr($(heq) y)

Proof state:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommRing K
inst✝³ : CommRing L
inst✝² : CommRing M
i : K →+* L
p : ℕ
inst✝¹ : ExpChar M p
inst✝ : IsPRadical i p
h : pNilradical M p = ⊥
f g : L →+* M
heq : (fun f => f.comp i) f = (fun f => f.comp i) g
⊢ f = g

Tactic:
ext x

Result:
case a
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommRing K
inst✝³ : CommRing L
inst✝² : CommRing M
i : K →+* L
p : ℕ
inst✝¹ : ExpChar M p
inst✝ : IsPRadical i p
h : pNilradical M p = ⊥
f g : L →+* M
heq : (fun f => f.comp i) f = (fun f => f.comp i) g
x : L
⊢ f x = g x

Proof state:
case a.intro.intro
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommRing K
inst✝³ : CommRing L
inst✝² : CommRing M
i : K →+* L
p : ℕ
inst✝¹ : ExpChar M p
inst✝ : IsPRadical i p
h : pNilradical M p = ⊥
f g : L →+* M
heq : (fun f => f.comp i) f = (fun f => f.comp i) g
x : L
n : ℕ
y : K
hx : i y = x ^ p ^ n
⊢ f x = g x

Tactic:
apply_fun _ using pow_expChar_pow_inj_of_pNilradical_eq_bot M p h n

Result:
case a.intro.intro
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommRing K
inst✝³ : CommRing L
inst✝² : CommRing M
i : K →+* L
p : ℕ
inst✝¹ : ExpChar M p
inst✝ : IsPRadical i p
h : pNilradical M p = ⊥
f g : L →+* M
heq : (fun f => f.comp i) f = (fun f => f.comp i) g
x : L
n : ℕ
y : K
hx : i y = x ^ p ^ n
⊢ f x ^ p ^ n = g x ^ p ^ n

Proof state:
case a.intro.intro
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommRing K
inst✝³ : CommRing L
inst✝² : CommRing M
i : K →+* L
p : ℕ
inst✝¹ : ExpChar M p
inst✝ : IsPRadical i p
h : pNilradical M p = ⊥
f g : L →+* M
heq : (fun f => f.comp i) f = (fun f => f.comp i) g
x : L
n : ℕ
y : K
hx : i y = x ^ p ^ n
⊢ f x ^ p ^ n = g x ^ p ^ n

Tactic:
simpa only [← map_pow, ← hx] using congr($(heq) y)

Result:
no goals

Proof state:
case a
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommRing K
inst✝³ : CommRing L
inst✝² : CommRing M
i : K →+* L
p : ℕ
inst✝¹ : ExpChar M p
inst✝ : IsPRadical i p
h : pNilradical M p = ⊥
f g : L →+* M
heq : (fun f => f.comp i) f = (fun f => f.comp i) g
x : L
⊢ f x = g x

Tactic:
obtain ⟨n, y, hx⟩ := IsPRadical.pow_mem i p x

Result:
case a.intro.intro
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommRing K
inst✝³ : CommRing L
inst✝² : CommRing M
i : K →+* L
p : ℕ
inst✝¹ : ExpChar M p
inst✝ : IsPRadical i p
h : pNilradical M p = ⊥
f g : L →+* M
heq : (fun f => f.comp i) f = (fun f => f.comp i) g
x : L
n : ℕ
y : K
hx : i y = x ^ p ^ n
⊢ f x = g x
-- Mathlib/Algebra/Group/Pi/Basic.lean
theorem elim_mul_mul [Mul γ] : Sum.elim (a * a') (b * b') = Sum.elim a b * Sum.elim a' b'

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst✝ : Mul γ
x : α ⊕ β
⊢ Sum.elim (a * a') (b * b') x = (Sum.elim a b * Sum.elim a' b') x

Tactic:
cases x <;> rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst✝ : Mul γ
⊢ Sum.elim (a * a') (b * b') = Sum.elim a b * Sum.elim a' b'

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst✝ : Mul γ
x : α ⊕ β
⊢ Sum.elim (a * a') (b * b') x = (Sum.elim a b * Sum.elim a' b') x
-- Mathlib/NumberTheory/FLT/Three.lean
private lemma lambda_not_dvd_y : ¬ λ ∣ S.y := fun h ↦ by
  replace h := mul_dvd_mul_left ((η : 𝓞 K) - 1) h
  rw [coe_eta, ← y_spec, ← pow_two] at h
  exact lambda_sq_not_dvd_a_add_eta_mul_b _ h

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : (↑η - 1) * λ ∣ (↑η - 1) * FermatLastTheoremForThreeGen.Solution.y S
⊢ False

Tactic:
rw [coe_eta, ← y_spec, ← pow_two] at h

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ^ 2 ∣ S.a + ↑η * S.b
⊢ False

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ FermatLastTheoremForThreeGen.Solution.y S
⊢ False

Tactic:
replace h := mul_dvd_mul_left ((η : 𝓞 K) - 1) h

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : (↑η - 1) * λ ∣ (↑η - 1) * FermatLastTheoremForThreeGen.Solution.y S
⊢ False

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ^ 2 ∣ S.a + ↑η * S.b
⊢ False

Tactic:
exact lambda_sq_not_dvd_a_add_eta_mul_b _ h

Result:
no goals
-- Mathlib/Data/Matrix/RowCol.lean
theorem submatrix_updateCol_equiv [DecidableEq o] [DecidableEq n] (A : Matrix m n α) (j : n)
    (c : m → α) (e : l ≃ m) (f : o ≃ n) : (A.updateCol j c).submatrix e f =
    updateCol (A.submatrix e f) (f.symm j) fun i => c (e i) :=
  Eq.trans (by simp_rw [Equiv.apply_symm_apply]) (updateCol_submatrix_equiv A _ _ e f).symm

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : DecidableEq o
inst✝ : DecidableEq n
A : Matrix m n α
j : n
c : m → α
e : l ≃ m
f : o ≃ n
⊢ (A.updateCol j c).submatrix ⇑e ⇑f = (A.updateCol (f (f.symm j)) fun i => c (e (e.symm i))).submatrix ⇑e ⇑f

Tactic:
simp_rw [Equiv.apply_symm_apply]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem prod_univ_eight [CommMonoid β] (f : Fin 8 → β) :
    ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6 * f 7

Proof state:
β : Type u_2
inst✝ : CommMonoid β
f : Fin 8 → β
⊢ ∏ i : Fin 8, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6 * f 7

Tactic:
rw [prod_univ_castSucc, prod_univ_seven]

Result:
β : Type u_2
inst✝ : CommMonoid β
f : Fin 8 → β
⊢ f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (castSucc 3) * f (castSucc 4) * f (castSucc 5) * f (castSucc 6) *
      f (last 7) =
    f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6 * f 7

Proof state:
β : Type u_2
inst✝ : CommMonoid β
f : Fin 8 → β
⊢ f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (castSucc 3) * f (castSucc 4) * f (castSucc 5) * f (castSucc 6) *
      f (last 7) =
    f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6 * f 7

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Convex/Cone/InnerDual.lean
theorem pointed_innerDualCone : s.innerDualCone.Pointed := fun x _ => by rw [inner_zero_right]

Proof state:
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s : Set H
x : H
x✝ : x ∈ s
⊢ 0 ≤ inner x 0

Tactic:
rw [inner_zero_right]

Result:
no goals
-- Mathlib/Algebra/ModEq.lean
theorem modEq_refl (a : α) : a ≡ a [PMOD p] :=
  ⟨0, by simp⟩

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
p a : α
⊢ a - a = 0 • p

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Kernel/Condexp.lean
theorem _root_.MeasureTheory.Integrable.condExpKernel_ae (hf_int : Integrable f μ) :
    ∀ᵐ ω ∂μ, Integrable f (condExpKernel μ m ω)

Proof state:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
hf_int : Integrable f μ
a✝ : Nontrivial Ω
⊢ ∀ᵐ (ω : Ω) ∂μ, Integrable f ((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
hf_int : Integrable f μ
a✝ : Nontrivial Ω
⊢ ∀ᵐ (ω : Ω) ∂μ, Integrable f (((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
hf_int : Integrable f μ
⊢ ∀ᵐ (ω : Ω) ∂μ, Integrable f ((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
hf_int : Integrable f μ
a✝ : Nontrivial Ω
⊢ ∀ᵐ (ω : Ω) ∂μ, Integrable f ((condExpKernel μ m) ω)

Proof state:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
hf_int : Integrable f μ
a✝ : Nontrivial Ω
⊢ ∀ᵐ (ω : Ω) ∂μ, Integrable f (((condDistrib id id μ).comap id ⋯) ω)

Tactic:
convert Integrable.condDistrib_ae
  (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
  (hf_int.comp_snd_map_prod_id (inf_le_right : m ⊓ mΩ ≤ mΩ)) using 1

Result:
no goals
-- Mathlib/Order/Interval/Finset/Fin.lean
@[simp]
lemma card_Icc : #(Icc a b) = b + 1 - a

Proof state:
n : ℕ
a b : Fin n
⊢ #(Icc a b) = ↑b + 1 - ↑a

Tactic:
rw [← Nat.card_Icc, ← map_valEmbedding_Icc, card_map]

Result:
no goals
-- Mathlib/SetTheory/Surreal/Multiplication.lean
lemma P3_comm : P3 x₁ x₂ y₁ y₂ ↔ P3 y₁ y₂ x₁ x₂

Proof state:
x₁ x₂ y₁ y₂ : PGame
⊢ P3 x₁ x₂ y₁ y₂ ↔ P3 y₁ y₂ x₁ x₂

Tactic:
rw [P3, P3, add_comm]

Result:
x₁ x₂ y₁ y₂ : PGame
⊢ ⟦x₂ * y₁⟧ + ⟦x₁ * y₂⟧ < ⟦x₁ * y₁⟧ + ⟦x₂ * y₂⟧ ↔ ⟦y₁ * x₂⟧ + ⟦y₂ * x₁⟧ < ⟦y₁ * x₁⟧ + ⟦y₂ * x₂⟧

Proof state:
x₁ x₂ y₁ y₂ : PGame
⊢ ⟦x₂ * y₁⟧ + ⟦x₁ * y₂⟧ < ⟦x₁ * y₁⟧ + ⟦x₂ * y₂⟧ ↔ ⟦y₁ * x₂⟧ + ⟦y₂ * x₁⟧ < ⟦y₁ * x₁⟧ + ⟦y₂ * x₂⟧

Tactic:
congr! 2 <;> rw [quot_mul_comm]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem exists_insert_toList_zoom_node {t : RBNode α} (ht : Balanced t c n)
    (e : zoom (cmp v) t = (node c' l v' r, p)) :
    ∃ L R, t.toList = L ++ v' :: R ∧ (t.insert cmp v).toList = L ++ v :: R

Proof state:
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
c' : RBColor
l : RBNode α
v' : α
r : RBNode α
p : Path α
v : α
t : RBNode α
ht : t.Balanced c n
e : zoom (cmp v) t = (node c' l v' r, p)
⊢ t.toList = p.listL ++ l.toList ++ v' :: (r.toList ++ p.listR) ∧
    (insert cmp t v).toList = p.listL ++ l.toList ++ v :: (r.toList ++ p.listR)

Tactic:
simp [← zoom_toList e, insert_toList_zoom_node ht e]

Result:
no goals

Proof state:
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
c' : RBColor
l : RBNode α
v' : α
r : RBNode α
p : Path α
v : α
t : RBNode α
ht : t.Balanced c n
e : zoom (cmp v) t = (node c' l v' r, p)
⊢ ∃ L R, t.toList = L ++ v' :: R ∧ (insert cmp t v).toList = L ++ v :: R

Tactic:
refine ⟨p.listL ++ l.toList, r.toList ++ p.listR, ?_⟩

Result:
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
c' : RBColor
l : RBNode α
v' : α
r : RBNode α
p : Path α
v : α
t : RBNode α
ht : t.Balanced c n
e : zoom (cmp v) t = (node c' l v' r, p)
⊢ t.toList = p.listL ++ l.toList ++ v' :: (r.toList ++ p.listR) ∧
    (insert cmp t v).toList = p.listL ++ l.toList ++ v :: (r.toList ++ p.listR)
-- Mathlib/Algebra/Lie/Semisimple/Basic.lean
theorem subsingleton_of_hasTrivialRadical_lie_abelian [HasTrivialRadical R L] [h : IsLieAbelian L] :
    Subsingleton L

Proof state:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : HasTrivialRadical R L
h : IsLieAbelian L
⊢ Subsingleton L

Tactic:
rw [isLieAbelian_iff_center_eq_top R L, center_eq_bot] at h

Result:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : HasTrivialRadical R L
h : ⊥ = ⊤
⊢ Subsingleton L

Proof state:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : HasTrivialRadical R L
h : ⊥ = ⊤
⊢ Subsingleton L

Tactic:
exact (LieSubmodule.subsingleton_iff R L L).mp (subsingleton_of_bot_eq_top h)

Result:
no goals
-- Mathlib/Computability/Partrec.lean
theorem vector_ofFn {n} {f : Fin n → α → σ} (hf : ∀ i, Computable (f i)) :
    Computable fun a => List.Vector.ofFn fun i => f i a :=
  (Partrec.vector_mOfFn hf).of_eq fun a => by simp

Proof state:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
f : Fin n → α → σ
hf : ∀ (i : Fin n), Computable (f i)
a : α
⊢ (Vector.mOfFn fun i => ↑(f i) a) = (↑fun a => List.Vector.ofFn fun i => f i a) a

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/NormedSpace/HahnBanach/Extension.lean
theorem exists_dual_vector'' (x : E) : ∃ g : E →L[𝕜] 𝕜, ‖g‖ ≤ 1 ∧ g x = ‖x‖

Proof state:
case pos
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x = 0
⊢ 0 x = ↑‖x‖

Tactic:
symm

Result:
case pos
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x = 0
⊢ ↑‖x‖ = 0 x

Proof state:
case neg.intro.intro
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : ¬x = 0
g : E →L[𝕜] 𝕜
g_norm : ‖g‖ = 1
g_eq : g x = ↑‖x‖
⊢ ∃ g, ‖g‖ ≤ 1 ∧ g x = ↑‖x‖

Tactic:
exact ⟨g, g_norm.le, g_eq⟩

Result:
no goals

Proof state:
case neg
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : ¬x = 0
⊢ ∃ g, ‖g‖ ≤ 1 ∧ g x = ↑‖x‖

Tactic:
rcases exists_dual_vector 𝕜 x hx with ⟨g, g_norm, g_eq⟩

Result:
case neg.intro.intro
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : ¬x = 0
g : E →L[𝕜] 𝕜
g_norm : ‖g‖ = 1
g_eq : g x = ↑‖x‖
⊢ ∃ g, ‖g‖ ≤ 1 ∧ g x = ↑‖x‖

Proof state:
case pos
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x = 0
⊢ ↑‖x‖ = 0 x

Tactic:
simp [hx]

Result:
no goals

Proof state:
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
⊢ ∃ g, ‖g‖ ≤ 1 ∧ g x = ↑‖x‖

Tactic:
by_cases hx : x = 0

Result:
case pos
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x = 0
⊢ ∃ g, ‖g‖ ≤ 1 ∧ g x = ↑‖x‖

case neg
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : ¬x = 0
⊢ ∃ g, ‖g‖ ≤ 1 ∧ g x = ↑‖x‖

Proof state:
case pos
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x = 0
⊢ ∃ g, ‖g‖ ≤ 1 ∧ g x = ↑‖x‖

Tactic:
refine ⟨0, by simp, ?_⟩

Result:
case pos
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x = 0
⊢ 0 x = ↑‖x‖

Proof state:
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x = 0
⊢ ‖0‖ ≤ 1

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey!_eq_get!_getKey? [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :
    m.getKey! a = (m.getKey? a).get!

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.WF
a : α
⊢ m.getKey! a = (m.getKey? a).get!

Tactic:
simp_to_raw using Raw₀.getKey!_eq_get!_getKey?

Result:
no goals
-- Mathlib/Topology/Algebra/FilterBasis.lean
theorem nhds_one_eq (B : GroupFilterBasis G) :
    @nhds G B.topology (1 : G) = B.toFilterBasis.filter

Proof state:
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ 𝓝 1 = toFilterBasis.filter

Tactic:
rw [B.nhds_eq]

Result:
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ B.N 1 = toFilterBasis.filter

Proof state:
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ map (fun y => y) toFilterBasis.filter = toFilterBasis.filter

Tactic:
exact map_id

Result:
no goals

Proof state:
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ B.N 1 = toFilterBasis.filter

Tactic:
simp only [N, one_mul]

Result:
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ map (fun y => y) toFilterBasis.filter = toFilterBasis.filter
-- Mathlib/Data/Finset/Image.lean
theorem image_insert [DecidableEq α] (f : α → β) (a : α) (s : Finset α) :
    (insert a s).image f = insert (f a) (s.image f)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : α → β
a : α
s : Finset α
⊢ image f (insert a s) = insert (f a) (image f s)

Tactic:
simp only [insert_eq, image_singleton, image_union]

Result:
no goals