harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem edist_le_tsum_of_edist_le_of_tendsto {f : ℕ → α} (d : ℕ → ℝ≥0∞)
    (hf : ∀ n, edist (f n) (f n.succ) ≤ d n) {a : α} (ha : Tendsto f atTop (𝓝 a)) (n : ℕ) :
    edist (f n) a ≤ ∑' m, d (n + m)

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ ∑ k ∈ Finset.range (m - n), d (n + k) ≤ ∑' (m : ℕ), d (n + m)

Tactic:
exact sum_le_tsum _ (fun _ _ => zero_le _) ENNReal.summable

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ edist (f n) a ≤ ∑' (m : ℕ), d (n + m)

Tactic:
refine le_of_tendsto (tendsto_const_nhds.edist ha) (mem_atTop_sets.2 ⟨n, fun m hnm => ?_⟩)

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ m ∈ {x | (fun c => edist (f n) (f c) ≤ ∑' (m : ℕ), d (n + m)) x}

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ m ∈ {x | (fun c => edist (f n) (f c) ≤ ∑' (m : ℕ), d (n + m)) x}

Tactic:
change edist _ _ ≤ _

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ edist (f n) (f m) ≤ ∑' (m : ℕ), d (n + m)

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ ∑ i ∈ Finset.Ico n m, d i ≤ ∑' (m : ℕ), d (n + m)

Tactic:
rw [Finset.sum_Ico_eq_sum_range]

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ ∑ k ∈ Finset.range (m - n), d (n + k) ≤ ∑' (m : ℕ), d (n + m)

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ edist (f n) (f m) ≤ ∑' (m : ℕ), d (n + m)

Tactic:
refine le_trans (edist_le_Ico_sum_of_edist_le hnm fun _ _ => hf _) ?_

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ ∑ i ∈ Finset.Ico n m, d i ≤ ∑' (m : ℕ), d (n + m)
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem contDiffOn_succ_iff_deriv_of_isOpen (hs : IsOpen s₂) :
    ContDiffOn 𝕜 (n + 1) f₂ s₂ ↔
      DifferentiableOn 𝕜 f₂ s₂ ∧ (n = ω → AnalyticOn 𝕜 f₂ s₂) ∧
        ContDiffOn 𝕜 n (deriv f₂) s₂

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f₂ : 𝕜 → F
s₂ : Set 𝕜
hs : IsOpen s₂
⊢ ContDiffOn 𝕜 (n + 1) f₂ s₂ ↔ DifferentiableOn 𝕜 f₂ s₂ ∧ (n = ω → AnalyticOn 𝕜 f₂ s₂) ∧ ContDiffOn 𝕜 n (deriv f₂) s₂

Tactic:
rw [contDiffOn_succ_iff_derivWithin hs.uniqueDiffOn]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f₂ : 𝕜 → F
s₂ : Set 𝕜
hs : IsOpen s₂
⊢ DifferentiableOn 𝕜 f₂ s₂ ∧ (n = ω → AnalyticOn 𝕜 f₂ s₂) ∧ ContDiffOn 𝕜 n (derivWithin f₂ s₂) s₂ ↔
    DifferentiableOn 𝕜 f₂ s₂ ∧ (n = ω → AnalyticOn 𝕜 f₂ s₂) ∧ ContDiffOn 𝕜 n (deriv f₂) s₂

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f₂ : 𝕜 → F
s₂ : Set 𝕜
hs : IsOpen s₂
⊢ DifferentiableOn 𝕜 f₂ s₂ ∧ (n = ω → AnalyticOn 𝕜 f₂ s₂) ∧ ContDiffOn 𝕜 n (derivWithin f₂ s₂) s₂ ↔
    DifferentiableOn 𝕜 f₂ s₂ ∧ (n = ω → AnalyticOn 𝕜 f₂ s₂) ∧ ContDiffOn 𝕜 n (deriv f₂) s₂

Tactic:
exact Iff.rfl.and (Iff.rfl.and (contDiffOn_congr fun _ => derivWithin_of_isOpen hs))

Result:
no goals
-- Mathlib/Logic/Nontrivial/Basic.lean
theorem Subtype.nontrivial_iff_exists_ne (p : α → Prop) (x : Subtype p) :
    Nontrivial (Subtype p) ↔ ∃ (y : α) (_ : p y), y ≠ x

Proof state:
α : Type u_1
p : α → Prop
x : Subtype p
⊢ Nontrivial (Subtype p) ↔ ∃ y x_1, y ≠ x.val

Tactic:
simp only [_root_.nontrivial_iff_exists_ne x, Subtype.exists, Ne, Subtype.ext_iff]

Result:
no goals
-- Mathlib/FieldTheory/IsAlgClosed/Classification.lean
theorem ringEquiv_of_Cardinal_eq_of_charP (p : ℕ) [Fact p.Prime] [CharP K p] [CharP L p]
    (hK : ℵ₀ < #K) (hKL : Nonempty (K ≃ L)) : Nonempty (K ≃+* L)

Proof state:
case intro.intro
K : Type u
L : Type v
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this✝ : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
t : Set L
ht : IsTranscendenceBasis (ZMod p) Subtype.val
hL : ℵ₀ < #L
⊢ Nonempty (K ≃+* L)

Tactic:
have : Cardinal.lift.{v} #s = Cardinal.lift.{u} #t := by
  rw [← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _
      hs (le_of_lt (lt_aleph0_of_finite _)) hK),
    ← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _
      ht (le_of_lt (lt_aleph0_of_finite _)) hL)]
  exact Cardinal.lift_mk_eq'.2 hKL

Result:
case intro.intro
K : Type u
L : Type v
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this✝¹ : Algebra (ZMod p) K := ZMod.algebra K p
this✝ : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
t : Set L
ht : IsTranscendenceBasis (ZMod p) Subtype.val
hL : ℵ₀ < #L
this : Cardinal.lift.{v, u} #↑s = Cardinal.lift.{u, v} #↑t
⊢ Nonempty (K ≃+* L)

Proof state:
K : Type u
L : Type v
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this✝ : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
t : Set L
ht : IsTranscendenceBasis (ZMod p) Subtype.val
hL : ℵ₀ < #L
⊢ Cardinal.lift.{v, u} #K = Cardinal.lift.{u, v} #L

Tactic:
exact Cardinal.lift_mk_eq'.2 hKL

Result:
no goals

Proof state:
case intro
K : Type u
L : Type v
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this✝ : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
⊢ Nonempty (K ≃+* L)

Tactic:
obtain ⟨t, ht⟩ := exists_isTranscendenceBasis (ZMod p)
  (show Function.Injective (algebraMap (ZMod p) L) from RingHom.injective _)

Result:
case intro.intro
K : Type u
L : Type v
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this✝ : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
t : Set L
ht : IsTranscendenceBasis (ZMod p) Subtype.val
⊢ Nonempty (K ≃+* L)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem isEqv_eq [DecidableEq α] {l₁ l₂ : Array α} : l₁.isEqv l₂ (· == ·) = (l₁ = l₂)

Proof state:
case mk
α : Type u_1
inst✝ : DecidableEq α
l₂ : Array α
toList✝ : List α
⊢ (({ toList := toList✝ }.isEqv l₂ fun x1 x2 => x1 == x2) = true) = ({ toList := toList✝ } = l₂)

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
inst✝ : DecidableEq α
toList✝¹ toList✝ : List α
⊢ (({ toList := toList✝¹ }.isEqv { toList := toList✝ } fun x1 x2 => x1 == x2) = true) =
    ({ toList := toList✝¹ } = { toList := toList✝ })

Proof state:
case mk.mk
α : Type u_1
inst✝ : DecidableEq α
toList✝¹ toList✝ : List α
⊢ (({ toList := toList✝¹ }.isEqv { toList := toList✝ } fun x1 x2 => x1 == x2) = true) =
    ({ toList := toList✝¹ } = { toList := toList✝ })

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : Array α
⊢ ((l₁.isEqv l₂ fun x1 x2 => x1 == x2) = true) = (l₁ = l₂)

Tactic:
cases l₁

Result:
case mk
α : Type u_1
inst✝ : DecidableEq α
l₂ : Array α
toList✝ : List α
⊢ (({ toList := toList✝ }.isEqv l₂ fun x1 x2 => x1 == x2) = true) = ({ toList := toList✝ } = l₂)
-- Mathlib/Topology/Instances/NNReal/Lemmas.lean
theorem tendsto_tsum_compl_atTop_zero {α : Type*} (f : α → ℝ≥0) :
    Tendsto (fun s : Finset α => ∑' b : { x // x ∉ s }, f b) atTop (𝓝 0)

Proof state:
α : Type u_2
f : α → ℝ≥0
⊢ Tendsto (fun s => ∑' (b : { x // x ∉ s }), f ↑b) atTop (𝓝 0)

Tactic:
simp_rw [← tendsto_coe, coe_tsum, NNReal.coe_zero]

Result:
α : Type u_2
f : α → ℝ≥0
⊢ Tendsto (fun a => ∑' (a_1 : { x // x ∉ a }), ↑(f ↑a_1)) atTop (𝓝 0)

Proof state:
α : Type u_2
f : α → ℝ≥0
⊢ Tendsto (fun a => ∑' (a_1 : { x // x ∉ a }), ↑(f ↑a_1)) atTop (𝓝 0)

Tactic:
exact tendsto_tsum_compl_atTop_zero fun a : α => (f a : ℝ)

Result:
no goals
-- Mathlib/MeasureTheory/Function/UniformIntegrable.lean
theorem MemLp.eLpNormEssSup_indicator_norm_ge_eq_zero (hf : MemLp f ∞ μ)
    (hmeas : StronglyMeasurable f) :
    ∃ M : ℝ, eLpNormEssSup ({ x | M ≤ ‖f x‖₊ }.indicator f) μ = 0

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ⊤ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ⊤
this : {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} ⊆ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
hle : μ {a | eLpNormEssSup f μ < ‖f a‖ₑ} = 0
⊢ μ {x | eLpNormEssSup f μ < ↑‖f x‖₊} ≤ 0

Tactic:
exact nonpos_iff_eq_zero.2 hle

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ⊤ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ⊤
⊢ ∃ M, eLpNormEssSup ({x | M ≤ ↑‖f x‖₊}.indicator f) μ = 0

Tactic:
refine ⟨(eLpNorm f ∞ μ + 1).toReal, ?_⟩

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ⊤ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ⊤
⊢ eLpNormEssSup ({x | (eLpNorm f ⊤ μ + 1).toReal ≤ ↑‖f x‖₊}.indicator f) μ = 0

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ⊤ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ⊤
this : {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} ⊆ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
⊢ μ {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} ≤ 0

Tactic:
refine (measure_mono this).trans ?_

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ⊤ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ⊤
this : {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} ⊆ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
⊢ μ {x | eLpNormEssSup f μ < ↑‖f x‖₊} ≤ 0

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ⊤ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ⊤
this : {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} ⊆ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
⊢ μ {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} = 0

Tactic:
rw [← nonpos_iff_eq_zero]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f ⊤ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ⊤
this : {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} ⊆ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
⊢ μ {x | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} ≤ 0
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem degree_div_le (p q : R[X]) : degree (p / q) ≤ degree p

Proof state:
case pos
R : Type u
inst✝ : Field R
p q : R[X]
hq : q = 0
⊢ (p / q).degree ≤ p.degree

Tactic:
simp [hq]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : Field R
p q : R[X]
hq : ¬q = 0
⊢ (p /ₘ (q * C q.leadingCoeff⁻¹)).degree ≤ p.degree

Tactic:
exact degree_divByMonic_le _ _

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : Field R
p q : R[X]
hq : ¬q = 0
⊢ (p / q).degree ≤ p.degree

Tactic:
rw [div_def, mul_comm, degree_mul_leadingCoeff_inv _ hq]

Result:
case neg
R : Type u
inst✝ : Field R
p q : R[X]
hq : ¬q = 0
⊢ (p /ₘ (q * C q.leadingCoeff⁻¹)).degree ≤ p.degree

Proof state:
R : Type u
inst✝ : Field R
p q : R[X]
⊢ (p / q).degree ≤ p.degree

Tactic:
by_cases hq : q = 0

Result:
case pos
R : Type u
inst✝ : Field R
p q : R[X]
hq : q = 0
⊢ (p / q).degree ≤ p.degree

case neg
R : Type u
inst✝ : Field R
p q : R[X]
hq : ¬q = 0
⊢ (p / q).degree ≤ p.degree
-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
lemma ker_ideal_of_isPullback_of_isOpenImmersion {X Y U V : Scheme.{u}}
    (f : X ⟶ Y) (f' : U ⟶ V) (iU : U ⟶ X) (iV : V ⟶ Y) [IsOpenImmersion iV]
    [QuasiCompact f] (H : IsPullback f' iU iV f) (W) :
    f'.ker.ideal W =
      (f.ker.ideal ⟨iV ''ᵁ W, W.2.image_of_isOpenImmersion _⟩).comap (iV.appIso W).inv.hom

Proof state:
case h
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : QuasiCompact f
H : IsPullback f' iU iV f
W : ↑V.affineOpens
this✝² : QuasiCompact f'
this✝¹ : IsOpenImmersion iU
x : ↑Γ(V, ↑W)
this✝ : iU ''ᵁ f' ⁻¹ᵁ ↑W = f ⁻¹ᵁ iV ''ᵁ ↑W
e : Γ(X, f ⁻¹ᵁ iV ''ᵁ ↑W) ≅ Γ(U, f' ⁻¹ᵁ ↑W) := Functor.mapIso X.presheaf (eqToIso this✝).op ≪≫ Hom.appIso iU (f' ⁻¹ᵁ ↑W)
this : (Hom.appIso iV ↑W).inv ≫ Hom.app f (iV ''ᵁ ↑W) = Hom.app f' ↑W ≫ e.inv
⊢ x ∈ (Hom.ker f').ideal W ↔
    x ∈ Ideal.comap (CommRingCat.Hom.hom (Hom.appIso iV ↑W).inv) ((Hom.ker f).ideal ⟨iV ''ᵁ ↑W, ⋯⟩)

Tactic:
simp only [Scheme.Hom.ker_apply, RingHom.mem_ker, Ideal.mem_comap, ← RingHom.comp_apply,
  ← CommRingCat.hom_comp, Scheme.Hom.appIso_inv_app, this]

Result:
case h
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : QuasiCompact f
H : IsPullback f' iU iV f
W : ↑V.affineOpens
this✝² : QuasiCompact f'
this✝¹ : IsOpenImmersion iU
x : ↑Γ(V, ↑W)
this✝ : iU ''ᵁ f' ⁻¹ᵁ ↑W = f ⁻¹ᵁ iV ''ᵁ ↑W
e : Γ(X, f ⁻¹ᵁ iV ''ᵁ ↑W) ≅ Γ(U, f' ⁻¹ᵁ ↑W) := Functor.mapIso X.presheaf (eqToIso this✝).op ≪≫ Hom.appIso iU (f' ⁻¹ᵁ ↑W)
this : (Hom.appIso iV ↑W).inv ≫ Hom.app f (iV ''ᵁ ↑W) = Hom.app f' ↑W ≫ e.inv
⊢ (CommRingCat.Hom.hom (Hom.app f' ↑W)) x = 0 ↔ (CommRingCat.Hom.hom (Hom.app f' ↑W ≫ e.inv)) x = 0

Proof state:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : QuasiCompact f
H : IsPullback f' iU iV f
W : ↑V.affineOpens
⊢ (Hom.ker f').ideal W = Ideal.comap (CommRingCat.Hom.hom (Hom.appIso iV ↑W).inv) ((Hom.ker f).ideal ⟨iV ''ᵁ ↑W, ⋯⟩)

Tactic:
have : QuasiCompact f' := MorphismProperty.of_isPullback H.flip inferInstance

Result:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : QuasiCompact f
H : IsPullback f' iU iV f
W : ↑V.affineOpens
this : QuasiCompact f'
⊢ (Hom.ker f').ideal W = Ideal.comap (CommRingCat.Hom.hom (Hom.appIso iV ↑W).inv) ((Hom.ker f).ideal ⟨iV ''ᵁ ↑W, ⋯⟩)

Proof state:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : QuasiCompact f
H : IsPullback f' iU iV f
W : ↑V.affineOpens
this✝ : QuasiCompact f'
this : IsOpenImmersion iU
⊢ (Hom.ker f').ideal W = Ideal.comap (CommRingCat.Hom.hom (Hom.appIso iV ↑W).inv) ((Hom.ker f).ideal ⟨iV ''ᵁ ↑W, ⋯⟩)

Tactic:
ext x

Result:
case h
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : QuasiCompact f
H : IsPullback f' iU iV f
W : ↑V.affineOpens
this✝ : QuasiCompact f'
this : IsOpenImmersion iU
x : ↑Γ(V, ↑W)
⊢ x ∈ (Hom.ker f').ideal W ↔
    x ∈ Ideal.comap (CommRingCat.Hom.hom (Hom.appIso iV ↑W).inv) ((Hom.ker f).ideal ⟨iV ''ᵁ ↑W, ⋯⟩)
-- Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean
lemma inv_variableChange_Δ' : (W.variableChange C).Δ'⁻¹ = C.u ^ 12 * W.Δ'⁻¹

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst✝ : W.IsElliptic
⊢ (W.variableChange C).Δ'⁻¹ = C.u ^ 12 * W.Δ'⁻¹

Tactic:
rw [variableChange_Δ', mul_inv, inv_pow, inv_inv]

Result:
no goals
-- Mathlib/Algebra/Algebra/Operations.lean
lemma mem_smul_iff_inv_mul_mem {S} [Field S] [Algebra R S] {x : S} {p : Submodule R S} {y : S}
    (hx : x ≠ 0) : y ∈ x • p ↔ x⁻¹ * y ∈ p

Proof state:
case mp
R : Type u
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : Field S
inst✝ : Algebra R S
x : S
p : Submodule R S
y : S
hx : x ≠ 0
⊢ y ∈ x • p → x⁻¹ * y ∈ p

Tactic:
rintro ⟨a, ha : a ∈ p, rfl⟩

Result:
case mp.intro.intro
R : Type u
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : Field S
inst✝ : Algebra R S
x : S
p : Submodule R S
hx : x ≠ 0
a : S
ha : a ∈ p
⊢ x⁻¹ * (DistribMulAction.toLinearMap R S x) a ∈ p

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : Field S
inst✝ : Algebra R S
x : S
p : Submodule R S
y : S
hx : x ≠ 0
h : x⁻¹ * y ∈ p
⊢ (DistribMulAction.toLinearMap R S x) (x⁻¹ * y) = y

Tactic:
simp [mul_inv_cancel_left₀ hx]

Result:
no goals

Proof state:
case mpr
R : Type u
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : Field S
inst✝ : Algebra R S
x : S
p : Submodule R S
y : S
hx : x ≠ 0
⊢ x⁻¹ * y ∈ p → y ∈ x • p

Tactic:
exact fun h ↦ ⟨_, h, by simp [mul_inv_cancel_left₀ hx]⟩

Result:
no goals

Proof state:
case mp.intro.intro
R : Type u
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : Field S
inst✝ : Algebra R S
x : S
p : Submodule R S
hx : x ≠ 0
a : S
ha : a ∈ p
⊢ x⁻¹ * (DistribMulAction.toLinearMap R S x) a ∈ p

Tactic:
simpa [inv_mul_cancel_left₀ hx]

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : Field S
inst✝ : Algebra R S
x : S
p : Submodule R S
y : S
hx : x ≠ 0
⊢ y ∈ x • p ↔ x⁻¹ * y ∈ p

Tactic:
constructor

Result:
case mp
R : Type u
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : Field S
inst✝ : Algebra R S
x : S
p : Submodule R S
y : S
hx : x ≠ 0
⊢ y ∈ x • p → x⁻¹ * y ∈ p

case mpr
R : Type u
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : Field S
inst✝ : Algebra R S
x : S
p : Submodule R S
y : S
hx : x ≠ 0
⊢ x⁻¹ * y ∈ p → y ∈ x • p
-- Mathlib/NumberTheory/Divisors.lean
theorem primeFactors_eq_to_filter_divisors_prime (n : ℕ) :
    n.primeFactors = {p ∈ divisors n | p.Prime}

Proof state:
case inr
n : ℕ
hn : n > 0
⊢ n.primeFactors = filter (fun p => Prime p) n.divisors

Tactic:
ext q

Result:
case inr.h
n : ℕ
hn : n > 0
q : ℕ
⊢ q ∈ n.primeFactors ↔ q ∈ filter (fun p => Prime p) n.divisors

Proof state:
case inr.h
n : ℕ
hn : n > 0
q : ℕ
⊢ q ∈ n.primeFactors ↔ q ∈ filter (fun p => Prime p) n.divisors

Tactic:
simpa [hn, hn.ne', mem_primeFactorsList] using and_comm

Result:
no goals

Proof state:
case inl

⊢ primeFactors 0 = filter (fun p => Prime p) (divisors 0)

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
⊢ n.primeFactors = filter (fun p => Prime p) n.divisors

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn)

Result:
case inl

⊢ primeFactors 0 = filter (fun p => Prime p) (divisors 0)

case inr
n : ℕ
hn : n > 0
⊢ n.primeFactors = filter (fun p => Prime p) n.divisors
-- Mathlib/Logic/Equiv/Basic.lean
theorem prodCongr_refl_left (e : β₁ ≃ β₂) :
    prodCongr (Equiv.refl α₁) e = prodCongrRight fun _ => e

Proof state:
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : β₁ ≃ β₂
⊢ (Equiv.refl α₁).prodCongr e = prodCongrRight fun x => e

Tactic:
ext ⟨a, b⟩ : 1

Result:
case H.mk
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : β₁ ≃ β₂
a : α₁
b : β₁
⊢ ((Equiv.refl α₁).prodCongr e) (a, b) = (prodCongrRight fun x => e) (a, b)

Proof state:
case H.mk
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : β₁ ≃ β₂
a : α₁
b : β₁
⊢ ((Equiv.refl α₁).prodCongr e) (a, b) = (prodCongrRight fun x => e) (a, b)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem take_reverse {α} {xs : List α} {n : Nat} :
    xs.reverse.take n = (xs.drop (xs.length - n)).reverse

Proof state:
α : Type u_1
xs_hd : α
xs_tl : List α
xs_ih : ∀ {n : Nat}, n ≤ xs_tl.length → take n xs_tl.reverse = (drop (xs_tl.length - n) xs_tl).reverse
h : (xs_hd :: xs_tl).length ≤ (xs_hd :: xs_tl).length
this : xs_tl.length + 1 = (xs_tl.reverse ++ [xs_hd]).length
⊢ take (xs_tl.length + 1) (xs_tl.reverse ++ [xs_hd]) = (xs_hd :: xs_tl).reverse

Tactic:
rw [this, take_length, reverse_cons]

Result:
no goals

Proof state:
case inr
α : Type u_1
xs_hd : α
xs_tl : List α
xs_ih : ∀ {n : Nat}, n ≤ xs_tl.length → take n xs_tl.reverse = (drop (xs_tl.length - n) xs_tl).reverse
n : Nat
h : n ≤ (xs_hd :: xs_tl).length
h' : n = (xs_hd :: xs_tl).length
⊢ take n (xs_tl.reverse ++ [xs_hd]) = (drop (xs_tl.length + 1 - n) (xs_hd :: xs_tl)).reverse

Tactic:
subst h'

Result:
case inr
α : Type u_1
xs_hd : α
xs_tl : List α
xs_ih : ∀ {n : Nat}, n ≤ xs_tl.length → take n xs_tl.reverse = (drop (xs_tl.length - n) xs_tl).reverse
h : (xs_hd :: xs_tl).length ≤ (xs_hd :: xs_tl).length
⊢ take (xs_hd :: xs_tl).length (xs_tl.reverse ++ [xs_hd]) =
    (drop (xs_tl.length + 1 - (xs_hd :: xs_tl).length) (xs_hd :: xs_tl)).reverse

Proof state:
case inr
α : Type u_1
xs_hd : α
xs_tl : List α
xs_ih : ∀ {n : Nat}, n ≤ xs_tl.length → take n xs_tl.reverse = (drop (xs_tl.length - n) xs_tl).reverse
h : (xs_hd :: xs_tl).length ≤ (xs_hd :: xs_tl).length
⊢ xs_tl.length + 1 = xs_tl.length + [xs_hd].length

Tactic:
rfl

Result:
no goals