harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Bornology/Basic.lean
theorem isBounded_empty : IsBounded (∅ : Set α)

Proof state:
α : Type u_2
x✝ : Bornology α
⊢ univ ∈ cobounded α

Tactic:
exact univ_mem

Result:
no goals

Proof state:
α : Type u_2
x✝ : Bornology α
⊢ IsBounded ∅

Tactic:
rw [isBounded_def, compl_empty]

Result:
α : Type u_2
x✝ : Bornology α
⊢ univ ∈ cobounded α
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast?_insertEntry [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
    {v : β k} : getValueCast? a (insertEntry k v l) =
      if h : k == a then some (cast (congrArg β (eq_of_beq h)) v) else getValueCast? a l

Proof state:
case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
v : β k
hl : containsKey k l = true
⊢ (if h : true = true ∧ (k == a) = true then some (cast ⋯ v) else getValueCast? a l) =
    if h : (k == a) = true then some (cast ⋯ v) else getValueCast? a l

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
v : β k
hl : containsKey k l = false
⊢ getValueCast? a (insertEntry k v l) = if h : (k == a) = true then some (cast ⋯ v) else getValueCast? a l

Tactic:
rw [insertEntry_of_containsKey_eq_false hl, getValueCast?_cons]

Result:
no goals

Proof state:
case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
v : β k
hl : containsKey k l = true
⊢ getValueCast? a (insertEntry k v l) = if h : (k == a) = true then some (cast ⋯ v) else getValueCast? a l

Tactic:
rw [insertEntry_of_containsKey hl, getValueCast?_replaceEntry, hl]

Result:
case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
v : β k
hl : containsKey k l = true
⊢ (if h : true = true ∧ (k == a) = true then some (cast ⋯ v) else getValueCast? a l) =
    if h : (k == a) = true then some (cast ⋯ v) else getValueCast? a l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
v : β k
⊢ getValueCast? a (insertEntry k v l) = if h : (k == a) = true then some (cast ⋯ v) else getValueCast? a l

Tactic:
cases hl : containsKey k l

Result:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
v : β k
hl : containsKey k l = false
⊢ getValueCast? a (insertEntry k v l) = if h : (k == a) = true then some (cast ⋯ v) else getValueCast? a l

case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
v : β k
hl : containsKey k l = true
⊢ getValueCast? a (insertEntry k v l) = if h : (k == a) = true then some (cast ⋯ v) else getValueCast? a l
-- Mathlib/Analysis/Convex/Caratheodory.lean
theorem minCardFinsetOfMemConvexHull_nonempty : (minCardFinsetOfMemConvexHull hx).Nonempty

Proof state:
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ (convexHull 𝕜) s
⊢ (minCardFinsetOfMemConvexHull hx).Nonempty

Tactic:
rw [← Finset.coe_nonempty, ← @convexHull_nonempty_iff 𝕜]

Result:
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ (convexHull 𝕜) s
⊢ ((convexHull 𝕜) ↑(minCardFinsetOfMemConvexHull hx)).Nonempty

Proof state:
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ (convexHull 𝕜) s
⊢ ((convexHull 𝕜) ↑(minCardFinsetOfMemConvexHull hx)).Nonempty

Tactic:
exact ⟨x, mem_minCardFinsetOfMemConvexHull hx⟩

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean
theorem isRoot_of_hasEigenvalue {f : End K V} {μ : K} (h : f.HasEigenvalue μ) :
    (minpoly K f).IsRoot μ

Proof state:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
μ : K
h : f.HasEigenvalue μ
⊢ (minpoly K f).IsRoot μ

Tactic:
rcases (Submodule.ne_bot_iff _).1 h with ⟨w, ⟨H, ne0⟩⟩

Result:
case intro.intro
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
μ : K
h : f.HasEigenvalue μ
w : V
H : w ∈ (f.genEigenspace μ) 1
ne0 : w ≠ 0
⊢ (minpoly K f).IsRoot μ

Proof state:
case intro.intro
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
μ : K
h : f.HasEigenvalue μ
w : V
H : w ∈ (f.genEigenspace μ) 1
ne0 : w ≠ 0
⊢ eval μ (minpoly K f) • w = 0

Tactic:
simp [← aeval_apply_of_hasEigenvector ⟨H, ne0⟩, minpoly.aeval K f]

Result:
no goals

Proof state:
case intro.intro
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
μ : K
h : f.HasEigenvalue μ
w : V
H : w ∈ (f.genEigenspace μ) 1
ne0 : w ≠ 0
⊢ (minpoly K f).IsRoot μ

Tactic:
refine Or.resolve_right (smul_eq_zero.1 ?_) ne0

Result:
case intro.intro
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
μ : K
h : f.HasEigenvalue μ
w : V
H : w ∈ (f.genEigenspace μ) 1
ne0 : w ≠ 0
⊢ eval μ (minpoly K f) • w = 0
-- Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean
theorem exists_iterate_derivative_eq_factorial_smul (p : R[X]) (k : ℕ) :
    ∃ gp : R[X], gp.natDegree ≤ p.natDegree - k ∧ derivative^[k] p = k ! • gp

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ fold max 0 (natDegree ∘ fun i => C ((i + k).choose k • p.coeff (i + k)) * X ^ i) ((⇑derivative)^[k] p).support ≤
    p.natDegree - k

Tactic:
rw [fold_max_le]

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ 0 ≤ p.natDegree - k ∧
    ∀ x ∈ ((⇑derivative)^[k] p).support,
      (natDegree ∘ fun i => C ((i + k).choose k • p.coeff (i + k)) * X ^ i) x ≤ p.natDegree - k

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ ∃ gp, gp.natDegree ≤ p.natDegree - k ∧ (⇑derivative)^[k] p = k ! • gp

Tactic:
refine ⟨_, (natDegree_sum_le _ _).trans ?_, iterate_derivative_eq_factorial_smul_sum p k⟩

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ fold max 0 (natDegree ∘ fun i => C ((i + k).choose k • p.coeff (i + k)) * X ^ i) ((⇑derivative)^[k] p).support ≤
    p.natDegree - k

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
k i : ℕ
hi : i ∈ ((⇑derivative)^[k] p).support
⊢ (C ((i + k).choose k • p.coeff (i + k)) * X ^ i).natDegree ≤ p.natDegree - k

Tactic:
exact (natDegree_C_mul_le _ _).trans <| (natDegree_X_pow_le _).trans <|
  (le_natDegree_of_mem_supp _ hi).trans <| natDegree_iterate_derivative _ _

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ 0 ≤ p.natDegree - k ∧
    ∀ x ∈ ((⇑derivative)^[k] p).support,
      (natDegree ∘ fun i => C ((i + k).choose k • p.coeff (i + k)) * X ^ i) x ≤ p.natDegree - k

Tactic:
refine ⟨Nat.zero_le _, fun i hi => ?_⟩

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
k i : ℕ
hi : i ∈ ((⇑derivative)^[k] p).support
⊢ (natDegree ∘ fun i => C ((i + k).choose k • p.coeff (i + k)) * X ^ i) i ≤ p.natDegree - k

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
k i : ℕ
hi : i ∈ ((⇑derivative)^[k] p).support
⊢ (natDegree ∘ fun i => C ((i + k).choose k • p.coeff (i + k)) * X ^ i) i ≤ p.natDegree - k

Tactic:
dsimp only [Function.comp]

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
k i : ℕ
hi : i ∈ ((⇑derivative)^[k] p).support
⊢ (C ((i + k).choose k • p.coeff (i + k)) * X ^ i).natDegree ≤ p.natDegree - k
-- Mathlib/RingTheory/Ideal/Colon.lean
@[simp]
lemma annihilator_map_mkQ_eq_colon : annihilator (P.map N.mkQ) = N.colon P

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N P : Submodule R M
⊢ (map N.mkQ P).annihilator = N.colon P

Tactic:
ext

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N P : Submodule R M
x✝ : R
⊢ x✝ ∈ (map N.mkQ P).annihilator ↔ x✝ ∈ N.colon P

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N P : Submodule R M
x✝ : R
⊢ x✝ ∈ (map N.mkQ P).annihilator ↔ x✝ ∈ N.colon P

Tactic:
rw [mem_annihilator, mem_colon]

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N P : Submodule R M
x✝ : R
⊢ (∀ n ∈ map N.mkQ P, x✝ • n = 0) ↔ ∀ p ∈ P, x✝ • p ∈ N

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N P : Submodule R M
x✝ : R
⊢ (∀ n ∈ map N.mkQ P, x✝ • n = 0) ↔ ∀ p ∈ P, x✝ • p ∈ N

Tactic:
exact ⟨fun H p hp ↦ (Quotient.mk_eq_zero N).1 (H (Quotient.mk p) (mem_map_of_mem hp)),
  fun H _ ⟨p, hp, hpm⟩ ↦ hpm ▸ ((Quotient.mk_eq_zero N).2 <| H p hp)⟩

Result:
no goals
-- Mathlib/Probability/Process/Stopping.lean
theorem progMeasurable_min_stopping_time [MetrizableSpace ι] (hτ : IsStoppingTime f τ) :
    ProgMeasurable f fun i ω => min i (τ ω)

Proof state:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
τ : Ω → ι
f : Filtration ι m
inst✝ : MetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x => Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x => ↑(↑x).1
j : ι
ω : ↑s
⊢ ω ∈ (fun x => τ (↑x).2) ⁻¹' Set.Iic j ↔ ω ∈ (fun x => (↑x).2) ⁻¹' {ω | τ ω ≤ i ⊓ j}

Tactic:
simp only [Set.mem_preimage, Set.mem_Iic, iff_and_self, le_min_iff, Set.mem_setOf_eq]

Result:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
τ : Ω → ι
f : Filtration ι m
inst✝ : MetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x => Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x => ↑(↑x).1
j : ι
ω : ↑s
⊢ τ (↑ω).2 ≤ j → τ (↑ω).2 ≤ i
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem prime_card [Finite α] : (Nat.card α).Prime

Proof state:
case intro.refine_1
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Nat.card α
h : Subgroup.zpowers (g ^ n) = ⊤
hgo : orderOf (g ^ n) = Nat.card α / n
⊢ ∀ (x : α), x ∈ Subgroup.zpowers (g ^ n)

Tactic:
intro x

Result:
case intro.refine_1
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Nat.card α
h : Subgroup.zpowers (g ^ n) = ⊤
hgo : orderOf (g ^ n) = Nat.card α / n
x : α
⊢ x ∈ Subgroup.zpowers (g ^ n)

Proof state:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
⊢ Nat.Prime (Nat.card α)

Tactic:
obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := α)

Result:
case intro
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
⊢ Nat.Prime (Nat.card α)

Proof state:
case intro.refine_1
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Nat.card α
h : Subgroup.zpowers (g ^ n) = ⊤
hgo : Nat.card α = Nat.card α * n
⊢ n = 1

Tactic:
exact (mul_left_cancel₀ (ne_of_gt h0) ((mul_one (Nat.card α)).trans hgo)).symm

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
⊢ Nat.Prime (Nat.card α)

Tactic:
have h0 : 0 < Nat.card α := Nat.card_pos

Result:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Finite α
h0 : 0 < Nat.card α
⊢ Nat.Prime (Nat.card α)
-- Mathlib/Data/Finset/PImage.lean
theorem pimage_inter [DecidableEq α] : (s ∩ t).pimage f ⊆ s.pimage f ∩ t.pimage f

Proof state:
α : Type u_1
β : Type u_2
inst✝² : DecidableEq β
f : α →. β
inst✝¹ : (x : α) → Decidable (f x).Dom
s t : Finset α
inst✝ : DecidableEq α
⊢ pimage f (s ∩ t) ⊆ pimage f s ∩ pimage f t

Tactic:
simp only [← coe_subset, coe_pimage, coe_inter, PFun.image_inter]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Shift.lean
/-- Translation in the domain does not change the derivative. -/
lemma HasDerivAt.comp_add_const (x a : 𝕜) (hf : HasDerivAt f f' (x + a)) :
    HasDerivAt (fun x ↦ f (x + a)) f' x

Proof state:
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x a : 𝕜
hf : HasDerivAt f f' (x + a)
⊢ HasDerivAt (fun x => f (x + a)) f' x

Tactic:
simpa [Function.comp_def] using HasDerivAt.scomp (𝕜 := 𝕜) x hf <| hasDerivAt_id' x |>.add_const a

Result:
no goals
-- Mathlib/GroupTheory/Sylow.lean
theorem finite_of_ker_is_pGroup {H : Type*} [Group H] {f : H →* G}
    (hf : IsPGroup p f.ker) [Finite (Sylow p G)] : Finite (Sylow p H) :=
  let h_exists := fun P : Sylow p H => P.exists_comap_eq_of_ker_isPGroup hf
  let g : Sylow p H → Sylow p G := fun P => Classical.choose (h_exists P)
  have hg : ∀ P : Sylow p H, (g P).1.comap f = P := fun P => Classical.choose_spec (h_exists P)
  Finite.of_injective g fun P Q h => ext (by rw [← hg, h]; exact (h_exists Q).choose_spec)

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
f : H →* G
hf : IsPGroup p ↥f.ker
inst✝ : Finite (Sylow p G)
h_exists : ∀ (P : Sylow p H), ∃ Q, comap f ↑Q = ↑P := fun P => exists_comap_eq_of_ker_isPGroup P hf
g : Sylow p H → Sylow p G := fun P => Classical.choose ⋯
hg : ∀ (P : Sylow p H), comap f ↑(g P) = ↑P
P Q : Sylow p H
h : g P = g Q
⊢ comap f ↑(g Q) = ↑Q

Tactic:
exact (h_exists Q).choose_spec

Result:
no goals

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
f : H →* G
hf : IsPGroup p ↥f.ker
inst✝ : Finite (Sylow p G)
h_exists : ∀ (P : Sylow p H), ∃ Q, comap f ↑Q = ↑P := fun P => exists_comap_eq_of_ker_isPGroup P hf
g : Sylow p H → Sylow p G := fun P => Classical.choose ⋯
hg : ∀ (P : Sylow p H), comap f ↑(g P) = ↑P
P Q : Sylow p H
h : g P = g Q
⊢ ↑P = ↑Q

Tactic:
rw [← hg, h]

Result:
p : ℕ
G : Type u_1
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
f : H →* G
hf : IsPGroup p ↥f.ker
inst✝ : Finite (Sylow p G)
h_exists : ∀ (P : Sylow p H), ∃ Q, comap f ↑Q = ↑P := fun P => exists_comap_eq_of_ker_isPGroup P hf
g : Sylow p H → Sylow p G := fun P => Classical.choose ⋯
hg : ∀ (P : Sylow p H), comap f ↑(g P) = ↑P
P Q : Sylow p H
h : g P = g Q
⊢ comap f ↑(g Q) = ↑Q
-- Mathlib/Topology/MetricSpace/Isometry.lean
theorem ediam_univ (h : α ≃ᵢ β) : EMetric.diam (univ : Set α) = EMetric.diam (univ : Set β)

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
⊢ EMetric.diam univ = EMetric.diam univ

Tactic:
rw [← h.range_eq_univ, h.isometry.ediam_range]

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Factorization.lean
theorem count_coe {J : Ideal R} (hJ : J ≠ 0) :
    count K v J = (Associates.mk v.asIdeal).count (Associates.mk J).factors

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
J : Ideal R
hJ : J ≠ 0
⊢ count K v ↑J = ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors)

Tactic:
rw [count_well_defined K (J := J) (a := 1), Ideal.span_singleton_one, sub_eq_self,
  Nat.cast_eq_zero, ← Ideal.one_eq_top, Associates.mk_one, Associates.factors_one,
  Associates.count_zero v.associates_irreducible]

Result:
case hI
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
J : Ideal R
hJ : J ≠ 0
⊢ ↑J ≠ 0

case h_aJ
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
J : Ideal R
hJ : J ≠ 0
⊢ ↑J = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑J

Proof state:
case hI
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
J : Ideal R
hJ : J ≠ 0
⊢ ↑J ≠ 0

Tactic:
simpa only [ne_eq, coeIdeal_eq_zero]

Result:
no goals

Proof state:
case h_aJ
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
J : Ideal R
hJ : J ≠ 0
⊢ ↑J = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑J

Tactic:
simp only [_root_.map_one, inv_one, spanSingleton_one, one_mul]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Hom.lean
theorem map_id : map (MonoidHom.id M) = MonoidHom.id Mˣ

Proof state:
M : Type u
inst✝ : Monoid M
⊢ map (MonoidHom.id M) = MonoidHom.id Mˣ

Tactic:
ext

Result:
case h.a
M : Type u
inst✝ : Monoid M
x✝ : Mˣ
⊢ ↑((map (MonoidHom.id M)) x✝) = ↑((MonoidHom.id Mˣ) x✝)

Proof state:
case h.a
M : Type u
inst✝ : Monoid M
x✝ : Mˣ
⊢ ↑((map (MonoidHom.id M)) x✝) = ↑((MonoidHom.id Mˣ) x✝)

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/WellFoundedSet.lean
theorem partiallyWellOrderedOn_iff_finite_antichains [IsSymm α r] :
    s.PartiallyWellOrderedOn r ↔ ∀ t, t ⊆ s → IsAntichain r t → t.Finite

Proof state:
case refine_2.intro.refl.intro.refl.inr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : IsRefl α r
inst✝ : IsSymm α r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m ≠ f n
h : n < m
⊢ rᶜ (f m) (f n)

Tactic:
exact mt symm (H _ _ h)

Result:
no goals

Proof state:
case refine_1.inr.inr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : IsRefl α r
inst✝ : IsSymm α r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : n < m
⊢ r (f n) (f n)

Tactic:
exact refl _

Result:
no goals

Proof state:
case refine_1.inr.inl
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : IsRefl α r
inst✝ : IsSymm α r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : m = n
⊢ m = n

Tactic:
exact h

Result:
no goals
-- Mathlib/Geometry/Euclidean/Triangle.lean
theorem dist_sq_add_dist_sq_eq_two_mul_dist_midpoint_sq_add_half_dist_sq (a b c : P) :
    dist a b ^ 2 + dist a c ^ 2 = 2 * (dist a (midpoint ℝ b c) ^ 2 + (dist b c / 2) ^ 2)

Proof state:
case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
hbc : ¬b = c
m : P := midpoint ℝ b c
⊢ dist a b ^ 2 + dist a c ^ 2 = 2 * (dist a (midpoint ℝ b c) ^ 2 + (dist b c / 2) ^ 2)

Tactic:
have : dist b c ≠ 0 := (dist_pos.mpr hbc).ne'

Result:
case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
hbc : ¬b = c
m : P := midpoint ℝ b c
this : dist b c ≠ 0
⊢ dist a b ^ 2 + dist a c ^ 2 = 2 * (dist a (midpoint ℝ b c) ^ 2 + (dist b c / 2) ^ 2)

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
hbc : ¬b = c
m : P := midpoint ℝ b c
this : dist b c ≠ 0
hm :
  dist a b ^ 2 * (2⁻¹ * dist b c) + dist a c ^ 2 * (2⁻¹ * dist b c) =
    dist b c * (dist a (midpoint ℝ b c) ^ 2 + 2⁻¹ * dist b c * (2⁻¹ * dist b c))
⊢ (dist a b ^ 2 + dist a c ^ 2) * (dist b c * 2) = 2 * (dist a b ^ 2 * dist b c * 2 / 2 + dist a c ^ 2 * dist b c)

Tactic:
ring

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
⊢ dist a b ^ 2 + dist a c ^ 2 = 2 * (dist a (midpoint ℝ b c) ^ 2 + (dist b c / 2) ^ 2)

Tactic:
by_cases hbc : b = c

Result:
case pos
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
hbc : b = c
⊢ dist a b ^ 2 + dist a c ^ 2 = 2 * (dist a (midpoint ℝ b c) ^ 2 + (dist b c / 2) ^ 2)

case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
hbc : ¬b = c
⊢ dist a b ^ 2 + dist a c ^ 2 = 2 * (dist a (midpoint ℝ b c) ^ 2 + (dist b c / 2) ^ 2)

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
hbc : ¬b = c
m : P := midpoint ℝ b c
this : dist b c ≠ 0
hm :
  dist a b ^ 2 * (2⁻¹ * dist b c) + dist a c ^ 2 * (2⁻¹ * dist b c) =
    dist b c * (dist a (midpoint ℝ b c) ^ 2 + 2⁻¹ * dist b c * (2⁻¹ * dist b c))
⊢ 2 * (dist b c * (dist a (midpoint ℝ b c) ^ 2 * (2 * 2) + dist b c * dist b c)) * 2 ^ 2 =
    2 * (dist a (midpoint ℝ b c) ^ 2 * 2 ^ 2 + dist b c ^ 2) * (dist b c * (2 * 2))

Tactic:
ring

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- One direction of `le_inv_mul_iff₀` where `c` is allowed to be `0` (but `b` must be nonnegative).
-/
lemma mul_le_of_le_inv_mul₀ (hb : 0 ≤ b) (hc : 0 ≤ c) (h : a ≤ c⁻¹ * b) : c * a ≤ b

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : PosMulMono G₀
hb : 0 ≤ b
hc : 0 ≤ c
h : a ≤ c⁻¹ * b
⊢ c * a ≤ b

Tactic:
obtain rfl | hc := hc.eq_or_lt

Result:
case inl
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b : G₀
inst✝ : PosMulMono G₀
hb : 0 ≤ b
hc : 0 ≤ 0
h : a ≤ 0⁻¹ * b
⊢ 0 * a ≤ b

case inr
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : PosMulMono G₀
hb : 0 ≤ b
hc✝ : 0 ≤ c
h : a ≤ c⁻¹ * b
hc : 0 < c
⊢ c * a ≤ b

Proof state:
case inr
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : PosMulMono G₀
hb : 0 ≤ b
hc✝ : 0 ≤ c
h : a ≤ c⁻¹ * b
hc : 0 < c
⊢ c * a ≤ b

Tactic:
rwa [le_inv_mul_iff₀ hc] at h

Result:
no goals

Proof state:
case inl
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b : G₀
inst✝ : PosMulMono G₀
hb : 0 ≤ b
hc : 0 ≤ 0
h : a ≤ 0⁻¹ * b
⊢ 0 * a ≤ b

Tactic:
simpa using hb

Result:
no goals