harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Real/ConjExponents.lean
lemma mul_eq_add : p * q = p + q

Proof state:
case inl
q : ℝ≥0∞
h : ⊤.IsConjExponent q
⊢ ⊤ * q = ⊤ + q

Tactic:
simp [h.symm.ne_zero]

Result:
no goals

Proof state:
case inr.inr
p q : ℝ≥0∞
h : p.IsConjExponent q
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ p * q = p + q

Tactic:
rw [← mul_one (_ * _), ← h.inv_add_inv_conj, mul_add, mul_right_comm,
  ENNReal.mul_inv_cancel h.ne_zero hp, one_mul, mul_assoc,
  ENNReal.mul_inv_cancel h.symm.ne_zero hq, mul_one, add_comm]

Result:
no goals

Proof state:
p q : ℝ≥0∞
h : p.IsConjExponent q
⊢ p * q = p + q

Tactic:
obtain rfl | hp := eq_or_ne p ∞

Result:
case inl
q : ℝ≥0∞
h : ⊤.IsConjExponent q
⊢ ⊤ * q = ⊤ + q

case inr
p q : ℝ≥0∞
h : p.IsConjExponent q
hp : p ≠ ⊤
⊢ p * q = p + q

Proof state:
case inr
p q : ℝ≥0∞
h : p.IsConjExponent q
hp : p ≠ ⊤
⊢ p * q = p + q

Tactic:
obtain rfl | hq := eq_or_ne q ∞

Result:
case inr.inl
p : ℝ≥0∞
hp : p ≠ ⊤
h : p.IsConjExponent ⊤
⊢ p * ⊤ = p + ⊤

case inr.inr
p q : ℝ≥0∞
h : p.IsConjExponent q
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ p * q = p + q

Proof state:
case inr.inl
p : ℝ≥0∞
hp : p ≠ ⊤
h : p.IsConjExponent ⊤
⊢ p * ⊤ = p + ⊤

Tactic:
simp [h.ne_zero]

Result:
no goals
-- Mathlib/NumberTheory/PythagoreanTriples.lean
theorem pythagoreanTriple_comm {x y z : ℤ} : PythagoreanTriple x y z ↔ PythagoreanTriple y x z

Proof state:
x y z : ℤ
⊢ PythagoreanTriple x y z ↔ PythagoreanTriple y x z

Tactic:
delta PythagoreanTriple

Result:
x y z : ℤ
⊢ x * x + y * y = z * z ↔ y * y + x * x = z * z

Proof state:
x y z : ℤ
⊢ x * x + y * y = z * z ↔ y * y + x * x = z * z

Tactic:
rw [add_comm]

Result:
no goals
-- Mathlib/Topology/Order/NhdsSet.lean
theorem Ioi_mem_nhdsSet_Ici_iff : Ioi a ∈ 𝓝ˢ (Ici b) ↔ a < b

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b : α
⊢ Ioi a ∈ 𝓝ˢ (Ici b) ↔ a < b

Tactic:
rw [isOpen_Ioi.mem_nhdsSet, Ici_subset_Ioi]

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/QExpansion.lean
lemma qExpansionFormalMultilinearSeries_apply_norm (m : ℕ) :
    ‖qExpansionFormalMultilinearSeries n f m‖ = ‖(qExpansion n f).coeff ℂ m‖

Proof state:
F : Type u_1
inst✝ : FunLike F ℍ ℂ
n : ℕ
f : F
m : ℕ
⊢ ‖qExpansionFormalMultilinearSeries n f m‖ = ‖(PowerSeries.coeff ℂ m) (qExpansion n f)‖

Tactic:
rw [qExpansionFormalMultilinearSeries,
  ← (ContinuousMultilinearMap.piFieldEquiv ℂ (Fin m) ℂ).symm.norm_map]

Result:
F : Type u_1
inst✝ : FunLike F ℍ ℂ
n : ℕ
f : F
m : ℕ
⊢ ‖(ContinuousMultilinearMap.piFieldEquiv ℂ (Fin m) ℂ).symm
        ((PowerSeries.coeff ℂ m) (qExpansion n f) • ContinuousMultilinearMap.mkPiAlgebraFin ℂ m ℂ)‖ =
    ‖(PowerSeries.coeff ℂ m) (qExpansion n f)‖

Proof state:
F : Type u_1
inst✝ : FunLike F ℍ ℂ
n : ℕ
f : F
m : ℕ
⊢ ‖(ContinuousMultilinearMap.piFieldEquiv ℂ (Fin m) ℂ).symm
        ((PowerSeries.coeff ℂ m) (qExpansion n f) • ContinuousMultilinearMap.mkPiAlgebraFin ℂ m ℂ)‖ =
    ‖(PowerSeries.coeff ℂ m) (qExpansion n f)‖

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
@[simp]
lemma Scheme.ofRestrict_appIso (U) :
    (X.ofRestrict h).appIso U = Iso.refl _

Proof state:
case w
U✝ : TopCat
X : Scheme
f : U✝ ⟶ TopCat.of ↑↑X.toPresheafedSpace
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : (X.restrict h).Opens
⊢ (Hom.appIso (X.ofRestrict h) U).hom = (Iso.refl Γ(X, X.ofRestrict h ''ᵁ U)).hom

Tactic:
simp only [restrict_presheaf_obj, Hom.appIso_hom', ofRestrict_appLE, homOfLE_refl, op_id,
  CategoryTheory.Functor.map_id, Iso.refl_hom]

Result:
no goals

Proof state:
U✝ : TopCat
X : Scheme
f : U✝ ⟶ TopCat.of ↑↑X.toPresheafedSpace
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : (X.restrict h).Opens
⊢ Hom.appIso (X.ofRestrict h) U = Iso.refl Γ(X, X.ofRestrict h ''ᵁ U)

Tactic:
ext1

Result:
case w
U✝ : TopCat
X : Scheme
f : U✝ ⟶ TopCat.of ↑↑X.toPresheafedSpace
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : (X.restrict h).Opens
⊢ (Hom.appIso (X.ofRestrict h) U).hom = (Iso.refl Γ(X, X.ofRestrict h ''ᵁ U)).hom
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem attachWith_map {o : Option α} (f : α → β) {P : β → Prop} {H : ∀ (b : β), b ∈ o.map f → P b} :
    (o.map f).attachWith P H = (o.attachWith (P ∘ f) (fun _ h => H _ (mem_map_of_mem f h))).map
      fun ⟨x, h⟩ => ⟨f x, h⟩

Proof state:
α : Type u_1
β : Type u_2
o : Option α
f : α → β
P : β → Prop
H : ∀ (b : β), b ∈ Option.map f o → P b
⊢ (Option.map f o).attachWith P H =
    Option.map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨f x, h⟩)
      (o.attachWith (P ∘ f) ⋯)

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/BigOperators.lean
lemma geo_series_const (a : α) {x : α} (hx1 : |x| < 1) :
    IsCauSeq abs fun m ↦ ∑ n ∈ range m, (a * x ^ n)

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
a x : α
hx1 : |x| < 1
⊢ IsCauSeq abs fun m => ∑ n ∈ range m, a * x ^ n

Tactic:
simpa [mul_sum, Pi.mul_def] using (const a).mul (geo_series x hx1)

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean
theorem quadraticChar_neg_one_iff_not_isSquare {a : F} : quadraticChar F a = -1 ↔ ¬IsSquare a

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 = -1 ↔ ¬IsSquare a

Tactic:
rw [quadraticChar_eq_neg_one_iff_not_one ha, quadraticChar_one_iff_isSquare ha]

Result:
no goals

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 = -1 ↔ ¬IsSquare a

Tactic:
simp only [ha, MulChar.map_zero, zero_eq_neg, one_ne_zero, IsSquare.zero, not_true]

Result:
no goals

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

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 = -1 ↔ ¬IsSquare a

case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬a = 0
⊢ (quadraticChar F) a = -1 ↔ ¬IsSquare a
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem NF.below_of_lt {e n a b} (H : repr e < b) :
    NF (ONote.oadd e n a) → NFBelow (ONote.oadd e n a) b
  | ⟨⟨b', h⟩⟩ => by (obtain - | ⟨h₁, h₂, h₃⟩ := h; exact NFBelow.oadd' h₁ h₂ H)

Proof state:
case oadd'
e : ONote
n : ℕ+
a : ONote
b : Ordinal.{0}
H : e.repr < b
b' eb✝ : Ordinal.{0}
h₁ : e.NFBelow eb✝
h₂ : a.NFBelow e.repr
h₃ : e.repr < b'
⊢ (e.oadd n a).NFBelow b

Tactic:
exact NFBelow.oadd' h₁ h₂ H

Result:
no goals

Proof state:
e : ONote
n : ℕ+
a : ONote
b : Ordinal.{0}
H : e.repr < b
b' : Ordinal.{0}
h : (e.oadd n a).NFBelow b'
⊢ (e.oadd n a).NFBelow b

Tactic:
(obtain - | ⟨h₁, h₂, h₃⟩ := h; exact NFBelow.oadd' h₁ h₂ H)

Result:
no goals

Proof state:
e : ONote
n : ℕ+
a : ONote
b : Ordinal.{0}
H : e.repr < b
b' : Ordinal.{0}
h : (e.oadd n a).NFBelow b'
⊢ (e.oadd n a).NFBelow b

Tactic:
obtain - | ⟨h₁, h₂, h₃⟩ := h

Result:
case oadd'
e : ONote
n : ℕ+
a : ONote
b : Ordinal.{0}
H : e.repr < b
b' eb✝ : Ordinal.{0}
h₁ : e.NFBelow eb✝
h₂ : a.NFBelow e.repr
h₃ : e.repr < b'
⊢ (e.oadd n a).NFBelow b
-- Mathlib/Data/Fin/Tuple/Sort.lean
theorem graph.card (f : Fin n → α) : (graph f).card = n

Proof state:
case H
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Function.Injective fun i => (f i, i)

Tactic:
intro _ _

Result:
case H
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
a₁✝ a₂✝ : Fin n
⊢ (fun i => (f i, i)) a₁✝ = (fun i => (f i, i)) a₂✝ → a₁✝ = a₂✝

Proof state:
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ (graph f).card = n

Tactic:
rw [graph, Finset.card_image_of_injective]

Result:
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Finset.univ.card = n

case H
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Function.Injective fun i => (f i, i)

Proof state:
case H
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
a₁✝ a₂✝ : Fin n
⊢ (f a₁✝, a₁✝).1 = (f a₂✝, a₂✝).1 ∧ (f a₁✝, a₁✝).2 = (f a₂✝, a₂✝).2 → a₁✝ = a₂✝

Tactic:
simp

Result:
no goals

Proof state:
case H
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
a₁✝ a₂✝ : Fin n
⊢ (fun i => (f i, i)) a₁✝ = (fun i => (f i, i)) a₂✝ → a₁✝ = a₂✝

Tactic:
dsimp only

Result:
case H
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
a₁✝ a₂✝ : Fin n
⊢ (f a₁✝, a₁✝) = (f a₂✝, a₂✝) → a₁✝ = a₂✝

Proof state:
case H
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
a₁✝ a₂✝ : Fin n
⊢ (f a₁✝, a₁✝) = (f a₂✝, a₂✝) → a₁✝ = a₂✝

Tactic:
rw [Prod.ext_iff]

Result:
case H
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
a₁✝ a₂✝ : Fin n
⊢ (f a₁✝, a₁✝).1 = (f a₂✝, a₂✝).1 ∧ (f a₁✝, a₁✝).2 = (f a₂✝, a₂✝).2 → a₁✝ = a₂✝

Proof state:
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Finset.univ.card = n

Tactic:
exact Finset.card_fin _

Result:
no goals
-- Mathlib/Topology/Algebra/Polynomial.lean
theorem exists_forall_norm_le [ProperSpace R] (p : R[X]) : ∃ x, ∀ y, ‖p.eval x‖ ≤ ‖p.eval y‖ :=
  if hp0 : 0 < degree p then
    p.continuous.norm.exists_forall_le <| p.tendsto_norm_atTop hp0 tendsto_norm_cocompact_atTop
  else
    ⟨p.coeff 0, by rw [eq_C_of_degree_le_zero (le_of_not_gt hp0)]; simp⟩

Proof state:
R : Type u_2
inst✝² : NormedRing R
inst✝¹ : IsAbsoluteValue norm
inst✝ : ProperSpace R
p : R[X]
hp0 : ¬0 < p.degree
⊢ ∀ (y : R), ‖eval (p.coeff 0) p‖ ≤ ‖eval y p‖

Tactic:
rw [eq_C_of_degree_le_zero (le_of_not_gt hp0)]

Result:
R : Type u_2
inst✝² : NormedRing R
inst✝¹ : IsAbsoluteValue norm
inst✝ : ProperSpace R
p : R[X]
hp0 : ¬0 < p.degree
⊢ ∀ (y : R), ‖eval ((C (p.coeff 0)).coeff 0) (C (p.coeff 0))‖ ≤ ‖eval y (C (p.coeff 0))‖

Proof state:
R : Type u_2
inst✝² : NormedRing R
inst✝¹ : IsAbsoluteValue norm
inst✝ : ProperSpace R
p : R[X]
hp0 : ¬0 < p.degree
⊢ ∀ (y : R), ‖eval ((C (p.coeff 0)).coeff 0) (C (p.coeff 0))‖ ≤ ‖eval y (C (p.coeff 0))‖

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/Restrict.lean
lemma resLE_congr (e₁ : U = U') (e₂ : V = V') (P : MorphismProperty Scheme.{u}) :
    P (f.resLE U V e) ↔ P (f.resLE U' V' (e₁ ▸ e₂ ▸ e))

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
P : MorphismProperty Scheme
⊢ P (resLE f U V e) ↔ P (resLE f U V ⋯)

Tactic:
rfl

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
e₂ : V = V'
P : MorphismProperty Scheme
⊢ P (resLE f U V e) ↔ P (resLE f U V' ⋯)

Tactic:
subst e₂

Result:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
P : MorphismProperty Scheme
⊢ P (resLE f U V e) ↔ P (resLE f U V ⋯)

Proof state:
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
e₁ : U = U'
e₂ : V = V'
P : MorphismProperty Scheme
⊢ P (resLE f U V e) ↔ P (resLE f U' V' ⋯)

Tactic:
subst e₁

Result:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
e₂ : V = V'
P : MorphismProperty Scheme
⊢ P (resLE f U V e) ↔ P (resLE f U V' ⋯)
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem tan_toReal (θ : Angle) : Real.tan θ.toReal = tan θ

Proof state:
θ : Angle
⊢ Real.tan θ.toReal = θ.tan

Tactic:
conv_rhs => rw [← coe_toReal θ, tan_coe]

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem mul [MonoidWithZero β] [ContinuousMul β] (hf : FinStronglyMeasurable f μ)
    (hg : FinStronglyMeasurable g μ) : FinStronglyMeasurable (f * g) μ

Proof state:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : MonoidWithZero β
inst✝ : ContinuousMul β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
⊢ FinStronglyMeasurable (f * g) μ

Tactic:
refine
  ⟨fun n => hf.approx n * hg.approx n, ?_, fun x =>
    (hf.tendsto_approx x).mul (hg.tendsto_approx x)⟩

Result:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : MonoidWithZero β
inst✝ : ContinuousMul β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
⊢ ∀ (n : ℕ), μ (support ⇑((fun n => hf.approx n * hg.approx n) n)) < ⊤

Proof state:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : MonoidWithZero β
inst✝ : ContinuousMul β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
⊢ ∀ (n : ℕ), μ (support ⇑((fun n => hf.approx n * hg.approx n) n)) < ⊤

Tactic:
intro n

Result:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : MonoidWithZero β
inst✝ : ContinuousMul β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
n : ℕ
⊢ μ (support ⇑((fun n => hf.approx n * hg.approx n) n)) < ⊤

Proof state:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : MonoidWithZero β
inst✝ : ContinuousMul β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
n : ℕ
⊢ μ (support ⇑((fun n => hf.approx n * hg.approx n) n)) < ⊤

Tactic:
exact (measure_mono (support_mul_subset_left _ _)).trans_lt (hf.fin_support_approx n)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
    have : i < (a.push x).size

Proof state:
α : Type u_1
a : Array α
x : α
i : Nat
h : i < a.size
⊢ let_fun this := ⋯;
  (a.push x)[i] = a[i]

Tactic:
simp only [push, ← getElem_toList, List.concat_eq_append, List.getElem_append_left, h]

Result:
no goals

Proof state:
α : Type ?u.18023
a : Array α
x : α
i : Nat
h : i < a.size
⊢ i < (a.push x).size

Tactic:
simp [*, Nat.lt_succ_of_le, Nat.le_of_lt]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem sum_fintype [Fintype ι] (μ : ι → Measure α) : sum μ = ∑ i, μ i

Proof state:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst✝ : Fintype ι
μ : ι → Measure α
⊢ sum μ = ∑ i : ι, μ i

Tactic:
ext1 s hs

Result:
case h
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst✝ : Fintype ι
μ : ι → Measure α
s : Set α
hs : MeasurableSet s
⊢ (sum μ) s = (∑ i : ι, μ i) s

Proof state:
case h
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst✝ : Fintype ι
μ : ι → Measure α
s : Set α
hs : MeasurableSet s
⊢ (sum μ) s = (∑ i : ι, μ i) s

Tactic:
simp only [sum_apply, finset_sum_apply, hs, tsum_fintype]

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem prod_norm_eq_of_L2 (x : WithLp 2 (α × β)) :
    ‖x‖ = √(‖x.fst‖ ^ 2 + ‖x.snd‖ ^ 2)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : WithLp 2 (α × β)
⊢ 2 = ↑2

Tactic:
norm_cast

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : WithLp 2 (α × β)
⊢ (‖x.1‖ ^ 2 + ‖x.2‖ ^ 2) ^ (1 / ↑2) = (‖x.1‖ ^ 2 + ‖x.2‖ ^ 2) ^ (1 / 2)

Tactic:
norm_cast

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : WithLp 2 (α × β)
⊢ ‖x‖ = √(‖x.1‖ ^ 2 + ‖x.2‖ ^ 2)

Tactic:
rw [prod_norm_eq_of_nat 2 (by norm_cast) _, Real.sqrt_eq_rpow]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : WithLp 2 (α × β)
⊢ (‖x.1‖ ^ 2 + ‖x.2‖ ^ 2) ^ (1 / ↑2) = (‖x.1‖ ^ 2 + ‖x.2‖ ^ 2) ^ (1 / 2)
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem mul_le_of_limit {a b c : Ordinal} (h : IsLimit b) : a * b ≤ c ↔ ∀ b' < b, a * b' ≤ c :=
  ⟨fun h _ l => (mul_le_mul_left' l.le _).trans h, fun H =>
    -- Porting note: `induction` tactics are required because of the parser bug.
    le_of_not_lt <| by
      induction a using inductionOn with
      | H α r =>
        induction b using inductionOn with
        | H β s =>
          exact mul_le_of_limit_aux h H⟩

Proof state:
case H
b c : Ordinal.{u_4}
h : b.IsLimit
α : Type u_4
r : α → α → Prop
inst✝ : IsWellOrder α r
H : ∀ b' < b, type r * b' ≤ c
⊢ ¬c < type r * b

Tactic:
induction b using inductionOn with
| H β s =>
  exact mul_le_of_limit_aux h H

Result:
no goals

Proof state:
a b c : Ordinal.{u_4}
h : b.IsLimit
H : ∀ b' < b, a * b' ≤ c
⊢ ¬c < a * b

Tactic:
induction a using inductionOn with
| H α r =>
  induction b using inductionOn with
  | H β s =>
    exact mul_le_of_limit_aux h H

Result:
no goals

Proof state:
case H.H
c : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
inst✝¹ : IsWellOrder α r
β : Type u_4
s : β → β → Prop
inst✝ : IsWellOrder β s
h : (type s).IsLimit
H : ∀ b' < type s, type r * b' ≤ c
⊢ ¬c < type r * type s

Tactic:
exact mul_le_of_limit_aux h H

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
@[simp]
lemma map_dblY (P : Fin 3 → R) : (W'.map f).toProjective.dblY (f ∘ P) = f (W'.dblY P)

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ -f (W'.negDblY P) - (map W' f).toProjective.a₁ * f (W'.dblX P) - (map W' f).toProjective.a₃ * f (W'.dblZ P) =
    f (-W'.negDblY P - W'.a₁ * W'.dblX P - W'.a₃ * W'.dblZ P)

Tactic:
map_simp

Result:
no goals

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ (map W' f).toProjective.dblY (⇑f ∘ P) = f (W'.dblY P)

Tactic:
simp only [dblY, negY_eq, map_negDblY, map_dblX, map_dblZ]

Result:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ -f (W'.negDblY P) - (map W' f).toProjective.a₁ * f (W'.dblX P) - (map W' f).toProjective.a₃ * f (W'.dblZ P) =
    f (-W'.negDblY P - W'.a₁ * W'.dblX P - W'.a₃ * W'.dblZ P)
-- Mathlib/RingTheory/Polynomial/Vieta.lean
theorem _root_.Finset.prod_X_add_C_coeff {σ} (s : Finset σ) (r : σ → R) {k : ℕ} (h : k ≤ #s) :
    (∏ i ∈ s, (X + C (r i))).coeff k = ∑ t ∈ s.powersetCard (#s - k), ∏ i ∈ t, r i

Proof state:
R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
s : Finset σ
r : σ → R
k : ℕ
h : k ≤ #s
⊢ ∑ t ∈ Finset.powersetCard (s.val.card - k) s, t.prod r = ∑ t ∈ Finset.powersetCard (#s - k) s, ∏ i ∈ t, r i

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
s : Finset σ
r : σ → R
k : ℕ
h : k ≤ #s
⊢ (∏ i ∈ s, (X + C (r i))).coeff k = ∑ t ∈ Finset.powersetCard (#s - k) s, ∏ i ∈ t, r i

Tactic:
rw [Finset.prod, prod_X_add_C_coeff' _ r h, Finset.esymm_map_val]

Result:
R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
s : Finset σ
r : σ → R
k : ℕ
h : k ≤ #s
⊢ ∑ t ∈ Finset.powersetCard (s.val.card - k) s, t.prod r = ∑ t ∈ Finset.powersetCard (#s - k) s, ∏ i ∈ t, r i
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem extraction_of_frequently_atTop' {P : ℕ → Prop} (h : ∀ N, ∃ n > N, P n) :
    ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ n, P (φ n)

Proof state:
P : ℕ → Prop
h : ∀ (N : ℕ), ∃ n > N, P n
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)

Tactic:
choose u hu hu' using h

Result:
P : ℕ → Prop
u : ℕ → ℕ
hu : ∀ (N : ℕ), u N > N
hu' : ∀ (N : ℕ), P (u N)
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)

Proof state:
case refine_2
P : ℕ → Prop
u : ℕ → ℕ
hu : ∀ (N : ℕ), u N > N
hu' : ∀ (N : ℕ), P (u N)
n : ℕ
⊢ P ((fun n => u^[n + 1] 0) n)

Tactic:
simpa only [Function.iterate_succ_apply'] using hu' _

Result:
no goals

Proof state:
P : ℕ → Prop
u : ℕ → ℕ
hu : ∀ (N : ℕ), u N > N
hu' : ∀ (N : ℕ), P (u N)
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)

Tactic:
refine ⟨fun n => u^[n + 1] 0, strictMono_nat_of_lt_succ fun n => ?_, fun n => ?_⟩

Result:
case refine_1
P : ℕ → Prop
u : ℕ → ℕ
hu : ∀ (N : ℕ), u N > N
hu' : ∀ (N : ℕ), P (u N)
n : ℕ
⊢ u^[n + 1] 0 < u^[n + 1 + 1] 0

case refine_2
P : ℕ → Prop
u : ℕ → ℕ
hu : ∀ (N : ℕ), u N > N
hu' : ∀ (N : ℕ), P (u N)
n : ℕ
⊢ P ((fun n => u^[n + 1] 0) n)

Proof state:
case refine_1
P : ℕ → Prop
u : ℕ → ℕ
hu : ∀ (N : ℕ), u N > N
hu' : ∀ (N : ℕ), P (u N)
n : ℕ
⊢ u^[n + 1] 0 < u^[n + 1 + 1] 0

Tactic:
exact Trans.trans (hu _) (Function.iterate_succ_apply' _ _ _).symm

Result:
no goals
-- Mathlib/FieldTheory/CardinalEmb.lean
theorem cardinal_eq_of_isSeparable [Algebra.IsSeparable F E] :
    #(Field.Emb F E) = (fun c ↦ if ℵ₀ ≤ c then 2 ^ c else c) (Module.rank F E)

Proof state:
case pos
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
h : ℵ₀ ≤ Module.rank F E
⊢ #(Emb F E) = 2 ^ Module.rank F E

Tactic:
exact cardinal_eq_two_pow_rank h

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
⊢ #(Emb F E) = if ℵ₀ ≤ Module.rank F E then 2 ^ Module.rank F E else Module.rank F E

Tactic:
split_ifs with h

Result:
case pos
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
h : ℵ₀ ≤ Module.rank F E
⊢ #(Emb F E) = 2 ^ Module.rank F E

case neg
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
h : ¬ℵ₀ ≤ Module.rank F E
⊢ #(Emb F E) = Module.rank F E

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
⊢ #(Emb F E) = (fun c => if ℵ₀ ≤ c then 2 ^ c else c) (Module.rank F E)

Tactic:
dsimp only

Result:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
⊢ #(Emb F E) = if ℵ₀ ≤ Module.rank F E then 2 ^ Module.rank F E else Module.rank F E

Proof state:
case neg
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
h : IsNoetherian F E
⊢ #(Emb F E) = Module.rank F E

Tactic:
rw [← Module.finrank_eq_rank, ← toNat_eq_iff Module.finrank_pos.ne',
  ← Nat.card, ← finSepDegree, finSepDegree_eq_finrank_of_isSeparable]

Result:
no goals

Proof state:
case neg
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
h : ¬ℵ₀ ≤ Module.rank F E
⊢ #(Emb F E) = Module.rank F E

Tactic:
rw [not_le, ← IsNoetherian.iff_rank_lt_aleph0] at h

Result:
case neg
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
h : IsNoetherian F E
⊢ #(Emb F E) = Module.rank F E
-- Mathlib/Data/Real/Irrational.lean
theorem of_int_mul (m : ℤ) (h : Irrational (m * x)) : Irrational x :=
  of_rat_mul m <| by rwa [cast_intCast]

Proof state:
x : ℝ
m : ℤ
h : Irrational (↑m * x)
⊢ Irrational (↑↑m * x)

Tactic:
rwa [cast_intCast]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Basis.lean
theorem exists_affine_subbasis {t : Set P} (ht : affineSpan k t = ⊤) :
    ∃ s ⊆ t, ∃ b : AffineBasis s k P, ⇑b = ((↑) : s → P)

Proof state:
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : DivisionRing k
inst✝ : Module k V
t : Set P
ht : affineSpan k t = ⊤
⊢ ∃ s ⊆ t, ∃ b, ⇑b = Subtype.val

Tactic:
obtain ⟨s, hst, h_tot, h_ind⟩ := exists_affineIndependent k V t

Result:
case intro.intro.intro
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : DivisionRing k
inst✝ : Module k V
t : Set P
ht : affineSpan k t = ⊤
s : Set P
hst : s ⊆ t
h_tot : affineSpan k s = affineSpan k t
h_ind : AffineIndependent k Subtype.val
⊢ ∃ s ⊆ t, ∃ b, ⇑b = Subtype.val

Proof state:
case intro.intro.intro
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : DivisionRing k
inst✝ : Module k V
t : Set P
ht : affineSpan k t = ⊤
s : Set P
hst : s ⊆ t
h_tot : affineSpan k s = affineSpan k t
h_ind : AffineIndependent k Subtype.val
⊢ affineSpan k (range Subtype.val) = ⊤

Tactic:
rw [Subtype.range_coe, h_tot, ht]

Result:
no goals

Proof state:
case intro.intro.intro
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : DivisionRing k
inst✝ : Module k V
t : Set P
ht : affineSpan k t = ⊤
s : Set P
hst : s ⊆ t
h_tot : affineSpan k s = affineSpan k t
h_ind : AffineIndependent k Subtype.val
⊢ ∃ s ⊆ t, ∃ b, ⇑b = Subtype.val

Tactic:
refine ⟨s, hst, ⟨(↑), h_ind, ?_⟩, rfl⟩

Result:
case intro.intro.intro
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : DivisionRing k
inst✝ : Module k V
t : Set P
ht : affineSpan k t = ⊤
s : Set P
hst : s ⊆ t
h_tot : affineSpan k s = affineSpan k t
h_ind : AffineIndependent k Subtype.val
⊢ affineSpan k (range Subtype.val) = ⊤