harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findSome?_eq_some_iff {f : α → Option β} {l : List α} {b : β} :
    l.findSome? f = some b ↔ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ x ∈ l₁, f x = none

Proof state:
case cons.h_2
α : Type u_1
β : Type u_2
f : α → Option β
b : β
p : α
l : List α
ih : findSome? f l = some b ↔ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none
b' : Option β
h : f p = none
⊢ findSome? f l = some b ↔ ∃ l₁ a l₂, p :: l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

Tactic:
rw [ih]

Result:
case cons.h_2
α : Type u_1
β : Type u_2
f : α → Option β
b : β
p : α
l : List α
ih : findSome? f l = some b ↔ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none
b' : Option β
h : f p = none
⊢ (∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none) ↔
    ∃ l₁ a l₂, p :: l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

Proof state:
case cons.h_2.mpr.intro.intro.intro.intro.intro.nil
α : Type u_1
β : Type u_2
f : α → Option β
b : β
p : α
l : List α
ih : findSome? f l = some b ↔ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none
b' : Option β
h : f p = none
a : α
l₂ : List α
h₂ : f a = some b
h₁ : p :: l = [] ++ a :: l₂
h₃ : ∀ (x : α), x ∈ [] → f x = none
⊢ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

Tactic:
simp_all

Result:
no goals

Proof state:
case cons.h_1.mp
α : Type u_1
β : Type u_2
f : α → Option β
b : β
p : α
l : List α
ih : findSome? f l = some b ↔ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none
x✝ : Option β
b' : β
h : f p = some b'
⊢ b' = b → ∃ l₁ a, (∃ x, p :: l = l₁ ++ a :: x) ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

Tactic:
rintro rfl

Result:
case cons.h_1.mp
α : Type u_1
β : Type u_2
f : α → Option β
p : α
l : List α
x✝ : Option β
b' : β
h : f p = some b'
ih : findSome? f l = some b' ↔ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b' ∧ ∀ (x : α), x ∈ l₁ → f x = none
⊢ ∃ l₁ a, (∃ x, p :: l = l₁ ++ a :: x) ∧ f a = some b' ∧ ∀ (x : α), x ∈ l₁ → f x = none

Proof state:
case cons.h_1
α : Type u_1
β : Type u_2
f : α → Option β
b : β
p : α
l : List α
ih : findSome? f l = some b ↔ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none
x✝ : Option β
b' : β
h : f p = some b'
⊢ b' = b ↔ ∃ l₁ a, (∃ x, p :: l = l₁ ++ a :: x) ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

Tactic:
constructor

Result:
case cons.h_1.mp
α : Type u_1
β : Type u_2
f : α → Option β
b : β
p : α
l : List α
ih : findSome? f l = some b ↔ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none
x✝ : Option β
b' : β
h : f p = some b'
⊢ b' = b → ∃ l₁ a, (∃ x, p :: l = l₁ ++ a :: x) ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

case cons.h_1.mpr
α : Type u_1
β : Type u_2
f : α → Option β
b : β
p : α
l : List α
ih : findSome? f l = some b ↔ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none
x✝ : Option β
b' : β
h : f p = some b'
⊢ (∃ l₁ a, (∃ x, p :: l = l₁ ++ a :: x) ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none) → b' = b
-- Mathlib/Data/Set/Opposite.lean
theorem singleton_unop (x : αᵒᵖ) : ({x} : Set αᵒᵖ).unop = {unop x}

Proof state:
α : Type u_1
x : αᵒᵖ
⊢ {x}.unop = {unop x}

Tactic:
ext

Result:
case h
α : Type u_1
x : αᵒᵖ
x✝ : α
⊢ x✝ ∈ {x}.unop ↔ x✝ ∈ {unop x}

Proof state:
case h.mpr
α : Type u_1
x : αᵒᵖ
x✝ : α
⊢ x✝ ∈ {unop x} → x✝ ∈ {x}.unop

Tactic:
apply unop_injective

Result:
no goals

Proof state:
case h.mp
α : Type u_1
x : αᵒᵖ
x✝ : α
⊢ x✝ ∈ {x}.unop → x✝ ∈ {unop x}

Tactic:
apply op_injective

Result:
no goals

Proof state:
case h
α : Type u_1
x : αᵒᵖ
x✝ : α
⊢ x✝ ∈ {x}.unop ↔ x✝ ∈ {unop x}

Tactic:
constructor

Result:
case h.mp
α : Type u_1
x : αᵒᵖ
x✝ : α
⊢ x✝ ∈ {x}.unop → x✝ ∈ {unop x}

case h.mpr
α : Type u_1
x : αᵒᵖ
x✝ : α
⊢ x✝ ∈ {unop x} → x✝ ∈ {x}.unop
-- Mathlib/Algebra/Exact.lean
lemma LinearEquiv.conj_exact_iff_exact (e : N ≃ₗ[R] N') :
    Function.Exact (e ∘ₗ f) (g ∘ₗ (e.symm : N' →ₗ[R] N)) ↔ Exact f g

Proof state:
R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_5
P : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid N'
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
e : N ≃ₗ[R] N'
⊢ Submodule.map (↑e) (LinearMap.ker g) = Submodule.map (↑e) (LinearMap.range f) ↔ LinearMap.ker g = LinearMap.range f

Tactic:
exact (Submodule.map_injective_of_injective e.injective).eq_iff

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_5
P : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid N'
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
e : N ≃ₗ[R] N'
⊢ Exact ⇑(↑e ∘ₗ f) ⇑(g ∘ₗ ↑e.symm) ↔ Exact ⇑f ⇑g

Tactic:
simp_rw [LinearMap.exact_iff, LinearMap.ker_comp, ← e.map_eq_comap, LinearMap.range_comp]

Result:
R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_5
P : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid N'
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
e : N ≃ₗ[R] N'
⊢ Submodule.map (↑e) (LinearMap.ker g) = Submodule.map (↑e) (LinearMap.range f) ↔ LinearMap.ker g = LinearMap.range f
-- Mathlib/NumberTheory/Transcendental/Liouville/Basic.lean
theorem irrational {x : ℝ} (h : Liouville x) : Irrational x

Proof state:
a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (↑a / ↑b)
p q : ℤ
q1 : 1 < q
a0 : ↑a / ↑b ≠ ↑p / ↑q
a1 : |↑a / ↑b - ↑p / ↑q| < 1 / ↑q ^ (b + 1)
qR0 : 0 < ↑q
b0 : ↑b ≠ 0
bq0 : 0 < ↑b * ↑q
⊢ |a * q - ↑b * p| * q ^ (b + 1) < ↑b * q

Tactic:
rw [div_sub_div _ _ b0 qR0.ne', abs_div, div_lt_div_iff₀ (abs_pos.mpr bq0.ne') (pow_pos qR0 _),
  abs_of_pos bq0, one_mul] at a1

Result:
a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (↑a / ↑b)
p q : ℤ
q1 : 1 < q
a0 : ↑a / ↑b ≠ ↑p / ↑q
a1 : |↑a * ↑q - ↑b * ↑p| * ↑q ^ (b + 1) < ↑b * ↑q
qR0 : 0 < ↑q
b0 : ↑b ≠ 0
bq0 : 0 < ↑b * ↑q
⊢ |a * q - ↑b * p| * q ^ (b + 1) < ↑b * q

Proof state:
a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (↑a / ↑b)
p q : ℤ
q1 : 1 < q
a0 : ↑a / ↑b ≠ ↑p / ↑q
a1 : |↑a * ↑q - ↑b * ↑p| * ↑q ^ (b + 1) < ↑b * ↑q
qR0 : 0 < ↑q
b0 : ↑b ≠ 0
bq0 : 0 < ↑b * ↑q
⊢ |a * q - ↑b * p| * q ^ (b + 1) < ↑b * q

Tactic:
exact mod_cast a1

Result:
no goals

Proof state:
case intro.mk'.intro.intro.intro.intro
a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (↑a / ↑b)
p q : ℤ
q1 : 1 < q
a0 : ↑a / ↑b ≠ ↑p / ↑q
a1 : |↑a / ↑b - ↑p / ↑q| < 1 / ↑q ^ (b + 1)
qR0 : 0 < ↑q
⊢ False

Tactic:
have b0 : (b : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr bN0

Result:
case intro.mk'.intro.intro.intro.intro
a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (↑a / ↑b)
p q : ℤ
q1 : 1 < q
a0 : ↑a / ↑b ≠ ↑p / ↑q
a1 : |↑a / ↑b - ↑p / ↑q| < 1 / ↑q ^ (b + 1)
qR0 : 0 < ↑q
b0 : ↑b ≠ 0
⊢ False
-- Mathlib/Topology/Path.lean
theorem truncate_one_one {a b : X} (γ : Path a b) :
    γ.truncate 1 1 = (Path.refl b).cast (by rw [min_self, γ.extend_one]) γ.extend_one

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_3
γ✝ : Path x y
a b : X
γ : Path a b
⊢ γ.extend (1 ⊓ 1) = b

Tactic:
rw [min_self, γ.extend_one]

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
⊢ γ.truncate 1 1 = (refl b).cast ⋯ ⋯

Tactic:
convert γ.truncate_self 1

Result:
no goals
-- Mathlib/Data/Finset/Sups.lean
lemma sized_compls (hn : n ≤ Fintype.card α) :
    (𝒜ᶜˢ : Set (Finset α)).Sized n ↔ (𝒜 : Set (Finset α)).Sized (Fintype.card α - n) where
  mp h𝒜

Proof state:
α : Type u_4
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
n : ℕ
hn : n ≤ Fintype.card α
h𝒜 : Set.Sized n ↑𝒜ᶜˢ
⊢ Set.Sized (Fintype.card α - n) ↑𝒜

Tactic:
simpa using h𝒜.compls

Result:
no goals

Proof state:
α : Type u_4
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
n : ℕ
hn : n ≤ Fintype.card α
h𝒜 : Set.Sized (Fintype.card α - n) ↑𝒜
⊢ Set.Sized n ↑𝒜ᶜˢ

Tactic:
simpa only [Nat.sub_sub_self hn] using h𝒜.compls

Result:
no goals
-- Mathlib/Data/List/MinMax.lean
theorem argmax_cons (f : α → β) (a : α) (l : List α) :
    argmax f (a :: l) =
      Option.casesOn (argmax f l) (some a) fun c => if f a < f c then some c else some a :=
  List.reverseRecOn l rfl fun hd tl ih => by
    rw [← cons_append, argmax_concat, ih, argmax_concat]
    rcases h : argmax f hd with - | m
    · simp [h]
    dsimp
    rw [← apply_ite, ← apply_ite]
    dsimp
    split_ifs <;> try rfl
    · exact absurd (lt_trans ‹f a < f m› ‹_›) ‹_›
    · cases (‹f a < f tl›.lt_or_lt _).elim ‹_› ‹_›

Proof state:
case some
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
⊢ Option.rec (some tl) (fun val => if f val < f tl then some tl else some val) (if f a < f m then some m else some a) =
    Option.rec (some a) (fun val => if f a < f val then some val else some a) (if f m < f tl then some tl else some m)

Tactic:
rw [← apply_ite, ← apply_ite]

Result:
case some
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
⊢ Option.rec (some tl) (fun val => if f val < f tl then some tl else some val) (some (if f a < f m then m else a)) =
    Option.rec (some a) (fun val => if f a < f val then some val else some a) (some (if f m < f tl then tl else m))

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
h✝² : f a < f m
h✝¹ : f m < f tl
h✝ : ¬f a < f tl
⊢ some tl = some a

Tactic:
exact absurd (lt_trans ‹f a < f m› ‹_›) ‹_›

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
h✝² : ¬f a < f m
h✝¹ : ¬f a < f tl
h✝ : ¬f m < f tl
⊢ some a = some a

Tactic:
rfl

Result:
no goals
-- Mathlib/Probability/Variance.lean
theorem variance_smul' {A : Type*} [CommSemiring A] [Algebra A ℝ] (c : A) (X : Ω → ℝ)
    (μ : Measure Ω) : variance (c • X) μ = c ^ 2 • variance X μ

Proof state:
case h.e'_2.e_X
Ω : Type u_1
mΩ : MeasurableSpace Ω
A : Type u_2
inst✝¹ : CommSemiring A
inst✝ : Algebra A ℝ
c : A
X : Ω → ℝ
μ : Measure Ω
⊢ c • X = (algebraMap A ℝ) c • X

Tactic:
simp only [algebraMap_smul]

Result:
no goals

Proof state:
case h.e'_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
A : Type u_2
inst✝¹ : CommSemiring A
inst✝ : Algebra A ℝ
c : A
X : Ω → ℝ
μ : Measure Ω
⊢ Var[c • X; μ] = Var[(algebraMap A ℝ) c • X; μ]

Tactic:
congr

Result:
case h.e'_2.e_X
Ω : Type u_1
mΩ : MeasurableSpace Ω
A : Type u_2
inst✝¹ : CommSemiring A
inst✝ : Algebra A ℝ
c : A
X : Ω → ℝ
μ : Measure Ω
⊢ c • X = (algebraMap A ℝ) c • X

Proof state:
case h.e'_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
A : Type u_2
inst✝¹ : CommSemiring A
inst✝ : Algebra A ℝ
c : A
X : Ω → ℝ
μ : Measure Ω
⊢ c ^ 2 • Var[X; μ] = (algebraMap A ℝ) c ^ 2 * Var[X; μ]

Tactic:
simp only [Algebra.smul_def, map_pow]

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
A : Type u_2
inst✝¹ : CommSemiring A
inst✝ : Algebra A ℝ
c : A
X : Ω → ℝ
μ : Measure Ω
⊢ Var[c • X; μ] = c ^ 2 • Var[X; μ]

Tactic:
convert variance_smul (algebraMap A ℝ c) X μ using 1

Result:
case h.e'_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
A : Type u_2
inst✝¹ : CommSemiring A
inst✝ : Algebra A ℝ
c : A
X : Ω → ℝ
μ : Measure Ω
⊢ Var[c • X; μ] = Var[(algebraMap A ℝ) c • X; μ]

case h.e'_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
A : Type u_2
inst✝¹ : CommSemiring A
inst✝ : Algebra A ℝ
c : A
X : Ω → ℝ
μ : Measure Ω
⊢ c ^ 2 • Var[X; μ] = (algebraMap A ℝ) c ^ 2 * Var[X; μ]
-- Mathlib/Data/Part.lean
theorem some_ne_none (x : α) : some x ≠ none

Proof state:
α : Type u_1
x : α
⊢ some x ≠ none

Tactic:
intro h

Result:
α : Type u_1
x : α
h : some x = none
⊢ False

Proof state:
α : Type u_1
x : α
h : some x = none
⊢ False

Tactic:
exact true_ne_false (congr_arg Dom h)

Result:
no goals
-- Mathlib/GroupTheory/Perm/List.lean
theorem formPerm_pow_length_eq_one_of_nodup (hl : Nodup l) : formPerm l ^ length l = 1

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
this : x ∉ {x | (l.formPerm ^ l.length) x ≠ x}
⊢ (l.formPerm ^ l.length) x = 1 x

Tactic:
simpa using this

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
H : x ∈ {x | l.formPerm x ≠ x}
⊢ x ∈ l

Tactic:
simpa using support_formPerm_le' _ H

Result:
no goals

Proof state:
case H
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
⊢ (l.formPerm ^ l.length) x = 1 x

Tactic:
by_cases hx : x ∈ l

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∈ l
⊢ (l.formPerm ^ l.length) x = 1 x

case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
⊢ (l.formPerm ^ l.length) x = 1 x

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
⊢ l.formPerm ^ l.length = 1

Tactic:
ext x

Result:
case H
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
⊢ (l.formPerm ^ l.length) x = 1 x

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
H : x ∈ {x | (l.formPerm ^ l.length) x ≠ x}
⊢ x ∈ l

Tactic:
replace H := set_support_zpow_subset l.formPerm l.length H

Result:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
H : x ∈ {x | l.formPerm x ≠ x}
⊢ x ∈ l

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∈ l
⊢ (l.formPerm ^ l.length) x = 1 x

Tactic:
obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx

Result:
case pos.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
⊢ (l.formPerm ^ l.length) l[k] = 1 l[k]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
H : x ∈ {x | (l.formPerm ^ l.length) x ≠ x}
⊢ False

Tactic:
refine hx ?_

Result:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
H : x ∈ {x | (l.formPerm ^ l.length) x ≠ x}
⊢ x ∈ l

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
⊢ x ∉ {x | (l.formPerm ^ l.length) x ≠ x}

Tactic:
intro H

Result:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
H : x ∈ {x | (l.formPerm ^ l.length) x ≠ x}
⊢ False

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
⊢ (l.formPerm ^ l.length) x = 1 x

Tactic:
have : x ∉ { x | (l.formPerm ^ l.length) x ≠ x } := by
  intro H
  refine hx ?_
  replace H := set_support_zpow_subset l.formPerm l.length H
  simpa using support_formPerm_le' _ H

Result:
case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
this : x ∉ {x | (l.formPerm ^ l.length) x ≠ x}
⊢ (l.formPerm ^ l.length) x = 1 x

Proof state:
case pos.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
⊢ (l.formPerm ^ l.length) l[k] = 1 l[k]

Tactic:
simp [formPerm_pow_apply_getElem _ hl, Nat.mod_eq_of_lt hk]

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem add_left_cancel_iff {a b c : PartENat} (ha : a ≠ ⊤) : a + b = a + c ↔ b = c

Proof state:
a b c : PartENat
ha : a ≠ ⊤
⊢ a + b = a + c ↔ b = c

Tactic:
rw [add_comm a, add_comm a, PartENat.add_right_cancel_iff ha]

Result:
no goals
-- Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
theorem ofHasUnitMulPowIrreducibleFactorization {R : Type u} [CommRing R] [IsDomain R]
    (hR : HasUnitMulPowIrreducibleFactorization R) : IsDiscreteValuationRing R

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
hR : HasUnitMulPowIrreducibleFactorization R
⊢ IsDiscreteValuationRing R

Tactic:
letI : UniqueFactorizationMonoid R := hR.toUniqueFactorizationMonoid

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
hR : HasUnitMulPowIrreducibleFactorization R
this : UniqueFactorizationMonoid R := HasUnitMulPowIrreducibleFactorization.toUniqueFactorizationMonoid hR
⊢ IsDiscreteValuationRing R

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
hR : HasUnitMulPowIrreducibleFactorization R
this : UniqueFactorizationMonoid R := HasUnitMulPowIrreducibleFactorization.toUniqueFactorizationMonoid hR
⊢ IsDiscreteValuationRing R

Tactic:
apply of_ufd_of_unique_irreducible _ hR.unique_irreducible

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
hR : HasUnitMulPowIrreducibleFactorization R
this : UniqueFactorizationMonoid R := HasUnitMulPowIrreducibleFactorization.toUniqueFactorizationMonoid hR
⊢ ∃ p, Irreducible p

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
hR : HasUnitMulPowIrreducibleFactorization R
this : UniqueFactorizationMonoid R := HasUnitMulPowIrreducibleFactorization.toUniqueFactorizationMonoid hR
⊢ ∃ p, Irreducible p

Tactic:
obtain ⟨p, hp, H⟩ := hR

Result:
case intro.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Irreducible p
H : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (p ^ n) x
this : UniqueFactorizationMonoid R :=
  HasUnitMulPowIrreducibleFactorization.toUniqueFactorizationMonoid (Exists.intro p ⟨hp, H⟩)
⊢ ∃ p, Irreducible p

Proof state:
case intro.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Irreducible p
H : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (p ^ n) x
this : UniqueFactorizationMonoid R :=
  HasUnitMulPowIrreducibleFactorization.toUniqueFactorizationMonoid (Exists.intro p ⟨hp, H⟩)
⊢ ∃ p, Irreducible p

Tactic:
exact ⟨p, hp⟩

Result:
no goals
-- Mathlib/Probability/Kernel/Condexp.lean
theorem _root_.MeasureTheory.StronglyMeasurable.integral_condExpKernel' [NormedSpace ℝ F]
    (hf : StronglyMeasurable f) :
    StronglyMeasurable[m ⊓ 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 : StronglyMeasurable f
a✝ : Nontrivial Ω
⊢ StronglyMeasurable fun ω => ∫ (y : Ω), f y ∂(condDistrib id id μ) (id ω)

Tactic:
exact (hf.comp_measurable measurable_snd).integral_condDistrib

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 : StronglyMeasurable f
a✝ : Nontrivial Ω
⊢ StronglyMeasurable fun ω => ∫ (y : Ω), f y ∂(condExpKernel μ m) ω

Tactic:
simp_rw [condExpKernel_apply_eq_condDistrib]

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 : StronglyMeasurable f
a✝ : Nontrivial Ω
⊢ StronglyMeasurable fun ω => ∫ (y : Ω), f y ∂(condDistrib id id μ) (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 : StronglyMeasurable f
⊢ StronglyMeasurable 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 : StronglyMeasurable f
a✝ : Nontrivial Ω
⊢ StronglyMeasurable fun ω => ∫ (y : Ω), f y ∂(condExpKernel μ m) ω
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem uniformCauchySeqOn_iff_uniformCauchySeqOnFilter :
    UniformCauchySeqOn F p s ↔ UniformCauchySeqOnFilter F p (𝓟 s)

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
⊢ UniformCauchySeqOn F p s ↔ UniformCauchySeqOnFilter F p (𝓟 s)

Tactic:
simp only [UniformCauchySeqOn, UniformCauchySeqOnFilter]

Result:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
⊢ (∀ u ∈ 𝓤 β, ∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u) ↔
    ∀ u ∈ 𝓤 β, ∀ᶠ (m : (ι × ι) × α) in (p ×ˢ p) ×ˢ 𝓟 s, (F m.1.1 m.2, F m.1.2 m.2) ∈ u

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
⊢ (∀ u ∈ 𝓤 β, ∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u) ↔
    ∀ u ∈ 𝓤 β, ∀ᶠ (m : (ι × ι) × α) in (p ×ˢ p) ×ˢ 𝓟 s, (F m.1.1 m.2, F m.1.2 m.2) ∈ u

Tactic:
refine forall₂_congr fun u hu => ?_

Result:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ (∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u) ↔
    ∀ᶠ (m : (ι × ι) × α) in (p ×ˢ p) ×ˢ 𝓟 s, (F m.1.1 m.2, F m.1.2 m.2) ∈ u

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ (∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u) ↔
    ∀ᶠ (m : (ι × ι) × α) in (p ×ˢ p) ×ˢ 𝓟 s, (F m.1.1 m.2, F m.1.2 m.2) ∈ u

Tactic:
rw [eventually_prod_principal_iff]

Result:
no goals
-- Mathlib/Topology/Homotopy/HSpaces.lean
theorem qRight_zero_right (t : I) :
    (qRight (t, 0) : ℝ) = if (t : ℝ) ≤ 1 / 2 then (2 : ℝ) * t else 1

Proof state:
case neg
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 ≤ 2 * ↑t

Tactic:
linarith

Result:
no goals

Proof state:
t : ↑I
⊢ ↑(Set.projIcc 0 1 qRight.proof_1 (2 * ↑t)) = if ↑t ≤ 1 / 2 then 2 * ↑t else 1

Tactic:
split_ifs

Result:
case pos
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ ↑(Set.projIcc 0 1 qRight.proof_1 (2 * ↑t)) = 2 * ↑t

case neg
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ ↑(Set.projIcc 0 1 qRight.proof_1 (2 * ↑t)) = 1

Proof state:
case neg
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ ↑(Set.projIcc 0 1 qRight.proof_1 (2 * ↑t)) = 1

Tactic:
rw [(Set.projIcc_eq_right _).2]

Result:
case neg
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 ≤ 2 * ↑t

t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 0 < 1

Proof state:
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ ↑t ≤ 1 / 2

Tactic:
tauto

Result:
no goals

Proof state:
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 0 < 1

Tactic:
exact zero_lt_one

Result:
no goals

Proof state:
t : ↑I
⊢ ↑(qRight (t, 0)) = if ↑t ≤ 1 / 2 then 2 * ↑t else 1

Tactic:
simp only [qRight, coe_zero, add_zero, div_one]

Result:
t : ↑I
⊢ ↑(Set.projIcc 0 1 qRight.proof_1 (2 * ↑t)) = if ↑t ≤ 1 / 2 then 2 * ↑t else 1

Proof state:
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ ↑t ∈ Set.Icc 0 (1 / 2)

Tactic:
refine ⟨t.2.1, ?_⟩

Result:
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ ↑t ≤ 1 / 2

Proof state:
case pos
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ ↑(Set.projIcc 0 1 qRight.proof_1 (2 * ↑t)) = 2 * ↑t

Tactic:
rw [Set.projIcc_of_mem _ ((mul_pos_mem_iff zero_lt_two).2 _)]

Result:
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ ↑t ∈ Set.Icc 0 (1 / 2)
-- Mathlib/LinearAlgebra/Matrix/IsDiag.lean
theorem IsDiag.isSymm [Zero α] {A : Matrix n n α} (h : A.IsDiag) : A.IsSymm

Proof state:
case a
α : Type u_1
n : Type u_4
inst✝ : Zero α
A : Matrix n n α
h : A.IsDiag
i j : n
⊢ Aᵀ i j = A i j

Tactic:
by_cases g : i = j

Result:
case pos
α : Type u_1
n : Type u_4
inst✝ : Zero α
A : Matrix n n α
h : A.IsDiag
i j : n
g : i = j
⊢ Aᵀ i j = A i j

case neg
α : Type u_1
n : Type u_4
inst✝ : Zero α
A : Matrix n n α
h : A.IsDiag
i j : n
g : ¬i = j
⊢ Aᵀ i j = A i j

Proof state:
case neg
α : Type u_1
n : Type u_4
inst✝ : Zero α
A : Matrix n n α
h : A.IsDiag
i j : n
g : ¬i = j
⊢ Aᵀ i j = A i j

Tactic:
simp [h g, h (Ne.symm g)]

Result:
no goals

Proof state:
α : Type u_1
n : Type u_4
inst✝ : Zero α
A : Matrix n n α
h : A.IsDiag
⊢ A.IsSymm

Tactic:
ext i j

Result:
case a
α : Type u_1
n : Type u_4
inst✝ : Zero α
A : Matrix n n α
h : A.IsDiag
i j : n
⊢ Aᵀ i j = A i j

Proof state:
case pos
α : Type u_1
n : Type u_4
inst✝ : Zero α
A : Matrix n n α
h : A.IsDiag
i j : n
g : i = j
⊢ Aᵀ i j = A i j

Tactic:
rw [g, transpose_apply]

Result:
no goals