harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/LSeries/SumCoeff.lean
theorem LSeriesSummable_of_sum_norm_bigO
    (hO : (fun n ↦ ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n ↦ (n : ℝ) ^ r)
    (hr : 0 ≤ r) (hs : r < s.re) :
    LSeriesSummable f s

Proof state:
f : ℕ → ℂ
r : ℝ
s : ℂ
hO : (fun n => ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n => ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
⊢ LSeriesSummable f s

Tactic:
have h₁ : (fun n ↦ if n = 0 then 0 else f n) =ᶠ[atTop] f := by
  filter_upwards [eventually_ne_atTop 0] with n hn using by simp_rw [if_neg hn]

Result:
f : ℕ → ℂ
r : ℝ
s : ℂ
hO : (fun n => ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n => ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : (fun n => if n = 0 then 0 else f n) =ᶠ[atTop] f
⊢ LSeriesSummable f s

Proof state:
f : ℕ → ℂ
r : ℝ
s : ℂ
hO : (fun n => ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n => ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
⊢ (fun n => if n = 0 then 0 else f n) =ᶠ[atTop] f

Tactic:
filter_upwards [eventually_ne_atTop 0] with n hn using by simp_rw [if_neg hn]

Result:
no goals

Proof state:
f : ℕ → ℂ
r : ℝ
s : ℂ
hO : (fun n => ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n => ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : (fun n => if n = 0 then 0 else f n) =ᶠ[atTop] f
⊢ LSeriesSummable f s

Tactic:
refine (LSeriesSummable_of_sum_norm_bigO_aux (if_pos rfl) ?_ hr hs).congr' _ h₁

Result:
f : ℕ → ℂ
r : ℝ
s : ℂ
hO : (fun n => ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n => ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : (fun n => if n = 0 then 0 else f n) =ᶠ[atTop] f
⊢ (fun n => ∑ k ∈ Icc 1 n, ‖if k = 0 then 0 else f k‖) =O[atTop] fun n => ↑n ^ r

Proof state:
f : ℕ → ℂ
r : ℝ
s : ℂ
hO : (fun n => ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n => ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : (fun n => if n = 0 then 0 else f n) =ᶠ[atTop] f
⊢ (fun n => ∑ k ∈ Icc 1 n, ‖if k = 0 then 0 else f k‖) =O[atTop] fun n => ↑n ^ r

Tactic:
refine hO.congr' (Eventually.of_forall fun _ ↦ Finset.sum_congr rfl fun _ h ↦ ?_) EventuallyEq.rfl

Result:
f : ℕ → ℂ
r : ℝ
s : ℂ
hO : (fun n => ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n => ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : (fun n => if n = 0 then 0 else f n) =ᶠ[atTop] f
x✝¹ x✝ : ℕ
h : x✝ ∈ Icc 1 x✝¹
⊢ ‖f x✝‖ = ‖if x✝ = 0 then 0 else f x✝‖

Proof state:
f : ℕ → ℂ
r : ℝ
s : ℂ
hO : (fun n => ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n => ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : (fun n => if n = 0 then 0 else f n) =ᶠ[atTop] f
x✝¹ x✝ : ℕ
h : x✝ ∈ Icc 1 x✝¹
⊢ ‖f x✝‖ = ‖if x✝ = 0 then 0 else f x✝‖

Tactic:
rw [if_neg (zero_lt_one.trans_le (mem_Icc.mp h).1).ne']

Result:
no goals

Proof state:
f : ℕ → ℂ
r : ℝ
s : ℂ
hO : (fun n => ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n => ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
n : ℕ
hn : n ≠ 0
⊢ (if n = 0 then 0 else f n) = f n

Tactic:
simp_rw [if_neg hn]

Result:
no goals
-- Mathlib/Topology/Homotopy/Product.lean
theorem comp_pi_eq_pi_comp (γ₀ : ∀ i, Path.Homotopic.Quotient (as i) (bs i))
    (γ₁ : ∀ i, Path.Homotopic.Quotient (bs i) (cs i)) : pi γ₀ ⬝ pi γ₁ = pi fun i ↦ γ₀ i ⬝ γ₁ i

Proof state:
case h.h
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
a : (i : ι) → Path (bs i) (cs i)
a✝ : (i : ι) → Path (as i) (bs i)
⊢ (pi fun i => ⟦(a✝ i).trans (a i)⟧) = pi fun i => ⟦a✝ i⟧ ⬝ ⟦a i⟧

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
γ₀ : (i : ι) → Homotopic.Quotient (as i) (bs i)
γ₁ : (i : ι) → Homotopic.Quotient (bs i) (cs i)
⊢ pi γ₀ ⬝ pi γ₁ = pi fun i => γ₀ i ⬝ γ₁ i

Tactic:
induction γ₁ using Quotient.induction_on_pi with | _ a =>
induction γ₀ using Quotient.induction_on_pi
simp only [pi_lift]
rw [← Path.Homotopic.comp_lift, Path.trans_pi_eq_pi_trans, ← pi_lift]
rfl

Result:
no goals

Proof state:
case h.h
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
a : (i : ι) → Path (bs i) (cs i)
a✝ : (i : ι) → Path (as i) (bs i)
⊢ ((pi fun i => ⟦a✝ i⟧) ⬝ pi fun i => ⟦a i⟧) = pi fun i => (fun i => ⟦a✝ i⟧) i ⬝ (fun i => ⟦a i⟧) i

Tactic:
simp only [pi_lift]

Result:
case h.h
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
a : (i : ι) → Path (bs i) (cs i)
a✝ : (i : ι) → Path (as i) (bs i)
⊢ ⟦Path.pi a✝⟧ ⬝ ⟦Path.pi a⟧ = pi fun i => ⟦a✝ i⟧ ⬝ ⟦a i⟧

Proof state:
case h.h
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
a : (i : ι) → Path (bs i) (cs i)
a✝ : (i : ι) → Path (as i) (bs i)
⊢ ⟦Path.pi a✝⟧ ⬝ ⟦Path.pi a⟧ = pi fun i => ⟦a✝ i⟧ ⬝ ⟦a i⟧

Tactic:
rw [← Path.Homotopic.comp_lift, Path.trans_pi_eq_pi_trans, ← pi_lift]

Result:
case h.h
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
a : (i : ι) → Path (bs i) (cs i)
a✝ : (i : ι) → Path (as i) (bs i)
⊢ (pi fun i => ⟦(a✝ i).trans (a i)⟧) = pi fun i => ⟦a✝ i⟧ ⬝ ⟦a i⟧

Proof state:
case h
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
γ₀ : (i : ι) → Homotopic.Quotient (as i) (bs i)
a : (i : ι) → Path (bs i) (cs i)
⊢ (pi γ₀ ⬝ pi fun i => ⟦a i⟧) = pi fun i => γ₀ i ⬝ (fun i => ⟦a i⟧) i

Tactic:
induction γ₀ using Quotient.induction_on_pi

Result:
case h.h
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
a : (i : ι) → Path (bs i) (cs i)
a✝ : (i : ι) → Path (as i) (bs i)
⊢ ((pi fun i => ⟦a✝ i⟧) ⬝ pi fun i => ⟦a i⟧) = pi fun i => (fun i => ⟦a✝ i⟧) i ⬝ (fun i => ⟦a i⟧) i
-- Mathlib/NumberTheory/Padics/PadicNorm.lean
theorem eq_zpow_of_nonzero {q : ℚ} (hq : q ≠ 0) :
    padicNorm p q = (p : ℚ) ^ (-padicValRat p q)

Proof state:
p : ℕ
q : ℚ
hq : q ≠ 0
⊢ padicNorm p q = ↑p ^ (-padicValRat p q)

Tactic:
simp [hq, padicNorm]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
theorem norm_le_pow_iff_norm_lt_pow_add_one (x : ℤ_[p]) (n : ℤ) :
    ‖x‖ ≤ (p : ℝ) ^ n ↔ ‖x‖ < (p : ℝ) ^ (n + 1)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℤ
⊢ ‖↑x‖ ≤ ↑p ^ n ↔ ‖↑x‖ < ↑p ^ (n + 1)

Tactic:
exact Padic.norm_le_pow_iff_norm_lt_pow_add_one _ _

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℤ
⊢ ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)

Tactic:
rw [norm_def]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℤ
⊢ ‖↑x‖ ≤ ↑p ^ n ↔ ‖↑x‖ < ↑p ^ (n + 1)
-- Mathlib/Algebra/Order/Sub/Basic.lean
theorem tsub_le_tsub_iff_left (ha : AddLECancellable a) (hc : AddLECancellable c)
    (h : c ≤ a) : a - b ≤ a - c ↔ c ≤ b

Proof state:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
ha : AddLECancellable a
hc : AddLECancellable c
h : c ≤ a
⊢ a + c ≤ a + b → c ≤ b

Tactic:
apply ha

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
ha : AddLECancellable a
hc : AddLECancellable c
h : c ≤ a
⊢ a - b ≤ a - c ↔ c ≤ b

Tactic:
refine ⟨?_, fun h => tsub_le_tsub_left h a⟩

Result:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
ha : AddLECancellable a
hc : AddLECancellable c
h : c ≤ a
⊢ a - b ≤ a - c → c ≤ b

Proof state:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
ha : AddLECancellable a
hc : AddLECancellable c
h : c ≤ a
⊢ a - b ≤ a - c → c ≤ b

Tactic:
rw [tsub_le_iff_left, ← hc.add_tsub_assoc_of_le h, hc.le_tsub_iff_right (h.trans le_add_self),
  add_comm b]

Result:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
ha : AddLECancellable a
hc : AddLECancellable c
h : c ≤ a
⊢ a + c ≤ a + b → c ≤ b
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem C_comp_two_mul_X (n : ℤ) : (C R n).comp (2 * X) = 2 * T R n

Proof state:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : (C R (↑n + 1)).comp (2 * X) = 2 * T R (↑n + 1)
ih2 : (C R ↑n).comp (2 * X) = 2 * T R ↑n
⊢ (C R (↑n + 2)).comp (2 * X) = 2 * T R (↑n + 2)

Tactic:
simp_rw [C_add_two, T_add_two, sub_comp, mul_comp, X_comp, ih1, ih2]

Result:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : (C R (↑n + 1)).comp (2 * X) = 2 * T R (↑n + 1)
ih2 : (C R ↑n).comp (2 * X) = 2 * T R ↑n
⊢ 2 * X * (2 * T R (↑n + 1)) - 2 * T R ↑n = 2 * (2 * X * T R (↑n + 1) - T R ↑n)

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ (C R n).comp (2 * X) = 2 * T R n

Tactic:
induction n using Polynomial.Chebyshev.induct with
| zero => simp
| one => simp
| add_two n ih1 ih2 =>
  simp_rw [C_add_two, T_add_two, sub_comp, mul_comp, X_comp, ih1, ih2]
  ring
| neg_add_one n ih1 ih2 =>
  simp_rw [C_sub_one, T_sub_one, sub_comp, mul_comp, X_comp, ih1, ih2]
  ring

Result:
no goals

Proof state:
case one
R : Type u_1
inst✝ : CommRing R
⊢ (C R 1).comp (2 * X) = 2 * T R 1

Tactic:
simp

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝ : CommRing R
⊢ (C R 0).comp (2 * X) = 2 * T R 0

Tactic:
simp

Result:
no goals

Proof state:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : (C R (-↑n)).comp (2 * X) = 2 * T R (-↑n)
ih2 : (C R (-↑n + 1)).comp (2 * X) = 2 * T R (-↑n + 1)
⊢ (C R (-↑n - 1)).comp (2 * X) = 2 * T R (-↑n - 1)

Tactic:
simp_rw [C_sub_one, T_sub_one, sub_comp, mul_comp, X_comp, ih1, ih2]

Result:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : (C R (-↑n)).comp (2 * X) = 2 * T R (-↑n)
ih2 : (C R (-↑n + 1)).comp (2 * X) = 2 * T R (-↑n + 1)
⊢ 2 * X * (2 * T R (-↑n)) - 2 * T R (-↑n + 1) = 2 * (2 * X * T R (-↑n) - T R (-↑n + 1))

Proof state:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : (C R (-↑n)).comp (2 * X) = 2 * T R (-↑n)
ih2 : (C R (-↑n + 1)).comp (2 * X) = 2 * T R (-↑n + 1)
⊢ 2 * X * (2 * T R (-↑n)) - 2 * T R (-↑n + 1) = 2 * (2 * X * T R (-↑n) - T R (-↑n + 1))

Tactic:
ring

Result:
no goals

Proof state:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : (C R (↑n + 1)).comp (2 * X) = 2 * T R (↑n + 1)
ih2 : (C R ↑n).comp (2 * X) = 2 * T R ↑n
⊢ 2 * X * (2 * T R (↑n + 1)) - 2 * T R ↑n = 2 * (2 * X * T R (↑n + 1) - T R ↑n)

Tactic:
ring

Result:
no goals
-- Mathlib/Analysis/SumIntegralComparisons.lean
theorem MonotoneOn.sum_le_integral_Ico (hab : a ≤ b) (hf : MonotoneOn f (Set.Icc a b)) :
    ∑ x ∈ Finset.Ico a b, f x ≤ ∫ x in a..b, f x

Proof state:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
⊢ ∑ x ∈ Finset.Ico a b, f ↑x ≤ ∫ (x : ℝ) in ↑a..↑b, f x

Tactic:
rw [← neg_le_neg_iff, ← Finset.sum_neg_distrib, ← intervalIntegral.integral_neg]

Result:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
⊢ ∫ (x : ℝ) in ↑a..↑b, -f x ≤ ∑ x ∈ Finset.Ico a b, -f ↑x

Proof state:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
⊢ ∫ (x : ℝ) in ↑a..↑b, -f x ≤ ∑ x ∈ Finset.Ico a b, -f ↑x

Tactic:
exact hf.neg.integral_le_sum_Ico hab

Result:
no goals
-- Mathlib/Data/Set/Sigma.lean
theorem mk_preimage_sigma_eq_if [DecidablePred (· ∈ s)] :
    Sigma.mk i ⁻¹' s.sigma t = if i ∈ s then t i else ∅

Proof state:
ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : DecidablePred fun x => x ∈ s
⊢ Sigma.mk i ⁻¹' s.sigma t = if i ∈ s then t i else ∅

Tactic:
split_ifs <;> simp [*]

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Basic.lean
theorem Finset.norm_prod_le' {α : Type*} [NormedCommRing α] (s : Finset ι) (hs : s.Nonempty)
    (f : ι → α) : ‖∏ i ∈ s, f i‖ ≤ ∏ i ∈ s, ‖f i‖

Proof state:
case mk.mk
ι : Type u_4
α : Type u_5
inst✝ : NormedCommRing α
f : ι → α
val✝ : Multiset ι
l : List ι
hl : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι)) l)
hs : { val := Quot.mk (⇑(List.isSetoid ι)) l, nodup := hl }.Nonempty
⊢ ‖∏ i ∈ { val := Quot.mk (⇑(List.isSetoid ι)) l, nodup := hl }, f i‖ ≤
    ∏ i ∈ { val := Quot.mk (⇑(List.isSetoid ι)) l, nodup := hl }, ‖f i‖

Tactic:
have : l.map f ≠ [] := by simpa using hs

Result:
case mk.mk
ι : Type u_4
α : Type u_5
inst✝ : NormedCommRing α
f : ι → α
val✝ : Multiset ι
l : List ι
hl : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι)) l)
hs : { val := Quot.mk (⇑(List.isSetoid ι)) l, nodup := hl }.Nonempty
this : List.map f l ≠ []
⊢ ‖∏ i ∈ { val := Quot.mk (⇑(List.isSetoid ι)) l, nodup := hl }, f i‖ ≤
    ∏ i ∈ { val := Quot.mk (⇑(List.isSetoid ι)) l, nodup := hl }, ‖f i‖

Proof state:
ι : Type u_4
α : Type u_5
inst✝ : NormedCommRing α
f : ι → α
val✝ : Multiset ι
l : List ι
hl : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι)) l)
hs : { val := Quot.mk (⇑(List.isSetoid ι)) l, nodup := hl }.Nonempty
⊢ List.map f l ≠ []

Tactic:
simpa using hs

Result:
no goals

Proof state:
ι : Type u_4
α : Type u_5
inst✝ : NormedCommRing α
s : Finset ι
hs : s.Nonempty
f : ι → α
⊢ ‖∏ i ∈ s, f i‖ ≤ ∏ i ∈ s, ‖f i‖

Tactic:
rcases s with ⟨⟨l⟩, hl⟩

Result:
case mk.mk
ι : Type u_4
α : Type u_5
inst✝ : NormedCommRing α
f : ι → α
val✝ : Multiset ι
l : List ι
hl : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι)) l)
hs : { val := Quot.mk (⇑(List.isSetoid ι)) l, nodup := hl }.Nonempty
⊢ ‖∏ i ∈ { val := Quot.mk (⇑(List.isSetoid ι)) l, nodup := hl }, f i‖ ≤
    ∏ i ∈ { val := Quot.mk (⇑(List.isSetoid ι)) l, nodup := hl }, ‖f i‖

Proof state:
case mk.mk
ι : Type u_4
α : Type u_5
inst✝ : NormedCommRing α
f : ι → α
val✝ : Multiset ι
l : List ι
hl : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι)) l)
hs : { val := Quot.mk (⇑(List.isSetoid ι)) l, nodup := hl }.Nonempty
this : List.map f l ≠ []
⊢ ‖∏ i ∈ { val := Quot.mk (⇑(List.isSetoid ι)) l, nodup := hl }, f i‖ ≤
    ∏ i ∈ { val := Quot.mk (⇑(List.isSetoid ι)) l, nodup := hl }, ‖f i‖

Tactic:
simpa using List.norm_prod_le' this

Result:
no goals
-- Mathlib/RingTheory/Unramified/Locus.lean
lemma unramifiedLocus_eq_compl_support :
    unramifiedLocus R A = (Module.support A (Ω[A⁄R]))ᶜ

Proof state:
R A : Type u
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ unramifiedLocus R A = (Module.support A (Ω[A⁄R]))ᶜ

Tactic:
ext p

Result:
case h
R A : Type u
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : PrimeSpectrum A
⊢ p ∈ unramifiedLocus R A ↔ p ∈ (Module.support A (Ω[A⁄R]))ᶜ

Proof state:
case h
R A : Type u
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : PrimeSpectrum A
⊢ p ∈ unramifiedLocus R A ↔ Subsingleton (LocalizedModule p.asIdeal.primeCompl (Ω[A⁄R]))

Tactic:
have := IsLocalizedModule.iso p.asIdeal.primeCompl
  (KaehlerDifferential.map R R A (Localization.AtPrime p.asIdeal))

Result:
case h
R A : Type u
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : PrimeSpectrum A
this : LocalizedModule p.asIdeal.primeCompl (Ω[A⁄R]) ≃ₗ[A] Ω[Localization.AtPrime p.asIdeal⁄R]
⊢ p ∈ unramifiedLocus R A ↔ Subsingleton (LocalizedModule p.asIdeal.primeCompl (Ω[A⁄R]))

Proof state:
case h
R A : Type u
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : PrimeSpectrum A
⊢ p ∈ unramifiedLocus R A ↔ p ∈ (Module.support A (Ω[A⁄R]))ᶜ

Tactic:
simp only [Set.mem_compl_iff, Module.not_mem_support_iff]

Result:
case h
R A : Type u
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : PrimeSpectrum A
⊢ p ∈ unramifiedLocus R A ↔ Subsingleton (LocalizedModule p.asIdeal.primeCompl (Ω[A⁄R]))

Proof state:
case h
R A : Type u
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : PrimeSpectrum A
this : LocalizedModule p.asIdeal.primeCompl (Ω[A⁄R]) ≃ₗ[A] Ω[Localization.AtPrime p.asIdeal⁄R]
⊢ p ∈ unramifiedLocus R A ↔ Subsingleton (LocalizedModule p.asIdeal.primeCompl (Ω[A⁄R]))

Tactic:
exact (Algebra.formallyUnramified_iff _ _).trans this.subsingleton_congr.symm

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsCycleOn.apply_mem_iff (hf : f.IsCycleOn s) : f x ∈ s ↔ x ∈ s :=
  ⟨fun hx => by
    convert hf.1.perm_inv.1 hx
    rw [inv_apply_self], fun hx => hf.1.mapsTo hx⟩

Proof state:
α : Type u_2
f : Perm α
s : Set α
x : α
hf : f.IsCycleOn s
hx : f x ∈ s
⊢ x ∈ s

Tactic:
convert hf.1.perm_inv.1 hx

Result:
case h.e'_5
α : Type u_2
f : Perm α
s : Set α
x : α
hf : f.IsCycleOn s
hx : f x ∈ s
⊢ x = f⁻¹ (f x)

Proof state:
case h.e'_5
α : Type u_2
f : Perm α
s : Set α
x : α
hf : f.IsCycleOn s
hx : f x ∈ s
⊢ x = f⁻¹ (f x)

Tactic:
rw [inv_apply_self]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem tprod_dite_left (P : Prop) [Decidable P] (x : β → P → α) :
    ∏' b : β, (if h : P then x b h else 1) = if h : P then ∏' b : β, x b h else 1

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
P : Prop
inst✝ : Decidable P
x : β → P → α
⊢ (∏' (b : β), if h : P then x b h else 1) = if h : P then ∏' (b : β), x b h else 1

Tactic:
by_cases hP : P <;> simp [hP]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/ScaleRoots.lean
@[simp]
lemma scaleRoots_zero (p : R[X]) :
    p.scaleRoots 0 = p.leadingCoeff • X ^ p.natDegree

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h₁ : p.natDegree ≤ n
h₂ : n = p.natDegree
⊢ p.coeff n = p.leadingCoeff

Tactic:
subst h₂

Result:
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
h₁ : p.natDegree ≤ p.natDegree
⊢ p.coeff p.natDegree = p.leadingCoeff

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
h₁ : p.natDegree ≤ p.natDegree
⊢ p.coeff p.natDegree = p.leadingCoeff

Tactic:
rfl

Result:
no goals

Proof state:
case a
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (if p.natDegree ≤ n then p.coeff n else 0) = if n = p.natDegree then p.leadingCoeff else 0

Tactic:
split_ifs with h₁ h₂ h₂

Result:
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h₁ : p.natDegree ≤ n
h₂ : n = p.natDegree
⊢ p.coeff n = p.leadingCoeff

case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h₁ : p.natDegree ≤ n
h₂ : ¬n = p.natDegree
⊢ p.coeff n = 0

case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h₁ : ¬p.natDegree ≤ n
h₂ : n = p.natDegree
⊢ 0 = p.leadingCoeff

case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h₁ : ¬p.natDegree ≤ n
h₂ : ¬n = p.natDegree
⊢ 0 = 0

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h₁ : ¬p.natDegree ≤ n
h₂ : n = p.natDegree
⊢ 0 = p.leadingCoeff

Tactic:
exact (h₁ h₂.ge).elim

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ p.scaleRoots 0 = p.leadingCoeff • X ^ p.natDegree

Tactic:
ext n

Result:
case a
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p.scaleRoots 0).coeff n = (p.leadingCoeff • X ^ p.natDegree).coeff n

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h₁ : ¬p.natDegree ≤ n
h₂ : ¬n = p.natDegree
⊢ 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
case a
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p.scaleRoots 0).coeff n = (p.leadingCoeff • X ^ p.natDegree).coeff n

Tactic:
simp only [coeff_scaleRoots, ne_eq, tsub_eq_zero_iff_le, not_le, zero_pow_eq, mul_ite,
  mul_one, mul_zero, coeff_smul, coeff_X_pow, smul_eq_mul]

Result:
case a
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (if p.natDegree ≤ n then p.coeff n else 0) = if n = p.natDegree then p.leadingCoeff else 0

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h₁ : p.natDegree ≤ n
h₂ : ¬n = p.natDegree
⊢ p.coeff n = 0

Tactic:
exact coeff_eq_zero_of_natDegree_lt (lt_of_le_of_ne h₁ (Ne.symm h₂))

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem sub.elim {motive : Nat → Prop}
    (x y : Nat)
    (h₁ : y ≤ x → (k : Nat) → x = y + k → motive k)
    (h₂ : x < y → motive 0)
    : motive (x - y)

Proof state:
motive : Nat → Prop
x y : Nat
h₁ : y ≤ x → ∀ (k : Nat), x = y + k → motive k
h₂ : x < y → motive 0
⊢ motive (x - y)

Tactic:
cases Nat.lt_or_ge x y with
| inl hlt => rw [Nat.sub_eq_zero_of_le (Nat.le_of_lt hlt)]; exact h₂ hlt
| inr hle => exact h₁ hle (x - y) (Nat.add_sub_of_le hle).symm

Result:
no goals

Proof state:
case inl
motive : Nat → Prop
x y : Nat
h₁ : y ≤ x → ∀ (k : Nat), x = y + k → motive k
h₂ : x < y → motive 0
hlt : x < y
⊢ motive 0

Tactic:
exact h₂ hlt

Result:
no goals

Proof state:
case inl
motive : Nat → Prop
x y : Nat
h₁ : y ≤ x → ∀ (k : Nat), x = y + k → motive k
h₂ : x < y → motive 0
hlt : x < y
⊢ motive (x - y)

Tactic:
rw [Nat.sub_eq_zero_of_le (Nat.le_of_lt hlt)]

Result:
case inl
motive : Nat → Prop
x y : Nat
h₁ : y ≤ x → ∀ (k : Nat), x = y + k → motive k
h₂ : x < y → motive 0
hlt : x < y
⊢ motive 0

Proof state:
case inr
motive : Nat → Prop
x y : Nat
h₁ : y ≤ x → ∀ (k : Nat), x = y + k → motive k
h₂ : x < y → motive 0
hle : x ≥ y
⊢ motive (x - y)

Tactic:
exact h₁ hle (x - y) (Nat.add_sub_of_le hle).symm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKeyD_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a fallback : α} :
    m.1.isEmpty = true → m.getKeyD a fallback = fallback

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
a fallback : α
⊢ (toListModel m.val.buckets).isEmpty = true → List.getKeyD a (toListModel m.val.buckets) fallback = fallback

Tactic:
empty

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
a fallback : α
⊢ m.val.isEmpty = true → m.getKeyD a fallback = fallback

Tactic:
simp_to_model

Result:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
a fallback : α
⊢ (toListModel m.val.buckets).isEmpty = true → List.getKeyD a (toListModel m.val.buckets) fallback = fallback
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem updateBucket [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α]
    {m : Array (AssocList α β)} {h : 0 < m.size} {a : α} {f : AssocList α β → AssocList α β}
    (hf : ∀ l p, p ∈ (f l).toList → containsKey p.1 l.toList ∨ hash p.1 = hash a)
    (hm : IsHashSelf m) : IsHashSelf (updateBucket m h a f)

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : PartialEquivBEq α
inst✝ : LawfulHashable α
m : Array (AssocList α β)
h : 0 < m.size
a : α
f : AssocList α β → AssocList α β
hf :
  ∀ (l : AssocList α β) (p : (a : α) × β a), p ∈ (f l).toList → containsKey p.fst l.toList = true ∨ hash p.fst = hash a
hm : IsHashSelf m
⊢ IsHashSelf (Internal.updateBucket m h a f)

Tactic:
rw [Internal.updateBucket]

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : PartialEquivBEq α
inst✝ : LawfulHashable α
m : Array (AssocList α β)
h : 0 < m.size
a : α
f : AssocList α β → AssocList α β
hf :
  ∀ (l : AssocList α β) (p : (a : α) × β a), p ∈ (f l).toList → containsKey p.fst l.toList = true ∨ hash p.fst = hash a
hm : IsHashSelf m
⊢ IsHashSelf
    (match mkIdx m.size h (hash a) with
    | ⟨i, h⟩ => m.uset i (f m[i]) h)

Proof state:
case inr
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : PartialEquivBEq α
inst✝ : LawfulHashable α
m : Array (AssocList α β)
h : 0 < m.size
a : α
f : AssocList α β → AssocList α β
hf✝ :
  ∀ (l : AssocList α β) (p : (a : α) × β a), p ∈ (f l).toList → containsKey p.fst l.toList = true ∨ hash p.fst = hash a
hm : IsHashSelf m
h' : HashesTo m[(mkIdx m.size h (hash a)).val].toList (mkIdx m.size h (hash a)).val.toNat m.size
x✝ : 0 < m.size
p : (a : α) × β a
hp : p ∈ (f m[(mkIdx m.size h (hash a)).val]).toList
hf : hash p.fst = hash a
⊢ (mkIdx m.size x✝ (hash p.fst)).val.toNat = (mkIdx m.size h (hash a)).val.toNat

Tactic:
rw [hf]

Result:
no goals