harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem choose_le_succ_of_lt_half_left {r n : ℕ} (h : r < n / 2) :
    choose n r ≤ choose n (r + 1)

Proof state:
case h
r n : ℕ
h : r < n / 2
⊢ r + 1 ≤ n - r

Tactic:
rw [← Nat.lt_iff_add_one_le, Nat.lt_sub_iff_add_lt, ← Nat.mul_two]

Result:
case h
r n : ℕ
h : r < n / 2
⊢ r * 2 < n

Proof state:
r n : ℕ
h : r < n / 2
⊢ n.choose (r + 1) * (r + 1) ≤ n.choose (r + 1) * (n - r)

Tactic:
apply Nat.mul_le_mul_left

Result:
case h
r n : ℕ
h : r < n / 2
⊢ r + 1 ≤ n - r

Proof state:
case h
r n : ℕ
h : r < n / 2
⊢ r * 2 < n

Tactic:
exact lt_of_lt_of_le (Nat.mul_lt_mul_of_pos_right h Nat.zero_lt_two) (n.div_mul_le_self 2)

Result:
no goals

Proof state:
r n : ℕ
h : r < n / 2
⊢ n.choose r * (n - r) ≤ n.choose (r + 1) * (n - r)

Tactic:
rw [← choose_succ_right_eq]

Result:
r n : ℕ
h : r < n / 2
⊢ n.choose (r + 1) * (r + 1) ≤ n.choose (r + 1) * (n - r)

Proof state:
r n : ℕ
h : r < n / 2
⊢ n.choose r ≤ n.choose (r + 1)

Tactic:
refine Nat.le_of_mul_le_mul_right ?_ (Nat.sub_pos_of_lt (h.trans_le (n.div_le_self 2)))

Result:
r n : ℕ
h : r < n / 2
⊢ n.choose r * (n - r) ≤ n.choose (r + 1) * (n - r)
-- Mathlib/GroupTheory/Sylow.lean
theorem IsPGroup.exists_le_sylow {P : Subgroup G} (hP : IsPGroup p P) : ∃ Q : Sylow p G, P ≤ Q :=
  Exists.elim
    (zorn_le_nonempty₀ { Q : Subgroup G | IsPGroup p Q }
      (fun c hc1 hc2 Q hQ =>
        ⟨{  carrier := ⋃ R : c, R
            one_mem' := ⟨Q, ⟨⟨Q, hQ⟩, rfl⟩, Q.one_mem⟩
            inv_mem' := fun {_} ⟨_, ⟨R, rfl⟩, hg⟩ => ⟨R, ⟨R, rfl⟩, R.1.inv_mem hg⟩
            mul_mem' := fun {_} _ ⟨_, ⟨R, rfl⟩, hg⟩ ⟨_, ⟨S, rfl⟩, hh⟩ =>
              (hc2.total R.2 S.2).elim (fun T => ⟨S, ⟨S, rfl⟩, S.1.mul_mem (T hg) hh⟩) fun T =>
                ⟨R, ⟨R, rfl⟩, R.1.mul_mem hg (T hh)⟩ },
          fun ⟨g, _, ⟨S, rfl⟩, hg⟩ => by
          refine Exists.imp (fun k hk => ?_) (hc1 S.2 ⟨g, hg⟩)
          rwa [Subtype.ext_iff, coe_pow] at hk ⊢, fun M hM _ hg => ⟨M, ⟨⟨M, hM⟩, rfl⟩, hg⟩⟩)
      P hP)
    fun {Q} h => ⟨⟨Q, h.2.prop, h.2.eq_of_ge⟩, h.1⟩

Proof state:
p : ℕ
G : Type u_1
inst✝ : Group G
P : Subgroup G
hP : IsPGroup p ↥P
c : Set (Subgroup G)
hc1 : c ⊆ {Q | IsPGroup p ↥Q}
hc2 : IsChain (fun x1 x2 => x1 ≤ x2) c
Q : Subgroup G
hQ : Q ∈ c
x✝ : ↥{ carrier := ⋃ R, ↑↑R, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
g : G
S : ↑c
hg : g ∈ (fun R => ↑↑R) S
⊢ ∃ k, ⟨g, ⋯⟩ ^ p ^ k = 1

Tactic:
refine Exists.imp (fun k hk => ?_) (hc1 S.2 ⟨g, hg⟩)

Result:
p : ℕ
G : Type u_1
inst✝ : Group G
P : Subgroup G
hP : IsPGroup p ↥P
c : Set (Subgroup G)
hc1 : c ⊆ {Q | IsPGroup p ↥Q}
hc2 : IsChain (fun x1 x2 => x1 ≤ x2) c
Q : Subgroup G
hQ : Q ∈ c
x✝ : ↥{ carrier := ⋃ R, ↑↑R, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
g : G
S : ↑c
hg : g ∈ (fun R => ↑↑R) S
k : ℕ
hk : ⟨g, hg⟩ ^ p ^ k = 1
⊢ ⟨g, ⋯⟩ ^ p ^ k = 1

Proof state:
p : ℕ
G : Type u_1
inst✝ : Group G
P : Subgroup G
hP : IsPGroup p ↥P
c : Set (Subgroup G)
hc1 : c ⊆ {Q | IsPGroup p ↥Q}
hc2 : IsChain (fun x1 x2 => x1 ≤ x2) c
Q : Subgroup G
hQ : Q ∈ c
x✝ : ↥{ carrier := ⋃ R, ↑↑R, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
g : G
S : ↑c
hg : g ∈ (fun R => ↑↑R) S
k : ℕ
hk : ⟨g, hg⟩ ^ p ^ k = 1
⊢ ⟨g, ⋯⟩ ^ p ^ k = 1

Tactic:
rwa [Subtype.ext_iff, coe_pow] at hk ⊢

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Basic.lean
theorem zero_le_orderTop_iff {x : HahnSeries Γ R} : 0 ≤ x.orderTop ↔ 0 ≤ x.order

Proof state:
case neg
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : HahnSeries Γ R
h : ¬x = 0
⊢ 0 ≤ x.orderTop ↔ 0 ≤ x.order

Tactic:
simp_all [order_of_ne h, orderTop_of_ne h, zero_lt_orderTop_iff]

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : HahnSeries Γ R
⊢ 0 ≤ x.orderTop ↔ 0 ≤ x.order

Tactic:
by_cases h : x = 0

Result:
case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : HahnSeries Γ R
h : x = 0
⊢ 0 ≤ x.orderTop ↔ 0 ≤ x.order

case neg
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : HahnSeries Γ R
h : ¬x = 0
⊢ 0 ≤ x.orderTop ↔ 0 ≤ x.order

Proof state:
case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : HahnSeries Γ R
h : x = 0
⊢ 0 ≤ x.orderTop ↔ 0 ≤ x.order

Tactic:
simp_all

Result:
no goals
-- Mathlib/RingTheory/Noetherian/Defs.lean
theorem isNoetherian_iff_fg_wellFounded :
    IsNoetherian R M ↔ WellFoundedGT { N : Submodule R M // N.FG }

Proof state:
case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
⊢ IsNoetherian R M

Tactic:
constructor

Result:
case mpr.noetherian
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
⊢ ∀ (s : Submodule R M), s.FG

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ : ∀ x ∈ {N' | ↑N' ≤ N}, ¬x > ⟨N₀, h₁⟩
h₃ : ¬N ≤ N₀
x : M
hx₁ : x ∈ N
hx₂ : x ∉ N₀
⊢ span R ↑{x} = span R {x}

Tactic:
rw [Finset.coe_singleton]

Result:
no goals

Proof state:
case mpr.noetherian
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
N : Submodule R M
⊢ N.FG

Tactic:
obtain ⟨⟨N₀, h₁⟩, e : N₀ ≤ N, h₂⟩ :=
  WellFounded.has_min H.wf { N' : α | N'.1 ≤ N } ⟨⟨⊥, Submodule.fg_bot⟩, @bot_le _ _ _ N⟩

Result:
case mpr.noetherian.intro.mk.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ : ∀ x ∈ {N' | ↑N' ≤ N}, ¬x > ⟨N₀, h₁⟩
⊢ N.FG
-- Mathlib/RingTheory/Polynomial/Selmer.lean
theorem X_pow_sub_X_sub_one_irreducible_rat (hn1 : n ≠ 1) : Irreducible (X ^ n - X - 1 : ℚ[X])

Proof state:
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
⊢ Irreducible (X ^ n - X - 1)

Tactic:
have hp : (X ^ n - X - 1 : ℤ[X]) = trinomial 0 1 n (-1) (-1) 1 := by
  simp only [trinomial, C_neg, C_1]; ring

Result:
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
⊢ Irreducible (X ^ n - X - 1)

Proof state:
case pos
n : ℕ
hn1 : n ≠ 1
hn0 : n = 0
⊢ Irreducible (X ^ n - X - 1)

Tactic:
rw [hn0, pow_zero, sub_sub, add_comm, ← sub_sub, sub_self, zero_sub]

Result:
case pos
n : ℕ
hn1 : n ≠ 1
hn0 : n = 0
⊢ Irreducible (-X)

Proof state:
n : ℕ
hn1 : n ≠ 1
⊢ Irreducible (X ^ n - X - 1)

Tactic:
by_cases hn0 : n = 0

Result:
case pos
n : ℕ
hn1 : n ≠ 1
hn0 : n = 0
⊢ Irreducible (X ^ n - X - 1)

case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
⊢ Irreducible (X ^ n - X - 1)

Proof state:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
⊢ X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1

Tactic:
simp only [trinomial, C_neg, C_1]

Result:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
⊢ X ^ n - X - 1 = -1 * X ^ 0 + -1 * X ^ 1 + 1 * X ^ n

Proof state:
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
⊢ X ^ n - X - 1 = -1 * X ^ 0 + -1 * X ^ 1 + 1 * X ^ n

Tactic:
ring

Result:
no goals

Proof state:
case neg.refine_1
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
hn : 1 < n
⊢ (X ^ n - X - 1).IsPrimitive

Tactic:
exact hp.symm ▸ (trinomial_monic zero_lt_one hn).isPrimitive

Result:
no goals

Proof state:
case neg.refine_2
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
hn : 1 < n
h : Irreducible (map (Int.castRingHom ℚ) (X ^ n - X - 1))
⊢ Irreducible (X ^ n - X - 1)

Tactic:
rwa [Polynomial.map_sub, Polynomial.map_sub, Polynomial.map_pow, Polynomial.map_one,
  Polynomial.map_X] at h

Result:
no goals

Proof state:
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
hn : 1 < n
⊢ Irreducible (X ^ n - X - 1)

Tactic:
have h := (IsPrimitive.Int.irreducible_iff_irreducible_map_cast ?_).mp
  (X_pow_sub_X_sub_one_irreducible hn1)

Result:
case neg.refine_2
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
hn : 1 < n
h : Irreducible (map (Int.castRingHom ℚ) (X ^ n - X - 1))
⊢ Irreducible (X ^ n - X - 1)

case neg.refine_1
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
hn : 1 < n
⊢ (X ^ n - X - 1).IsPrimitive

Proof state:
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
⊢ Irreducible (X ^ n - X - 1)

Tactic:
have hn : 1 < n := Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨hn0, hn1⟩

Result:
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
hn : 1 < n
⊢ Irreducible (X ^ n - X - 1)

Proof state:
case pos
n : ℕ
hn1 : n ≠ 1
hn0 : n = 0
⊢ Irreducible (-X)

Tactic:
exact Associated.irreducible ⟨-1, mul_neg_one X⟩ irreducible_X

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Rank.lean
theorem mem_range_rank_of_le {o : Ordinal} (h : o ≤ rank r a) : o ∈ Set.range (rank r)

Proof state:
α : Type u
a : α
r : α → α → Prop
hwf : IsWellFounded α r
o : Ordinal.{u}
h : o ≤ rank r a
⊢ o ∈ Set.range (rank r)

Tactic:
obtain ⟨b, hb, rfl⟩ := Acc.mem_range_rank_of_le (hwf.apply r a) h

Result:
case intro.intro
α : Type u
a : α
r : α → α → Prop
hwf : IsWellFounded α r
b : α
hb : Acc r b
h : hb.rank ≤ rank r a
⊢ hb.rank ∈ Set.range (rank r)

Proof state:
case intro.intro
α : Type u
a : α
r : α → α → Prop
hwf : IsWellFounded α r
b : α
hb : Acc r b
h : hb.rank ≤ rank r a
⊢ hb.rank ∈ Set.range (rank r)

Tactic:
exact ⟨b, rfl⟩

Result:
no goals
-- Mathlib/Probability/Process/Adapted.lean
theorem finset_prod {γ} [CommMonoid β] [ContinuousMul β] {U : γ → ι → Ω → β}
    {s : Finset γ} (h : ∀ c ∈ s, ProgMeasurable f (U c)) :
    ProgMeasurable f fun i a => ∏ c ∈ s, U c i a

Proof state:
case h.e'_9
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁴ : TopologicalSpace β
inst✝³ : Preorder ι
f : Filtration ι m
inst✝² : MeasurableSpace ι
γ : Type u_4
inst✝¹ : CommMonoid β
inst✝ : ContinuousMul β
U : γ → ι → Ω → β
s : Finset γ
h : ∀ c ∈ s, ProgMeasurable f (U c)
⊢ (fun i a => ∏ c ∈ s, U c i a) = ∏ c ∈ s, U c

Tactic:
ext (i a)

Result:
case h.e'_9.h.h
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁴ : TopologicalSpace β
inst✝³ : Preorder ι
f : Filtration ι m
inst✝² : MeasurableSpace ι
γ : Type u_4
inst✝¹ : CommMonoid β
inst✝ : ContinuousMul β
U : γ → ι → Ω → β
s : Finset γ
h : ∀ c ∈ s, ProgMeasurable f (U c)
i : ι
a : Ω
⊢ ∏ c ∈ s, U c i a = (∏ c ∈ s, U c) i a

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁴ : TopologicalSpace β
inst✝³ : Preorder ι
f : Filtration ι m
inst✝² : MeasurableSpace ι
γ : Type u_4
inst✝¹ : CommMonoid β
inst✝ : ContinuousMul β
U : γ → ι → Ω → β
s : Finset γ
h : ∀ c ∈ s, ProgMeasurable f (U c)
⊢ ProgMeasurable f fun i a => ∏ c ∈ s, U c i a

Tactic:
convert ProgMeasurable.finset_prod' h using 1

Result:
case h.e'_9
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁴ : TopologicalSpace β
inst✝³ : Preorder ι
f : Filtration ι m
inst✝² : MeasurableSpace ι
γ : Type u_4
inst✝¹ : CommMonoid β
inst✝ : ContinuousMul β
U : γ → ι → Ω → β
s : Finset γ
h : ∀ c ∈ s, ProgMeasurable f (U c)
⊢ (fun i a => ∏ c ∈ s, U c i a) = ∏ c ∈ s, U c

Proof state:
case h.e'_9.h.h
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁴ : TopologicalSpace β
inst✝³ : Preorder ι
f : Filtration ι m
inst✝² : MeasurableSpace ι
γ : Type u_4
inst✝¹ : CommMonoid β
inst✝ : ContinuousMul β
U : γ → ι → Ω → β
s : Finset γ
h : ∀ c ∈ s, ProgMeasurable f (U c)
i : ι
a : Ω
⊢ ∏ c ∈ s, U c i a = (∏ c ∈ s, U c) i a

Tactic:
simp only [Finset.prod_apply]

Result:
no goals
-- Mathlib/Data/List/Indexes.lean
theorem foldrIdx_eq_foldrIdxSpec (f : ℕ → α → β → β) (b as start) :
    foldrIdx f b as start = foldrIdxSpec f b as start

Proof state:
case cons
α : Type u
β : Type v
f : ℕ → α → β → β
b : β
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (start : ℕ), foldrIdx f b tail✝ start = foldrIdxSpec f b tail✝ start
start : ℕ
⊢ foldrIdx f b (head✝ :: tail✝) start = foldrIdxSpec f b (head✝ :: tail✝) start

Tactic:
simp only [foldrIdx, foldrIdxSpec_cons, *]

Result:
no goals

Proof state:
α : Type u
β : Type v
f : ℕ → α → β → β
b : β
as : List α
start : ℕ
⊢ foldrIdx f b as start = foldrIdxSpec f b as start

Tactic:
induction as generalizing start

Result:
case nil
α : Type u
β : Type v
f : ℕ → α → β → β
b : β
start : ℕ
⊢ foldrIdx f b [] start = foldrIdxSpec f b [] start

case cons
α : Type u
β : Type v
f : ℕ → α → β → β
b : β
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (start : ℕ), foldrIdx f b tail✝ start = foldrIdxSpec f b tail✝ start
start : ℕ
⊢ foldrIdx f b (head✝ :: tail✝) start = foldrIdxSpec f b (head✝ :: tail✝) start

Proof state:
case nil
α : Type u
β : Type v
f : ℕ → α → β → β
b : β
start : ℕ
⊢ foldrIdx f b [] start = foldrIdxSpec f b [] start

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurable_to_bool {f : α → Bool} (h : MeasurableSet (f ⁻¹' {true})) : Measurable f

Proof state:
case h
α : Type u_1
inst✝ : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ ∀ (x : Bool), MeasurableSet (f ⁻¹' {x})

Tactic:
rintro (- | -)

Result:
case h.false
α : Type u_1
inst✝ : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ MeasurableSet (f ⁻¹' {false})

case h.true
α : Type u_1
inst✝ : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ MeasurableSet (f ⁻¹' {true})

Proof state:
case h.true
α : Type u_1
inst✝ : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ MeasurableSet (f ⁻¹' {true})

Tactic:
exact h

Result:
no goals

Proof state:
case h.e'_3
α : Type u_1
inst✝ : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ f ⁻¹' {false} = (f ⁻¹' {true})ᶜ

Tactic:
rw [← preimage_compl, Bool.compl_singleton, Bool.not_true]

Result:
no goals

Proof state:
case h.false
α : Type u_1
inst✝ : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ MeasurableSet (f ⁻¹' {false})

Tactic:
convert h.compl

Result:
case h.e'_3
α : Type u_1
inst✝ : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ f ⁻¹' {false} = (f ⁻¹' {true})ᶜ

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ Measurable f

Tactic:
apply measurable_to_countable'

Result:
case h
α : Type u_1
inst✝ : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ ∀ (x : Bool), MeasurableSet (f ⁻¹' {x})
-- Mathlib/FieldTheory/Separable.lean
theorem Separable.inj_of_prod_X_sub_C [Nontrivial R] {ι : Sort _} {f : ι → R} {s : Finset ι}
    (hfs : (∏ i ∈ s, (X - C (f i))).Separable) {x y : ι} (hx : x ∈ s) (hy : y ∈ s)
    (hfxy : f x = f y) : x = y

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_1
f : ι → R
s : Finset ι
hfs : (∏ i ∈ s, (X - C (f i))).Separable
x y : ι
hx : x ∈ s
hy : y ∈ s
hfxy : f x = f y
hxy : ¬x = y
⊢ False

Tactic:
rw [← insert_erase hx, prod_insert (not_mem_erase _ _), ←
  insert_erase (mem_erase_of_ne_of_mem (Ne.symm hxy) hy), prod_insert (not_mem_erase _ _), ←
  mul_assoc, hfxy, ← sq] at hfs

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_1
f : ι → R
s : Finset ι
x y : ι
hfs : ((X - C (f y)) ^ 2 * ∏ x ∈ (s.erase x).erase y, (X - C (f x))).Separable
hx : x ∈ s
hy : y ∈ s
hfxy : f x = f y
hxy : ¬x = y
⊢ False

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_1
f : ι → R
s : Finset ι
hfs : (∏ i ∈ s, (X - C (f i))).Separable
x y : ι
hx : x ∈ s
hy : y ∈ s
hfxy : f x = f y
⊢ x = y

Tactic:
classical
by_contra hxy
rw [← insert_erase hx, prod_insert (not_mem_erase _ _), ←
  insert_erase (mem_erase_of_ne_of_mem (Ne.symm hxy) hy), prod_insert (not_mem_erase _ _), ←
  mul_assoc, hfxy, ← sq] at hfs
cases (hfs.of_mul_left.of_pow (not_isUnit_X_sub_C _) two_ne_zero).2

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_1
f : ι → R
s : Finset ι
hfs : (∏ i ∈ s, (X - C (f i))).Separable
x y : ι
hx : x ∈ s
hy : y ∈ s
hfxy : f x = f y
⊢ x = y

Tactic:
by_contra hxy

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_1
f : ι → R
s : Finset ι
hfs : (∏ i ∈ s, (X - C (f i))).Separable
x y : ι
hx : x ∈ s
hy : y ∈ s
hfxy : f x = f y
hxy : ¬x = y
⊢ False

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_1
f : ι → R
s : Finset ι
x y : ι
hfs : ((X - C (f y)) ^ 2 * ∏ x ∈ (s.erase x).erase y, (X - C (f x))).Separable
hx : x ∈ s
hy : y ∈ s
hfxy : f x = f y
hxy : ¬x = y
⊢ False

Tactic:
cases (hfs.of_mul_left.of_pow (not_isUnit_X_sub_C _) two_ne_zero).2

Result:
no goals
-- Mathlib/Order/Rel/GaloisConnection.lean
theorem rightDual_mem_leftFixedPoint (I : Set β) : R.rightDual I ∈ R.leftFixedPoints

Proof state:
case a.a
α : Type u_1
β : Type u_2
R : Rel α β
I : Set β
⊢ (fun b => ∀ ⦃a : α⦄, a ∈ R.rightDual I → R a b) ≤ I

Tactic:
exact R.gc_leftDual_rightDual.l_u_le I

Result:
no goals

Proof state:
case a
α : Type u_1
β : Type u_2
R : Rel α β
I : Set β
⊢ R.rightDual I ≤ R.rightDual (R.leftDual (R.rightDual I))

Tactic:
exact R.gc_leftDual_rightDual.le_u_l (R.rightDual I)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
R : Rel α β
I : Set β
⊢ R.rightDual I ∈ R.leftFixedPoints

Tactic:
apply le_antisymm

Result:
case a
α : Type u_1
β : Type u_2
R : Rel α β
I : Set β
⊢ R.rightDual (R.leftDual (R.rightDual I)) ≤ R.rightDual I

case a
α : Type u_1
β : Type u_2
R : Rel α β
I : Set β
⊢ R.rightDual I ≤ R.rightDual (R.leftDual (R.rightDual I))

Proof state:
case a
α : Type u_1
β : Type u_2
R : Rel α β
I : Set β
⊢ R.rightDual (R.leftDual (R.rightDual I)) ≤ R.rightDual I

Tactic:
apply R.gc_leftDual_rightDual.monotone_u

Result:
case a.a
α : Type u_1
β : Type u_2
R : Rel α β
I : Set β
⊢ (fun b => ∀ ⦃a : α⦄, a ∈ R.rightDual I → R a b) ≤ I
-- Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean
theorem irreducible_iff_prime_of_exists_prime_factors {p : α} : Irreducible p ↔ Prime p

Proof state:
case neg
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
hp0 : ¬p = 0
⊢ Irreducible p ↔ Prime p

Tactic:
refine ⟨fun h => ?_, Prime.irreducible⟩

Result:
case neg
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
hp0 : ¬p = 0
h : Irreducible p
⊢ Prime p

Proof state:
case neg
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
hp0 : ¬p = 0
h : Irreducible p
⊢ Prime p

Tactic:
obtain ⟨f, hf⟩ := pf p hp0

Result:
case neg.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
hp0 : ¬p = 0
h : Irreducible p
f : Multiset α
hf : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ p
⊢ Prime p

Proof state:
case neg.intro.intro.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
hp0 : ¬p = 0
h : Irreducible p
q : α
hq : p ~ᵤ q
hf : (∀ b ∈ {q}, Prime b) ∧ {q}.prod ~ᵤ p
⊢ Prime p

Tactic:
rw [hq.prime_iff]

Result:
case neg.intro.intro.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
hp0 : ¬p = 0
h : Irreducible p
q : α
hq : p ~ᵤ q
hf : (∀ b ∈ {q}, Prime b) ∧ {q}.prod ~ᵤ p
⊢ Prime q

Proof state:
case neg.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
hp0 : ¬p = 0
h : Irreducible p
f : Multiset α
hf : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ p
⊢ Prime p

Tactic:
obtain ⟨q, hq, rfl⟩ := prime_factors_irreducible h hf

Result:
case neg.intro.intro.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
hp0 : ¬p = 0
h : Irreducible p
q : α
hq : p ~ᵤ q
hf : (∀ b ∈ {q}, Prime b) ∧ {q}.prod ~ᵤ p
⊢ Prime p

Proof state:
case neg.intro.intro.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
hp0 : ¬p = 0
h : Irreducible p
q : α
hq : p ~ᵤ q
hf : (∀ b ∈ {q}, Prime b) ∧ {q}.prod ~ᵤ p
⊢ Prime q

Tactic:
exact hf.1 q (Multiset.mem_singleton_self _)

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
hp0 : p = 0
⊢ Irreducible p ↔ Prime p

Tactic:
simp [hp0]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
⊢ Irreducible p ↔ Prime p

Tactic:
by_cases hp0 : p = 0

Result:
case pos
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
hp0 : p = 0
⊢ Irreducible p ↔ Prime p

case neg
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
hp0 : ¬p = 0
⊢ Irreducible p ↔ Prime p
-- Mathlib/Topology/Compactness/Lindelof.lean
theorem mem_coclosed_Lindelof' : s ∈ coclosedLindelof X ↔
    ∃ t, IsClosed t ∧ IsLindelof t ∧ sᶜ ⊆ t

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ s ∈ coclosedLindelof X ↔ ∃ t, IsClosed t ∧ IsLindelof t ∧ sᶜ ⊆ t

Tactic:
simp only [mem_coclosedLindelof, compl_subset_comm]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
@[simp] lemma compProd_zero_left (κ : Kernel α β) : (0 : Measure α) ⊗ₘ κ = 0

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ 0 ⊗ₘ κ = 0

Tactic:
simp [compProd]

Result:
no goals
-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
theorem mem_centralizer_iff {s : Set A} {z : A} :
    z ∈ centralizer R s ↔ ∀ g ∈ s, g * z = z * g ∧ star g * z = z * star g

Proof state:
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : NonUnitalSemiring A
inst✝³ : StarRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
z : A
⊢ (∀ x ∈ s, x * z = z * x) → ((∀ x ∈ star s, x * z = z * x) ↔ ∀ x ∈ s, star x * z = z * star x)

Tactic:
exact fun _ =>
  ⟨fun hz a ha => hz _ (Set.star_mem_star.mpr ha), fun hz a ha => star_star a ▸ hz _ ha⟩

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : NonUnitalSemiring A
inst✝³ : StarRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
z : A
⊢ z ∈ centralizer R s ↔ ∀ g ∈ s, g * z = z * g ∧ star g * z = z * star g

Tactic:
show (∀ g ∈ s ∪ star s, g * z = z * g) ↔ ∀ g ∈ s, g * z = z * g ∧ star g * z = z * star g

Result:
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : NonUnitalSemiring A
inst✝³ : StarRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
z : A
⊢ (∀ g ∈ s ∪ star s, g * z = z * g) ↔ ∀ g ∈ s, g * z = z * g ∧ star g * z = z * star g

Proof state:
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : NonUnitalSemiring A
inst✝³ : StarRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
z : A
⊢ (∀ g ∈ s ∪ star s, g * z = z * g) ↔ ∀ g ∈ s, g * z = z * g ∧ star g * z = z * star g

Tactic:
simp only [Set.mem_union, or_imp, forall_and, and_congr_right_iff]

Result:
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : NonUnitalSemiring A
inst✝³ : StarRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
z : A
⊢ (∀ x ∈ s, x * z = z * x) → ((∀ x ∈ star s, x * z = z * x) ↔ ∀ x ∈ s, star x * z = z * star x)