harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
theorem dist_le_dist_coe_div_sqrt (z w : ℍ) : dist z w ≤ dist (z : ℂ) w / √(z.im * w.im)

Proof state:
z w : ℍ
⊢ dist z w ≤ dist ↑z ↑w / √(z.im * w.im)

Tactic:
rw [dist_le_iff_le_sinh, ← div_mul_eq_div_div_swap, self_le_sinh_iff]

Result:
z w : ℍ
⊢ 0 ≤ dist ↑z ↑w / (2 * √(z.im * w.im))

Proof state:
z w : ℍ
⊢ 0 ≤ dist ↑z ↑w / (2 * √(z.im * w.im))

Tactic:
positivity

Result:
no goals
-- Mathlib/RingTheory/TensorProduct/Basic.lean
theorem baseChange_smul : (r • f).baseChange A = r • f.baseChange A

Proof state:
case a.h.h
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
r : R
f : M →ₗ[R] N
x✝ : M
⊢ ((AlgebraTensorModule.curry (baseChange A (r • f))) 1) x✝ = ((AlgebraTensorModule.curry (r • baseChange A f)) 1) x✝

Tactic:
simp [baseChange_tmul]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
r : R
f : M →ₗ[R] N
⊢ baseChange A (r • f) = r • baseChange A f

Tactic:
ext

Result:
case a.h.h
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
r : R
f : M →ₗ[R] N
x✝ : M
⊢ ((AlgebraTensorModule.curry (baseChange A (r • f))) 1) x✝ = ((AlgebraTensorModule.curry (r • baseChange A f)) 1) x✝
-- Mathlib/Probability/UniformOn.lean
theorem uniformOn_eq_one_of (hs : s.Finite) (hs' : s.Nonempty) (ht : s ⊆ t) :
    uniformOn s t = 1

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
hs : s.Finite
hs' : s.Nonempty
ht : s ⊆ t
⊢ (uniformOn s) t = 1

Tactic:
haveI := uniformOn_isProbabilityMeasure hs hs'

Result:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
hs : s.Finite
hs' : s.Nonempty
ht : s ⊆ t
this : IsProbabilityMeasure (uniformOn s)
⊢ (uniformOn s) t = 1

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
hs : s.Finite
hs' : s.Nonempty
ht : s ⊆ t
this : IsProbabilityMeasure (uniformOn s)
⊢ (uniformOn s) s ≤ (uniformOn s) t

Tactic:
exact measure_mono ht

Result:
no goals

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
hs : s.Finite
hs' : s.Nonempty
ht : s ⊆ t
this : IsProbabilityMeasure (uniformOn s)
⊢ ¬(uniformOn s) t < 1

Tactic:
rw [not_lt, ← uniformOn_self hs hs']

Result:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
hs : s.Finite
hs' : s.Nonempty
ht : s ⊆ t
this : IsProbabilityMeasure (uniformOn s)
⊢ (uniformOn s) s ≤ (uniformOn s) t

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
hs : s.Finite
hs' : s.Nonempty
ht : s ⊆ t
this : IsProbabilityMeasure (uniformOn s)
⊢ (uniformOn s) t = 1

Tactic:
refine eq_of_le_of_not_lt prob_le_one ?_

Result:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
hs : s.Finite
hs' : s.Nonempty
ht : s ⊆ t
this : IsProbabilityMeasure (uniformOn s)
⊢ ¬(uniformOn s) t < 1
-- Mathlib/Topology/Algebra/Monoid.lean
theorem continuousMul_of_comm_of_nhds_one (M : Type u) [CommMonoid M] [TopologicalSpace M]
    (hmul : Tendsto (uncurry ((· * ·) : M → M → M)) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1))
    (hleft : ∀ x₀ : M, 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)) : ContinuousMul M

Proof state:
M : Type u
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 => x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
⊢ ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)

Tactic:
intro x₀

Result:
M : Type u
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 => x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
x₀ : M
⊢ 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)

Proof state:
M : Type u
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 => x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
x₀ : M
⊢ 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)

Tactic:
simp_rw [mul_comm, hleft x₀]

Result:
no goals

Proof state:
M : Type u
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 => x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
⊢ ContinuousMul M

Tactic:
apply ContinuousMul.of_nhds_one hmul hleft

Result:
M : Type u
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 => x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
⊢ ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
@[to_additive]
lemma IsFundamentalDomain.quotientMeasure_eq [Countable G] [MeasurableSpace G] {s t : Set α}
    [SMulInvariantMeasure G α μ] [MeasurableSMul G α] (fund_dom_s : IsFundamentalDomain G s μ)
    (fund_dom_t : IsFundamentalDomain G t μ) :
    (μ.restrict s).map π = (μ.restrict t).map π

Proof state:
case h.hA.h
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : Countable G
inst✝² : MeasurableSpace G
s t : Set α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : MeasurableSMul G α
fund_dom_s : IsFundamentalDomain G s μ
fund_dom_t : IsFundamentalDomain G t μ
U : Set (Quotient α_mod_G)
meas_U : MeasurableSet U
g : G
x : α
⊢ x ∈ (fun x => g • x) ⁻¹' (Quotient.mk α_mod_G ⁻¹' U) ↔ x ∈ Quotient.mk α_mod_G ⁻¹' U

Tactic:
have : Quotient.mk α_mod_G (g • x) = Quotient.mk α_mod_G x := by
  apply Quotient.sound
  use g

Result:
case h.hA.h
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : Countable G
inst✝² : MeasurableSpace G
s t : Set α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : MeasurableSMul G α
fund_dom_s : IsFundamentalDomain G s μ
fund_dom_t : IsFundamentalDomain G t μ
U : Set (Quotient α_mod_G)
meas_U : MeasurableSet U
g : G
x : α
this : ⟦g • x⟧ = ⟦x⟧
⊢ x ∈ (fun x => g • x) ⁻¹' (Quotient.mk α_mod_G ⁻¹' U) ↔ x ∈ Quotient.mk α_mod_G ⁻¹' U

Proof state:
case h.hA.h
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : Countable G
inst✝² : MeasurableSpace G
s t : Set α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : MeasurableSMul G α
fund_dom_s : IsFundamentalDomain G s μ
fund_dom_t : IsFundamentalDomain G t μ
U : Set (Quotient α_mod_G)
meas_U : MeasurableSet U
g : G
x : α
this : ⟦g • x⟧ = ⟦x⟧
⊢ x ∈ (fun x => g • x) ⁻¹' (Quotient.mk α_mod_G ⁻¹' U) ↔ x ∈ Quotient.mk α_mod_G ⁻¹' U

Tactic:
simp only [mem_preimage, this]

Result:
no goals
-- Mathlib/Computability/ContextFreeGrammar.lean
/-- Add extra postfix to context-free deriving. -/
lemma Derives.append_right {v w : List (Symbol T g.NT)}
    (hvw : g.Derives v w) (p : List (Symbol T g.NT)) :
    g.Derives (v ++ p) (w ++ p)

Proof state:
case tail
T : Type u_1
g : ContextFreeGrammar T
v w p b✝ c✝ : List (Symbol T g.NT)
a✝ : Relation.ReflTransGen g.Produces v b✝
last : g.Produces b✝ c✝
ih : g.Derives (v ++ p) (b✝ ++ p)
⊢ g.Derives (v ++ p) (c✝ ++ p)

Tactic:
exact ih.trans_produces <| last.append_right p

Result:
no goals

Proof state:
case refl
T : Type u_1
g : ContextFreeGrammar T
v w p : List (Symbol T g.NT)
⊢ g.Derives (v ++ p) (v ++ p)

Tactic:
rfl

Result:
no goals

Proof state:
T : Type u_1
g : ContextFreeGrammar T
v w : List (Symbol T g.NT)
hvw : g.Derives v w
p : List (Symbol T g.NT)
⊢ g.Derives (v ++ p) (w ++ p)

Tactic:
induction hvw with
| refl => rfl
| tail _ last ih => exact ih.trans_produces <| last.append_right p

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Ring.lean
theorem hasSum_div_const_iff (h : a₂ ≠ 0) : HasSum (fun i ↦ f i / a₂) (a₁ / a₂) ↔ HasSum f a₁

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalSemiring α
f : ι → α
a₁ a₂ : α
h : a₂ ≠ 0
⊢ HasSum (fun i => f i / a₂) (a₁ / a₂) ↔ HasSum f a₁

Tactic:
simpa only [div_eq_mul_inv] using hasSum_mul_right_iff (inv_ne_zero h)

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma negAddY_of_X_eq' {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q)
    (hx : P x * Q z ^ 2 = Q x * P z ^ 2) :
    W'.negAddY P Q * (P z * Q z) ^ 3 = (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 3

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ (P y * Q z ^ 3 - Q y * P z ^ 3) *
        ((P y * Q z ^ 3 - Q y * P z ^ 3) ^ 2 + W'.a₁ * (P y * Q z ^ 3 - Q y * P z ^ 3) * P z * Q z * 0 -
                W'.a₂ * P z ^ 2 * Q z ^ 2 * 0 ^ 2 -
              P x * Q z ^ 2 * 0 ^ 2 -
            Q x * P z ^ 2 * 0 ^ 2 -
          P x * Q z ^ 2 * 0 ^ 2) +
      P y * Q z ^ 3 * 0 ^ 3 =
    (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 3

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W'.negAddY P Q * (P z * Q z) ^ 3 = (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 3

Tactic:
rw [negAddY_eq', addX_eq' hP hQ, addZ_of_X_eq hx]

Result:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ (P y * Q z ^ 3 - Q y * P z ^ 3) *
        ((P y * Q z ^ 3 - Q y * P z ^ 3) ^ 2 + W'.a₁ * (P y * Q z ^ 3 - Q y * P z ^ 3) * P z * Q z * 0 -
                W'.a₂ * P z ^ 2 * Q z ^ 2 * 0 ^ 2 -
              P x * Q z ^ 2 * 0 ^ 2 -
            Q x * P z ^ 2 * 0 ^ 2 -
          P x * Q z ^ 2 * 0 ^ 2) +
      P y * Q z ^ 3 * 0 ^ 3 =
    (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 3
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem mk_coeFn (f : α →ₘ[μ] β) : mk f f.aestronglyMeasurable = f

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
⊢ mk
      (if h : ∃ b, f = mk (const α b) ⋯ then const α (Classical.choose h)
      else AEStronglyMeasurable.mk ↑(Quotient.out f) ⋯)
      ⋯ =
    f

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
h : ∃ b, f = mk (const α b) ⋯
⊢ mk (const α (Classical.choose h)) ⋯ = f

case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
h : ¬∃ b, f = mk (const α b) ⋯
⊢ mk (AEStronglyMeasurable.mk ↑(Quotient.out f) ⋯) ⋯ = f

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
h : ∃ b, f = mk (const α b) ⋯
⊢ mk (const α (Classical.choose h)) ⋯ = f

Tactic:
exact Classical.choose_spec h |>.symm

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
⊢ mk ↑f ⋯ = f

Tactic:
conv_lhs => simp only [cast]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
⊢ mk
      (if h : ∃ b, f = mk (const α b) ⋯ then const α (Classical.choose h)
      else AEStronglyMeasurable.mk ↑(Quotient.out f) ⋯)
      ⋯ =
    f

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
h : ¬∃ b, f = mk (const α b) ⋯
⊢ mk (AEStronglyMeasurable.mk ↑(Quotient.out f) ⋯) ⋯ = Quotient.mk'' (Quotient.out f)

Tactic:
rw [← mk, mk_eq_mk]

Result:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
h : ¬∃ b, f = mk (const α b) ⋯
⊢ AEStronglyMeasurable.mk ↑(Quotient.out f) ⋯ =ᶠ[ae μ] ↑(Quotient.out f)

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
h : ¬∃ b, f = mk (const α b) ⋯
⊢ mk (AEStronglyMeasurable.mk ↑(Quotient.out f) ⋯) ⋯ = f

Tactic:
conv_rhs => rw [← Quotient.out_eq' f]

Result:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
h : ¬∃ b, f = mk (const α b) ⋯
⊢ mk (AEStronglyMeasurable.mk ↑(Quotient.out f) ⋯) ⋯ = Quotient.mk'' (Quotient.out f)

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
h : ¬∃ b, f = mk (const α b) ⋯
⊢ AEStronglyMeasurable.mk ↑(Quotient.out f) ⋯ =ᶠ[ae μ] ↑(Quotient.out f)

Tactic:
exact (AEStronglyMeasurable.ae_eq_mk _).symm

Result:
no goals
-- Mathlib/Topology/ContinuousMap/CompactlySupported.lean
@[simp] lemma toReal_add (f g : C_c(α, ℝ≥0)) : (f + g).toReal = f.toReal + g.toReal

Proof state:
case h
α : Type u_2
inst✝ : TopologicalSpace α
f g : α →C_c ℝ≥0
x✝ : α
⊢ (f + g).toReal x✝ = (f.toReal + g.toReal) x✝

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
f g : α →C_c ℝ≥0
⊢ (f + g).toReal = f.toReal + g.toReal

Tactic:
ext

Result:
case h
α : Type u_2
inst✝ : TopologicalSpace α
f g : α →C_c ℝ≥0
x✝ : α
⊢ (f + g).toReal x✝ = (f.toReal + g.toReal) x✝
-- Mathlib/Data/Real/GoldenRatio.lean
theorem inv_goldConj : ψ⁻¹ = -φ

Proof state:
⊢ ψ⁻¹ = -φ

Tactic:
rw [inv_eq_iff_eq_inv, ← neg_inv, ← neg_eq_iff_eq_neg]

Result:
⊢ -ψ = φ⁻¹

Proof state:
⊢ -ψ = φ⁻¹

Tactic:
exact inv_gold.symm

Result:
no goals
-- Mathlib/Topology/Compactification/OnePoint.lean
@[simp]
lemma some_eq_iff (x₁ x₂ : X) : (some x₁ = some x₂) ↔ (x₁ = x₂)

Proof state:
X : Type u_1
x₁ x₂ : X
⊢ ↑x₁ = ↑x₂ ↔ x₁ = x₂

Tactic:
rw [iff_eq_eq]

Result:
X : Type u_1
x₁ x₂ : X
⊢ (↑x₁ = ↑x₂) = (x₁ = x₂)

Proof state:
X : Type u_1
x₁ x₂ : X
⊢ (↑x₁ = ↑x₂) = (x₁ = x₂)

Tactic:
exact Option.some.injEq x₁ x₂

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem norm_le_of_tsum_le (hp : 0 < p.toReal) {C : ℝ} (hC : 0 ≤ C) {f : lp E p}
    (hf : ∑' i, ‖f i‖ ^ p.toReal ≤ C ^ p.toReal) : ‖f‖ ≤ C

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
C : ℝ
hC : 0 ≤ C
f : ↥(lp E p)
hf : ∑' (i : α), ‖↑f i‖ ^ p.toReal ≤ C ^ p.toReal
⊢ ∑' (i : α), ‖↑f i‖ ^ p.toReal ≤ C ^ p.toReal

Tactic:
exact hf

Result:
no goals

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
C : ℝ
hC : 0 ≤ C
f : ↥(lp E p)
hf : ∑' (i : α), ‖↑f i‖ ^ p.toReal ≤ C ^ p.toReal
⊢ ‖f‖ ≤ C

Tactic:
rw [← Real.rpow_le_rpow_iff (norm_nonneg' _) hC hp, norm_rpow_eq_tsum hp]

Result:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
C : ℝ
hC : 0 ≤ C
f : ↥(lp E p)
hf : ∑' (i : α), ‖↑f i‖ ^ p.toReal ≤ C ^ p.toReal
⊢ ∑' (i : α), ‖↑f i‖ ^ p.toReal ≤ C ^ p.toReal
-- Mathlib/Data/List/Sublists.lean
theorem sublistsLen_one (l : List α) : sublistsLen 1 l = l.reverse.map ([·]) :=
  l.rec (by rw [sublistsLen_succ_nil, reverse_nil, map_nil]) fun a s ih ↦ by
    rw [sublistsLen_succ_cons, ih, reverse_cons, map_append, sublistsLen_zero]; rfl

Proof state:
α : Type u
l : List α
a : α
s : List α
ih : sublistsLen 1 s = map (fun x => [x]) s.reverse
⊢ map (fun x => [x]) s.reverse ++ map (cons a) [[]] = map (fun x => [x]) s.reverse ++ map (fun x => [x]) [a]

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
l : List α
⊢ sublistsLen 1 [] = map (fun x => [x]) [].reverse

Tactic:
rw [sublistsLen_succ_nil, reverse_nil, map_nil]

Result:
no goals

Proof state:
α : Type u
l : List α
a : α
s : List α
ih : sublistsLen 1 s = map (fun x => [x]) s.reverse
⊢ sublistsLen 1 (a :: s) = map (fun x => [x]) (a :: s).reverse

Tactic:
rw [sublistsLen_succ_cons, ih, reverse_cons, map_append, sublistsLen_zero]

Result:
α : Type u
l : List α
a : α
s : List α
ih : sublistsLen 1 s = map (fun x => [x]) s.reverse
⊢ map (fun x => [x]) s.reverse ++ map (cons a) [[]] = map (fun x => [x]) s.reverse ++ map (fun x => [x]) [a]
-- Mathlib/Geometry/Euclidean/Inversion/ImageHyperplane.lean
theorem preimage_inversion_sphere_dist_center (hR : R ≠ 0) (hy : y ≠ c) :
    inversion c R ⁻¹' sphere y (dist y c) =
      insert c (perpBisector c (inversion c R y) : Set P)

Proof state:
case h
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
x : P
⊢ x ∈ inversion c R ⁻¹' sphere y (dist y c) ↔ x ∈ insert c ↑(perpBisector c (inversion c R y))

Tactic:
rcases eq_or_ne x c with rfl | hx

Result:
case h.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
y : P
R : ℝ
hR : R ≠ 0
x : P
hy : y ≠ x
⊢ x ∈ inversion x R ⁻¹' sphere y (dist y x) ↔ x ∈ insert x ↑(perpBisector x (inversion x R y))

case h.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
x : P
hx : x ≠ c
⊢ x ∈ inversion c R ⁻¹' sphere y (dist y c) ↔ x ∈ insert c ↑(perpBisector c (inversion c R y))

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
⊢ inversion c R ⁻¹' sphere y (dist y c) = insert c ↑(perpBisector c (inversion c R y))

Tactic:
ext x

Result:
case h
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
x : P
⊢ x ∈ inversion c R ⁻¹' sphere y (dist y c) ↔ x ∈ insert c ↑(perpBisector c (inversion c R y))

Proof state:
case h.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
x : P
hx : x ≠ c
⊢ x ∈ inversion c R ⁻¹' sphere y (dist y c) ↔ x ∈ insert c ↑(perpBisector c (inversion c R y))

Tactic:
rw [mem_preimage, mem_sphere, ← inversion_mem_perpBisector_inversion_iff hR] <;> simp [*]

Result:
no goals

Proof state:
case h.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
y : P
R : ℝ
hR : R ≠ 0
x : P
hy : y ≠ x
⊢ x ∈ inversion x R ⁻¹' sphere y (dist y x) ↔ x ∈ insert x ↑(perpBisector x (inversion x R y))

Tactic:
simp [dist_comm]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean
theorem IsPrimitive.zmod_char_eq_one_iff (n : ℕ) [NeZero n]
    {ψ : AddChar (ZMod n) C} (hψ : IsPrimitive ψ) (a : ZMod n) :
    ψ a = 1 ↔ a = 0

Proof state:
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ψ : AddChar (ZMod n) C
hψ : ψ.IsPrimitive
a : ZMod n
⊢ ψ a = 1 ↔ a = 0

Tactic:
refine ⟨fun h => not_imp_comm.mp (@hψ a) ?_, fun ha => by rw [ha, map_zero_eq_one]⟩

Result:
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ψ : AddChar (ZMod n) C
hψ : ψ.IsPrimitive
a : ZMod n
h : ψ a = 1
⊢ ¬ψ.mulShift a ≠ 1

Proof state:
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ψ : AddChar (ZMod n) C
hψ : ψ.IsPrimitive
a : ZMod n
h : ψ a = 1
⊢ ¬ψ.mulShift a ≠ 1

Tactic:
rw [zmod_char_ne_one_iff n (mulShift ψ a), mulShift_apply, mul_one, h, Classical.not_not]

Result:
no goals

Proof state:
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ψ : AddChar (ZMod n) C
hψ : ψ.IsPrimitive
a : ZMod n
ha : a = 0
⊢ ψ a = 1

Tactic:
rw [ha, map_zero_eq_one]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem add_mul_succ {a b : Ordinal} (c) (ba : b + a = a) : (a + b) * succ c = a * succ c + b

Proof state:
a b c : Ordinal.{u_4}
ba : b + a = a
⊢ (a + b) * succ c = a * succ c + b

Tactic:
induction c using limitRecOn with
| H₁ => simp only [succ_zero, mul_one]
| H₂ c IH =>
  rw [mul_succ, IH, ← add_assoc, add_assoc _ b, ba, ← mul_succ]
| H₃ c l IH =>
  rw [mul_succ, add_mul_limit_aux ba l IH, mul_succ, add_assoc]

Result:
no goals

Proof state:
case H₁
a b : Ordinal.{u_4}
ba : b + a = a
⊢ (a + b) * succ 0 = a * succ 0 + b

Tactic:
simp only [succ_zero, mul_one]

Result:
no goals

Proof state:
case H₃
a b : Ordinal.{u_4}
ba : b + a = a
c : Ordinal.{u_4}
l : c.IsLimit
IH : ∀ o' < c, (a + b) * succ o' = a * succ o' + b
⊢ (a + b) * succ c = a * succ c + b

Tactic:
rw [mul_succ, add_mul_limit_aux ba l IH, mul_succ, add_assoc]

Result:
no goals

Proof state:
case H₂
a b : Ordinal.{u_4}
ba : b + a = a
c : Ordinal.{u_4}
IH : (a + b) * succ c = a * succ c + b
⊢ (a + b) * succ (succ c) = a * succ (succ c) + b

Tactic:
rw [mul_succ, IH, ← add_assoc, add_assoc _ b, ba, ← mul_succ]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addY_of_X_eq' {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q)
    (hx : P x * Q z ^ 2 = Q x * P z ^ 2) :
    W'.addY P Q * (P z * Q z) ^ 3 = (-(P y * Q z ^ 3 - Q y * P z ^ 3)) ^ 3

Proof state:
case a.a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W'.addY P Q * (P z * Q z) ^ 3 + W'.negAddY P Q * (P z * Q z) ^ 3 -
      ((-(P y * Q z ^ 3 - Q y * P z ^ 3)) ^ 3 + (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 3) =
    0

Tactic:
rw [addY, negY_eq, addZ_of_X_eq hx]

Result:
case a.a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ (-W'.negAddY P Q - W'.a₁ * W'.addX P Q * 0 - W'.a₃ * 0 ^ 3) * (P z * Q z) ^ 3 + W'.negAddY P Q * (P z * Q z) ^ 3 -
      ((-(P y * Q z ^ 3 - Q y * P z ^ 3)) ^ 3 + (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 3) =
    0

Proof state:
case a.a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ (-W'.negAddY P Q - W'.a₁ * W'.addX P Q * 0 - W'.a₃ * 0 ^ 3) * (P z * Q z) ^ 3 + W'.negAddY P Q * (P z * Q z) ^ 3 -
      ((-(P y * Q z ^ 3 - Q y * P z ^ 3)) ^ 3 + (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 3) =
    0

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W'.addY P Q * (P z * Q z) ^ 3 = (-(P y * Q z ^ 3 - Q y * P z ^ 3)) ^ 3

Tactic:
linear_combination (norm := (rw [addY, negY_eq, addZ_of_X_eq hx]; ring1))
  -negAddY_of_X_eq' hP hQ hx

Result:
no goals