harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/List.lean
theorem continuousAt_eraseIdx {n : ℕ} {i : Fin (n + 1)} :
    ∀ {l : List.Vector α (n + 1)}, ContinuousAt (List.Vector.eraseIdx i) l
  | ⟨l, hl⟩ => by
    rw [ContinuousAt, List.Vector.eraseIdx, tendsto_subtype_rng]
    simp only [Vector.eraseIdx_val]
    exact Tendsto.comp List.tendsto_eraseIdx continuousAt_subtype_val

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
l : List α
hl : l.length = n + 1
⊢ ContinuousAt (List.Vector.eraseIdx i) ⟨l, hl⟩

Tactic:
rw [ContinuousAt, List.Vector.eraseIdx, tendsto_subtype_rng]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
l : List α
hl : l.length = n + 1
⊢ Tendsto (fun x => ↑(List.Vector.eraseIdx i x)) (𝓝 ⟨l, hl⟩) (𝓝 ↑⟨l.eraseIdx ↑i, ⋯⟩)

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
l : List α
hl : l.length = n + 1
⊢ Tendsto (fun x => ↑(List.Vector.eraseIdx i x)) (𝓝 ⟨l, hl⟩) (𝓝 ↑⟨l.eraseIdx ↑i, ⋯⟩)

Tactic:
simp only [Vector.eraseIdx_val]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
l : List α
hl : l.length = n + 1
⊢ Tendsto (fun x => (↑x).eraseIdx ↑i) (𝓝 ⟨l, hl⟩) (𝓝 (l.eraseIdx ↑i))

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
l : List α
hl : l.length = n + 1
⊢ Tendsto (fun x => (↑x).eraseIdx ↑i) (𝓝 ⟨l, hl⟩) (𝓝 (l.eraseIdx ↑i))

Tactic:
exact Tendsto.comp List.tendsto_eraseIdx continuousAt_subtype_val

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/RankNullity.lean
theorem LinearMap.lift_rank_eq_of_surjective {f : M →ₗ[R] M'} (h : Surjective f) :
    lift.{v} (Module.rank R M) =
      lift.{u} (Module.rank R M') + lift.{v} (Module.rank R (LinearMap.ker f))

Proof state:
R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M'
h : Surjective ⇑f
⊢ lift.{v, u} (Module.rank R M) = lift.{u, v} (Module.rank R M') + lift.{v, u} (Module.rank R ↥(ker f))

Tactic:
rw [← lift_rank_range_add_rank_ker f, ← rank_range_of_surjective f h]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
theorem weightedHomogeneousComponent_eq_zero'
    (h : ∀ d : σ →₀ ℕ, d ∈ φ.support → weight w d ≠ n) :
    weightedHomogeneousComponent w n φ = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (weight w) d ≠ n
⊢ ∀ x ∈ Finset.filter (fun d => (weight w) d = n) φ.support, (monomial x) (coeff x φ) = 0

Tactic:
intro d hd

Result:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (weight w) d ≠ n
d : σ →₀ ℕ
hd : d ∈ Finset.filter (fun d => (weight w) d = n) φ.support
⊢ (monomial d) (coeff d φ) = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (weight w) d ≠ n
d : σ →₀ ℕ
hd : d ∈ φ.support ∧ (weight w) d = n
⊢ False

Tactic:
exact h _ hd.1 hd.2

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (weight w) d ≠ n
⊢ (weightedHomogeneousComponent w n) φ = 0

Tactic:
rw [weightedHomogeneousComponent_apply, sum_eq_zero]

Result:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (weight w) d ≠ n
⊢ ∀ x ∈ Finset.filter (fun d => (weight w) d = n) φ.support, (monomial x) (coeff x φ) = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (weight w) d ≠ n
d : σ →₀ ℕ
hd : d ∈ φ.support ∧ (weight w) d = n
⊢ (monomial d) (coeff d φ) = 0

Tactic:
exfalso

Result:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (weight w) d ≠ n
d : σ →₀ ℕ
hd : d ∈ φ.support ∧ (weight w) d = n
⊢ False

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (weight w) d ≠ n
⊢ (weightedHomogeneousComponent w n) φ = 0

Tactic:
classical
rw [weightedHomogeneousComponent_apply, sum_eq_zero]
intro d hd; rw [mem_filter] at hd
exfalso; exact h _ hd.1 hd.2

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (weight w) d ≠ n
d : σ →₀ ℕ
hd : d ∈ Finset.filter (fun d => (weight w) d = n) φ.support
⊢ (monomial d) (coeff d φ) = 0

Tactic:
rw [mem_filter] at hd

Result:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (weight w) d ≠ n
d : σ →₀ ℕ
hd : d ∈ φ.support ∧ (weight w) d = n
⊢ (monomial d) (coeff d φ) = 0
-- Mathlib/CategoryTheory/SmallObject/TransfiniteIteration.lean
lemma iterationFunctor_obj (i : J) {j : J} (iter : Φ.Iteration j) (hi : i ≤ j) :
    (Φ.iterationFunctor J).obj i = iter.F.obj ⟨i, hi⟩ :=
  Iteration.congr_obj (Φ.iter i) iter i (by simp) hi

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i j : J
iter : Φ.Iteration j
hi : i ≤ j
⊢ i ≤ i

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem sub_add_min_cancel (n m : Nat) : n - m + min n m = n

Proof state:
n m : Nat
⊢ n - m + min n m = n

Tactic:
rw [Nat.sub_eq_sub_min, Nat.sub_add_cancel (Nat.min_le_left ..)]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Addition.lean
theorem ne_zero_of_eq_add_single [Zero Γ] {x y : HahnSeries Γ R}
    (hxy : x = y + single x.order x.leadingCoeff) (hy : y ≠ 0) : x ≠ 0

Proof state:
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : Zero Γ
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
h : x = 0
⊢ False

Tactic:
simp only [h, order_zero, leadingCoeff_zero, map_zero, add_zero] at hxy

Result:
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : Zero Γ
x y : HahnSeries Γ R
hy : y ≠ 0
h : x = 0
hxy : 0 = y
⊢ False

Proof state:
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : Zero Γ
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
⊢ x ≠ 0

Tactic:
by_contra h

Result:
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : Zero Γ
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
h : x = 0
⊢ False

Proof state:
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : Zero Γ
x y : HahnSeries Γ R
hy : y ≠ 0
h : x = 0
hxy : 0 = y
⊢ False

Tactic:
exact hy hxy.symm

Result:
no goals
-- Mathlib/Data/Matrix/Defs.lean
theorem transpose_transpose (M : Matrix m n α) : Mᵀᵀ = M

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i✝ : m
j✝ : n
⊢ Mᵀᵀ i✝ j✝ = M i✝ j✝

Tactic:
rfl

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
⊢ Mᵀᵀ = M

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i✝ : m
j✝ : n
⊢ Mᵀᵀ i✝ j✝ = M i✝ j✝
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/ArctanDeriv.lean
theorem tendsto_abs_tan_of_cos_eq_zero {x : ℝ} (hx : cos x = 0) :
    Tendsto (fun x => abs (tan x)) (𝓝[≠] x) atTop

Proof state:
x : ℝ
hx✝ : cos x = 0
hx : Complex.cos ↑x = 0
⊢ Tendsto Complex.ofReal (𝓝[≠] x) (𝓝[≠] ↑x)

Tactic:
refine Tendsto.inf Complex.continuous_ofReal.continuousAt ?_

Result:
x : ℝ
hx✝ : cos x = 0
hx : Complex.cos ↑x = 0
⊢ Tendsto Complex.ofReal (𝓟 {x}ᶜ) (𝓟 {↑x}ᶜ)

Proof state:
x : ℝ
hx✝ : cos x = 0
hx : Complex.cos ↑x = 0
⊢ Tendsto (fun x => |tan x|) (𝓝[≠] x) atTop

Tactic:
simp only [← Real.norm_eq_abs, ← Complex.norm_real, Complex.ofReal_tan]

Result:
x : ℝ
hx✝ : cos x = 0
hx : Complex.cos ↑x = 0
⊢ Tendsto (fun x => ‖Complex.tan ↑x‖) (𝓝[≠] x) atTop

Proof state:
x : ℝ
hx✝ : cos x = 0
hx : Complex.cos ↑x = 0
⊢ Tendsto Complex.ofReal (𝓟 {x}ᶜ) (𝓟 {↑x}ᶜ)

Tactic:
exact tendsto_principal_principal.2 fun y => mt Complex.ofReal_inj.1

Result:
no goals

Proof state:
x : ℝ
hx : cos x = 0
⊢ Tendsto (fun x => |tan x|) (𝓝[≠] x) atTop

Tactic:
have hx : Complex.cos x = 0 := mod_cast hx

Result:
x : ℝ
hx✝ : cos x = 0
hx : Complex.cos ↑x = 0
⊢ Tendsto (fun x => |tan x|) (𝓝[≠] x) atTop

Proof state:
x : ℝ
hx✝ : cos x = 0
hx : Complex.cos ↑x = 0
⊢ Tendsto (fun x => ‖Complex.tan ↑x‖) (𝓝[≠] x) atTop

Tactic:
refine (Complex.tendsto_norm_tan_of_cos_eq_zero hx).comp ?_

Result:
x : ℝ
hx✝ : cos x = 0
hx : Complex.cos ↑x = 0
⊢ Tendsto Complex.ofReal (𝓝[≠] x) (𝓝[≠] ↑x)
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem lift_le_aleph1 {c : Cardinal.{u}} : lift.{v} c ≤ ℵ₁ ↔ c ≤ ℵ₁

Proof state:
c : Cardinal.{u}
⊢ lift.{v, u} c ≤ ℵ_ 1 ↔ c ≤ ℵ_ 1

Tactic:
simpa using lift_le (b := ℵ₁)

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
lemma isCompact_isOpen_iff_ideal {s : Set (PrimeSpectrum R)} :
    IsCompact s ∧ IsOpen s ↔ ∃ I : Ideal R, I.FG ∧ (zeroLocus I)ᶜ = s

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ IsCompact s ∧ IsOpen s ↔ ∃ I, I.FG ∧ (zeroLocus ↑I)ᶜ = s

Tactic:
rw [isCompact_isOpen_iff]

Result:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (∃ t, (zeroLocus ↑t)ᶜ = s) ↔ ∃ I, I.FG ∧ (zeroLocus ↑I)ᶜ = s

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (∃ t, (zeroLocus ↑t)ᶜ = s) ↔ ∃ I, I.FG ∧ (zeroLocus ↑I)ᶜ = s

Tactic:
exact ⟨fun ⟨s, e⟩ ↦ ⟨.span s, ⟨s, rfl⟩, by simpa using e⟩,
  fun ⟨I, ⟨s, hs⟩, e⟩ ↦ ⟨s, by simpa [hs.symm] using e⟩⟩

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
s✝ : Set (PrimeSpectrum R)
x✝ : ∃ I, I.FG ∧ (zeroLocus ↑I)ᶜ = s✝
I : Ideal R
s : Finset R
hs : Ideal.span ↑s = I
e : (zeroLocus ↑I)ᶜ = s✝
⊢ (zeroLocus ↑s)ᶜ = s✝

Tactic:
simpa [hs.symm] using e

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
s✝ : Set (PrimeSpectrum R)
x✝ : ∃ t, (zeroLocus ↑t)ᶜ = s✝
s : Finset R
e : (zeroLocus ↑s)ᶜ = s✝
⊢ (zeroLocus ↑(Ideal.span ↑s))ᶜ = s✝

Tactic:
simpa using e

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
lemma integral_toReal_rnDeriv' [IsFiniteMeasure μ] [SigmaFinite ν] :
    ∫ x, (μ.rnDeriv ν x).toReal ∂ν = (μ Set.univ).toReal - (μ.singularPart ν Set.univ).toReal

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = (μ Set.univ).toReal - ((μ.singularPart ν) Set.univ).toReal

Tactic:
rw [← ENNReal.toReal_sub_of_le (μ.singularPart_le ν Set.univ) (measure_ne_top _ _),
  ← Measure.sub_apply .univ (Measure.singularPart_le μ ν), Measure.measure_sub_singularPart,
  ← Measure.setIntegral_toReal_rnDeriv_eq_withDensity, setIntegral_univ]

Result:
no goals
-- Mathlib/Probability/Kernel/Defs.lean
theorem sum_comm [Countable ι] (κ : ι → ι → Kernel α β) :
    (Kernel.sum fun n => Kernel.sum (κ n)) = Kernel.sum fun m => Kernel.sum fun n => κ n m

Proof state:
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
κ : ι → ι → Kernel α β
a : α
s : Set β
a✝ : MeasurableSet s
⊢ ((Kernel.sum fun n => Kernel.sum (κ n)) a) s = ((Kernel.sum fun m => Kernel.sum fun n => κ n m) a) s

Tactic:
simp_rw [sum_apply]

Result:
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
κ : ι → ι → Kernel α β
a : α
s : Set β
a✝ : MeasurableSet s
⊢ (Measure.sum fun n => Measure.sum fun n_1 => (κ n n_1) a) s =
    (Measure.sum fun n => Measure.sum fun n_1 => (κ n_1 n) a) s

Proof state:
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
κ : ι → ι → Kernel α β
a : α
s : Set β
a✝ : MeasurableSet s
⊢ (Measure.sum fun n => Measure.sum fun n_1 => (κ n n_1) a) s =
    (Measure.sum fun n => Measure.sum fun n_1 => (κ n_1 n) a) s

Tactic:
rw [Measure.sum_comm]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
κ : ι → ι → Kernel α β
⊢ (Kernel.sum fun n => Kernel.sum (κ n)) = Kernel.sum fun m => Kernel.sum fun n => κ n m

Tactic:
ext a s

Result:
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
κ : ι → ι → Kernel α β
a : α
s : Set β
a✝ : MeasurableSet s
⊢ ((Kernel.sum fun n => Kernel.sum (κ n)) a) s = ((Kernel.sum fun m => Kernel.sum fun n => κ n m) a) s
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
/-- Strict **Cauchy-Schwarz** is equivalent to linear independence for positive definite symmetric
forms. -/
lemma apply_sq_lt_iff_linearIndependent_of_symm [NoZeroSMulDivisors R M]
    (hp : ∀ x, x ≠ 0 → 0 < B x x) (hB: B.IsSymm) (x y : M) :
    (B x y) ^ 2 < (B x x) * (B y y) ↔ LinearIndependent R ![x, y]

Proof state:
R : Type u_1
M : Type u_5
inst✝³ : LinearOrderedCommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : LinearMap.BilinForm R M
inst✝ : NoZeroSMulDivisors R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
hB : IsSymm B
x y : M
⊢ (B x) y * (B y) x < (B x) x * (B y) y ↔ LinearIndependent R ![x, y]

Tactic:
exact apply_mul_apply_lt_iff_linearIndependent B hp x y

Result:
no goals

Proof state:
R : Type u_1
M : Type u_5
inst✝³ : LinearOrderedCommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : LinearMap.BilinForm R M
inst✝ : NoZeroSMulDivisors R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
hB : IsSymm B
x y : M
⊢ (B x) y ^ 2 = (B x) y * (B y) x

Tactic:
rw [sq, ← hB, RingHom.id_apply]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_5
inst✝³ : LinearOrderedCommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : LinearMap.BilinForm R M
inst✝ : NoZeroSMulDivisors R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
hB : IsSymm B
x y : M
⊢ (B x) y ^ 2 < (B x) x * (B y) y ↔ LinearIndependent R ![x, y]

Tactic:
rw [show (B x y) ^ 2 = (B x y) * (B y x) by rw [sq, ← hB, RingHom.id_apply]]

Result:
R : Type u_1
M : Type u_5
inst✝³ : LinearOrderedCommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : LinearMap.BilinForm R M
inst✝ : NoZeroSMulDivisors R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
hB : IsSymm B
x y : M
⊢ (B x) y * (B y) x < (B x) x * (B y) y ↔ LinearIndependent R ![x, y]
-- Mathlib/Analysis/SpecialFunctions/NonIntegrable.lean
theorem intervalIntegrable_inv_iff {a b : ℝ} :
    IntervalIntegrable (fun x => x⁻¹) volume a b ↔ a = b ∨ (0 : ℝ) ∉ [[a, b]]

Proof state:
a b : ℝ
⊢ IntervalIntegrable (fun x => x⁻¹) volume a b ↔ a = b ∨ 0 ∉ [[a, b]]

Tactic:
simp only [← intervalIntegrable_sub_inv_iff, sub_zero]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem omega0_lt_preOmega_iff {x : Ordinal} : ω < preOmega x ↔ ω < x

Proof state:
x : Ordinal.{u_1}
⊢ ω < preOmega x ↔ ω < x

Tactic:
conv_lhs => rw [← preOmega_omega0, preOmega_lt_preOmega]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Inverse.lean
theorem eq_divided_by_X_pow_order_Iff_Unit {f : k⟦X⟧} (hf : f ≠ 0) :
    f = divided_by_X_pow_order hf ↔ IsUnit f :=
  ⟨fun h ↦ by rw [h]; exact isUnit_divided_by_X_pow_order hf, fun h ↦ by
    have : f.order.lift (order_finite_iff_ne_zero.mpr hf) = 0

Proof state:
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
h : f = divided_by_X_pow_order hf
⊢ IsUnit f

Tactic:
rw [h]

Result:
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
h : f = divided_by_X_pow_order hf
⊢ IsUnit (divided_by_X_pow_order hf)

Proof state:
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
h : IsUnit f
⊢ f = divided_by_X_pow_order hf

Tactic:
have : f.order.lift (order_finite_iff_ne_zero.mpr hf) = 0 := by
  simp [order_zero_of_unit h]

Result:
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
h : IsUnit f
this : f.order.lift ⋯ = 0
⊢ f = divided_by_X_pow_order hf

Proof state:
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
h : IsUnit f
this : f.order.lift ⋯ = 0
⊢ f = divided_by_X_pow_order hf

Tactic:
convert (self_eq_X_pow_order_mul_divided_by_X_pow_order hf).symm

Result:
case h.e'_3
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
h : IsUnit f
this : f.order.lift ⋯ = 0
⊢ divided_by_X_pow_order hf = X ^ f.order.lift ⋯ * divided_by_X_pow_order hf

Proof state:
case h.e'_3
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
h : IsUnit f
this : f.order.lift ⋯ = 0
⊢ divided_by_X_pow_order hf = X ^ f.order.lift ⋯ * divided_by_X_pow_order hf

Tactic:
simp only [this, pow_zero, one_mul]

Result:
no goals

Proof state:
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
h : IsUnit f
⊢ f.order.lift ⋯ = 0

Tactic:
simp [order_zero_of_unit h]

Result:
no goals

Proof state:
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
h : f = divided_by_X_pow_order hf
⊢ IsUnit (divided_by_X_pow_order hf)

Tactic:
exact isUnit_divided_by_X_pow_order hf

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
theorem cyclotomicRing_isIntegralClosure_of_prime :
    IsIntegralClosure (CyclotomicRing p ℤ ℚ) ℤ (CyclotomicField p ℚ)

Proof state:
p : ℕ+
hp : Fact (Nat.Prime ↑p)
⊢ IsIntegralClosure (CyclotomicRing (p ^ 1) ℤ ℚ) ℤ (CyclotomicField (p ^ 1) ℚ)

Tactic:
exact cyclotomicRing_isIntegralClosure_of_prime_pow

Result:
no goals

Proof state:
p : ℕ+
hp : Fact (Nat.Prime ↑p)
⊢ IsIntegralClosure (CyclotomicRing p ℤ ℚ) ℤ (CyclotomicField p ℚ)

Tactic:
rw [← pow_one p]

Result:
p : ℕ+
hp : Fact (Nat.Prime ↑p)
⊢ IsIntegralClosure (CyclotomicRing (p ^ 1) ℤ ℚ) ℤ (CyclotomicField (p ^ 1) ℚ)
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
lemma singularPart_restrict (μ ν : Measure α) [HaveLebesgueDecomposition μ ν]
    {s : Set α} (hs : MeasurableSet s) :
    (μ.restrict s).singularPart ν = (μ.singularPart ν).restrict s

Proof state:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
s : Set α
hs : MeasurableSet s
⊢ Measurable (s.indicator (μ.rnDeriv ν))

Tactic:
exact (μ.measurable_rnDeriv ν).indicator hs

Result:
no goals

Proof state:
case refine_3.h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
s : Set α
hs : MeasurableSet s
t : Set α
a✝ : MeasurableSet t
⊢ (μ.restrict s) t = ((μ.singularPart ν).restrict s + ν.withDensity (s.indicator (μ.rnDeriv ν))) t

Tactic:
rw [withDensity_indicator hs, ← restrict_withDensity hs, ← Measure.restrict_add,
  ← μ.haveLebesgueDecomposition_add ν]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
s : Set α
hs : MeasurableSet s
⊢ (μ.restrict s).singularPart ν = (μ.singularPart ν).restrict s

Tactic:
refine (Measure.eq_singularPart (f := s.indicator (μ.rnDeriv ν)) ?_ ?_ ?_).symm

Result:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
s : Set α
hs : MeasurableSet s
⊢ Measurable (s.indicator (μ.rnDeriv ν))

case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
s : Set α
hs : MeasurableSet s
⊢ (μ.singularPart ν).restrict s ⟂ₘ ν

case refine_3
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
s : Set α
hs : MeasurableSet s
⊢ μ.restrict s = (μ.singularPart ν).restrict s + ν.withDensity (s.indicator (μ.rnDeriv ν))

Proof state:
case refine_3
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
s : Set α
hs : MeasurableSet s
⊢ μ.restrict s = (μ.singularPart ν).restrict s + ν.withDensity (s.indicator (μ.rnDeriv ν))

Tactic:
ext t

Result:
case refine_3.h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
s : Set α
hs : MeasurableSet s
t : Set α
a✝ : MeasurableSet t
⊢ (μ.restrict s) t = ((μ.singularPart ν).restrict s + ν.withDensity (s.indicator (μ.rnDeriv ν))) t

Proof state:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
s : Set α
hs : MeasurableSet s
⊢ (μ.singularPart ν).restrict s ⟂ₘ ν

Tactic:
exact (Measure.mutuallySingular_singularPart μ ν).restrict s

Result:
no goals
-- Mathlib/Order/Atoms.lean
theorem isCoatomic_iff [OrderTop α] [OrderTop β] (f : α ≃o β) :
    IsCoatomic α ↔ IsCoatomic β

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderTop α
inst✝ : OrderTop β
f : α ≃o β
⊢ IsCoatomic α ↔ IsCoatomic β

Tactic:
simp only [← isAtomic_dual_iff_isCoatomic, f.dual.isAtomic_iff]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
theorem _root_.AddAction.IsBlock.translate
    {G : Type*} [AddGroup G] {X : Type*} [AddAction G X] (B : Set X)
    (g : G) (hB : AddAction.IsBlock G B) :
    AddAction.IsBlock G (g +ᵥ B)

Proof state:
case hB
G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
g : G
hB : AddAction.IsBlock (↥⊤) B
⊢ AddAction.IsBlock (↥(AddSubgroup.comap (AddEquiv.toAddMonoidHom (Additive.toMul (AddAut.conj g))) ⊤)) B

Tactic:
rwa [AddSubgroup.comap_top]

Result:
no goals

Proof state:
G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
g : G
hB : AddAction.IsBlock (↥⊤) B
⊢ AddAction.IsBlock (↥(AddSubgroup.map ?m.115980 (AddSubgroup.comap ?m.115980 ⊤))) (g +ᵥ B)

Tactic:
apply AddAction.IsBlock.of_addSubgroup_of_conjugate

Result:
case hB
G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
g : G
hB : AddAction.IsBlock (↥⊤) B
⊢ AddAction.IsBlock (↥(AddSubgroup.comap (AddEquiv.toAddMonoidHom (Additive.toMul (AddAut.conj g))) ⊤)) B

Proof state:
G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
g : G
hB : AddAction.IsBlock G B
⊢ AddAction.IsBlock G (g +ᵥ B)

Tactic:
rw [← AddAction.isBlock_top] at hB ⊢

Result:
G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
g : G
hB : AddAction.IsBlock (↥⊤) B
⊢ AddAction.IsBlock (↥⊤) (g +ᵥ B)

Proof state:
G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
g : G
hB : AddAction.IsBlock (↥⊤) B
⊢ AddAction.IsBlock (↥⊤) (g +ᵥ B)

Tactic:
rw [← AddSubgroup.map_comap_eq_self_of_surjective (G := G) ?_ ⊤]

Result:
G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
g : G
hB : AddAction.IsBlock (↥⊤) B
⊢ AddAction.IsBlock (↥(AddSubgroup.map ?m.115980 (AddSubgroup.comap ?m.115980 ⊤))) (g +ᵥ B)

G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
g : G
hB : AddAction.IsBlock (↥⊤) B
⊢ G →+ G

G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
g : G
hB : AddAction.IsBlock (↥⊤) B
⊢ Function.Surjective ⇑?m.115980

Proof state:
G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
g : G
hB : AddAction.IsBlock (↥⊤) B
⊢ Function.Surjective ⇑(AddEquiv.toAddMonoidHom (Additive.toMul (AddAut.conj g)))

Tactic:
exact (AddAut.conj g).surjective

Result:
no goals