harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
lemma rnDeriv_pos' [HaveLebesgueDecomposition ν μ] [SigmaFinite μ] (hμν : μ ≪ ν) :
    ∀ᵐ x ∂μ, 0 < ν.rnDeriv μ x

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : ν.HaveLebesgueDecomposition μ
inst✝ : SigmaFinite μ
hμν : μ ≪ ν
⊢ {x | (fun x => 0 < ν.rnDeriv μ x) x} ∈ ae (μ.withDensity (ν.rnDeriv μ))

Tactic:
filter_upwards [Measure.rnDeriv_pos (withDensity_absolutelyContinuous μ (ν.rnDeriv μ)),
  (withDensity_absolutelyContinuous μ (ν.rnDeriv μ)).ae_le
  (Measure.rnDeriv_withDensity μ (Measure.measurable_rnDeriv ν μ))] with x hx hx2

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : ν.HaveLebesgueDecomposition μ
inst✝ : SigmaFinite μ
hμν : μ ≪ ν
x : α
hx : 0 < (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ x
hx2 : (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ x = ν.rnDeriv μ x
⊢ 0 < ν.rnDeriv μ x

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : ν.HaveLebesgueDecomposition μ
inst✝ : SigmaFinite μ
hμν : μ ≪ ν
x : α
hx : 0 < (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ x
hx2 : (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ x = ν.rnDeriv μ x
⊢ 0 < ν.rnDeriv μ x

Tactic:
rwa [← hx2]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : ν.HaveLebesgueDecomposition μ
inst✝ : SigmaFinite μ
hμν : μ ≪ ν
⊢ ∀ᵐ (x : α) ∂μ, 0 < ν.rnDeriv μ x

Tactic:
refine (absolutelyContinuous_withDensity_rnDeriv hμν).ae_le ?_

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : ν.HaveLebesgueDecomposition μ
inst✝ : SigmaFinite μ
hμν : μ ≪ ν
⊢ {x | (fun x => 0 < ν.rnDeriv μ x) x} ∈ ae (μ.withDensity (ν.rnDeriv μ))
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_alter_eq_sub_one [LawfulBEq α] {k : α} {f : Option β → Option β}
    (h : m.WF) (h₁ : k ∈ m) (h₂ : (f (Const.get? m k)).isNone) :
    (Const.alter m k f).size = m.size - 1

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝ : LawfulBEq α
k : α
f : Option β → Option β
h : m.WF
h₁ : k ∈ m
h₂ : (f (get? m k)).isNone = true
⊢ (alter m k f).size = m.size - 1

Tactic:
revert h₁ h₂

Result:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝ : LawfulBEq α
k : α
f : Option β → Option β
h : m.WF
⊢ k ∈ m → (f (get? m k)).isNone = true → (alter m k f).size = m.size - 1

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝ : LawfulBEq α
k : α
f : Option β → Option β
h : m.WF
⊢ k ∈ m → (f (get? m k)).isNone = true → (alter m k f).size = m.size - 1

Tactic:
simp only [mem_iff_contains]

Result:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝ : LawfulBEq α
k : α
f : Option β → Option β
h : m.WF
⊢ m.contains k = true → (f (get? m k)).isNone = true → (alter m k f).size = m.size - 1

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝ : LawfulBEq α
k : α
f : Option β → Option β
h : m.WF
⊢ m.contains k = true → (f (get? m k)).isNone = true → (alter m k f).size = m.size - 1

Tactic:
simp_to_raw using Raw₀.Const.size_alter_eq_sub_one

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem range_comp_incl_top : (f.comp (incl (⊤ : AddSubgroup V₁))).range = f.range

Proof state:
V₁ : Type u_3
V₂ : Type u_4
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
⊢ (f.comp (incl ⊤)).range = f.range

Tactic:
simp [comp_range, incl_range, ← AddMonoidHom.range_eq_map]

Result:
V₁ : Type u_3
V₂ : Type u_4
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
⊢ f.toAddMonoidHom.range = f.range

Proof state:
V₁ : Type u_3
V₂ : Type u_4
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
⊢ f.toAddMonoidHom.range = f.range

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem testBit_implies_ge {x : Nat} (p : testBit x i = true) : x ≥ 2^i

Proof state:
i x : Nat
p : x.testBit i = true
⊢ x ≥ 2 ^ i

Tactic:
simp only [testBit_to_div_mod] at p

Result:
i x : Nat
p : decide (x / 2 ^ i % 2 = 1) = true
⊢ x ≥ 2 ^ i

Proof state:
i x : Nat
p : decide (x / 2 ^ i % 2 = 1) = true
⊢ x ≥ 2 ^ i

Tactic:
apply Decidable.by_contra

Result:
case a
i x : Nat
p : decide (x / 2 ^ i % 2 = 1) = true
⊢ ¬x ≥ 2 ^ i → False

Proof state:
case a
i x : Nat
p : decide (x / 2 ^ i % 2 = 1) = true
not_ge : ¬x ≥ 2 ^ i
x_lt : x < 2 ^ i
⊢ False

Tactic:
simp [div_eq_of_lt x_lt] at p

Result:
no goals

Proof state:
case a
i x : Nat
p : decide (x / 2 ^ i % 2 = 1) = true
not_ge : ¬x ≥ 2 ^ i
⊢ False

Tactic:
have x_lt : x < 2^i := Nat.lt_of_not_le not_ge

Result:
case a
i x : Nat
p : decide (x / 2 ^ i % 2 = 1) = true
not_ge : ¬x ≥ 2 ^ i
x_lt : x < 2 ^ i
⊢ False

Proof state:
case a
i x : Nat
p : decide (x / 2 ^ i % 2 = 1) = true
⊢ ¬x ≥ 2 ^ i → False

Tactic:
intro not_ge

Result:
case a
i x : Nat
p : decide (x / 2 ^ i % 2 = 1) = true
not_ge : ¬x ≥ 2 ^ i
⊢ False
-- Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean
theorem exists_neg_pow_of_isOfFinOrder [IsCyclotomicExtension {n} ℚ K]
    (hno : Odd (n : ℕ)) {ζ x : K} (hζ : IsPrimitiveRoot ζ n) (hx : IsOfFinOrder x) :
    ∃ r : ℕ, x = (-ζ) ^ r :=  by
  have hnegζ : IsPrimitiveRoot (-ζ) (2 * n)

Proof state:
case h.e'_4
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
⊢ 2 * ↑n = orderOf (-ζ)

Tactic:
rw [neg_eq_neg_one_mul, (Commute.all _ _).orderOf_mul_eq_mul_orderOf_of_coprime]

Result:
case h.e'_4
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
⊢ 2 * ↑n = orderOf (-1) * orderOf ζ

case h.e'_4
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
⊢ (orderOf (-1)).Coprime (orderOf ζ)

Proof state:
case intro.intro.intro.intro.intro.intro.intro
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * ↑n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlzero : NeZero l
this : NeZero ↑l
a : ℕ
ha : 2 * ↑n = l * a
hlroot : x ^ (2 * ↑n) = 1
s : ℕ
hs : (-ζ) ^ s = x
⊢ ∃ r, x = (-ζ) ^ r

Tactic:
exact ⟨s, hs.symm⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * ↑n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlroot : (cyclotomic l K).IsRoot x
⊢ ∃ r, x = (-ζ) ^ r

Tactic:
have hlzero : NeZero l := ⟨fun h ↦ by simp [h] at hl⟩

Result:
case intro.intro.intro.intro
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * ↑n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlroot : (cyclotomic l K).IsRoot x
hlzero : NeZero l
⊢ ∃ r, x = (-ζ) ^ r
-- Mathlib/MeasureTheory/Measure/Dirac.lean
theorem dirac_apply [MeasurableSingletonClass α] (a : α) (s : Set α) :
    dirac a s = s.indicator 1 a

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
⊢ (dirac a) {a}ᶜ = 0

Tactic:
simp [dirac_apply' _ (measurableSet_singleton _).compl]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∈ s
⊢ (dirac a) s = s.indicator 1 a

Tactic:
rw [dirac_apply_of_mem h, indicator_of_mem h, Pi.one_apply]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
⊢ (dirac a) s = s.indicator 1 a

Tactic:
rw [indicator_of_not_mem h, ← nonpos_iff_eq_zero]

Result:
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
⊢ (dirac a) s ≤ 0

Proof state:
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
⊢ (dirac a) s ≤ 0

Tactic:
calc
  dirac a s ≤ dirac a {a}ᶜ := measure_mono (subset_compl_comm.1 <| singleton_subset_iff.2 h)
  _ = 0 := by simp [dirac_apply' _ (measurableSet_singleton _).compl]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
⊢ (dirac a) s = s.indicator 1 a

Tactic:
by_cases h : a ∈ s

Result:
case pos
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∈ s
⊢ (dirac a) s = s.indicator 1 a

case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
⊢ (dirac a) s = s.indicator 1 a
-- Mathlib/Algebra/Group/Prod.lean
theorem prod_unique (f : M →ₙ* N × P) : ((fst N P).comp f).prod ((snd N P).comp f) = f :=
  ext fun x => by simp only [prod_apply, coe_fst, coe_snd, comp_apply]

Proof state:
M : Type u_3
N : Type u_4
P : Type u_5
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
f : M →ₙ* N × P
x : M
⊢ (((fst N P).comp f).prod ((snd N P).comp f)) x = f x

Tactic:
simp only [prod_apply, coe_fst, coe_snd, comp_apply]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem image_inter (hf : LeftInvOn f' f s) :
    f '' (s₁ ∩ s) = f' ⁻¹' (s₁ ∩ s) ∩ f '' s

Proof state:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
x : α
hx : x ∈ s
h₁ : f x ∈ f' ⁻¹' s₁
⊢ f' (f x) ∈ s

Tactic:
rwa [hf hx]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f' ⁻¹' s₁ ∩ f '' s ⊆ f' ⁻¹' (s₁ ∩ s) ∩ f '' s

Tactic:
rintro _ ⟨h₁, x, hx, rfl⟩

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
x : α
hx : x ∈ s
h₁ : f x ∈ f' ⁻¹' s₁
⊢ f x ∈ f' ⁻¹' (s₁ ∩ s) ∩ f '' s

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
x : α
hx : x ∈ s
h₁ : f x ∈ f' ⁻¹' s₁
⊢ f x ∈ f' ⁻¹' (s₁ ∩ s) ∩ f '' s

Tactic:
exact ⟨⟨h₁, by rwa [hf hx]⟩, mem_image_of_mem _ hx⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f' ⁻¹' s₁ ∩ f '' s = f' ⁻¹' (s₁ ∩ s) ∩ f '' s

Tactic:
refine Subset.antisymm ?_ (inter_subset_inter_left _ (preimage_mono inter_subset_left))

Result:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f' ⁻¹' s₁ ∩ f '' s ⊆ f' ⁻¹' (s₁ ∩ s) ∩ f '' s

Proof state:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f '' (s₁ ∩ s) = f' ⁻¹' (s₁ ∩ s) ∩ f '' s

Tactic:
rw [hf.image_inter']

Result:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f' ⁻¹' s₁ ∩ f '' s = f' ⁻¹' (s₁ ∩ s) ∩ f '' s
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
theorem deleteOne_preserves_ratUnits {n : Nat} (f : DefaultFormula n) (id : Nat) :
    (deleteOne f id).ratUnits = f.ratUnits

Proof state:
n : Nat
f : DefaultFormula n
id : Nat
⊢ (match f.clauses[id]! with
      | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
      | some val =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }).ratUnits =
    f.ratUnits

Tactic:
split <;> simp only

Result:
no goals

Proof state:
n : Nat
f : DefaultFormula n
id : Nat
⊢ (f.deleteOne id).ratUnits = f.ratUnits

Tactic:
simp only [deleteOne]

Result:
n : Nat
f : DefaultFormula n
id : Nat
⊢ (match f.clauses[id]! with
      | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
      | some val =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }).ratUnits =
    f.ratUnits
-- Mathlib/Algebra/Order/Round.lean
theorem abs_sub_round_eq_min (x : α) : |x - round x| = min (fract x) (1 - fract x)

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x ≥ 1 - fract x
⊢ 0 < fract x

Tactic:
replace hx : 0 < fract x + fract x := lt_of_lt_of_le zero_lt_one (tsub_le_iff_left.mp hx)

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : 0 < fract x + fract x
⊢ 0 < fract x

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
⊢ |x - ↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉)| = if fract x < 1 - fract x then fract x else 1 - fract x

Tactic:
rcases lt_or_ge (fract x) (1 - fract x) with hx | hx

Result:
case inl
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x < 1 - fract x
⊢ |x - ↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉)| = if fract x < 1 - fract x then fract x else 1 - fract x

case inr
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x ≥ 1 - fract x
⊢ |x - ↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉)| = if fract x < 1 - fract x then fract x else 1 - fract x

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : 0 < fract x + fract x
⊢ 0 < fract x

Tactic:
simpa only [← two_mul, mul_pos_iff_of_pos_left, zero_lt_two] using hx

Result:
no goals

Proof state:
case inl
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x < 1 - fract x
⊢ |x - ↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉)| = if fract x < 1 - fract x then fract x else 1 - fract x

Tactic:
rw [if_pos hx, if_pos hx, self_sub_floor, abs_fract]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
⊢ |x - ↑(round x)| = fract x ⊓ (1 - fract x)

Tactic:
simp_rw [round, min_def_lt, two_mul, ← lt_tsub_iff_left]

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
⊢ |x - ↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉)| = if fract x < 1 - fract x then fract x else 1 - fract x

Proof state:
case inr
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x ≥ 1 - fract x
this : 0 < fract x
⊢ |x - ↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉)| = if fract x < 1 - fract x then fract x else 1 - fract x

Tactic:
rw [if_neg (not_lt.mpr hx), if_neg (not_lt.mpr hx), abs_sub_comm, ceil_sub_self_eq this.ne.symm,
  abs_one_sub_fract]

Result:
no goals

Proof state:
case inr
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x ≥ 1 - fract x
⊢ |x - ↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉)| = if fract x < 1 - fract x then fract x else 1 - fract x

Tactic:
have : 0 < fract x := by
  replace hx : 0 < fract x + fract x := lt_of_lt_of_le zero_lt_one (tsub_le_iff_left.mp hx)
  simpa only [← two_mul, mul_pos_iff_of_pos_left, zero_lt_two] using hx

Result:
case inr
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x ≥ 1 - fract x
this : 0 < fract x
⊢ |x - ↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉)| = if fract x < 1 - fract x then fract x else 1 - fract x
-- Mathlib/LinearAlgebra/AnnihilatingPolynomial.lean
theorem annIdealGenerator_eq_minpoly (a : A) : annIdealGenerator 𝕜 a = minpoly 𝕜 a

Proof state:
case pos.intro.intro
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : annIdealGenerator 𝕜 a = 0
p : 𝕜[X]
p_monic : p.Monic
hp : (aeval a) p = 0
⊢ False

Tactic:
refine p_monic.ne_zero (Ideal.mem_bot.mp ?_)

Result:
case pos.intro.intro
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : annIdealGenerator 𝕜 a = 0
p : 𝕜[X]
p_monic : p.Monic
hp : (aeval a) p = 0
⊢ p ∈ ⊥

Proof state:
case pos
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : annIdealGenerator 𝕜 a = 0
⊢ annIdealGenerator 𝕜 a = minpoly 𝕜 a

Tactic:
rw [h, minpoly.eq_zero]

Result:
case pos
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : annIdealGenerator 𝕜 a = 0
⊢ ¬IsIntegral 𝕜 a

Proof state:
case pos.intro.intro
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : annIdealGenerator 𝕜 a = 0
p : 𝕜[X]
p_monic : p.Monic
hp : (aeval a) p = 0
⊢ p ∈ ⊥

Tactic:
simpa only [annIdealGenerator_eq_zero_iff.mp h] using mem_annIdeal_iff_aeval_eq_zero.mpr hp

Result:
no goals

Proof state:
case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ annIdealGenerator 𝕜 a = minpoly 𝕜 a

Tactic:
exact minpoly.unique _ _ (monic_annIdealGenerator _ _ h) (annIdealGenerator_aeval_eq_zero _ _)
  fun q q_monic hq =>
    degree_annIdealGenerator_le_of_mem a q (mem_annIdeal_iff_aeval_eq_zero.mpr hq)
      q_monic.ne_zero

Result:
no goals

Proof state:
case pos
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : annIdealGenerator 𝕜 a = 0
⊢ ¬IsIntegral 𝕜 a

Tactic:
rintro ⟨p, p_monic, hp : aeval a p = 0⟩

Result:
case pos.intro.intro
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : annIdealGenerator 𝕜 a = 0
p : 𝕜[X]
p_monic : p.Monic
hp : (aeval a) p = 0
⊢ False

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
⊢ annIdealGenerator 𝕜 a = minpoly 𝕜 a

Tactic:
by_cases h : annIdealGenerator 𝕜 a = 0

Result:
case pos
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : annIdealGenerator 𝕜 a = 0
⊢ annIdealGenerator 𝕜 a = minpoly 𝕜 a

case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ annIdealGenerator 𝕜 a = minpoly 𝕜 a
-- Mathlib/Geometry/Manifold/AnalyticManifold.lean
theorem mem_analyticGroupoid_of_boundaryless [I.Boundaryless] (e : PartialHomeomorph H H) :
    e ∈ analyticGroupoid I ↔ AnalyticOnNhd 𝕜 (I ∘ e ∘ I.symm) (I '' e.source) ∧
      AnalyticOnNhd 𝕜 (I ∘ e.symm ∘ I.symm) (I '' e.target)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
inst✝ : I.Boundaryless
e : PartialHomeomorph H H
⊢ e ∈ analyticGroupoid I ↔
    AnalyticOnNhd 𝕜 (↑I ∘ ↑e ∘ ↑I.symm) (↑I '' e.source) ∧ AnalyticOnNhd 𝕜 (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I '' e.target)

Tactic:
simp only [mem_analyticGroupoid, I.range_eq_univ, inter_univ, I.image_eq]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
inst✝ : I.Boundaryless
e : PartialHomeomorph H H
⊢ AnalyticOn 𝕜 (↑I ∘ ↑e ∘ ↑I.symm) (↑I.symm ⁻¹' e.source) ∧
      AnalyticOn 𝕜 (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I.symm ⁻¹' e.target) ↔
    AnalyticOnNhd 𝕜 (↑I ∘ ↑e ∘ ↑I.symm) (↑I.symm ⁻¹' e.source) ∧
      AnalyticOnNhd 𝕜 (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I.symm ⁻¹' e.target)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
inst✝ : I.Boundaryless
e : PartialHomeomorph H H
⊢ IsOpen (↑I.symm ⁻¹' e.source)

Tactic:
exact I.continuous_symm.isOpen_preimage _ e.open_source

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
inst✝ : I.Boundaryless
e : PartialHomeomorph H H
⊢ IsOpen (↑I.symm ⁻¹' e.target)

Tactic:
exact I.continuous_symm.isOpen_preimage _ e.open_target

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
inst✝ : I.Boundaryless
e : PartialHomeomorph H H
⊢ AnalyticOn 𝕜 (↑I ∘ ↑e ∘ ↑I.symm) (↑I.symm ⁻¹' e.source) ∧
      AnalyticOn 𝕜 (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I.symm ⁻¹' e.target) ↔
    AnalyticOnNhd 𝕜 (↑I ∘ ↑e ∘ ↑I.symm) (↑I.symm ⁻¹' e.source) ∧
      AnalyticOnNhd 𝕜 (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I.symm ⁻¹' e.target)

Tactic:
rw [IsOpen.analyticOn_iff_analyticOnNhd, IsOpen.analyticOn_iff_analyticOnNhd]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
inst✝ : I.Boundaryless
e : PartialHomeomorph H H
⊢ IsOpen (↑I.symm ⁻¹' e.target)

𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
inst✝ : I.Boundaryless
e : PartialHomeomorph H H
⊢ IsOpen (↑I.symm ⁻¹' e.source)