harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Decomposition/Exhaustion.lean
lemma tendsto_measure_sigmaFiniteSetGE (μ ν : Measure α) [IsFiniteMeasure ν] :
    Tendsto (fun n ↦ ν (μ.sigmaFiniteSetGE ν n)) atTop
      (𝓝 (⨆ (s) (_ : MeasurableSet s) (_ : SigmaFinite (μ.restrict s)), ν s))

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
⊢ Tendsto (fun i => (⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) - 1 / ↑i) atTop
    (𝓝 (⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s))

Tactic:
nth_rewrite 2 [← tsub_zero (⨆ (s) (_ : MeasurableSet s) (_ : SigmaFinite (μ.restrict s)), ν s)]

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
⊢ Tendsto (fun i => (⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) - 1 / ↑i) atTop
    (𝓝 ((⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) - 0))

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
⊢ Tendsto (fun i => (⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) - 1 / ↑i) atTop
    (𝓝 ((⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) - 0))

Tactic:
refine ENNReal.Tendsto.sub tendsto_const_nhds ?_ (Or.inr ENNReal.zero_ne_top)

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
⊢ Tendsto (fun i => 1 / ↑i) atTop (𝓝 0)

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
⊢ Tendsto (fun i => 1 / ↑i) atTop (𝓝 0)

Tactic:
simp only [one_div]

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
⊢ Tendsto (fun i => (↑i)⁻¹) atTop (𝓝 0)

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
⊢ Tendsto (fun i => (↑i)⁻¹) atTop (𝓝 0)

Tactic:
exact ENNReal.tendsto_inv_nat_nhds_zero

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
⊢ Tendsto (fun n => ν (μ.sigmaFiniteSetGE ν n)) atTop
    (𝓝 (⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s))

Tactic:
refine tendsto_of_tendsto_of_tendsto_of_le_of_le ?_
  tendsto_const_nhds (measure_sigmaFiniteSetGE_ge μ ν) (measure_sigmaFiniteSetGE_le μ ν)

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
⊢ Tendsto (fun i => (⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) - 1 / ↑i) atTop
    (𝓝 (⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s))
-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf [IsTopologicalAddGroup E]
    (p : SeminormFamily 𝕜 E ι) :
    WithSeminorms p ↔
      t = ⨅ i, (p i).toSeminormedAddCommGroup.toUniformSpace.toTopologicalSpace

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ WithSeminorms p ↔ t = ⨅ i, UniformSpace.toTopologicalSpace

Tactic:
rw [p.withSeminorms_iff_nhds_eq_iInf,
  IsTopologicalAddGroup.ext_iff inferInstance (topologicalAddGroup_iInf fun i => inferInstance),
  nhds_iInf]

Result:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ 𝓝 0 = ⨅ i, comap (⇑(p i)) (𝓝 0) ↔ 𝓝 0 = ⨅ i, 𝓝 0

Proof state:
case a
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
i : ι
⊢ comap (⇑(p i)) (𝓝 0) = 𝓝 0

Tactic:
exact @comap_norm_nhds_zero _ (p i).toSeminormedAddGroup

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ 𝓝 0 = ⨅ i, comap (⇑(p i)) (𝓝 0) ↔ 𝓝 0 = ⨅ i, 𝓝 0

Tactic:
congrm _ = ⨅ i, ?_

Result:
case a
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
i : ι
⊢ comap (⇑(p i)) (𝓝 0) = 𝓝 0
-- Mathlib/RingTheory/ClassGroup.lean
theorem ClassGroup.mk_eq_mk {I J : (FractionalIdeal R⁰ <| FractionRing R)ˣ} :
    ClassGroup.mk I = ClassGroup.mk J ↔
      ∃ x : (FractionRing R)ˣ, I * toPrincipalIdeal R (FractionRing R) x = J

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I J : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ mk I = mk J ↔ ∃ x, I * (toPrincipalIdeal R (FractionRing R)) x = J

Tactic:
erw [QuotientGroup.mk'_eq_mk', canonicalEquiv_self, Units.map_id, Set.exists_range_iff]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I J : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ (∃ i,
      (MonoidHom.id (FractionalIdeal R⁰ (FractionRing R))ˣ) I * (toPrincipalIdeal R (FractionRing R)) i =
        (MonoidHom.id (FractionalIdeal R⁰ (FractionRing R))ˣ) J) ↔
    ∃ x, I * (toPrincipalIdeal R (FractionRing R)) x = J

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I J : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ (∃ i,
      (MonoidHom.id (FractionalIdeal R⁰ (FractionRing R))ˣ) I * (toPrincipalIdeal R (FractionRing R)) i =
        (MonoidHom.id (FractionalIdeal R⁰ (FractionRing R))ˣ) J) ↔
    ∃ x, I * (toPrincipalIdeal R (FractionRing R)) x = J

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Normed/Group/SeparationQuotient.lean
theorem norm_normedMk_eq_one (h : ∃ x : M, ‖x‖ ≠ 0) :
    ‖normedMk (M := M)‖ = 1

Proof state:
case h_above
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : ∃ x, ‖x‖ ≠ 0
⊢ ∀ (x : M), ‖normedMk x‖ ≤ 1 * ‖x‖

Tactic:
simpa only [normedMk_apply, one_mul] using fun _ ↦ le_rfl

Result:
no goals

Proof state:
case h_below
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : ∃ x, ‖x‖ ≠ 0
N : ℝ
a✝ : N ≥ 0
hle : ∀ (x : M), ‖normedMk x‖ ≤ N * ‖x‖
⊢ 1 ≤ N

Tactic:
obtain ⟨x, _⟩ := h

Result:
case h_below.intro
M : Type u_1
inst✝ : SeminormedAddCommGroup M
N : ℝ
a✝ : N ≥ 0
hle : ∀ (x : M), ‖normedMk x‖ ≤ N * ‖x‖
x : M
h✝ : ‖x‖ ≠ 0
⊢ 1 ≤ N

Proof state:
case h_below
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : ∃ x, ‖x‖ ≠ 0
⊢ ∀ N ≥ 0, (∀ (x : M), ‖normedMk x‖ ≤ N * ‖x‖) → 1 ≤ N

Tactic:
intro N _ hle

Result:
case h_below
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : ∃ x, ‖x‖ ≠ 0
N : ℝ
a✝ : N ≥ 0
hle : ∀ (x : M), ‖normedMk x‖ ≤ N * ‖x‖
⊢ 1 ≤ N

Proof state:
case h_below.intro
M : Type u_1
inst✝ : SeminormedAddCommGroup M
N : ℝ
a✝ : N ≥ 0
hle : ∀ (x : M), ‖normedMk x‖ ≤ N * ‖x‖
x : M
h✝ : ‖x‖ ≠ 0
⊢ 1 ≤ N

Tactic:
exact one_le_of_le_mul_right₀ (by positivity) (hle x)

Result:
no goals

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
N : ℝ
a✝ : N ≥ 0
hle : ∀ (x : M), ‖normedMk x‖ ≤ N * ‖x‖
x : M
h✝ : ‖x‖ ≠ 0
⊢ 0 < ‖normedMk x‖

Tactic:
positivity

Result:
no goals

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : ∃ x, ‖x‖ ≠ 0
⊢ ‖normedMk‖ = 1

Tactic:
apply NormedAddGroupHom.opNorm_eq_of_bounds _ zero_le_one

Result:
case h_above
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : ∃ x, ‖x‖ ≠ 0
⊢ ∀ (x : M), ‖normedMk x‖ ≤ 1 * ‖x‖

case h_below
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : ∃ x, ‖x‖ ≠ 0
⊢ ∀ N ≥ 0, (∀ (x : M), ‖normedMk x‖ ≤ N * ‖x‖) → 1 ≤ N
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Cooper.lean
theorem dvd_emod_add_of_dvd_add {a c d x : Int} (w : a ∣ x + c) (h : a ∣ d) : a ∣ (x % d) + c

Proof state:
a c d x : Int
w : a ∣ x + c
h : a ∣ d
⊢ a ∣ x % d + c

Tactic:
rw [← Int.one_mul x] at w

Result:
a c d x : Int
w : a ∣ 1 * x + c
h : a ∣ d
⊢ a ∣ x % d + c

Proof state:
a c d x : Int
w : a ∣ 1 * x + c
h : a ∣ d
⊢ a / ↑(a.gcd 1) ∣ d

Tactic:
simpa

Result:
no goals

Proof state:
a c d x : Int
w : a ∣ 1 * x + c
h : a ∣ d
⊢ a ∣ 1 * (x % d) + c

Tactic:
apply dvd_mul_emod_add_of_dvd_mul_add w (by simpa)

Result:
no goals

Proof state:
a c d x : Int
w : a ∣ 1 * x + c
h : a ∣ d
⊢ a ∣ x % d + c

Tactic:
rw [← Int.one_mul (x % d)]

Result:
a c d x : Int
w : a ∣ 1 * x + c
h : a ∣ d
⊢ a ∣ 1 * (x % d) + c
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem degree_one_le : degree (1 : R[X]) ≤ (0 : WithBot ℕ)

Proof state:
R : Type u
inst✝ : Semiring R
⊢ degree 1 ≤ 0

Tactic:
rw [← C_1]

Result:
R : Type u
inst✝ : Semiring R
⊢ (C 1).degree ≤ 0

Proof state:
R : Type u
inst✝ : Semiring R
⊢ (C 1).degree ≤ 0

Tactic:
exact degree_C_le

Result:
no goals
-- Mathlib/Algebra/Ring/Commute.lean
theorem mul_self_eq_mul_self_iff [NonUnitalNonAssocRing R] [NoZeroDivisors R] {a b : R}
    (h : Commute a b) : a * a = b * b ↔ a = b ∨ a = -b

Proof state:
R : Type u
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : NoZeroDivisors R
a b : R
h : Commute a b
⊢ a * a = b * b ↔ a = b ∨ a = -b

Tactic:
rw [← sub_eq_zero, h.mul_self_sub_mul_self_eq, mul_eq_zero, or_comm, sub_eq_zero,
  add_eq_zero_iff_eq_neg]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Roots.lean
theorem roots_cyclotomic_nodup [NeZero (n : R)] : (cyclotomic n R).roots.Nodup

Proof state:
case inr.intro
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
ζ : R
hζ : IsPrimitiveRoot ζ n
⊢ (cyclotomic n R).roots.Nodup

Tactic:
refine Multiset.nodup_of_le
  (roots.le_of_dvd (X_pow_sub_C_ne_zero (NeZero.pos_of_neZero_natCast R) 1) <|
    cyclotomic.dvd_X_pow_sub_one n R) hζ.nthRoots_one_nodup

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
⊢ (cyclotomic n R).roots.Nodup

Tactic:
obtain h | ⟨ζ, hζ⟩ := (cyclotomic n R).roots.empty_or_exists_mem

Result:
case inl
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
h : (cyclotomic n R).roots = 0
⊢ (cyclotomic n R).roots.Nodup

case inr.intro
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
ζ : R
hζ : ζ ∈ (cyclotomic n R).roots
⊢ (cyclotomic n R).roots.Nodup

Proof state:
case inl
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
h : (cyclotomic n R).roots = 0
⊢ (cyclotomic n R).roots.Nodup

Tactic:
exact h.symm ▸ Multiset.nodup_zero

Result:
no goals

Proof state:
case inr.intro
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
ζ : R
hζ : ζ ∈ (cyclotomic n R).roots
⊢ (cyclotomic n R).roots.Nodup

Tactic:
rw [mem_roots <| cyclotomic_ne_zero n R, isRoot_cyclotomic_iff] at hζ

Result:
case inr.intro
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
ζ : R
hζ : IsPrimitiveRoot ζ n
⊢ (cyclotomic n R).roots.Nodup
-- Mathlib/Data/QPF/Multivariate/Basic.lean
theorem mem_supp {α : TypeVec n} (x : F α) (i) (u : α i) :
    u ∈ supp x i ↔ ∀ a f, abs ⟨a, f⟩ = x → u ∈ f i '' univ

Proof state:
case mpr.intro.intro.intro
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
i : Fin2 n
u : α i
h : ∀ (a : (P F).A) (f : (P F).B a ⟹ α), abs ⟨a, f⟩ = x → u ∈ f i '' univ
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
xeq : x = abs ⟨a, f⟩
h' : ∀ (i : Fin2 n) (j : (P F).B a i), p i (f i j)
⊢ p i u

Tactic:
rcases h a f xeq.symm with ⟨i, _, hi⟩

Result:
case mpr.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
i✝ : Fin2 n
u : α i✝
h : ∀ (a : (P F).A) (f : (P F).B a ⟹ α), abs ⟨a, f⟩ = x → u ∈ f i✝ '' univ
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
xeq : x = abs ⟨a, f⟩
h' : ∀ (i : Fin2 n) (j : (P F).B a i), p i (f i j)
i : (P F).B a i✝
left✝ : i ∈ univ
hi : f i✝ i = u
⊢ p i✝ u

Proof state:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
i : Fin2 n
u : α i
⊢ u ∈ {y | ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i y} ↔
    ∀ (a : (P F).A) (f : (P F).B a ⟹ α), abs ⟨a, f⟩ = x → u ∈ f i '' univ

Tactic:
dsimp

Result:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
i : Fin2 n
u : α i
⊢ (∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u) ↔
    ∀ (a : (P F).A) (f : (P F).B a ⟹ α), abs ⟨a, f⟩ = x → u ∈ f i '' univ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Lemmas.lean
theorem monotone_bindM (f : γ → α → m (Option β)) (xs : Option α) (hmono : monotone f) :
    monotone (fun x => xs.bindM (f x))

Proof state:
case some.hmono₁
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → m (Option β)
hmono : monotone f
x : α
⊢ monotone fun x_1 => f x_1 x

Tactic:
apply monotone_apply

Result:
case some.hmono₁.h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → m (Option β)
hmono : monotone f
x : α
⊢ monotone f

Proof state:
case some.hmono₂
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → m (Option β)
hmono : monotone f
x : α
⊢ monotone fun x __do_lift => pure __do_lift

Tactic:
apply monotone_const

Result:
no goals

Proof state:
case some
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → m (Option β)
hmono : monotone f
x : α
⊢ monotone fun x_1 => Option.bindM (f x_1) (some x)

Tactic:
apply monotone_bind

Result:
case some.hmono₁
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → m (Option β)
hmono : monotone f
x : α
⊢ monotone fun x_1 => f x_1 x

case some.hmono₂
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → m (Option β)
hmono : monotone f
x : α
⊢ monotone fun x __do_lift => pure __do_lift

Proof state:
case none
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → m (Option β)
hmono : monotone f
⊢ monotone fun x => Option.bindM (f x) none

Tactic:
apply monotone_const

Result:
no goals

Proof state:
case some.hmono₁.h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → m (Option β)
hmono : monotone f
x : α
⊢ monotone f

Tactic:
apply hmono

Result:
no goals
-- Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
theorem associated_pow_irreducible {x : R} (hx : x ≠ 0) {ϖ : R} (hirr : Irreducible ϖ) :
    ∃ n : ℕ, Associated x (ϖ ^ n)

Proof state:
case h.e_a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x
H : Associates.mk fx.prod = Associates.mk x
x✝ : R
a✝ : x✝ ∈ fx
⊢ Associated x✝ ϖ

Tactic:
refine associated_of_irreducible _ ?_ hirr

Result:
case h.e_a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x
H : Associates.mk fx.prod = Associates.mk x
x✝ : R
a✝ : x✝ ∈ fx
⊢ Irreducible x✝

Proof state:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x
H : Associates.mk fx.prod = Associates.mk x
⊢ Associates.mk x = Associates.mk (ϖ ^ fx.card)

Tactic:
rw [← H, ← Associates.prod_mk, Associates.mk_pow, ← Multiset.prod_replicate]

Result:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hirr : Irreducible ϖ
this : WfDvdMonoid R
fx : Multiset R
hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x
H : Associates.mk fx.prod = Associates.mk x
⊢ (Multiset.map Associates.mk fx).prod = (Multiset.replicate fx.card (Associates.mk ϖ)).prod
-- Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean
theorem Fix.ind {α : TypeVec n} (p : Fix F α → Prop)
    (h : ∀ x : F (α.append1 (Fix F α)), LiftP (PredLast α p) x → p (Fix.mk x)) : ∀ x, p x

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (α.PredLast p) x → p (mk x)
x : (P F).W α
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), p (Quot.mk (⇑(wSetoid α)) (f i))
⊢ p (mk (abs ⟨a, (P F).appendContents f' fun x => ⟦f x⟧⟩))

Tactic:
apply h

Result:
case a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (α.PredLast p) x → p (mk x)
x : (P F).W α
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), p (Quot.mk (⇑(wSetoid α)) (f i))
⊢ LiftP (α.PredLast p) (abs ⟨a, (P F).appendContents f' fun x => ⟦f x⟧⟩)

Proof state:
case a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (α.PredLast p) x → p (mk x)
x : (P F).W α
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), p (Quot.mk (⇑(wSetoid α)) (f i))
i : Fin2 (n + 1)
j : (P F).B a i
⊢ α.PredLast p ((P F).appendContents f' (fun x => ⟦f x⟧) i j)

Tactic:
cases i

Result:
case a.fz
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (α.PredLast p) x → p (mk x)
x : (P F).W α
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), p (Quot.mk (⇑(wSetoid α)) (f i))
j : (P F).B a Fin2.fz
⊢ α.PredLast p ((P F).appendContents f' (fun x => ⟦f x⟧) Fin2.fz j)

case a.fs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (α.PredLast p) x → p (mk x)
x : (P F).W α
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), p (Quot.mk (⇑(wSetoid α)) (f i))
a✝ : Fin2 n
j : (P F).B a a✝.fs
⊢ α.PredLast p ((P F).appendContents f' (fun x => ⟦f x⟧) a✝.fs j)
-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean
theorem self (a : α) : variationOnFromTo f s a a = 0

Proof state:
case hs
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a : α
⊢ (s ∩ {a}).Subsingleton

Tactic:
exact fun x hx y hy => hx.2.trans hy.2.symm

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a : α
⊢ (if a ≤ a then (eVariationOn f (s ∩ Icc a a)).toReal else -(eVariationOn f (s ∩ Icc a a)).toReal) = 0

Tactic:
rw [if_pos le_rfl, Icc_self, eVariationOn.subsingleton, ENNReal.zero_toReal]

Result:
case hs
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a : α
⊢ (s ∩ {a}).Subsingleton

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a : α
⊢ variationOnFromTo f s a a = 0

Tactic:
dsimp only [variationOnFromTo]

Result:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a : α
⊢ (if a ≤ a then (eVariationOn f (s ∩ Icc a a)).toReal else -(eVariationOn f (s ∩ Icc a a)).toReal) = 0
-- Mathlib/Data/ZMod/Basic.lean
lemma ringEquivCongr_refl_apply {a : ℕ} (x : ZMod a) : ringEquivCongr rfl x = x

Proof state:
a : ℕ
x : ZMod a
⊢ (ringEquivCongr ⋯) x = x

Tactic:
rw [ringEquivCongr_refl]

Result:
a : ℕ
x : ZMod a
⊢ (RingEquiv.refl (ZMod a)) x = x

Proof state:
a : ℕ
x : ZMod a
⊢ (RingEquiv.refl (ZMod a)) x = x

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/DirectSum/Module.lean
theorem isInternal_ne_bot_iff {A : ι → Submodule R M} :
    IsInternal (fun i : {i // A i ≠ ⊥} ↦ A i) ↔ IsInternal A

Proof state:
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
⊢ (IsInternal fun i => A ↑i) ↔ IsInternal A

Tactic:
simp [isInternal_submodule_iff_iSupIndep_and_iSup_eq_top]

Result:
no goals
-- Mathlib/Algebra/Homology/TotalComplex.lean
@[reassoc (attr := simp)]
lemma ι_totalDesc (i₁ : I₁) (i₂ : I₂) (hi : ComplexShape.π c₁ c₂ c₁₂ (i₁, i₂) = i₁₂) :
    K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ K.totalDesc f = f i₁ i₂ hi

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
A : C
i₁₂ : I₁₂
f : (i₁ : I₁) → (i₂ : I₂) → c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂ → ((K.X i₁).X i₂ ⟶ A)
i₁ : I₁
i₂ : I₂
hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
⊢ K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ K.totalDesc f = f i₁ i₂ hi

Tactic:
simp [totalDesc, ιTotal]

Result:
no goals
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem basisDivisor_self : basisDivisor x x = 0

Proof state:
F : Type u_1
inst✝ : Field F
x : F
⊢ basisDivisor x x = 0

Tactic:
simp only [basisDivisor, sub_self, inv_zero, map_zero, zero_mul]

Result:
no goals
-- Mathlib/NumberTheory/Harmonic/GammaDeriv.lean
lemma differentiable_at_Gamma_nat_add_one (n : ℕ) :
    DifferentiableAt ℂ Gamma (n + 1)

Proof state:
n m : ℕ
⊢ ↑n + 1 ≠ -↑m

Tactic:
simp only [Ne, ← ofReal_natCast, ← ofReal_one, ← ofReal_add, ← ofReal_neg, ofReal_inj,
  eq_neg_iff_add_eq_zero]

Result:
n m : ℕ
⊢ ¬↑n + 1 + ↑m = 0

Proof state:
n : ℕ
⊢ DifferentiableAt ℂ Gamma (↑n + 1)

Tactic:
refine differentiableAt_Gamma _ (fun m ↦ ?_)

Result:
n m : ℕ
⊢ ↑n + 1 ≠ -↑m

Proof state:
n m : ℕ
⊢ ¬↑n + 1 + ↑m = 0

Tactic:
positivity

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Midpoint.lean
theorem Equiv.pointReflection_midpoint_left (x y : P) :
    (Equiv.pointReflection (midpoint R x y)) x = y

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ (pointReflection (midpoint R x y)) x = y

Tactic:
rw [midpoint, pointReflection_apply, lineMap_apply, vadd_vsub, vadd_vadd, ← add_smul, ← two_mul,
  mul_invOf_self, one_smul, vsub_vadd]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem findRev?_eq_find?_reverse (f : α → Bool) (as : Vector α n) :
    findRev? f as = find? f as.reverse

Proof state:
α : Type
n : Nat
f : α → Bool
as : Vector α n
⊢ findRev? f as = find? f as.reverse

Tactic:
simp [findRev?, find?]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval₂_eq_eval_map {x : S} : p.eval₂ f x = (p.map f).eval x

Proof state:
case h_monomial
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
n : ℕ
r : R
⊢ eval₂ f x ((monomial n) r) = eval x (map f ((monomial n) r))

Tactic:
simp

Result:
no goals

Proof state:
case h_add
R : Type u
S : Type v
inst✝¹ : Semiring R
p✝ : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
p q : R[X]
hp : eval₂ f x p = eval x (map f p)
hq : eval₂ f x q = eval x (map f q)
⊢ eval₂ f x (p + q) = eval x (map f (p + q))

Tactic:
simp [hp, hq]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x p = eval x (map f p)

Tactic:
induction p using Polynomial.induction_on' with
| h_add p q hp hq =>
  simp [hp, hq]
| h_monomial n r =>
  simp

Result:
no goals
-- Mathlib/GroupTheory/Index.lean
theorem mul_self_mem_of_index_two (h : H.index = 2) (a : G) : a * a ∈ H

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a : G
⊢ a * a ∈ H

Tactic:
rw [mul_mem_iff_of_index_two h]

Result:
no goals