harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/QuadraticDiscriminant.lean
theorem discrim_eq_zero_of_existsUnique (ha : a ≠ 0) (h : ∃! x, a * (x * x) + b * x + c = 0) :
    discrim a b c = 0

Proof state:
case intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
x : K
hx : -b + -(x * a) = x * a
⊢ (2 * a * x + b) ^ 2 = 0

Tactic:
linear_combination -(2 * a * x + b) * hx

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
h : ∃! x, discrim a b c = (2 * a * x + b) ^ 2
⊢ discrim a b c = 0

Tactic:
generalize discrim a b c = d at h

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
d : K
h : ∃! x, d = (2 * a * x + b) ^ 2
⊢ d = 0

Proof state:
case intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
x : K
hx : ∀ (y : K), (fun x_1 => (2 * a * x + b) ^ 2 = (2 * a * x_1 + b) ^ 2) y → y = x
⊢ (2 * a * x + b) ^ 2 = 0

Tactic:
specialize hx (-(x + b / a))

Result:
case intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
x : K
hx : (fun x_1 => (2 * a * x + b) ^ 2 = (2 * a * x_1 + b) ^ 2) (-(x + b / a)) → -(x + b / a) = x
⊢ (2 * a * x + b) ^ 2 = 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
x : K
hx : (2 * a * x + b) ^ 2 * a ^ 2 = (2 * a * (-b + -(x * a)) + b * a) ^ 2 → -b + -(x * a) = x * a
⊢ (2 * a * x + b) ^ 2 * a ^ 2 = (2 * a * (-b + -(x * a)) + b * a) ^ 2

Tactic:
ring

Result:
no goals

Proof state:
case intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
x : K
hx : (2 * a * x + b) ^ 2 * a ^ 2 = (2 * a * (-b + -(x * a)) + b * a) ^ 2 → -b + -(x * a) = x * a
⊢ (2 * a * x + b) ^ 2 = 0

Tactic:
specialize hx (by ring)

Result:
case intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
x : K
hx : -b + -(x * a) = x * a
⊢ (2 * a * x + b) ^ 2 = 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
d : K
h : ∃! x, d = (2 * a * x + b) ^ 2
⊢ d = 0

Tactic:
obtain ⟨x, rfl, hx⟩ := h

Result:
case intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
x : K
hx : ∀ (y : K), (fun x_1 => (2 * a * x + b) ^ 2 = (2 * a * x_1 + b) ^ 2) y → y = x
⊢ (2 * a * x + b) ^ 2 = 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
h : ∃! x, a * (x * x) + b * x + c = 0
⊢ discrim a b c = 0

Tactic:
simp_rw [quadratic_eq_zero_iff_discrim_eq_sq ha] at h

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
h : ∃! x, discrim a b c = (2 * a * x + b) ^ 2
⊢ discrim a b c = 0

Proof state:
case intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
x : K
hx : (fun x_1 => (2 * a * x + b) ^ 2 = (2 * a * x_1 + b) ^ 2) (-(x + b / a)) → -(x + b / a) = x
⊢ (2 * a * x + b) ^ 2 = 0

Tactic:
field_simp [ha] at hx

Result:
case intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
x : K
hx : (2 * a * x + b) ^ 2 * a ^ 2 = (2 * a * (-b + -(x * a)) + b * a) ^ 2 → -b + -(x * a) = x * a
⊢ (2 * a * x + b) ^ 2 = 0
-- Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
theorem HasFiniteIntegral.mono {f : α → β} {g : α → γ} (hg : HasFiniteIntegral g μ)
    (h : ∀ᵐ a ∂μ, ‖f a‖ ≤ ‖g a‖) : HasFiniteIntegral f μ

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
g : α → γ
hg : HasFiniteIntegral g μ
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ ‖g a‖
⊢ HasFiniteIntegral f μ

Tactic:
simp only [hasFiniteIntegral_iff_norm] at *

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
g : α → γ
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ ‖g a‖
hg : ∫⁻ (a : α), ENNReal.ofReal ‖g a‖ ∂μ < ⊤
⊢ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ < ⊤

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
g : α → γ
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ ‖g a‖
hg : ∫⁻ (a : α), ENNReal.ofReal ‖g a‖ ∂μ < ⊤
⊢ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ < ⊤

Tactic:
calc
  (∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ) ≤ ∫⁻ a : α, ENNReal.ofReal ‖g a‖ ∂μ :=
    lintegral_mono_ae (h.mono fun a h => ofReal_le_ofReal h)
  _ < ∞ := hg

Result:
no goals
-- Mathlib/Algebra/Group/Semiconj/Defs.lean
theorem mul_right (h : SemiconjBy a x y) (h' : SemiconjBy a x' y') :
    SemiconjBy a (x * x') (y * y')

Proof state:
S : Type u_1
inst✝ : Semigroup S
a x y x' y' : S
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ a * (x * x') = y * y' * a

Tactic:
rw [← mul_assoc, h.eq, mul_assoc, h'.eq, ← mul_assoc]

Result:
no goals

Proof state:
S : Type u_1
inst✝ : Semigroup S
a x y x' y' : S
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x * x') (y * y')

Tactic:
unfold SemiconjBy

Result:
S : Type u_1
inst✝ : Semigroup S
a x y x' y' : S
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ a * (x * x') = y * y' * a
-- Mathlib/NumberTheory/Divisors.lean
lemma divisorsAntidiag_neg :
    (-z).divisorsAntidiag =
      z.divisorsAntidiag.map (.prodMap (.refl _) (Equiv.neg _).toEmbedding)

Proof state:
z : ℤ
⊢ (-z).divisorsAntidiag = map ((Function.Embedding.refl ℤ).prodMap (Equiv.toEmbedding (Equiv.neg ℤ))) z.divisorsAntidiag

Tactic:
ext

Result:
case h
z : ℤ
a✝ : ℤ × ℤ
⊢ a✝ ∈ (-z).divisorsAntidiag ↔
    a✝ ∈ map ((Function.Embedding.refl ℤ).prodMap (Equiv.toEmbedding (Equiv.neg ℤ))) z.divisorsAntidiag

Proof state:
case h
z : ℤ
a✝ : ℤ × ℤ
⊢ a✝ ∈ (-z).divisorsAntidiag ↔
    a✝ ∈ map ((Function.Embedding.refl ℤ).prodMap (Equiv.toEmbedding (Equiv.neg ℤ))) z.divisorsAntidiag

Tactic:
simp [mem_divisorsAntidiag, Prod.ext_iff, neg_eq_iff_eq_neg]

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Basic.lean
lemma span_range_inclusionSpan :
    span S (range <| p.inclusionSpan S) = ⊤

Proof state:
case h
R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
x✝ : M
⊢ x✝ ∈ ⇑(span S ↑p).subtype '' range ⇑(inclusionSpan S p) ↔ x✝ ∈ ↑p

Tactic:
simpa [Subtype.ext_iff] using fun h ↦ subset_span h

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
⊢ ⇑(span S ↑p).subtype '' range ⇑(inclusionSpan S p) = ↑p

Tactic:
ext

Result:
case h
R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
x✝ : M
⊢ x✝ ∈ ⇑(span S ↑p).subtype '' range ⇑(inclusionSpan S p) ↔ x✝ ∈ ↑p

Proof state:
case a
R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
this : ⇑(span S ↑p).subtype '' range ⇑(inclusionSpan S p) = ↑p
⊢ map (span S ↑p).subtype (span S (range ⇑(inclusionSpan S p))) = map (span S ↑p).subtype ⊤

Tactic:
rw [map_subtype_top, map_span, this]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
⊢ span S (range ⇑(inclusionSpan S p)) = ⊤

Tactic:
have : (span S (p : Set M)).subtype '' range (inclusionSpan S p) = p := by
  ext; simpa [Subtype.ext_iff] using fun h ↦ subset_span h

Result:
R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
this : ⇑(span S ↑p).subtype '' range ⇑(inclusionSpan S p) = ↑p
⊢ span S (range ⇑(inclusionSpan S p)) = ⊤

Proof state:
R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
this : ⇑(span S ↑p).subtype '' range ⇑(inclusionSpan S p) = ↑p
⊢ span S (range ⇑(inclusionSpan S p)) = ⊤

Tactic:
apply map_injective_of_injective (span S (p : Set M)).injective_subtype

Result:
case a
R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
this : ⇑(span S ↑p).subtype '' range ⇑(inclusionSpan S p) = ↑p
⊢ map (span S ↑p).subtype (span S (range ⇑(inclusionSpan S p))) = map (span S ↑p).subtype ⊤
-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
theorem cbiSup_eq_of_not_forall {p : ι → Prop} {f : Subtype p → α} (hp : ¬ (∀ i, p i)) :
    ⨆ (i) (h : p i), f ⟨i, h⟩ = iSup f ⊔ sSup ∅

Proof state:
case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
i₀ : ι
hi₀ : ¬p i₀
this✝ : Nonempty ι
H : ¬BddAbove (range f)
this : iSup f = sSup ∅
⊢ (⨆ i, if h : p i then f ⟨i, h⟩ else sSup ∅) = sSup ∅

Tactic:
apply csSup_of_not_bddAbove

Result:
case neg.hs
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
i₀ : ι
hi₀ : ¬p i₀
this✝ : Nonempty ι
H : ¬BddAbove (range f)
this : iSup f = sSup ∅
⊢ ¬BddAbove (range fun i => if h : p i then f ⟨i, h⟩ else sSup ∅)
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem integral_bilinear_hasDerivAt_right_eq_neg_left_of_integrable
    (hu : ∀ x, HasDerivAt u (u' x) x) (hv : ∀ x, HasDerivAt v (v' x) x)
    (huv' : Integrable (fun x ↦ L (u x) (v' x))) (hu'v : Integrable (fun x ↦ L (u' x) (v x)))
    (huv : Integrable (fun x ↦ L (u x) (v x))) :
    ∫ (x : ℝ), L (u x) (v' x) = - ∫ (x : ℝ), L (u' x) (v x)

Proof state:
case pos
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
L : E →L[ℝ] F →L[ℝ] G
u : ℝ → E
v : ℝ → F
u' : ℝ → E
v' : ℝ → F
hu : ∀ (x : ℝ), HasDerivAt u (u' x) x
hv : ∀ (x : ℝ), HasDerivAt v (v' x) x
huv' : Integrable (fun x => (L (u x)) (v' x)) volume
hu'v : Integrable (fun x => (L (u' x)) (v x)) volume
huv : Integrable (fun x => (L (u x)) (v x)) volume
hG : CompleteSpace G
I : Tendsto (fun x => (L (u x)) (v x)) atBot (𝓝 0)
⊢ ∫ (x : ℝ), (L (u x)) (v' x) = -∫ (x : ℝ), (L (u' x)) (v x)

Tactic:
have J : Tendsto (fun x ↦ L (u x) (v x)) atTop (𝓝 0) :=
  tendsto_zero_of_hasDerivAt_of_integrableOn_Ioi (a := 0)
    (fun x _hx ↦ L.hasDerivAt_of_bilinear (hu x) (hv x))
    (huv'.add hu'v).integrableOn huv.integrableOn

Result:
case pos
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
L : E →L[ℝ] F →L[ℝ] G
u : ℝ → E
v : ℝ → F
u' : ℝ → E
v' : ℝ → F
hu : ∀ (x : ℝ), HasDerivAt u (u' x) x
hv : ∀ (x : ℝ), HasDerivAt v (v' x) x
huv' : Integrable (fun x => (L (u x)) (v' x)) volume
hu'v : Integrable (fun x => (L (u' x)) (v x)) volume
huv : Integrable (fun x => (L (u x)) (v x)) volume
hG : CompleteSpace G
I : Tendsto (fun x => (L (u x)) (v x)) atBot (𝓝 0)
J : Tendsto (fun x => (L (u x)) (v x)) atTop (𝓝 0)
⊢ ∫ (x : ℝ), (L (u x)) (v' x) = -∫ (x : ℝ), (L (u' x)) (v x)
-- Mathlib/RingTheory/OreLocalization/OreSet.lean
lemma nonempty_oreSet_iff_of_noZeroDivisors {R : Type*} [Ring R] [NoZeroDivisors R]
    {S : Submonoid R} :
    Nonempty (OreSet S) ↔ ∀ (r : R) (s : S), ∃ (r' : R) (s' : S), s' * r = r' * s

Proof state:
case mpr
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
S : Submonoid R
⊢ (∀ (r : R) (s : ↥S), ∃ r' s', ↑s' * r = r' * ↑s) → Nonempty (OreSet S)

Tactic:
intro H

Result:
case mpr
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
S : Submonoid R
H : ∀ (r : R) (s : ↥S), ∃ r' s', ↑s' * r = r' * ↑s
⊢ Nonempty (OreSet S)

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
S : Submonoid R
⊢ Nonempty (OreSet S) ↔ ∀ (r : R) (s : ↥S), ∃ r' s', ↑s' * r = r' * ↑s

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
S : Submonoid R
⊢ Nonempty (OreSet S) → ∀ (r : R) (s : ↥S), ∃ r' s', ↑s' * r = r' * ↑s

case mpr
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
S : Submonoid R
⊢ (∀ (r : R) (s : ↥S), ∃ r' s', ↑s' * r = r' * ↑s) → Nonempty (OreSet S)

Proof state:
case mpr
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
S : Submonoid R
r' : R → ↥S → R
s' : R → ↥S → ↥S
h : ∀ (r : R) (s : ↥S), ↑(s' r s) * r = r' r s * ↑s
⊢ Nonempty (OreSet S)

Tactic:
exact ⟨oreSetOfNoZeroDivisors r' s' h⟩

Result:
no goals

Proof state:
case mpr
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
S : Submonoid R
H : ∀ (r : R) (s : ↥S), ∃ r' s', ↑s' * r = r' * ↑s
⊢ Nonempty (OreSet S)

Tactic:
choose r' s' h using H

Result:
case mpr
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
S : Submonoid R
r' : R → ↥S → R
s' : R → ↥S → ↥S
h : ∀ (r : R) (s : ↥S), ↑(s' r s) * r = r' r s * ↑s
⊢ Nonempty (OreSet S)

Proof state:
case mp
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
S : Submonoid R
⊢ Nonempty (OreSet S) → ∀ (r : R) (s : ↥S), ∃ r' s', ↑s' * r = r' * ↑s

Tactic:
exact fun ⟨_⟩ ↦ fun r s ↦ ⟨oreNum r s, oreDenom r s, ore_eq r s⟩

Result:
no goals
-- Mathlib/AlgebraicGeometry/Sites/Etale.lean
lemma zariskiTopology_le_etaleTopology : zariskiTopology ≤ etaleTopology

Proof state:
⊢ zariskiTopology ≤ etaleTopology

Tactic:
apply grothendieckTopology_le_grothendieckTopology

Result:
case hPQ

⊢ @IsOpenImmersion ≤ @IsEtale

Proof state:
case hPQ

⊢ @IsOpenImmersion ≤ @IsEtale

Tactic:
intro X Y f hf

Result:
case hPQ
X Y : Scheme
f : X ⟶ Y
hf : IsOpenImmersion f
⊢ IsEtale f

Proof state:
case hPQ
X Y : Scheme
f : X ⟶ Y
hf : IsOpenImmersion f
⊢ IsEtale f

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem apply_swap_eq_self {v : α → β} {i j : α} (hv : v i = v j) (k : α) :
    v (swap i j k) = v k

Proof state:
case pos
α : Sort u_1
β : Sort u_4
inst✝ : DecidableEq α
v : α → β
i j : α
hv : v i = v j
k : α
hi : k = i
⊢ v ((swap i j) k) = v k

Tactic:
rw [hi, swap_apply_left, hv]

Result:
no goals

Proof state:
case neg
α : Sort u_1
β : Sort u_4
inst✝ : DecidableEq α
v : α → β
i j : α
hv : v i = v j
k : α
hi : ¬k = i
⊢ v ((swap i j) k) = v k

Tactic:
by_cases hj : k = j

Result:
case pos
α : Sort u_1
β : Sort u_4
inst✝ : DecidableEq α
v : α → β
i j : α
hv : v i = v j
k : α
hi : ¬k = i
hj : k = j
⊢ v ((swap i j) k) = v k

case neg
α : Sort u_1
β : Sort u_4
inst✝ : DecidableEq α
v : α → β
i j : α
hv : v i = v j
k : α
hi : ¬k = i
hj : ¬k = j
⊢ v ((swap i j) k) = v k

Proof state:
case pos
α : Sort u_1
β : Sort u_4
inst✝ : DecidableEq α
v : α → β
i j : α
hv : v i = v j
k : α
hi : ¬k = i
hj : k = j
⊢ v ((swap i j) k) = v k

Tactic:
rw [hj, swap_apply_right, hv]

Result:
no goals

Proof state:
α : Sort u_1
β : Sort u_4
inst✝ : DecidableEq α
v : α → β
i j : α
hv : v i = v j
k : α
⊢ v ((swap i j) k) = v k

Tactic:
by_cases hi : k = i

Result:
case pos
α : Sort u_1
β : Sort u_4
inst✝ : DecidableEq α
v : α → β
i j : α
hv : v i = v j
k : α
hi : k = i
⊢ v ((swap i j) k) = v k

case neg
α : Sort u_1
β : Sort u_4
inst✝ : DecidableEq α
v : α → β
i j : α
hv : v i = v j
k : α
hi : ¬k = i
⊢ v ((swap i j) k) = v k

Proof state:
case neg
α : Sort u_1
β : Sort u_4
inst✝ : DecidableEq α
v : α → β
i j : α
hv : v i = v j
k : α
hi : ¬k = i
hj : ¬k = j
⊢ v ((swap i j) k) = v k

Tactic:
rw [swap_apply_of_ne_of_ne hi hj]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem tendsto_measure_iUnion_accumulate {α ι : Type*}
    [Preorder ι] [IsCountablyGenerated (atTop : Filter ι)]
    {_ : MeasurableSpace α} {μ : Measure α} {f : ι → Set α} :
    Tendsto (fun i ↦ μ (Accumulate f i)) atTop (𝓝 (μ (⋃ i, f i)))

Proof state:
α : Type u_8
ι : Type u_9
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
x✝ : MeasurableSpace α
μ : Measure α
f : ι → Set α
h : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
⊢ Tendsto (fun i => μ (Accumulate f i)) atTop (𝓝 (⨆ i, μ (Accumulate f i)))

Tactic:
exact tendsto_atTop_iSup fun i j hij ↦ by gcongr

Result:
no goals

Proof state:
α : Type u_8
ι : Type u_9
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
x✝ : MeasurableSpace α
μ : Measure α
f : ι → Set α
h : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
i j : ι
hij : i ≤ j
⊢ μ (Accumulate f i) ≤ μ (Accumulate f j)

Tactic:
gcongr

Result:
no goals

Proof state:
α : Type u_8
ι : Type u_9
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
x✝ : MeasurableSpace α
μ : Measure α
f : ι → Set α
⊢ Tendsto (fun i => μ (Accumulate f i)) atTop (𝓝 (μ (⋃ i, f i)))

Tactic:
refine .of_neBot_imp fun h ↦ ?_

Result:
α : Type u_8
ι : Type u_9
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
x✝ : MeasurableSpace α
μ : Measure α
f : ι → Set α
h : atTop.NeBot
⊢ Tendsto (fun i => μ (Accumulate f i)) atTop (𝓝 (μ (⋃ i, f i)))

Proof state:
α : Type u_8
ι : Type u_9
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
x✝ : MeasurableSpace α
μ : Measure α
f : ι → Set α
h : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
⊢ Tendsto (fun i => μ (Accumulate f i)) atTop (𝓝 (μ (⋃ i, f i)))

Tactic:
rw [measure_iUnion_eq_iSup_accumulate]

Result:
α : Type u_8
ι : Type u_9
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
x✝ : MeasurableSpace α
μ : Measure α
f : ι → Set α
h : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
⊢ Tendsto (fun i => μ (Accumulate f i)) atTop (𝓝 (⨆ i, μ (Accumulate f i)))

Proof state:
α : Type u_8
ι : Type u_9
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
x✝ : MeasurableSpace α
μ : Measure α
f : ι → Set α
h : atTop.NeBot
⊢ Tendsto (fun i => μ (Accumulate f i)) atTop (𝓝 (μ (⋃ i, f i)))

Tactic:
have := (atTop_neBot_iff.1 h).2

Result:
α : Type u_8
ι : Type u_9
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
x✝ : MeasurableSpace α
μ : Measure α
f : ι → Set α
h : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
⊢ Tendsto (fun i => μ (Accumulate f i)) atTop (𝓝 (μ (⋃ i, f i)))
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem derivFamily_lt_ord_lift {ι : Type u} {f : ι → Ordinal → Ordinal} {c} (hc : IsRegular c)
    (hι : lift.{v} #ι < c) (hc' : c ≠ ℵ₀) (hf : ∀ i, ∀ b < c.ord, f i b < c.ord) {a} :
    a < c.ord → derivFamily f a < c.ord

Proof state:
case H₃
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : b.IsLimit
H : ∀ o' < b, o' < c.ord → derivFamily f o' < c.ord
hb' : b < c.ord
⊢ derivFamily f b < c.ord

Tactic:
have : ⨆ a : Iio b, _ = _ :=
  iSup_eq_bsup.{max u v, max u v} (f := fun x (_ : x < b) ↦ derivFamily f x)

Result:
case H₃
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : b.IsLimit
H : ∀ o' < b, o' < c.ord → derivFamily f o' < c.ord
hb' : b < c.ord
this : ⨆ a, derivFamily f ↑a = b.bsup fun x x_1 => derivFamily f x
⊢ derivFamily f b < c.ord

Proof state:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : b < c.ord → derivFamily f b < c.ord
hb' : succ b < c.ord
⊢ lift.{?u.136967, u} #ι < c.ord.cof

Tactic:
rwa [hc.cof_eq]

Result:
no goals
-- Mathlib/RingTheory/FiniteType.lean
theorem finiteType_iff_fg [CommRing R] [Nontrivial R] :
    FiniteType R R[M] ↔ AddMonoid.FG M

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝² : AddMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R R[M]
S : Finset M
hS : adjoin R (of' R M '' ↑S) = ⊤
⊢ AddMonoid.FG M

Tactic:
refine AddMonoid.fg_def.2 ⟨S, (eq_top_iff' _).2 fun m => ?_⟩

Result:
case intro
R : Type u_1
M : Type u_2
inst✝² : AddMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R R[M]
S : Finset M
hS : adjoin R (of' R M '' ↑S) = ⊤
m : M
⊢ m ∈ closure ↑S

Proof state:
R : Type u_1
M : Type u_2
inst✝² : AddMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R R[M]
⊢ AddMonoid.FG M

Tactic:
obtain ⟨S, hS⟩ := @exists_finset_adjoin_eq_top R M _ _ h

Result:
case intro
R : Type u_1
M : Type u_2
inst✝² : AddMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R R[M]
S : Finset M
hS : adjoin R (of' R M '' ↑S) = ⊤
⊢ AddMonoid.FG M

Proof state:
R : Type u_1
M : Type u_2
inst✝² : AddMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ FiniteType R R[M] ↔ AddMonoid.FG M

Tactic:
refine ⟨fun h => ?_, fun h => @AddMonoidAlgebra.finiteType_of_fg _ _ _ _ h⟩

Result:
R : Type u_1
M : Type u_2
inst✝² : AddMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R R[M]
⊢ AddMonoid.FG M

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝² : AddMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R R[M]
S : Finset M
hS : adjoin R (of' R M '' ↑S) = ⊤
m : M
⊢ m ∈ closure ↑S

Tactic:
have hm : of' R M m ∈ Subalgebra.toSubmodule (adjoin R (of' R M '' ↑S)) := by
  simp only [hS, top_toSubmodule, Submodule.mem_top]

Result:
case intro
R : Type u_1
M : Type u_2
inst✝² : AddMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R R[M]
S : Finset M
hS : adjoin R (of' R M '' ↑S) = ⊤
m : M
hm : of' R M m ∈ Subalgebra.toSubmodule (adjoin R (of' R M '' ↑S))
⊢ m ∈ closure ↑S

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝² : AddMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R R[M]
S : Finset M
hS : adjoin R (of' R M '' ↑S) = ⊤
m : M
hm : of' R M m ∈ span R ↑(Submonoid.closure (of' R M '' ↑S))
⊢ m ∈ closure ↑S

Tactic:
exact mem_closure_of_mem_span_closure hm

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : AddMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R R[M]
S : Finset M
hS : adjoin R (of' R M '' ↑S) = ⊤
m : M
⊢ of' R M m ∈ Subalgebra.toSubmodule (adjoin R (of' R M '' ↑S))

Tactic:
simp only [hS, top_toSubmodule, Submodule.mem_top]

Result:
no goals

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝² : AddMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R R[M]
S : Finset M
hS : adjoin R (of' R M '' ↑S) = ⊤
m : M
hm : of' R M m ∈ Subalgebra.toSubmodule (adjoin R (of' R M '' ↑S))
⊢ m ∈ closure ↑S

Tactic:
rw [adjoin_eq_span] at hm

Result:
case intro
R : Type u_1
M : Type u_2
inst✝² : AddMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R R[M]
S : Finset M
hS : adjoin R (of' R M '' ↑S) = ⊤
m : M
hm : of' R M m ∈ span R ↑(Submonoid.closure (of' R M '' ↑S))
⊢ m ∈ closure ↑S