harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/Perm/Subperm.lean
@[simp] lemma subperm_singleton_iff : l <+~ [a] ↔ l = [] ∨ l = [a]

Proof state:
α : Type u_1
l : List α
a : α
⊢ l <+~ [a] ↔ l = [] ∨ l = [a]

Tactic:
constructor

Result:
case mp
α : Type u_1
l : List α
a : α
⊢ l <+~ [a] → l = [] ∨ l = [a]

case mpr
α : Type u_1
l : List α
a : α
⊢ l = [] ∨ l = [a] → l <+~ [a]

Proof state:
case mp.intro.intro
α : Type u_1
l : List α
a : α
s : List α
hla : s ~ [a]
h : l <+ s
⊢ l = [] ∨ l = [a]

Tactic:
rwa [perm_singleton.mp hla, sublist_singleton] at h

Result:
no goals

Proof state:
case mpr.inl
α : Type u_1
a : α
⊢ [] <+~ [a]

case mpr.inr
α : Type u_1
a : α
⊢ [a] <+~ [a]

Tactic:
exacts [nil_subperm, Subperm.refl _]

Result:
no goals

Proof state:
case mpr
α : Type u_1
l : List α
a : α
⊢ l = [] ∨ l = [a] → l <+~ [a]

Tactic:
rintro (rfl | rfl)

Result:
case mpr.inl
α : Type u_1
a : α
⊢ [] <+~ [a]

case mpr.inr
α : Type u_1
a : α
⊢ [a] <+~ [a]

Proof state:
case mp
α : Type u_1
l : List α
a : α
⊢ (∃ l_1, l_1 ~ [a] ∧ l <+ l_1) → l = [] ∨ l = [a]

Tactic:
rintro ⟨s, hla, h⟩

Result:
case mp.intro.intro
α : Type u_1
l : List α
a : α
s : List α
hla : s ~ [a]
h : l <+ s
⊢ l = [] ∨ l = [a]

Proof state:
case mp
α : Type u_1
l : List α
a : α
⊢ l <+~ [a] → l = [] ∨ l = [a]

Tactic:
rw [subperm_iff]

Result:
case mp
α : Type u_1
l : List α
a : α
⊢ (∃ l_1, l_1 ~ [a] ∧ l <+ l_1) → l = [] ∨ l = [a]
-- Mathlib/Data/Int/Init.lean
lemma succ_neg_succ (a : ℤ) : succ (-succ a) = -a

Proof state:
a : ℤ
⊢ (-a.succ).succ = -a

Tactic:
rw [neg_succ, succ_pred]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem of_findIdx?_eq_some {xs : List α} {p : α → Bool} (w : xs.findIdx? p = some i) :
    match xs[i]? with | some a => p a | none => false

Proof state:
α : Type u_1
i : Nat
xs : List α
p : α → Bool
w : findIdx? p xs = some i
⊢ match xs[i]? with
  | some a => p a = true
  | none => false = true

Tactic:
induction xs generalizing i with
| nil => simp_all
| cons x xs ih =>
  simp_all only [findIdx?_cons, Nat.zero_add]
  split at w <;> cases i <;> simp_all [succ_inj']

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  ∀ {i : Nat},
    findIdx? p xs = some i →
      match xs[i]? with
      | some a => p a = true
      | none => false = true
i : Nat
w : (if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs)) = some i
⊢ match (x :: xs)[i]? with
  | some a => p a = true
  | none => false = true

Tactic:
split at w <;> cases i <;> simp_all [succ_inj']

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Bool
i : Nat
w : findIdx? p [] = some i
⊢ match [][i]? with
  | some a => p a = true
  | none => false = true

Tactic:
simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  ∀ {i : Nat},
    findIdx? p xs = some i →
      match xs[i]? with
      | some a => p a = true
      | none => false = true
i : Nat
w : findIdx? p (x :: xs) = some i
⊢ match (x :: xs)[i]? with
  | some a => p a = true
  | none => false = true

Tactic:
simp_all only [findIdx?_cons, Nat.zero_add]

Result:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  ∀ {i : Nat},
    findIdx? p xs = some i →
      match xs[i]? with
      | some a => p a = true
      | none => false = true
i : Nat
w : (if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs)) = some i
⊢ match (x :: xs)[i]? with
  | some a => p a = true
  | none => false = true
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem le_iInf_lintegral {ι : Sort*} (f : ι → α → ℝ≥0∞) :
    ∫⁻ a, ⨅ i, f i a ∂μ ≤ ⨅ i, ∫⁻ a, f i a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_5
f : ι → α → ℝ≥0∞
⊢ ∫⁻ (a : α), (⨅ i, f i) a ∂μ ≤ ⨅ i, ∫⁻ (a : α), f i a ∂μ

Tactic:
exact (monotone_lintegral μ).map_iInf_le

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_5
f : ι → α → ℝ≥0∞
⊢ ∫⁻ (a : α), ⨅ i, f i a ∂μ ≤ ⨅ i, ∫⁻ (a : α), f i a ∂μ

Tactic:
simp only [← iInf_apply]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_5
f : ι → α → ℝ≥0∞
⊢ ∫⁻ (a : α), (⨅ i, f i) a ∂μ ≤ ⨅ i, ∫⁻ (a : α), f i a ∂μ
-- Mathlib/GroupTheory/Index.lean
theorem mul_mem_iff_of_index_two (h : H.index = 2) {a b : G} : a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

Tactic:
by_cases ha : a ∈ H

Result:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∈ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

Proof state:
case neg.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∉ H
c : G
hc : ∀ (b : G), Xor' (b * c ∈ H) (b ∈ H)
⊢ a * b ∈ H

Tactic:
refine (hc _).or.resolve_left ?_

Result:
case neg.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∉ H
c : G
hc : ∀ (b : G), Xor' (b * c ∈ H) (b ∈ H)
⊢ a * b * c ∉ H

Proof state:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∉ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

Tactic:
simp only [ha, hb, iff_true]

Result:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∉ H
⊢ a * b ∈ H

Proof state:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∈ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

Tactic:
simp only [hb, iff_true, mul_mem_cancel_right hb]

Result:
no goals

Proof state:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∉ H
⊢ a * b ∈ H

Tactic:
rcases index_eq_two_iff.1 h with ⟨c, hc⟩

Result:
case neg.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∉ H
c : G
hc : ∀ (b : G), Xor' (b * c ∈ H) (b ∈ H)
⊢ a * b ∈ H

Proof state:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∈ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

Tactic:
simp only [ha, true_iff, mul_mem_cancel_left ha]

Result:
no goals

Proof state:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

Tactic:
by_cases hb : b ∈ H

Result:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∈ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∉ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

Proof state:
case neg.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∉ H
c : G
hc : ∀ (b : G), Xor' (b * c ∈ H) (b ∈ H)
⊢ a * b * c ∉ H

Tactic:
rwa [mul_assoc, mul_mem_cancel_right ((hc _).or.resolve_right hb)]

Result:
no goals
-- Mathlib/Data/Multiset/Filter.lean
lemma card_filter_le_iff (s : Multiset α) (P : α → Prop) [DecidablePred P] (n : ℕ) :
    card (s.filter P) ≤ n ↔ ∀ s' ≤ s, n < card s' → ∃ a ∈ s', ¬ P a

Proof state:
case mp
α : Type u_1
s : Multiset α
P : α → Prop
inst✝ : DecidablePred P
n : ℕ
⊢ (filter P s).card ≤ n → ∀ s' ≤ s, n < s'.card → ∃ a ∈ s', ¬P a

Tactic:
intro H s' hs' s'_card

Result:
case mp
α : Type u_1
s : Multiset α
P : α → Prop
inst✝ : DecidablePred P
n : ℕ
H : (filter P s).card ≤ n
s' : Multiset α
hs' : s' ≤ s
s'_card : n < s'.card
⊢ ∃ a ∈ s', ¬P a

Proof state:
α : Type u_1
s : Multiset α
P : α → Prop
inst✝ : DecidablePred P
n : ℕ
⊢ (filter P s).card ≤ n ↔ ∀ s' ≤ s, n < s'.card → ∃ a ∈ s', ¬P a

Tactic:
fconstructor

Result:
case mp
α : Type u_1
s : Multiset α
P : α → Prop
inst✝ : DecidablePred P
n : ℕ
⊢ (filter P s).card ≤ n → ∀ s' ≤ s, n < s'.card → ∃ a ∈ s', ¬P a

case mpr
α : Type u_1
s : Multiset α
P : α → Prop
inst✝ : DecidablePred P
n : ℕ
⊢ (∀ s' ≤ s, n < s'.card → ∃ a ∈ s', ¬P a) → (filter P s).card ≤ n

Proof state:
case mp
α : Type u_1
s : Multiset α
P : α → Prop
inst✝ : DecidablePred P
n : ℕ
H : (filter P s).card ≤ n
s' : Multiset α
hs' : s' ≤ s
s'_card : n < s'.card
rid : ∀ a ∈ s', P a
card : (filter P s').card ≤ n
⊢ False

Tactic:
exact s'_card.not_le (filter_eq_self.mpr rid ▸ card)

Result:
no goals

Proof state:
case mpr
α : Type u_1
s : Multiset α
P : α → Prop
inst✝ : DecidablePred P
n : ℕ
⊢ n < (filter P s).card → ∃ s' ≤ s, n < s'.card ∧ ∀ a ∈ s', P a

Tactic:
exact fun H ↦ ⟨s.filter P, filter_le _ _, H, fun a ha ↦ (mem_filter.mp ha).2⟩

Result:
no goals

Proof state:
case mp
α : Type u_1
s : Multiset α
P : α → Prop
inst✝ : DecidablePred P
n : ℕ
H : (filter P s).card ≤ n
s' : Multiset α
hs' : s' ≤ s
s'_card : n < s'.card
⊢ ∃ a ∈ s', ¬P a

Tactic:
by_contra! rid

Result:
case mp
α : Type u_1
s : Multiset α
P : α → Prop
inst✝ : DecidablePred P
n : ℕ
H : (filter P s).card ≤ n
s' : Multiset α
hs' : s' ≤ s
s'_card : n < s'.card
rid : ∀ a ∈ s', P a
⊢ False

Proof state:
case mpr
α : Type u_1
s : Multiset α
P : α → Prop
inst✝ : DecidablePred P
n : ℕ
⊢ (∀ s' ≤ s, n < s'.card → ∃ a ∈ s', ¬P a) → (filter P s).card ≤ n

Tactic:
contrapose!

Result:
case mpr
α : Type u_1
s : Multiset α
P : α → Prop
inst✝ : DecidablePred P
n : ℕ
⊢ n < (filter P s).card → ∃ s' ≤ s, n < s'.card ∧ ∀ a ∈ s', P a

Proof state:
case mp
α : Type u_1
s : Multiset α
P : α → Prop
inst✝ : DecidablePred P
n : ℕ
H : (filter P s).card ≤ n
s' : Multiset α
hs' : s' ≤ s
s'_card : n < s'.card
rid : ∀ a ∈ s', P a
⊢ False

Tactic:
have card := card_le_card (monotone_filter_left P hs') |>.trans H

Result:
case mp
α : Type u_1
s : Multiset α
P : α → Prop
inst✝ : DecidablePred P
n : ℕ
H : (filter P s).card ≤ n
s' : Multiset α
hs' : s' ≤ s
s'_card : n < s'.card
rid : ∀ a ∈ s', P a
card : (filter P s').card ≤ n
⊢ False
-- Mathlib/Data/Multiset/Filter.lean
theorem filterMap_eq_filter : filterMap (Option.guard p) = filter p :=
  funext fun s =>
    Quot.inductionOn s fun l => congr_arg ofList <| by
      rw [← List.filterMap_eq_filter]
      congr; funext a; simp

Proof state:
case e_f.h
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
a : α
⊢ Option.guard p a = Option.guard (fun x => decide (p x) = true) a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
⊢ List.filterMap (Option.guard p) l = List.filterMap (Option.guard fun x => decide (p x) = true) l

Tactic:
congr

Result:
case e_f
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
⊢ Option.guard p = Option.guard fun x => decide (p x) = true

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
⊢ List.filterMap (Option.guard p) l = List.filter (fun b => decide (p b)) l

Tactic:
rw [← List.filterMap_eq_filter]

Result:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
⊢ List.filterMap (Option.guard p) l = List.filterMap (Option.guard fun x => decide (p x) = true) l

Proof state:
case e_f
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
⊢ Option.guard p = Option.guard fun x => decide (p x) = true

Tactic:
funext a

Result:
case e_f.h
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
a : α
⊢ Option.guard p a = Option.guard (fun x => decide (p x) = true) a
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem map_injective (hf : Function.Injective f) :
    Function.Injective (map f : MvPolynomial σ R → MvPolynomial σ S₁)

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
hf : Injective ⇑f
p q : MvPolynomial σ R
h : ∀ (m : σ →₀ ℕ), f (coeff m p) = f (coeff m q)
m : σ →₀ ℕ
⊢ coeff m p = coeff m q

Tactic:
exact hf (h m)

Result:
no goals

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
hf : Injective ⇑f
⊢ Injective ⇑(map f)

Tactic:
intro p q h

Result:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
hf : Injective ⇑f
p q : MvPolynomial σ R
h : (map f) p = (map f) q
⊢ p = q

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
hf : Injective ⇑f
p q : MvPolynomial σ R
h : (map f) p = (map f) q
⊢ p = q

Tactic:
simp only [MvPolynomial.ext_iff, coeff_map] at h ⊢

Result:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
hf : Injective ⇑f
p q : MvPolynomial σ R
h : ∀ (m : σ →₀ ℕ), f (coeff m p) = f (coeff m q)
⊢ ∀ (m : σ →₀ ℕ), coeff m p = coeff m q

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
hf : Injective ⇑f
p q : MvPolynomial σ R
h : ∀ (m : σ →₀ ℕ), f (coeff m p) = f (coeff m q)
⊢ ∀ (m : σ →₀ ℕ), coeff m p = coeff m q

Tactic:
intro m

Result:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
hf : Injective ⇑f
p q : MvPolynomial σ R
h : ∀ (m : σ →₀ ℕ), f (coeff m p) = f (coeff m q)
m : σ →₀ ℕ
⊢ coeff m p = coeff m q
-- Mathlib/Data/Part.lean
theorem ne_none_iff {o : Part α} : o ≠ none ↔ ∃ x, o = some x

Proof state:
case mp
α : Type u_1
o : Part α
⊢ o ≠ none → ∃ x, o = some x

Tactic:
rw [Ne, eq_none_iff', not_not]

Result:
case mp
α : Type u_1
o : Part α
⊢ o.Dom → ∃ x, o = some x

Proof state:
α : Type u_1
o : Part α
⊢ o ≠ none ↔ ∃ x, o = some x

Tactic:
constructor

Result:
case mp
α : Type u_1
o : Part α
⊢ o ≠ none → ∃ x, o = some x

case mpr
α : Type u_1
o : Part α
⊢ (∃ x, o = some x) → o ≠ none

Proof state:
case mp
α : Type u_1
o : Part α
⊢ o.Dom → ∃ x, o = some x

Tactic:
exact fun h => ⟨o.get h, eq_some_iff.2 (get_mem h)⟩

Result:
no goals

Proof state:
case mpr.intro
α : Type u_1
x : α
⊢ some x ≠ none

Tactic:
apply some_ne_none

Result:
no goals

Proof state:
case mpr
α : Type u_1
o : Part α
⊢ (∃ x, o = some x) → o ≠ none

Tactic:
rintro ⟨x, rfl⟩

Result:
case mpr.intro
α : Type u_1
x : α
⊢ some x ≠ none
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey_insertEntryIfNew [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
    {k a : α} {v : β k} {h} : getKey a (insertEntryIfNew k v l) h =
    if h' : k == a ∧ containsKey k l = false then k
    else getKey a l (containsKey_of_containsKey_insertEntryIfNew' h h')

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey a (insertEntryIfNew k v l) = true
⊢ getKey a (insertEntryIfNew k v l) h = if h' : (k == a) = true ∧ containsKey k l = false then k else getKey a l ⋯

Tactic:
rw [← Option.some_inj, ← getKey?_eq_some_getKey, apply_dite Option.some,
  getKey?_insertEntryIfNew, ← dite_eq_ite]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey a (insertEntryIfNew k v l) = true
⊢ (if x : (k == a) = true ∧ containsKey k l = false then some k else getKey? a l) =
    if h : (k == a) = true ∧ containsKey k l = false then some k else some (getKey a l ⋯)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey a (insertEntryIfNew k v l) = true
⊢ (if x : (k == a) = true ∧ containsKey k l = false then some k else getKey? a l) =
    if h : (k == a) = true ∧ containsKey k l = false then some k else some (getKey a l ⋯)

Tactic:
simp [← getKey?_eq_some_getKey]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Iic_inter_Iic {a b : α} : Iic a ∩ Iic b = Iic (a ⊓ b)

Proof state:
case h
α : Type u_1
inst✝ : SemilatticeInf α
a b x : α
⊢ x ∈ Iic a ∩ Iic b ↔ x ∈ Iic (a ⊓ b)

Tactic:
simp [Iic]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : SemilatticeInf α
a b : α
⊢ Iic a ∩ Iic b = Iic (a ⊓ b)

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝ : SemilatticeInf α
a b x : α
⊢ x ∈ Iic a ∩ Iic b ↔ x ∈ Iic (a ⊓ b)
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem iUnion_Ioc_intCast : ⋃ n : ℤ, Ioc (n : α) (n + 1) = Set.univ

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Archimedean α
⊢ ⋃ n, Ioc (↑n) (↑n + 1) = univ

Tactic:
simpa only [zero_add] using iUnion_Ioc_add_intCast (0 : α)

Result:
no goals
-- Mathlib/MeasureTheory/Measure/SeparableMeasure.lean
theorem isSeparable_of_sigmaFinite [CountablyGenerated X] [SigmaFinite μ] :
    IsSeparable μ where
  exists_countable_measureDense

Proof state:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst✝¹ : CountablyGenerated X
inst✝ : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) := countableGeneratingSet X ∪ {x | ∃ n, μ.toFiniteSpanningSetsIn.set n = x}
count_𝒜 : 𝒜.Countable
⊢ ∃ 𝒜, 𝒜.Countable ∧ μ.MeasureDense 𝒜

Tactic:
refine ⟨generateSetAlgebra 𝒜, countable_generateSetAlgebra count_𝒜,
  Measure.MeasureDense.of_generateFrom_isSetAlgebra_sigmaFinite isSetAlgebra_generateSetAlgebra
  { set := μ.toFiniteSpanningSetsIn.set
    set_mem := fun n ↦ self_subset_generateSetAlgebra (𝒜 := 𝒜) <| Or.inr ⟨n, rfl⟩
    finite := μ.toFiniteSpanningSetsIn.finite
    spanning := μ.toFiniteSpanningSetsIn.spanning }
  (le_antisymm ?_ (generateFrom_le (fun s hs ↦ ?_)))⟩

Result:
case refine_1
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst✝¹ : CountablyGenerated X
inst✝ : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) := countableGeneratingSet X ∪ {x | ∃ n, μ.toFiniteSpanningSetsIn.set n = x}
count_𝒜 : 𝒜.Countable
⊢ m ≤ MeasurableSpace.generateFrom (generateSetAlgebra 𝒜)

case refine_2
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst✝¹ : CountablyGenerated X
inst✝ : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) := countableGeneratingSet X ∪ {x | ∃ n, μ.toFiniteSpanningSetsIn.set n = x}
count_𝒜 : 𝒜.Countable
s : Set X
hs : s ∈ generateSetAlgebra 𝒜
⊢ MeasurableSet s

Proof state:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst✝¹ : CountablyGenerated X
inst✝ : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
⊢ ∃ 𝒜, 𝒜.Countable ∧ μ.MeasureDense 𝒜

Tactic:
let 𝒜 := (countableGeneratingSet X) ∪ {μ.toFiniteSpanningSetsIn.set n | n : ℕ}

Result:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst✝¹ : CountablyGenerated X
inst✝ : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) := countableGeneratingSet X ∪ {x | ∃ n, μ.toFiniteSpanningSetsIn.set n = x}
⊢ ∃ 𝒜, 𝒜.Countable ∧ μ.MeasureDense 𝒜
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem eq_cycleOf_of_mem_cycleFactorsFinset_iff
    (g c : Perm α) (hc : c ∈ g.cycleFactorsFinset) (x : α) :
    c = g.cycleOf x ↔ x ∈ c.support

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
x : α
⊢ c = g.cycleOf x → x ∈ c.support

Tactic:
rintro rfl

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
hc : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ x ∈ (g.cycleOf x).support

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
hc : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ x ∈ (g.cycleOf x).support

Tactic:
rw [mem_support, cycleOf_apply_self, ne_eq, ← cycleOf_eq_one_iff]

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
hc : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ ¬g.cycleOf x = 1

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
hc : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ ¬g.cycleOf x = 1

Tactic:
exact (mem_cycleFactorsFinset_iff.mp hc).left.ne_one

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Primitive.lean
theorem IsPreprimitive.of_surjective [IsPreprimitive M α] (hf : Function.Surjective f) :
    IsPreprimitive N β where
  toIsPretransitive := toIsPretransitive.of_surjective_map hf
  isTrivialBlock_of_isBlock {B} hB

Proof state:
M : Type u_3
inst✝⁴ : Group M
α : Type u_4
inst✝³ : MulAction M α
N : Type u_5
β : Type u_6
inst✝² : Group N
inst✝¹ : MulAction N β
φ : M →* N
f : α →ₑ[⇑φ] β
inst✝ : IsPreprimitive M α
hf : Function.Surjective ⇑f
B : Set β
hB : IsBlock N B
⊢ IsTrivialBlock B

Tactic:
rw [← Set.image_preimage_eq B hf]

Result:
M : Type u_3
inst✝⁴ : Group M
α : Type u_4
inst✝³ : MulAction M α
N : Type u_5
β : Type u_6
inst✝² : Group N
inst✝¹ : MulAction N β
φ : M →* N
f : α →ₑ[⇑φ] β
inst✝ : IsPreprimitive M α
hf : Function.Surjective ⇑f
B : Set β
hB : IsBlock N B
⊢ IsTrivialBlock (⇑f '' (⇑f ⁻¹' B))

Proof state:
M : Type u_3
inst✝⁴ : Group M
α : Type u_4
inst✝³ : MulAction M α
N : Type u_5
β : Type u_6
inst✝² : Group N
inst✝¹ : MulAction N β
φ : M →* N
f : α →ₑ[⇑φ] β
inst✝ : IsPreprimitive M α
hf : Function.Surjective ⇑f
B : Set β
hB : IsBlock N B
⊢ IsTrivialBlock (⇑f '' (⇑f ⁻¹' B))

Tactic:
apply IsTrivialBlock.image hf

Result:
M : Type u_3
inst✝⁴ : Group M
α : Type u_4
inst✝³ : MulAction M α
N : Type u_5
β : Type u_6
inst✝² : Group N
inst✝¹ : MulAction N β
φ : M →* N
f : α →ₑ[⇑φ] β
inst✝ : IsPreprimitive M α
hf : Function.Surjective ⇑f
B : Set β
hB : IsBlock N B
⊢ IsTrivialBlock (⇑f ⁻¹' B)

Proof state:
M : Type u_3
inst✝⁴ : Group M
α : Type u_4
inst✝³ : MulAction M α
N : Type u_5
β : Type u_6
inst✝² : Group N
inst✝¹ : MulAction N β
φ : M →* N
f : α →ₑ[⇑φ] β
inst✝ : IsPreprimitive M α
hf : Function.Surjective ⇑f
B : Set β
hB : IsBlock N B
⊢ IsTrivialBlock (⇑f ⁻¹' B)

Tactic:
exact isTrivialBlock_of_isBlock (IsBlock.preimage f hB)

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean
theorem quadraticChar_isQuadratic : (quadraticChar F).IsQuadratic

Proof state:
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a = 0
⊢ (quadraticChar F) a = 0 ∨ (quadraticChar F) a = 1 ∨ (quadraticChar F) a = -1

Tactic:
left

Result:
case pos.h
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a = 0
⊢ (quadraticChar F) a = 0

Proof state:
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬a = 0
⊢ (quadraticChar F) a = 0 ∨ (quadraticChar F) a = 1 ∨ (quadraticChar F) a = -1

Tactic:
right

Result:
case neg.h
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬a = 0
⊢ (quadraticChar F) a = 1 ∨ (quadraticChar F) a = -1

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
⊢ (quadraticChar F) a = 0 ∨ (quadraticChar F) a = 1 ∨ (quadraticChar F) a = -1

Tactic:
by_cases ha : a = 0

Result:
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a = 0
⊢ (quadraticChar F) a = 0 ∨ (quadraticChar F) a = 1 ∨ (quadraticChar F) a = -1

case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬a = 0
⊢ (quadraticChar F) a = 0 ∨ (quadraticChar F) a = 1 ∨ (quadraticChar F) a = -1

Proof state:
case pos.h
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a = 0
⊢ (quadraticChar F) 0 = 0

Tactic:
exact quadraticChar_zero

Result:
no goals

Proof state:
case pos.h
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a = 0
⊢ (quadraticChar F) a = 0

Tactic:
rw [ha]

Result:
case pos.h
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a = 0
⊢ (quadraticChar F) 0 = 0

Proof state:
case neg.h
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬a = 0
⊢ (quadraticChar F) a = 1 ∨ (quadraticChar F) a = -1

Tactic:
exact quadraticChar_dichotomy ha

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
⊢ (quadraticChar F).IsQuadratic

Tactic:
intro a

Result:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
⊢ (quadraticChar F) a = 0 ∨ (quadraticChar F) a = 1 ∨ (quadraticChar F) a = -1