harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/RootSystem/RootPositive.lean
@[simp]
lemma zero_lt_apply_root_root_iff
    (hi : P.root i ∈ span S (range P.root) := subset_span (mem_range_self i))
    (hj : P.root j ∈ span S (range P.root) := subset_span (mem_range_self j)) :
    0 < B.posForm ⟨P.root i, hi⟩ ⟨P.root j, hj⟩ ↔ 0 < P.pairingIn S i j

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹⁰ : LinearOrderedCommRing S
inst✝⁹ : CommRing R
inst✝⁸ : Algebra S R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
hi : optParam (P.root i ∈ span S (range ⇑P.root)) ⋯
hj : optParam (P.root j ∈ span S (range ⇑P.root)) ⋯
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, hi⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, hj⟩
⊢ 2 * (B.posForm ri) rj = P.pairingIn S i j * (B.posForm rj) rj

Tactic:
apply FaithfulSMul.algebraMap_injective S R

Result:
case a
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹⁰ : LinearOrderedCommRing S
inst✝⁹ : CommRing R
inst✝⁸ : Algebra S R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
hi : optParam (P.root i ∈ span S (range ⇑P.root)) ⋯
hj : optParam (P.root j ∈ span S (range ⇑P.root)) ⋯
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, hi⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, hj⟩
⊢ (algebraMap S R) (2 * (B.posForm ri) rj) = (algebraMap S R) (P.pairingIn S i j * (B.posForm rj) rj)

Proof state:
case a
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹⁰ : LinearOrderedCommRing S
inst✝⁹ : CommRing R
inst✝⁸ : Algebra S R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
hi : optParam (P.root i ∈ span S (range ⇑P.root)) ⋯
hj : optParam (P.root j ∈ span S (range ⇑P.root)) ⋯
ri : ↥(span S (range ⇑P.root)) := ⟨P.root i, hi⟩
rj : ↥(span S (range ⇑P.root)) := ⟨P.root j, hj⟩
⊢ (algebraMap S R) (2 * (B.posForm ri) rj) = (algebraMap S R) (P.pairingIn S i j * (B.posForm rj) rj)

Tactic:
simpa [map_ofNat] using two_mul_apply_root_root B i j

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem append_assoc (s t u : Seq α) : append (append s t) u = append s (append t u)

Proof state:
case cons
α : Type u
s t u s1 s2 : Seq α
h : ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u)
x✝ : α
s✝ : Seq α
⊢ ∃ s t u, s✝ = (s.append t).append u ∧ s✝ = s.append (t.append u)

Tactic:
case cons _ u => refine ⟨nil, nil, u, ?_, ?_⟩ <;> simp

Result:
no goals
-- Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean
theorem functional_equation (s : ℂ) :
    P.Λ (P.k - s) = P.ε • P.symm.Λ s

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun t => P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun t => ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin P.g s
step3 : mellin (fun t => P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = P.ε • mellin P.g s
⊢ mellin P.f (↑P.k - s) = P.ε • mellin P.g s

Tactic:
rw [← step3]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun t => P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun t => ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin P.g s
step3 : mellin (fun t => P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = P.ε • mellin P.g s
⊢ mellin P.f (↑P.k - s) = mellin (fun t => P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun t => P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun t => ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin P.g s
step3 : mellin (fun t => P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = P.ε • mellin P.g s
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (↑P.k - s - 1) • P.f t = ↑t ^ (↑P.k - s - 1) • (fun t => P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) t

Tactic:
simp_rw [P.h_feq' t ht, ← mul_smul]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun t => P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun t => ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin P.g s
step3 : mellin (fun t => P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = P.ε • mellin P.g s
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (↑P.k - s - 1) • P.f t = (↑t ^ (↑P.k - s - 1) * (P.ε * (↑t ^ (-↑P.k) * (P.ε⁻¹ * ↑(t ^ P.k))))) • P.f t

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun t => P.g (t ^ (-1))) (-s) = |(-1)|⁻¹ • mellin P.g (-s / ↑(-1))
⊢ mellin P.f (↑P.k - s) = P.ε • mellin P.g s

Tactic:
simp_rw [abs_neg, abs_one, inv_one, one_smul, ofReal_neg, ofReal_one, div_neg, div_one, neg_neg,
  rpow_neg_one, ← one_div] at step1

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun t => P.g (1 / t)) (-s) = mellin P.g s
⊢ mellin P.f (↑P.k - s) = P.ε • mellin P.g s
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
lemma pow_sub₀ (a : G₀) (ha : a ≠ 0) (h : n ≤ m) : a ^ (m - n) = a ^ m * (a ^ n)⁻¹

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
ha : a ≠ 0
h : n ≤ m
h1 : m - n + n = m
h2 : a ^ (m - n) * a ^ n = a ^ m
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹

Tactic:
simpa only [div_eq_mul_inv] using eq_div_of_mul_eq (pow_ne_zero _ ha) h2

Result:
no goals

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
ha : a ≠ 0
h : n ≤ m
h1 : m - n + n = m
⊢ a ^ (m - n) * a ^ n = a ^ m

Tactic:
rw [← pow_add, h1]

Result:
no goals

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
ha : a ≠ 0
h : n ≤ m
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹

Tactic:
have h1 : m - n + n = m := Nat.sub_add_cancel h

Result:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
ha : a ≠ 0
h : n ≤ m
h1 : m - n + n = m
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
ha : a ≠ 0
h : n ≤ m
h1 : m - n + n = m
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹

Tactic:
have h2 : a ^ (m - n) * a ^ n = a ^ m := by rw [← pow_add, h1]

Result:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
ha : a ≠ 0
h : n ≤ m
h1 : m - n + n = m
h2 : a ^ (m - n) * a ^ n = a ^ m
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem Measurable.ennreal_induction {P : (α → ℝ≥0∞) → Prop}
    (h_ind : ∀ (c : ℝ≥0∞) ⦃s⦄, MeasurableSet s → P (Set.indicator s fun _ => c))
    (h_add :
      ∀ ⦃f g : α → ℝ≥0∞⦄,
        Disjoint (support f) (support g) → Measurable f → Measurable g → P f → P g → P (f + g))
    (h_iSup :
      ∀ ⦃f : ℕ → α → ℝ≥0∞⦄, (∀ n, Measurable (f n)) → Monotone f → (∀ n, P (f n)) →
        P fun x => ⨆ n, f n x)
    ⦃f : α → ℝ≥0∞⦄ (hf : Measurable f) : P f

Proof state:
case h.e'_1.h
α : Type u_1
mα : MeasurableSpace α
P : (α → ℝ≥0∞) → Prop
h_ind : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → P (s.indicator fun x => c)
h_add : ∀ ⦃f g : α → ℝ≥0∞⦄, Disjoint (support f) (support g) → Measurable f → Measurable g → P f → P g → P (f + g)
h_iSup : ∀ ⦃f : ℕ → α → ℝ≥0∞⦄, (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), P (f n)) → P fun x => ⨆ n, f n x
f : α → ℝ≥0∞
hf : Measurable f
x✝ : α
⊢ f x✝ = ⨆ n, (eapprox f n) x✝

Tactic:
rw [iSup_eapprox_apply hf]

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
P : (α → ℝ≥0∞) → Prop
h_ind : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → P (s.indicator fun x => c)
h_add : ∀ ⦃f g : α → ℝ≥0∞⦄, Disjoint (support f) (support g) → Measurable f → Measurable g → P f → P g → P (f + g)
h_iSup : ∀ ⦃f : ℕ → α → ℝ≥0∞⦄, (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), P (f n)) → P fun x => ⨆ n, f n x
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (n : ℕ), P ⇑(eapprox f n)

Tactic:
exact fun n =>
  SimpleFunc.induction (fun c s hs => h_ind c hs)
    (fun f g hfg hf hg => h_add hfg f.measurable g.measurable hf hg) (eapprox f n)

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
P : (α → ℝ≥0∞) → Prop
h_ind : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → P (s.indicator fun x => c)
h_add : ∀ ⦃f g : α → ℝ≥0∞⦄, Disjoint (support f) (support g) → Measurable f → Measurable g → P f → P g → P (f + g)
h_iSup : ∀ ⦃f : ℕ → α → ℝ≥0∞⦄, (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), P (f n)) → P fun x => ⨆ n, f n x
f : α → ℝ≥0∞
hf : Measurable f
⊢ P f

Tactic:
convert h_iSup (fun n => (eapprox f n).measurable) (monotone_eapprox f) _ using 2

Result:
case h.e'_1.h
α : Type u_1
mα : MeasurableSpace α
P : (α → ℝ≥0∞) → Prop
h_ind : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → P (s.indicator fun x => c)
h_add : ∀ ⦃f g : α → ℝ≥0∞⦄, Disjoint (support f) (support g) → Measurable f → Measurable g → P f → P g → P (f + g)
h_iSup : ∀ ⦃f : ℕ → α → ℝ≥0∞⦄, (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), P (f n)) → P fun x => ⨆ n, f n x
f : α → ℝ≥0∞
hf : Measurable f
x✝ : α
⊢ f x✝ = ⨆ n, (eapprox f n) x✝

α : Type u_1
mα : MeasurableSpace α
P : (α → ℝ≥0∞) → Prop
h_ind : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → P (s.indicator fun x => c)
h_add : ∀ ⦃f g : α → ℝ≥0∞⦄, Disjoint (support f) (support g) → Measurable f → Measurable g → P f → P g → P (f + g)
h_iSup : ∀ ⦃f : ℕ → α → ℝ≥0∞⦄, (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), P (f n)) → P fun x => ⨆ n, f n x
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (n : ℕ), P ⇑(eapprox f n)
-- Mathlib/Algebra/Group/Center.lean
theorem centralizer_eq_top_iff_subset : centralizer S = Set.univ ↔ S ⊆ center M :=
  eq_top_iff.trans <| ⟨
    fun h _ hx ↦ Semigroup.mem_center_iff.mpr fun _ ↦ by rw [h trivial _ hx],
    fun h _ _ _ hm ↦ (h hm).comm _⟩

Proof state:
M : Type u_1
S : Set M
inst✝ : Semigroup M
h : ⊤ ≤ S.centralizer
x✝¹ : M
hx : x✝¹ ∈ S
x✝ : M
⊢ x✝ * x✝¹ = x✝¹ * x✝

Tactic:
rw [h trivial _ hx]

Result:
no goals
-- Mathlib/Algebra/Ring/Subsemiring/Basic.lean
theorem rangeS_eq_map (f : R →+* S) : f.rangeS = (⊤ : Subsemiring R).map f

Proof state:
R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
⊢ f.rangeS = Subsemiring.map f ⊤

Tactic:
ext

Result:
case h
R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
x✝ : S
⊢ x✝ ∈ f.rangeS ↔ x✝ ∈ Subsemiring.map f ⊤

Proof state:
case h
R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
x✝ : S
⊢ x✝ ∈ f.rangeS ↔ x✝ ∈ Subsemiring.map f ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem mem_of_get_eq {a} : get s = a → a ∈ s

Proof state:
α : Type u
s : Computation α
h : s.Terminates
a : α
⊢ s.get = a → a ∈ s

Tactic:
intro h

Result:
α : Type u
s : Computation α
h✝ : s.Terminates
a : α
h : s.get = a
⊢ a ∈ s

Proof state:
α : Type u
s : Computation α
h✝ : s.Terminates
a : α
h : s.get = a
⊢ s.get ∈ s

Tactic:
apply get_mem

Result:
no goals

Proof state:
α : Type u
s : Computation α
h✝ : s.Terminates
a : α
h : s.get = a
⊢ a ∈ s

Tactic:
rw [← h]

Result:
α : Type u
s : Computation α
h✝ : s.Terminates
a : α
h : s.get = a
⊢ s.get ∈ s
-- Mathlib/Data/Int/Interval.lean
theorem image_Ico_emod (n a : ℤ) (h : 0 ≤ a) : (Ico n (n + a)).image (· % a) = Ico 0 a

Proof state:
case inr.h.mpr.inl.refine_1
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n ≤ i + a * (n / a + 1)

Tactic:
rw [add_comm (n / a), mul_add, mul_one, ← add_assoc]

Result:
case inr.h.mpr.inl.refine_1
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n ≤ i + a + a * (n / a)

Proof state:
case inr.h.mpr.inl.refine_1
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hia : 0 ≤ i ∧ i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n % a ≤ i + a

Tactic:
simpa only [zero_add] using add_le_add hia.left (Int.emod_lt_of_pos n ha).le

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
@[simp]
lemma Ψ_four : W.Ψ 4 = C W.preΨ₄ * W.ψ₂

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.Ψ 4 = C W.preΨ₄ * W.ψ₂

Tactic:
rw [← Nat.cast_four, Ψ_ofNat, preΨ'_four, if_pos <| by decide]

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ Even 4

Tactic:
decide

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem Measurable.map_prod_mk_right {μ : Measure α} [SFinite μ] :
    Measurable fun y : β => map (fun x : α => (x, y)) μ

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun b => μ ((fun x => (x, b)) ⁻¹' s)

Tactic:
exact measurable_measure_prod_mk_right hs

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun b => (map (fun x => (x, b)) μ) s

Tactic:
simp_rw [map_apply measurable_prod_mk_right hs]

Result:
case h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun b => μ ((fun x => (x, b)) ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
⊢ Measurable fun y => map (fun x => (x, y)) μ

Tactic:
apply measurable_of_measurable_coe

Result:
case h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
⊢ ∀ (s : Set (α × β)), MeasurableSet s → Measurable fun b => (map (fun x => (x, b)) μ) s

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
⊢ ∀ (s : Set (α × β)), MeasurableSet s → Measurable fun b => (map (fun x => (x, b)) μ) s

Tactic:
intro s hs

Result:
case h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun b => (map (fun x => (x, b)) μ) s
-- Mathlib/NumberTheory/FLT/Three.lean
/-- We have that `S.Solution'_descent.multiplicity < S.multiplicity`. -/
lemma Solution'_descent_multiplicity_lt :
    (Solution'_descent S).multiplicity < S.multiplicity

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : 2 ≤ S.multiplicity
⊢ S.multiplicity ≠ 0

Tactic:
omega

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.multiplicity ≠ 0

Tactic:
have := S.two_le_multiplicity

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : 2 ≤ S.multiplicity
⊢ S.multiplicity ≠ 0

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.Solution'_descent.multiplicity < S.multiplicity

Tactic:
rw [Solution'_descent_multiplicity S, Nat.sub_one]

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.multiplicity.pred < S.multiplicity

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.multiplicity.pred < S.multiplicity

Tactic:
exact Nat.pred_lt <| by have := S.two_le_multiplicity; omega

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem zero_rpow_eq_iff {x : ℝ} {a : ℝ} : 0 ^ x = a ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Proof state:
case mp
x a : ℝ
hyp : (0 ^ ↑x).re = a
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
by_cases h : x = 0

Result:
case pos
x a : ℝ
hyp : (0 ^ ↑x).re = a
h : x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

case neg
x a : ℝ
hyp : (0 ^ ↑x).re = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Proof state:
case pos
a : ℝ
hyp : (0 ^ ↑0).re = a
⊢ 0 ≠ 0 ∧ a = 0 ∨ 0 = 0 ∧ a = 1

Tactic:
simp only [Complex.one_re, Complex.ofReal_zero, Complex.cpow_zero] at hyp

Result:
case pos
a : ℝ
hyp : 1 = a
⊢ 0 ≠ 0 ∧ a = 0 ∨ 0 = 0 ∧ a = 1

Proof state:
case neg
x a : ℝ
hyp : (0 ^ ↑x).re = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
rw [Complex.zero_cpow (Complex.ofReal_ne_zero.mpr h)] at hyp

Result:
case neg
x a : ℝ
hyp : Complex.re 0 = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Proof state:
case pos
a : ℝ
hyp : 1 = a
⊢ 0 ≠ 0 ∧ a = 0 ∨ 0 = 0 ∧ a = 1

Tactic:
exact Or.inr ⟨rfl, hyp.symm⟩

Result:
no goals

Proof state:
case pos
x a : ℝ
hyp : (0 ^ ↑x).re = a
h : x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
subst h

Result:
case pos
a : ℝ
hyp : (0 ^ ↑0).re = a
⊢ 0 ≠ 0 ∧ a = 0 ∨ 0 = 0 ∧ a = 1

Proof state:
case neg
x a : ℝ
hyp : Complex.re 0 = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
exact Or.inl ⟨h, hyp.symm⟩

Result:
no goals

Proof state:
case mpr.inl.intro
x : ℝ
h : x ≠ 0
⊢ 0 ^ x = 0

Tactic:
exact zero_rpow h

Result:
no goals

Proof state:
case mpr.inr.intro

⊢ 0 ^ 0 = 1

Tactic:
exact rpow_zero _

Result:
no goals

Proof state:
case mp
x a : ℝ
hyp : 0 ^ x = a
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
simp only [rpow_def, Complex.ofReal_zero] at hyp

Result:
case mp
x a : ℝ
hyp : (0 ^ ↑x).re = a
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Proof state:
case mp
x a : ℝ
⊢ 0 ^ x = a → x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
intro hyp

Result:
case mp
x a : ℝ
hyp : 0 ^ x = a
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Proof state:
x a : ℝ
⊢ 0 ^ x = a ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
constructor

Result:
case mp
x a : ℝ
⊢ 0 ^ x = a → x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

case mpr
x a : ℝ
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1 → 0 ^ x = a

Proof state:
case mpr
x a : ℝ
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1 → 0 ^ x = a

Tactic:
rintro (⟨h, rfl⟩ | ⟨rfl, rfl⟩)

Result:
case mpr.inl.intro
x : ℝ
h : x ≠ 0
⊢ 0 ^ x = 0

case mpr.inr.intro

⊢ 0 ^ 0 = 1
-- Mathlib/Probability/ProbabilityMassFunction/Constructions.lean
@[simp]
lemma map_ofFintype [Fintype β] (f : α → ℝ≥0∞) (h : ∑ a, f a = 1) (g : α → β) :
    (ofFintype f h).map g = ofFintype (fun b ↦ ∑ a with g a = b, f a)
      (by simpa [Finset.sum_fiberwise_eq_sum_filter univ univ g f])

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
b : β
⊢ (∑' (a : α), if b = g a then f a else 0) = ∑ a : α, if b = g a then f a else 0

Tactic:
exact tsum_eq_sum fun _ h ↦ (h <| mem_univ _).elim

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
⊢ map g (ofFintype f h) = ofFintype (fun b => ∑ a ∈ filter (fun a => g a = b) univ, f a) ⋯

Tactic:
ext b : 1

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
b : β
⊢ (map g (ofFintype f h)) b = (ofFintype (fun b => ∑ a ∈ filter (fun a => g a = b) univ, f a) ⋯) b

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
f✝ : α → ℝ≥0∞
h✝ : ∑ a : α, f✝ a = 1
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
⊢ ∑ a : β, (fun b => ∑ a ∈ filter (fun a => g a = b) univ, f a) a = 1

Tactic:
simpa [Finset.sum_fiberwise_eq_sum_filter univ univ g f]

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
b : β
⊢ (map g (ofFintype f h)) b = (ofFintype (fun b => ∑ a ∈ filter (fun a => g a = b) univ, f a) ⋯) b

Tactic:
simp only [sum_filter, eq_comm, map_apply, ofFintype_apply]

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
b : β
⊢ (∑' (a : α), if b = g a then f a else 0) = ∑ a : α, if b = g a then f a else 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem or_or_or_comm : (a ∨ b) ∨ c ∨ d ↔ (a ∨ c) ∨ b ∨ d

Proof state:
a b c d : Prop
⊢ (a ∨ b) ∨ c ∨ d ↔ (a ∨ c) ∨ b ∨ d

Tactic:
rw [← or_assoc, @or_right_comm a, or_assoc]

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
theorem other_mem' [DecidableEq α] {a : α} {z : Sym2 α} (h : a ∈ z) : Mem.other' h ∈ z

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ Mem.other h ∈ z

Tactic:
exact other_mem h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ Mem.other' h ∈ z

Tactic:
rw [← other_eq_other']

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ Mem.other h ∈ z
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head_reverse {l : List α} (h : l.reverse ≠ []) :
    l.reverse.head h = getLast l (by simp_all)

Proof state:
case neg
α : Type u_1
a : α
l : List α
ih : ∀ (h : l.reverse ≠ []), l.reverse.head h = l.getLast ⋯
h : (a :: l).reverse ≠ []
h' : ¬l = []
⊢ (l.reverse ++ [a]).head ⋯ = (a :: l).getLast ⋯

Tactic:
simp only [head_eq_iff_head?_eq_some, head?_reverse] at ih

Result:
case neg
α : Type u_1
a : α
l : List α
h : (a :: l).reverse ≠ []
h' : ¬l = []
ih : ∀ (h : l.reverse ≠ []), l.getLast? = some (l.getLast ⋯)
⊢ (l.reverse ++ [a]).head ⋯ = (a :: l).getLast ⋯

Proof state:
case neg
α : Type u_1
a : α
l : List α
h : (a :: l).reverse ≠ []
h' : ¬l = []
ih : ∀ (h : l.reverse ≠ []), l.getLast? = some (l.getLast ⋯)
⊢ (l.reverse ++ [a]).head ⋯ = (a :: l).getLast ⋯

Tactic:
simp [ih, h, h', getLast_cons, head_eq_iff_head?_eq_some]

Result:
no goals

Proof state:
case cons
α : Type u_1
a : α
l : List α
ih : ∀ (h : l.reverse ≠ []), l.reverse.head h = l.getLast ⋯
h : (a :: l).reverse ≠ []
⊢ (a :: l).reverse.head h = (a :: l).getLast ⋯

Tactic:
simp only [reverse_cons]

Result:
case cons
α : Type u_1
a : α
l : List α
ih : ∀ (h : l.reverse ≠ []), l.reverse.head h = l.getLast ⋯
h : (a :: l).reverse ≠ []
⊢ (l.reverse ++ [a]).head ⋯ = (a :: l).getLast ⋯

Proof state:
case cons
α : Type u_1
a : α
l : List α
ih : ∀ (h : l.reverse ≠ []), l.reverse.head h = l.getLast ⋯
h : (a :: l).reverse ≠ []
⊢ (l.reverse ++ [a]).head ⋯ = (a :: l).getLast ⋯

Tactic:
by_cases h' : l = []

Result:
case pos
α : Type u_1
a : α
l : List α
ih : ∀ (h : l.reverse ≠ []), l.reverse.head h = l.getLast ⋯
h : (a :: l).reverse ≠ []
h' : l = []
⊢ (l.reverse ++ [a]).head ⋯ = (a :: l).getLast ⋯

case neg
α : Type u_1
a : α
l : List α
ih : ∀ (h : l.reverse ≠ []), l.reverse.head h = l.getLast ⋯
h : (a :: l).reverse ≠ []
h' : ¬l = []
⊢ (l.reverse ++ [a]).head ⋯ = (a :: l).getLast ⋯

Proof state:
case nil
α : Type u_1
h : [].reverse ≠ []
⊢ [].reverse.head h = [].getLast ⋯

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type ?u.309997
l : List α
h : l.reverse ≠ []
⊢ l ≠ []

Tactic:
simp_all

Result:
no goals

Proof state:
case pos
α : Type u_1
a : α
l : List α
ih : ∀ (h : l.reverse ≠ []), l.reverse.head h = l.getLast ⋯
h : (a :: l).reverse ≠ []
h' : l = []
⊢ (l.reverse ++ [a]).head ⋯ = (a :: l).getLast ⋯

Tactic:
simp_all

Result:
no goals
-- Mathlib/Data/Finset/Sum.lean
@[simp] lemma toLeft_cons_inl (ha) :
    (cons (inl a) u ha).toLeft = cons a u.toLeft (by simpa)

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
s₁ s₂ : Finset α
t₁ t₂ : Finset β
a : α
b : β
x : α ⊕ β
u v : Finset (α ⊕ β)
ha : inl a ∉ u
⊢ a ∉ u.toLeft

Tactic:
simpa

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
a : α
u : Finset (α ⊕ β)
ha : inl a ∉ u
y : α
⊢ y ∈ (cons (inl a) u ha).toLeft ↔ y ∈ cons a u.toLeft ⋯

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
a : α
u : Finset (α ⊕ β)
ha : inl a ∉ u
⊢ (cons (inl a) u ha).toLeft = cons a u.toLeft ⋯

Tactic:
ext y

Result:
case h
α : Type u_1
β : Type u_2
a : α
u : Finset (α ⊕ β)
ha : inl a ∉ u
y : α
⊢ y ∈ (cons (inl a) u ha).toLeft ↔ y ∈ cons a u.toLeft ⋯