harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
/-- The formula `x(P₁ + P₂) = x(P₁ - P₂) - ψ(P₁)ψ(P₂) / (x(P₂) - x(P₁))²`,
where `ψ(x,y) = 2y + a₁x + a₃`. -/
lemma addX_eq_addX_negY_sub {x₁ x₂ : F} (y₁ y₂ : F) (hx : x₁ ≠ x₂) :
    W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = W.addX x₁ x₂ (W.slope x₁ x₂ y₁ <| W.negY x₂ y₂) -
      (y₁ - W.negY x₁ y₁) * (y₂ - W.negY x₂ y₂) / (x₂ - x₁) ^ 2

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ ((y₁ - y₂) ^ 2 * (x₁ - x₂) + W.a₁ * (y₁ - y₂) * (x₁ - x₂) ^ 2 - (x₁ - x₂) ^ 2 * (x₁ - x₂) * W.a₂ -
          x₁ * ((x₁ - x₂) ^ 2 * (x₁ - x₂)) -
        (x₁ - x₂) ^ 2 * (x₁ - x₂) * x₂) *
      ((x₁ - x₂) ^ 2 * (x₁ - x₂) * (x₁ - x₂) ^ 2) =
    (((y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) ^ 2 * (x₁ - x₂) + W.a₁ * (y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) * (x₁ - x₂) ^ 2 -
                (x₁ - x₂) ^ 2 * (x₁ - x₂) * W.a₂ -
              x₁ * ((x₁ - x₂) ^ 2 * (x₁ - x₂)) -
            (x₁ - x₂) ^ 2 * (x₁ - x₂) * x₂) *
          (x₁ - x₂) ^ 2 -
        (x₁ - x₂) ^ 2 * (x₁ - x₂) * ((y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) * (y₂ - (-y₂ - W.a₁ * x₂ - W.a₃)))) *
      ((x₁ - x₂) ^ 2 * (x₁ - x₂))

Tactic:
ring1

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ -(x₁ - (((y₁ - y₂) / (x₁ - x₂)) ^ 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂)) - x₂ =
    -(x₁ -
            (((y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) / (x₁ - x₂)) ^ 2 + W.a₁ * ((y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) / (x₁ - x₂)) -
              W.a₂)) -
        x₂ -
      (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) * (y₂ - (-y₂ - W.a₁ * x₂ - W.a₃)) / (x₁ - x₂) ^ 2

Tactic:
field_simp [sub_ne_zero.mpr hx]

Result:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ ((y₁ - y₂) ^ 2 * (x₁ - x₂) + W.a₁ * (y₁ - y₂) * (x₁ - x₂) ^ 2 - (x₁ - x₂) ^ 2 * (x₁ - x₂) * W.a₂ -
          x₁ * ((x₁ - x₂) ^ 2 * (x₁ - x₂)) -
        (x₁ - x₂) ^ 2 * (x₁ - x₂) * x₂) *
      ((x₁ - x₂) ^ 2 * (x₁ - x₂) * (x₁ - x₂) ^ 2) =
    (((y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) ^ 2 * (x₁ - x₂) + W.a₁ * (y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) * (x₁ - x₂) ^ 2 -
                (x₁ - x₂) ^ 2 * (x₁ - x₂) * W.a₂ -
              x₁ * ((x₁ - x₂) ^ 2 * (x₁ - x₂)) -
            (x₁ - x₂) ^ 2 * (x₁ - x₂) * x₂) *
          (x₁ - x₂) ^ 2 -
        (x₁ - x₂) ^ 2 * (x₁ - x₂) * ((y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) * (y₂ - (-y₂ - W.a₁ * x₂ - W.a₃)))) *
      ((x₁ - x₂) ^ 2 * (x₁ - x₂))

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) =
    W.addX x₁ x₂ (W.slope x₁ x₂ y₁ (W.negY x₂ y₂)) - (y₁ - W.negY x₁ y₁) * (y₂ - W.negY x₂ y₂) / (x₂ - x₁) ^ 2

Tactic:
simp_rw [slope_of_X_ne hx, addX, negY, ← neg_sub x₁, neg_sq]

Result:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ -(x₁ - (((y₁ - y₂) / (x₁ - x₂)) ^ 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂)) - x₂ =
    -(x₁ -
            (((y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) / (x₁ - x₂)) ^ 2 + W.a₁ * ((y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) / (x₁ - x₂)) -
              W.a₂)) -
        x₂ -
      (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) * (y₂ - (-y₂ - W.a₁ * x₂ - W.a₃)) / (x₁ - x₂) ^ 2
-- Mathlib/Analysis/Analytic/Composition.lean
theorem AnalyticAt.comp_analyticWithinAt {g : F → G} {f : E → F} {x : E} {s : Set E}
    (hg : AnalyticAt 𝕜 g (f x)) (hf : AnalyticWithinAt 𝕜 f s x) :
    AnalyticWithinAt 𝕜 (g ∘ f) s x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
x : E
s : Set E
hg : AnalyticWithinAt 𝕜 g Set.univ (f x)
hf : AnalyticWithinAt 𝕜 f s x
⊢ AnalyticWithinAt 𝕜 (g ∘ f) s x

Tactic:
exact hg.comp hf (Set.mapsTo_univ _ _)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
x : E
s : Set E
hg : AnalyticAt 𝕜 g (f x)
hf : AnalyticWithinAt 𝕜 f s x
⊢ AnalyticWithinAt 𝕜 (g ∘ f) s x

Tactic:
rw [← analyticWithinAt_univ] at hg

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
x : E
s : Set E
hg : AnalyticWithinAt 𝕜 g Set.univ (f x)
hf : AnalyticWithinAt 𝕜 f s x
⊢ AnalyticWithinAt 𝕜 (g ∘ f) s x
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem norm_le_of_ae_bound [IsFiniteMeasure μ] {f : Lp E p μ} {C : ℝ} (hC : 0 ≤ C)
    (hfC : ∀ᵐ x ∂μ, ‖f x‖ ≤ C) : ‖f‖ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * C

Proof state:
case intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ ↑C
⊢ ‖f‖ ≤ ↑(measureUnivNNReal μ) ^ p.toReal⁻¹ * ↑C

Tactic:
have := nnnorm_le_of_ae_bound hfC

Result:
case intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ ↑C
this : ‖f‖₊ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * C
⊢ ‖f‖ ≤ ↑(measureUnivNNReal μ) ^ p.toReal⁻¹ * ↑C

Proof state:
case intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ ↑C
this : ‖f‖₊ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * C
⊢ ‖f‖ ≤ ↑(measureUnivNNReal μ) ^ p.toReal⁻¹ * ↑C

Tactic:
rwa [← NNReal.coe_le_coe, NNReal.coe_mul, NNReal.coe_rpow] at this

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ
hC : 0 ≤ C
hfC : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ C
⊢ ‖f‖ ≤ ↑(measureUnivNNReal μ) ^ p.toReal⁻¹ * C

Tactic:
lift C to ℝ≥0 using hC

Result:
case intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ ↑C
⊢ ‖f‖ ≤ ↑(measureUnivNNReal μ) ^ p.toReal⁻¹ * ↑C
-- Mathlib/Algebra/Azumaya/Defs.lean
@[simp]
lemma AlgHom.mulLeftRight_apply (a : A) (b : Aᵐᵒᵖ) (x : A) :
    AlgHom.mulLeftRight R A (a ⊗ₜ b) x = a * x * b.unop

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
b : Aᵐᵒᵖ
x : A
⊢ ((mulLeftRight R A) (a ⊗ₜ[R] b)) x = a * x * MulOpposite.unop b

Tactic:
simp only [AlgHom.mulLeftRight, Algebra.lsmul_coe]

Result:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
b : Aᵐᵒᵖ
x : A
⊢ a ⊗ₜ[R] b • x = a * x * MulOpposite.unop b

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
b : Aᵐᵒᵖ
x : A
⊢ (Algebra.moduleAux (a ⊗ₜ[R] b)) x = a * x * MulOpposite.unop b

Tactic:
simp [TensorProduct.Algebra.moduleAux, ← mul_assoc]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
b : Aᵐᵒᵖ
x : A
⊢ a ⊗ₜ[R] b • x = a * x * MulOpposite.unop b

Tactic:
change TensorProduct.Algebra.moduleAux _ _ = _

Result:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
b : Aᵐᵒᵖ
x : A
⊢ (Algebra.moduleAux (a ⊗ₜ[R] b)) x = a * x * MulOpposite.unop b
-- Mathlib/RingTheory/HopfAlgebra/Basic.lean
lemma sum_mul_antipode_eq_smul {a : A} (repr : Repr R a) :
    ∑ i ∈ repr.index, repr.left i * antipode (R := R) (repr.right i) =
      counit (R := R) a • 1

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
repr : Coalgebra.Repr R a
⊢ ∑ i ∈ repr.index, repr.left i * antipode (repr.right i) = counit a • 1

Tactic:
rw [sum_mul_antipode_eq, Algebra.smul_def, mul_one]

Result:
no goals
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem exists_retraction_of_isClosed {s : Set (∀ n, E n)} (hs : IsClosed s) (hne : s.Nonempty) :
    ∃ f : (∀ n, E n) → ∀ n, E n, (∀ x ∈ s, f x = x) ∧ range f = s ∧ Continuous f

Proof state:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : s.Nonempty
⊢ ∃ f, (∀ x ∈ s, f x = x) ∧ range f = s ∧ Continuous f

Tactic:
rcases exists_lipschitz_retraction_of_isClosed hs hne with ⟨f, fs, frange, hf⟩

Result:
case intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n
fs : ∀ x ∈ s, f x = x
frange : range f = s
hf : LipschitzWith 1 f
⊢ ∃ f, (∀ x ∈ s, f x = x) ∧ range f = s ∧ Continuous f

Proof state:
case intro.intro.intro
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n
fs : ∀ x ∈ s, f x = x
frange : range f = s
hf : LipschitzWith 1 f
⊢ ∃ f, (∀ x ∈ s, f x = x) ∧ range f = s ∧ Continuous f

Tactic:
exact ⟨f, fs, frange, hf.continuous⟩

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem mem_cycleFactorsFinset_iff {f p : Perm α} :
    p ∈ cycleFactorsFinset f ↔ p.IsCycle ∧ ∀ a ∈ p.support, p a = f a

Proof state:
case intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f p : Perm α
l : List (Perm α)
hl : l.Nodup
hl' : l.toFinset = f.cycleFactorsFinset
⊢ p ∈ f.cycleFactorsFinset ↔ p.IsCycle ∧ ∀ a ∈ p.support, p a = f a

Tactic:
rw [← hl']

Result:
case intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f p : Perm α
l : List (Perm α)
hl : l.Nodup
hl' : l.toFinset = f.cycleFactorsFinset
⊢ p ∈ l.toFinset ↔ p.IsCycle ∧ ∀ a ∈ p.support, p a = f a

Proof state:
case intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f p : Perm α
l : List (Perm α)
hl : l.Nodup
hl' : (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = f
⊢ p ∈ l.toFinset ↔ p.IsCycle ∧ ∀ a ∈ p.support, p a = f a

Tactic:
simpa [List.mem_toFinset, Ne, ← hl'.right.right] using
  mem_list_cycles_iff hl'.left hl'.right.left

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f p : Perm α
⊢ p ∈ f.cycleFactorsFinset ↔ p.IsCycle ∧ ∀ a ∈ p.support, p a = f a

Tactic:
obtain ⟨l, hl, hl'⟩ := f.cycleFactorsFinset.exists_list_nodup_eq

Result:
case intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f p : Perm α
l : List (Perm α)
hl : l.Nodup
hl' : l.toFinset = f.cycleFactorsFinset
⊢ p ∈ f.cycleFactorsFinset ↔ p.IsCycle ∧ ∀ a ∈ p.support, p a = f a

Proof state:
case intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f p : Perm α
l : List (Perm α)
hl : l.Nodup
hl' : l.toFinset = f.cycleFactorsFinset
⊢ p ∈ l.toFinset ↔ p.IsCycle ∧ ∀ a ∈ p.support, p a = f a

Tactic:
rw [eq_comm, cycleFactorsFinset_eq_list_toFinset hl] at hl'

Result:
case intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f p : Perm α
l : List (Perm α)
hl : l.Nodup
hl' : (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = f
⊢ p ∈ l.toFinset ↔ p.IsCycle ∧ ∀ a ∈ p.support, p a = f a
-- Mathlib/Algebra/Group/ForwardDiff.lean
@[simp] lemma fwdDiff_iter_const_smul {R : Type*} [Semiring R] [Module R G]
    (r : R) (f : M → G) (n : ℕ) : Δ_[h]^[n] (r • f) = r • Δ_[h]^[n] f

Proof state:
case succ
M : Type u_1
G : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : AddCommGroup G
h : M
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Module R G
r : R
n : ℕ
IH : ∀ (f : M → G), Δ_[h]^[n] (r • f) = r • Δ_[h]^[n] f
f : M → G
⊢ Δ_[h]^[n + 1] (r • f) = r • Δ_[h]^[n + 1] f

Tactic:
simp only [iterate_succ_apply, fwdDiff_const_smul, IH]

Result:
no goals

Proof state:
case zero
M : Type u_1
G : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : AddCommGroup G
h : M
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Module R G
r : R
f : M → G
⊢ Δ_[h]^[0] (r • f) = r • Δ_[h]^[0] f

Tactic:
simp only [iterate_zero, id_eq]

Result:
no goals

Proof state:
M : Type u_1
G : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : AddCommGroup G
h : M
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Module R G
r : R
f : M → G
n : ℕ
⊢ Δ_[h]^[n] (r • f) = r • Δ_[h]^[n] f

Tactic:
induction' n with n IH generalizing f

Result:
case zero
M : Type u_1
G : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : AddCommGroup G
h : M
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Module R G
r : R
f : M → G
⊢ Δ_[h]^[0] (r • f) = r • Δ_[h]^[0] f

case succ
M : Type u_1
G : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : AddCommGroup G
h : M
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Module R G
r : R
n : ℕ
IH : ∀ (f : M → G), Δ_[h]^[n] (r • f) = r • Δ_[h]^[n] f
f : M → G
⊢ Δ_[h]^[n + 1] (r • f) = r • Δ_[h]^[n + 1] f
-- Mathlib/Algebra/Polynomial/Eval/Degree.lean
@[simp] lemma comp_C_mul_X_coeff {r : R} {n : ℕ} :
    (p.comp <| C r * X).coeff n = p.coeff n * r ^ n

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
h : n ∉ range (p.natDegree + 1)
⊢ p.coeff n * (r ^ n * if n = n then 1 else 0) = 0

Tactic:
rw [coeff_eq_zero_of_natDegree_lt, zero_mul]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
h : n ∉ range (p.natDegree + 1)
⊢ p.natDegree < n

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n b : ℕ
a✝ : b ∈ range (p.natDegree + 1)
h : b ≠ n
⊢ p.coeff b * (r ^ b * if n = b then 1 else 0) = 0

Tactic:
simp_rw [if_neg h.symm, mul_zero]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
⊢ (p.comp (C r * X)).coeff n = p.coeff n * r ^ n

Tactic:
simp_rw [comp, eval₂_eq_sum_range, (commute_X _).symm.mul_pow,
  ← C_pow, finset_sum_coeff, coeff_C_mul, coeff_X_pow]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
⊢ ∑ x ∈ range (p.natDegree + 1), p.coeff x * (r ^ x * if n = x then 1 else 0) = p.coeff n * r ^ n

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
⊢ ∀ b ∈ range (p.natDegree + 1), b ≠ n → p.coeff b * (r ^ b * if n = b then 1 else 0) = 0

Tactic:
intro b _ h

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n b : ℕ
a✝ : b ∈ range (p.natDegree + 1)
h : b ≠ n
⊢ p.coeff b * (r ^ b * if n = b then 1 else 0) = 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
⊢ ∑ x ∈ range (p.natDegree + 1), p.coeff x * (r ^ x * if n = x then 1 else 0) = p.coeff n * r ^ n

Tactic:
rw [Finset.sum_eq_single n _ fun h ↦ ?_, if_pos rfl, mul_one]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
⊢ ∀ b ∈ range (p.natDegree + 1), b ≠ n → p.coeff b * (r ^ b * if n = b then 1 else 0) = 0

R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
h : n ∉ range (p.natDegree + 1)
⊢ p.coeff n * (r ^ n * if n = n then 1 else 0) = 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
h : n ∉ range (p.natDegree + 1)
⊢ p.natDegree < n

Tactic:
rwa [Finset.mem_range_succ_iff, not_le] at h

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem IsBasis.exists_isBase (hI : M.IsBasis I X) : ∃ B, M.IsBase B ∧ I = B ∩ X :=
  let ⟨B,hB, hIB⟩ := hI.indep.exists_isBase_superset
  ⟨B, hB, subset_antisymm (subset_inter hIB hI.subset)
    (by rw [hI.eq_of_subset_indep (hB.indep.inter_right X) (subset_inter hIB hI.subset)
    inter_subset_right])⟩

Proof state:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ B ∩ X ⊆ I

Tactic:
rw [hI.eq_of_subset_indep (hB.indep.inter_right X) (subset_inter hIB hI.subset)
inter_subset_right]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sqrtTwoAddSeries_succ (x : ℝ) :
    ∀ n : ℕ, sqrtTwoAddSeries x (n + 1) = sqrtTwoAddSeries (√(2 + x)) n
  | 0 => rfl
  | n + 1 => by rw [sqrtTwoAddSeries, sqrtTwoAddSeries_succ _ _, sqrtTwoAddSeries]

Proof state:
x : ℝ
n : ℕ
⊢ x.sqrtTwoAddSeries (n + 1 + 1) = (√(2 + x)).sqrtTwoAddSeries (n + 1)

Tactic:
rw [sqrtTwoAddSeries, sqrtTwoAddSeries_succ _ _, sqrtTwoAddSeries]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Rank.lean
theorem rank_insert (x y : PSet) : rank (insert x y) = max (succ (rank x)) (rank y)

Proof state:
case a
x y : PSet.{u_1}
⊢ (insert x y).rank ≤ succ x.rank ⊔ y.rank

Tactic:
simp_rw [rank_le_iff, mem_insert_iff]

Result:
case a
x y : PSet.{u_1}
⊢ ∀ ⦃y_1 : PSet.{u_1}⦄, y_1.Equiv x ∨ y_1 ∈ y → y_1.rank < succ x.rank ⊔ y.rank

Proof state:
case a.inl
x y y✝ : PSet.{u_1}
h : y✝.Equiv x
⊢ y✝.rank < succ x.rank ⊔ y.rank

Tactic:
simp [rank_congr h]

Result:
no goals

Proof state:
case a.inr
x y y✝ : PSet.{u_1}
h : y✝ ∈ y
⊢ y✝.rank < succ x.rank ⊔ y.rank

Tactic:
simp [rank_lt_of_mem h]

Result:
no goals

Proof state:
case a.h₁
x y : PSet.{u_1}
⊢ succ x.rank ≤ (insert x y).rank

Tactic:
exact (rank_lt_of_mem (mem_insert x y)).succ_le

Result:
no goals

Proof state:
x y : PSet.{u_1}
⊢ (insert x y).rank = succ x.rank ⊔ y.rank

Tactic:
apply le_antisymm

Result:
case a
x y : PSet.{u_1}
⊢ (insert x y).rank ≤ succ x.rank ⊔ y.rank

case a
x y : PSet.{u_1}
⊢ succ x.rank ⊔ y.rank ≤ (insert x y).rank

Proof state:
case a.h₂
x y : PSet.{u_1}
⊢ y.rank ≤ (insert x y).rank

Tactic:
exact rank_mono (subset_iff.2 fun z => mem_insert_of_mem x)

Result:
no goals

Proof state:
case a
x y : PSet.{u_1}
⊢ succ x.rank ⊔ y.rank ≤ (insert x y).rank

Tactic:
apply max_le

Result:
case a.h₁
x y : PSet.{u_1}
⊢ succ x.rank ≤ (insert x y).rank

case a.h₂
x y : PSet.{u_1}
⊢ y.rank ≤ (insert x y).rank

Proof state:
case a
x y : PSet.{u_1}
⊢ ∀ ⦃y_1 : PSet.{u_1}⦄, y_1.Equiv x ∨ y_1 ∈ y → y_1.rank < succ x.rank ⊔ y.rank

Tactic:
rintro _ (h | h)

Result:
case a.inl
x y y✝ : PSet.{u_1}
h : y✝.Equiv x
⊢ y✝.rank < succ x.rank ⊔ y.rank

case a.inr
x y y✝ : PSet.{u_1}
h : y✝ ∈ y
⊢ y✝.rank < succ x.rank ⊔ y.rank
-- Mathlib/GroupTheory/QuotientGroup/Basic.lean
theorem mk_int_mul (n : ℤ) (a : R) : ((n * a : R) : R ⧸ N) = n • ↑a

Proof state:
R : Type u_1
inst✝¹ : NonAssocRing R
N : AddSubgroup R
inst✝ : N.Normal
n : ℤ
a : R
⊢ ↑(↑n * a) = n • ↑a

Tactic:
rw [← zsmul_eq_mul, mk_zsmul N a n]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem norm_compContinuous_linearIsometryEquiv (g : ContinuousMultilinearMap 𝕜 E₁ G)
    (f : ∀ i, E i ≃ₗᵢ[𝕜] E₁ i) :
    ‖g.compContinuousLinearMap fun i => (f i : E i →L[𝕜] E₁ i)‖ = ‖g‖

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i ≃ₗᵢ[𝕜] E₁ i
⊢ ‖g.compContinuousLinearMap fun i =>
        ↑{ toLinearEquiv := (f i).toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }‖ =
    ‖g‖

Tactic:
apply le_antisymm (g.norm_compContinuous_linearIsometry_le fun i => (f i).toLinearIsometry)

Result:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i ≃ₗᵢ[𝕜] E₁ i
⊢ ‖g‖ ≤ ‖g.compContinuousLinearMap fun i => (f i).toLinearIsometry.toContinuousLinearMap‖
-- Mathlib/Combinatorics/SetFamily/FourFunctions.lean
/-- The **Holley Inequality**. -/
lemma holley (hμ₀ : 0 ≤ μ) (hf : 0 ≤ f) (hg : 0 ≤ g) (hμ : Monotone μ)
    (hfg : ∑ a, f a = ∑ a, g a) (h : ∀ a b, f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)) :
    ∑ a, μ a * f a ≤ ∑ a, μ a * g a

Proof state:
case inr
α : Type u_1
β : Type u_2
inst✝³ : DistribLattice α
inst✝² : LinearOrderedCommSemiring β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hg : 0 ≤ g
hμ : Monotone μ
hfg : ∑ a : α, f a = ∑ a : α, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
⊢ ∑ a : α, μ a * f a ≤ ∑ a : α, μ a * g a

Tactic:
obtain rfl | hg := hg.eq_or_lt

Result:
case inr.inl
α : Type u_1
β : Type u_2
inst✝³ : DistribLattice α
inst✝² : LinearOrderedCommSemiring β
inst✝¹ : ExistsAddOfLE β
f μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hμ : Monotone μ
hf : 0 < f
hg : 0 ≤ 0
hfg : ∑ a : α, f a = ∑ a : α, 0 a
h : ∀ (a b : α), f a * 0 b ≤ f (a ⊓ b) * 0 (a ⊔ b)
⊢ ∑ a : α, μ a * f a ≤ ∑ a : α, μ a * 0 a

case inr.inr
α : Type u_1
β : Type u_2
inst✝³ : DistribLattice α
inst✝² : LinearOrderedCommSemiring β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hg✝ : 0 ≤ g
hμ : Monotone μ
hfg : ∑ a : α, f a = ∑ a : α, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
⊢ ∑ a : α, μ a * f a ≤ ∑ a : α, μ a * g a
-- Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean
/-- Any morphism between terminal objects is an isomorphism. -/
lemma isIso_of_isTerminal {X Y : C} (hX : IsTerminal X) (hY : IsTerminal Y) (f : X ⟶ Y) :
    IsIso f

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
hX : IsTerminal X
hY : IsTerminal Y
f : X ⟶ Y
⊢ IsIso f

Tactic:
refine ⟨⟨IsTerminal.from hX Y, ?_⟩⟩

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
hX : IsTerminal X
hY : IsTerminal Y
f : X ⟶ Y
⊢ f ≫ hX.from Y = 𝟙 X ∧ hX.from Y ≫ f = 𝟙 Y

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
hX : IsTerminal X
hY : IsTerminal Y
f : X ⟶ Y
⊢ hX.from Y ≫ f = 𝟙 Y

Tactic:
apply IsTerminal.hom_ext hY

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
hX : IsTerminal X
hY : IsTerminal Y
f : X ⟶ Y
⊢ f ≫ hX.from Y = 𝟙 X ∧ hX.from Y ≫ f = 𝟙 Y

Tactic:
simp only [IsTerminal.comp_from, IsTerminal.from_self, true_and]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
hX : IsTerminal X
hY : IsTerminal Y
f : X ⟶ Y
⊢ hX.from Y ≫ f = 𝟙 Y
-- Mathlib/RingTheory/DedekindDomain/Different.lean
lemma mem_dual (hI : I ≠ 0) {x} :
    x ∈ dual A K I ↔ ∀ a ∈ I, traceForm K L x a ∈ (algebraMap A K).range

Proof state:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
hI : I ≠ 0
x : L
⊢ x ∈ ⟨(↑I)ᵛ, ⋯⟩ ↔ ∀ a ∈ I, ((traceForm K L) x) a ∈ (algebraMap A K).range

Tactic:
exact forall₂_congr fun _ _ ↦ mem_one

Result:
no goals

Proof state:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
hI : I ≠ 0
x : L
⊢ x ∈ dual A K I ↔ ∀ a ∈ I, ((traceForm K L) x) a ∈ (algebraMap A K).range

Tactic:
rw [dual, dif_neg hI]

Result:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
hI : I ≠ 0
x : L
⊢ x ∈ ⟨(↑I)ᵛ, ⋯⟩ ↔ ∀ a ∈ I, ((traceForm K L) x) a ∈ (algebraMap A K).range