harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Filter/Bases.lean
theorem hasBasis_iInf_of_directed' {ι : Type*} {ι' : ι → Sort _} [Nonempty ι] {l : ι → Filter α}
    (s : ∀ i, ι' i → Set α) (p : ∀ i, ι' i → Prop) (hl : ∀ i, (l i).HasBasis (p i) (s i))
    (h : Directed (· ≥ ·) l) :
    (⨅ i, l i).HasBasis (fun ii' : Σi, ι' i => p ii'.1 ii'.2) fun ii' => s ii'.1 ii'.2

Proof state:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
inst✝ : Nonempty ι
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun x1 x2 => x1 ≥ x2) l
⊢ (⨅ i, l i).HasBasis (fun ii' => p ii'.fst ii'.snd) fun ii' => s ii'.fst ii'.snd

Tactic:
refine ⟨fun t => ?_⟩

Result:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
inst✝ : Nonempty ι
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun x1 x2 => x1 ≥ x2) l
t : Set α
⊢ t ∈ ⨅ i, l i ↔ ∃ i, p i.fst i.snd ∧ s i.fst i.snd ⊆ t

Proof state:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
inst✝ : Nonempty ι
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun x1 x2 => x1 ≥ x2) l
t : Set α
⊢ (∃ i, t ∈ l i) ↔ ∃ a b, p ⟨a, b⟩.fst ⟨a, b⟩.snd ∧ s ⟨a, b⟩.fst ⟨a, b⟩.snd ⊆ t

Tactic:
exact exists_congr fun i => (hl i).mem_iff

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
inst✝ : Nonempty ι
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun x1 x2 => x1 ≥ x2) l
t : Set α
⊢ t ∈ ⨅ i, l i ↔ ∃ i, p i.fst i.snd ∧ s i.fst i.snd ⊆ t

Tactic:
rw [mem_iInf_of_directed h, Sigma.exists]

Result:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
inst✝ : Nonempty ι
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun x1 x2 => x1 ≥ x2) l
t : Set α
⊢ (∃ i, t ∈ l i) ↔ ∃ a b, p ⟨a, b⟩.fst ⟨a, b⟩.snd ∧ s ⟨a, b⟩.fst ⟨a, b⟩.snd ⊆ t
-- Mathlib/Topology/Instances/AddCircle.lean
theorem finite_setOf_add_order_eq {n : ℕ} (hn : 0 < n) :
    { u : AddCircle p | addOrderOf u = n }.Finite :=
  finite_coe_iff.mp <| Nat.finite_of_card_ne_zero <| by simp [hn.ne']

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
⊢ Nat.card ↑{u | addOrderOf u = n} ≠ 0

Tactic:
simp [hn.ne']

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
@[reassoc (attr := simp), elementwise (attr := simp)]
lemma toCocycles_comp_isoTwoCocycles_hom :
    toCocycles A 1 2 ≫ (isoTwoCocycles A).hom =
      (oneCochainsLequiv A).toModuleIso.hom ≫
        ModuleCat.ofHom (shortComplexH2 A).moduleCatToCycles

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ toCocycles A 1 2 ≫ (isoTwoCocycles A).hom =
    (oneCochainsLequiv A).toModuleIso.hom ≫ ModuleCat.ofHom (shortComplexH2 A).moduleCatToCycles

Tactic:
simp [isoTwoCocycles]

Result:
no goals
-- Mathlib/Algebra/Group/Conj.lean
theorem isConj_one_right {a : α} : IsConj 1 a ↔ a = 1 :=
  ⟨fun ⟨_, hc⟩ => mul_right_cancel (hc.symm.trans ((mul_one _).trans (one_mul _).symm)), fun h => by
    rw [h]⟩

Proof state:
α : Type u
inst✝ : CancelMonoid α
a : α
h : a = 1
⊢ IsConj 1 a

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Data/QPF/Univariate/Basic.lean
theorem has_good_supp_iff {α : Type u} (x : F α) :
    (∀ p, Liftp p x ↔ ∀ u ∈ supp x, p u) ↔
      ∃ a f, abs ⟨a, f⟩ = x ∧ ∀ a' f', abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ

Proof state:
F : Type u → Type u
q : QPF F
α : Type u
x : F α
⊢ (∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u) ↔
    ∃ a f, abs ⟨a, f⟩ = x ∧ ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ

Tactic:
constructor

Result:
case mp
F : Type u → Type u
q : QPF F
α : Type u
x : F α
⊢ (∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u) →
    ∃ a f, abs ⟨a, f⟩ = x ∧ ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ

case mpr
F : Type u → Type u
q : QPF F
α : Type u
x : F α
⊢ (∃ a f, abs ⟨a, f⟩ = x ∧ ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ) →
    ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u

Proof state:
case mpr.intro.intro.intro.mpr.a
F : Type u → Type u
q : QPF F
α : Type u
x : F α
a : (P F).A
f : (P F).B a → α
xeq : abs ⟨a, f⟩ = x
h : ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ
p : α → Prop
h' : ∀ u ∈ supp x, p u
i : (P F).B a
a' : (P F).A
f' : (P F).B a' → α
xeq' : abs ⟨a', f'⟩ = x
⊢ f i ∈ f' '' univ

Tactic:
apply h a' f' xeq'

Result:
case mpr.intro.intro.intro.mpr.a.a
F : Type u → Type u
q : QPF F
α : Type u
x : F α
a : (P F).A
f : (P F).B a → α
xeq : abs ⟨a, f⟩ = x
h : ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ
p : α → Prop
h' : ∀ u ∈ supp x, p u
i : (P F).B a
a' : (P F).A
f' : (P F).B a' → α
xeq' : abs ⟨a', f'⟩ = x
⊢ f i ∈ f '' univ

Proof state:
F : Type u → Type u
q : QPF F
α : Type u
x : F α
h : ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
a : (P F).A
f : (P F).B a → α
xeq : x = abs ⟨a, f⟩
h' : ∀ (i : (P F).B a), supp x (f i)
a' : (P F).A
f' : (P F).B a' → α
h'' : abs ⟨a', f'⟩ = x
u : α
i : (P F).B a
left✝ : i ∈ univ
hfi : f i = u
⊢ f i ∈ supp x

Tactic:
apply h'

Result:
no goals

Proof state:
case mpr.intro.intro.intro.mp.intro.intro.intro.intro.intro
F : Type u → Type u
q : QPF F
α : Type u
x : F α
a : (P F).A
f : (P F).B a → α
xeq : abs ⟨a, f⟩ = x
h : ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ
p : α → Prop
a' : (P F).A
f' : (P F).B a' → α
xeq' : x = abs ⟨a', f'⟩
h' : ∀ (i : (P F).B a'), p (f' i)
u : α
usuppx : u ∈ supp x
i : (P F).B a'
left✝ : i ∈ univ
f'ieq : f' i = u
⊢ p (f' i)

Tactic:
apply h'

Result:
no goals

Proof state:
case mpr
F : Type u → Type u
q : QPF F
α : Type u
x : F α
⊢ (∃ a f, abs ⟨a, f⟩ = x ∧ ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ) →
    ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u

Tactic:
rintro ⟨a, f, xeq, h⟩ p

Result:
case mpr.intro.intro.intro
F : Type u → Type u
q : QPF F
α : Type u
x : F α
a : (P F).A
f : (P F).B a → α
xeq : abs ⟨a, f⟩ = x
h : ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ
p : α → Prop
⊢ Liftp p x ↔ ∀ u ∈ supp x, p u
-- Mathlib/RingTheory/PowerSeries/Trunc.lean
theorem trunc_trunc_mul {n} (f g : R ⟦X⟧) :
    trunc n ((trunc n f) * g : R⟦X⟧) = trunc n (f * g)

Proof state:
case neg
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : ¬m < n
⊢ 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
case a
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
⊢ (if m < n then (coeff R m) (↑(trunc n f) * g) else 0) = if m < n then (coeff R m) (f * g) else 0

Tactic:
split_ifs with h

Result:
case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : m < n
⊢ (coeff R m) (↑(trunc n f) * g) = (coeff R m) (f * g)

case neg
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : ¬m < n
⊢ 0 = 0

Proof state:
case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : m < n
⊢ (coeff R m) (↑(trunc n f) * g) = (coeff R m) (f * g)

Tactic:
rw [coeff_mul, coeff_mul, sum_congr rfl]

Result:
case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : m < n
⊢ ∀ x ∈ antidiagonal m, (coeff R x.1) ↑(trunc n f) * (coeff R x.2) g = (coeff R x.1) f * (coeff R x.2) g

Proof state:
case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : m < n
x✝ : ℕ × ℕ
hab : x✝ ∈ antidiagonal m
ha : x✝.1 < n
⊢ (coeff R x✝.1) ↑(trunc n f) * (coeff R x✝.2) g = (coeff R x✝.1) f * (coeff R x✝.2) g

Tactic:
rw [coeff_coe, coeff_trunc, if_pos ha]

Result:
no goals

Proof state:
case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : m < n
x✝ : ℕ × ℕ
hab : x✝ ∈ antidiagonal m
⊢ (coeff R x✝.1) ↑(trunc n f) * (coeff R x✝.2) g = (coeff R x✝.1) f * (coeff R x✝.2) g

Tactic:
have ha := lt_of_le_of_lt (antidiagonal.fst_le hab) h

Result:
case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : m < n
x✝ : ℕ × ℕ
hab : x✝ ∈ antidiagonal m
ha : x✝.1 < n
⊢ (coeff R x✝.1) ↑(trunc n f) * (coeff R x✝.2) g = (coeff R x✝.1) f * (coeff R x✝.2) g

Proof state:
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
⊢ trunc n (↑(trunc n f) * g) = trunc n (f * g)

Tactic:
ext m

Result:
case a
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
⊢ (trunc n (↑(trunc n f) * g)).coeff m = (trunc n (f * g)).coeff m

Proof state:
case a
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
⊢ (trunc n (↑(trunc n f) * g)).coeff m = (trunc n (f * g)).coeff m

Tactic:
rw [coeff_trunc, coeff_trunc]

Result:
case a
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
⊢ (if m < n then (coeff R m) (↑(trunc n f) * g) else 0) = if m < n then (coeff R m) (f * g) else 0

Proof state:
case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : m < n
⊢ ∀ x ∈ antidiagonal m, (coeff R x.1) ↑(trunc n f) * (coeff R x.2) g = (coeff R x.1) f * (coeff R x.2) g

Tactic:
intro _ hab

Result:
case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : m < n
x✝ : ℕ × ℕ
hab : x✝ ∈ antidiagonal m
⊢ (coeff R x✝.1) ↑(trunc n f) * (coeff R x✝.2) g = (coeff R x✝.1) f * (coeff R x✝.2) g
-- Mathlib/Data/Rat/Lemmas.lean
theorem den_dvd (a b : ℤ) : ((a /. b).den : ℤ) ∣ b

Proof state:
case neg.mk'
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
⊢ d ∣ n.natAbs * b.natAbs

Tactic:
rw [← Int.natAbs_mul, ← Int.natCast_dvd_natCast, Int.dvd_natAbs, ← e]

Result:
case neg.mk'
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
⊢ ↑d ∣ a * ↑d

Proof state:
case neg
a b : ℤ
b0 : ¬b = 0
⊢ ↑(a /. b).den ∣ b

Tactic:
rcases e : a /. b with ⟨n, d, h, c⟩

Result:
case neg.mk'
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
⊢ ↑{ num := n, den := d, den_nz := h, reduced := c }.den ∣ b

Proof state:
case neg.mk'
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
⊢ ↑d ∣ a * ↑d

Tactic:
simp

Result:
no goals

Proof state:
a b : ℤ
⊢ ↑(a /. b).den ∣ b

Tactic:
by_cases b0 : b = 0

Result:
case pos
a b : ℤ
b0 : b = 0
⊢ ↑(a /. b).den ∣ b

case neg
a b : ℤ
b0 : ¬b = 0
⊢ ↑(a /. b).den ∣ b

Proof state:
case neg.mk'
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
⊢ ↑{ num := n, den := d, den_nz := h, reduced := c }.den ∣ b

Tactic:
rw [mk'_eq_divInt, divInt_eq_iff b0 (ne_of_gt (Int.natCast_pos.2 (Nat.pos_of_ne_zero h)))] at e

Result:
case neg.mk'
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
⊢ ↑{ num := n, den := d, den_nz := h, reduced := c }.den ∣ b

Proof state:
case pos
a b : ℤ
b0 : b = 0
⊢ ↑(a /. b).den ∣ b

Tactic:
simp [b0]

Result:
no goals

Proof state:
case neg.mk'
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
⊢ ↑{ num := n, den := d, den_nz := h, reduced := c }.den ∣ b

Tactic:
refine Int.dvd_natAbs.1 <| Int.natCast_dvd_natCast.2 <| c.symm.dvd_of_dvd_mul_left ?_

Result:
case neg.mk'
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
⊢ d ∣ n.natAbs * b.natAbs
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem one_lt_rootMultiplicity_iff_isRoot
    {p : R[X]} {t : R} (h : p ≠ 0) :
    1 < p.rootMultiplicity t ↔ p.IsRoot t ∧ (derivative p).IsRoot t

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
⊢ (∀ m ≤ 1, ((⇑derivative)^[m] p).IsRoot t) ↔ p.IsRoot t ∧ (derivative p).IsRoot t

Tactic:
refine ⟨fun h ↦ ⟨h 0 (by norm_num), h 1 (by norm_num)⟩, fun ⟨h0, h1⟩ m hm ↦ ?_⟩

Result:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
x✝ : p.IsRoot t ∧ (derivative p).IsRoot t
m : ℕ
hm : m ≤ 1
h0 : p.IsRoot t
h1 : (derivative p).IsRoot t
⊢ ((⇑derivative)^[m] p).IsRoot t

Proof state:
case zero
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
x✝ : p.IsRoot t ∧ (derivative p).IsRoot t
h0 : p.IsRoot t
h1 : (derivative p).IsRoot t
hm : 0 ≤ 1
⊢ ((⇑derivative)^[0] p).IsRoot t

case succ.zero
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
x✝ : p.IsRoot t ∧ (derivative p).IsRoot t
h0 : p.IsRoot t
h1 : (derivative p).IsRoot t
hm : 0 + 1 ≤ 1
⊢ ((⇑derivative)^[0 + 1] p).IsRoot t

case succ.succ
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
x✝ : p.IsRoot t ∧ (derivative p).IsRoot t
h0 : p.IsRoot t
h1 : (derivative p).IsRoot t
m : ℕ
hm : m + 1 + 1 ≤ 1
⊢ ((⇑derivative)^[m + 1 + 1] p).IsRoot t

Tactic:
exacts [h0, h1, by omega]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
x✝ : p.IsRoot t ∧ (derivative p).IsRoot t
h0 : p.IsRoot t
h1 : (derivative p).IsRoot t
m : ℕ
hm : m + 1 + 1 ≤ 1
⊢ ((⇑derivative)^[m + 1 + 1] p).IsRoot t

Tactic:
omega

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h✝ : p ≠ 0
h : ∀ m ≤ 1, ((⇑derivative)^[m] p).IsRoot t
⊢ 0 ≤ 1

Tactic:
norm_num

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h✝ : p ≠ 0
h : ∀ m ≤ 1, ((⇑derivative)^[m] p).IsRoot t
⊢ 1 ≤ 1

Tactic:
norm_num

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
⊢ 1 < rootMultiplicity t p ↔ p.IsRoot t ∧ (derivative p).IsRoot t

Tactic:
rw [one_lt_rootMultiplicity_iff_isRoot_iterate_derivative h]

Result:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
⊢ (∀ m ≤ 1, ((⇑derivative)^[m] p).IsRoot t) ↔ p.IsRoot t ∧ (derivative p).IsRoot t

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
x✝ : p.IsRoot t ∧ (derivative p).IsRoot t
m : ℕ
hm : m ≤ 1
h0 : p.IsRoot t
h1 : (derivative p).IsRoot t
⊢ ((⇑derivative)^[m] p).IsRoot t

Tactic:
obtain (_|_|m) := m

Result:
case zero
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
x✝ : p.IsRoot t ∧ (derivative p).IsRoot t
h0 : p.IsRoot t
h1 : (derivative p).IsRoot t
hm : 0 ≤ 1
⊢ ((⇑derivative)^[0] p).IsRoot t

case succ.zero
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
x✝ : p.IsRoot t ∧ (derivative p).IsRoot t
h0 : p.IsRoot t
h1 : (derivative p).IsRoot t
hm : 0 + 1 ≤ 1
⊢ ((⇑derivative)^[0 + 1] p).IsRoot t

case succ.succ
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
x✝ : p.IsRoot t ∧ (derivative p).IsRoot t
h0 : p.IsRoot t
h1 : (derivative p).IsRoot t
m : ℕ
hm : m + 1 + 1 ≤ 1
⊢ ((⇑derivative)^[m + 1 + 1] p).IsRoot t
-- Mathlib/Algebra/Polynomial/Expand.lean
theorem expand_contract' [NoZeroDivisors R] {f : R[X]} (hf : Polynomial.derivative f = 0) :
    expand R p (contract p f) = f

Proof state:
case zero
R : Type u
inst✝³ : CommSemiring R
inst✝² : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
inst✝¹ : CharZero R
inst✝ : ExpChar R 1
⊢ (expand R 1) (contract 1 f) = f

Tactic:
rw [expand_one, contract_one]

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
⊢ (expand R p) (contract p f) = f

Tactic:
obtain _ | @⟨_, hprime, hchar⟩ := ‹ExpChar R p›

Result:
case zero
R : Type u
inst✝³ : CommSemiring R
inst✝² : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
inst✝¹ : CharZero R
inst✝ : ExpChar R 1
⊢ (expand R 1) (contract 1 f) = f

case prime
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hprime : Nat.Prime p
hchar : CharP R p
⊢ (expand R p) (contract p f) = f

Proof state:
case prime
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hprime : Nat.Prime p
hchar : CharP R p
⊢ (expand R p) (contract p f) = f

Tactic:
haveI := Fact.mk hchar

Result:
case prime
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hprime : Nat.Prime p
hchar : CharP R p
this : Fact (CharP R p)
⊢ (expand R p) (contract p f) = f

Proof state:
case prime
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hprime : Nat.Prime p
hchar : CharP R p
this : Fact (CharP R p)
⊢ (expand R p) (contract p f) = f

Tactic:
exact expand_contract p hf hprime.ne_zero

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem mem_filter_iff {p : α → Bool} {a : α} {o : Option α} :
    a ∈ o.filter p ↔ a ∈ o ∧ p a

Proof state:
α : Type u_1
p : α → Bool
a : α
o : Option α
⊢ a ∈ Option.filter p o ↔ a ∈ o ∧ p a = true

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/SumTwoSquares.lean
theorem Nat.eq_sq_add_sq_iff {n : ℕ} :
    (∃ x y : ℕ, n = x ^ 2 + y ^ 2) ↔ ∀ {q : ℕ}, q.Prime → q % 4 = 3 → Even (padicValNat q n)

Proof state:
case inr.refine_2.intro.intro.intro.intro.intro
n : ℕ
hn₀ : n > 0
H : ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : a ^ 2 * b = n
hb : Squarefree b
q : ℕ
hqp : Prime q
hqb : q ∣ b
hq4 : q % 4 = 3
hqb' : padicValNat q b = 1
hqi : Fact (Prime q)
⊢ Odd (padicValNat q n)

Tactic:
simp_rw [← hab, padicValNat.mul (pow_ne_zero 2 ha₀.ne') hb₀.ne', hqb',
  padicValNat.pow 2 ha₀.ne']

Result:
case inr.refine_2.intro.intro.intro.intro.intro
n : ℕ
hn₀ : n > 0
H : ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : a ^ 2 * b = n
hb : Squarefree b
q : ℕ
hqp : Prime q
hqb : q ∣ b
hq4 : q % 4 = 3
hqb' : padicValNat q b = 1
hqi : Fact (Prime q)
⊢ Odd (2 * padicValNat q a + 1)

Proof state:
case inr.refine_1.intro.intro.intro
n : ℕ
hn₀ : n > 0
q : ℕ
hq : Prime q
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
hqb : padicValNat q b = 0
hab : a ^ 2 * b ≠ 0
⊢ Even (padicValNat q n)

Tactic:
have ha₂ := left_ne_zero_of_mul hab

Result:
case inr.refine_1.intro.intro.intro
n : ℕ
hn₀ : n > 0
q : ℕ
hq : Prime q
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
hqb : padicValNat q b = 0
hab : a ^ 2 * b ≠ 0
ha₂ : a ^ 2 ≠ 0
⊢ Even (padicValNat q n)

Proof state:
case inr.refine_2.intro.intro.intro.intro.intro
n : ℕ
hn₀ : n > 0
H : ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : a ^ 2 * b = n
hb : Squarefree b
q : ℕ
hqp : Prime q
hqb : q ∣ b
hq4 : q % 4 = 3
hqb' : padicValNat q b = 1
hqi : Fact (Prime q)
⊢ Odd (2 * padicValNat q a + 1)

Tactic:
exact odd_two_mul_add_one _

Result:
no goals

Proof state:
case inr
n : ℕ
hn₀ : n > 0
⊢ (∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)) ↔ ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)

Tactic:
refine ⟨fun H q hq h => ?_, fun H => ?_⟩

Result:
case inr.refine_1
n : ℕ
hn₀ : n > 0
H : ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)
q : ℕ
hq : Prime q
h : q % 4 = 3
⊢ Even (padicValNat q n)

case inr.refine_2
n : ℕ
hn₀ : n > 0
H : ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
⊢ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)

Proof state:
case inr.refine_1.intro.intro.intro
n : ℕ
hn₀ : n > 0
q : ℕ
hq : Prime q
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
hqb : padicValNat q b = 0
hab : a ^ 2 * b ≠ 0
ha₂ : a ^ 2 ≠ 0
ha : ¬a = 0
hb : b ≠ 0
hqi : Fact (Prime q)
⊢ Even (2 * padicValNat q a)

Tactic:
exact even_two_mul _

Result:
no goals

Proof state:
case inr.refine_1.intro.intro.intro
n : ℕ
hn₀ : n > 0
q : ℕ
hq : Prime q
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
⊢ Even (padicValNat q n)

Tactic:
have hqb := padicValNat.eq_zero_of_not_dvd fun hf =>
  (hq.mod_four_ne_three_of_dvd_isSquare_neg_one hf h₂) h

Result:
case inr.refine_1.intro.intro.intro
n : ℕ
hn₀ : n > 0
q : ℕ
hq : Prime q
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
hqb : padicValNat q b = 0
⊢ Even (padicValNat q n)
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem card_omega0_opow {a : Ordinal} (h : a ≠ 0) : card (ω ^ a) = max ℵ₀ a.card

Proof state:
a : Ordinal.{u_1}
h : a ≠ 0
⊢ (ω ^ a).card = ℵ₀ ⊔ a.card

Tactic:
rw [card_opow_eq_of_omega0_le_left le_rfl h.bot_lt, card_omega0]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SpecialFunctions/Basic.lean
lemma aemeasurable_of_aemeasurable_exp (hf : AEMeasurable (fun x ↦ exp (f x)) μ) :
    AEMeasurable f μ

Proof state:
α : Type u_1
x✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
hf : AEMeasurable (fun x => rexp (f x)) μ
⊢ f = fun x => log (rexp (f x))

Tactic:
ext

Result:
case h
α : Type u_1
x✝¹ : MeasurableSpace α
f : α → ℝ
μ : Measure α
hf : AEMeasurable (fun x => rexp (f x)) μ
x✝ : α
⊢ f x✝ = log (rexp (f x✝))

Proof state:
α : Type u_1
x✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
hf : AEMeasurable (fun x => rexp (f x)) μ
this : f = fun x => log (rexp (f x))
⊢ AEMeasurable (fun x => log (rexp (f x))) μ

Tactic:
exact measurable_log.comp_aemeasurable hf

Result:
no goals

Proof state:
case h
α : Type u_1
x✝¹ : MeasurableSpace α
f : α → ℝ
μ : Measure α
hf : AEMeasurable (fun x => rexp (f x)) μ
x✝ : α
⊢ f x✝ = log (rexp (f x✝))

Tactic:
rw [log_exp]

Result:
no goals

Proof state:
α : Type u_1
x✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
hf : AEMeasurable (fun x => rexp (f x)) μ
this : f = fun x => log (rexp (f x))
⊢ AEMeasurable f μ

Tactic:
rw [this]

Result:
α : Type u_1
x✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
hf : AEMeasurable (fun x => rexp (f x)) μ
this : f = fun x => log (rexp (f x))
⊢ AEMeasurable (fun x => log (rexp (f x))) μ

Proof state:
α : Type u_1
x✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
hf : AEMeasurable (fun x => rexp (f x)) μ
⊢ AEMeasurable f μ

Tactic:
have : f = fun x ↦ log (exp (f x)) := by ext; rw [log_exp]

Result:
α : Type u_1
x✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
hf : AEMeasurable (fun x => rexp (f x)) μ
this : f = fun x => log (rexp (f x))
⊢ AEMeasurable f μ
-- Mathlib/Algebra/Star/Unitary.lean
theorem coe_zpow (U : unitary R) (z : ℤ) : ↑(U ^ z) = (U : R) ^ z

Proof state:
R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarMul R
U : ↥(unitary R)
z : ℤ
⊢ ↑(U ^ z) = ↑U ^ z

Tactic:
cases z

Result:
case ofNat
R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarMul R
U : ↥(unitary R)
a✝ : ℕ
⊢ ↑(U ^ Int.ofNat a✝) = ↑U ^ Int.ofNat a✝

case negSucc
R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarMul R
U : ↥(unitary R)
a✝ : ℕ
⊢ ↑(U ^ Int.negSucc a✝) = ↑U ^ Int.negSucc a✝

Proof state:
case negSucc
R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarMul R
U : ↥(unitary R)
a✝ : ℕ
⊢ ↑(U ^ Int.negSucc a✝) = ↑U ^ Int.negSucc a✝

Tactic:
simp [coe_inv]

Result:
no goals

Proof state:
case ofNat
R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarMul R
U : ↥(unitary R)
a✝ : ℕ
⊢ ↑(U ^ Int.ofNat a✝) = ↑U ^ Int.ofNat a✝

Tactic:
simp [SubmonoidClass.coe_pow]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem oangle_sub_right_eq_arccos_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    o.oangle y (y - x) = Real.arccos (‖y‖ / ‖y - x‖)

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle y (y - x)).sign = 1
⊢ o.oangle y (y - x) = ↑(Real.arccos (‖y‖ / ‖y - x‖))

Tactic:
rw [o.oangle_eq_angle_of_sign_eq_one hs,
  InnerProductGeometry.angle_sub_eq_arccos_of_inner_eq_zero
    (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle y (y - x)).sign = 1

Tactic:
rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ o.oangle y (y - x) = ↑(Real.arccos (‖y‖ / ‖y - x‖))

Tactic:
have hs : (o.oangle y (y - x)).sign = 1 := by
  rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle y (y - x)).sign = 1
⊢ o.oangle y (y - x) = ↑(Real.arccos (‖y‖ / ‖y - x‖))