harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean
lemma top_mem_range (A₀ : Subobject X) {J : Type w} [LinearOrder J] [OrderBot J] [SuccOrder J]
    [WellFoundedLT J] (hJ : HasCardinalLT (Subobject X) (Cardinal.mk J)) :
    ∃ (j : J), transfiniteIterate (largerSubobject hG) j A₀ = ⊤ :=
  top_mem_range_transfiniteIterate (largerSubobject hG) A₀ (lt_largerSubobject hG) (by simp)
    (fun h ↦ by simpa [hasCardinalLT_iff_cardinal_mk_lt] using hJ.of_injective _ h)

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
G : C
inst✝⁵ : Abelian C
hG : IsSeparator G
X : C
inst✝⁴ : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject X
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hJ : HasCardinalLT (Subobject X) (Cardinal.mk J)
⊢ largerSubobject hG ⊤ = ⊤

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
G : C
inst✝⁵ : Abelian C
hG : IsSeparator G
X : C
inst✝⁴ : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject X
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hJ : HasCardinalLT (Subobject X) (Cardinal.mk J)
h : Function.Injective fun j => transfiniteIterate (largerSubobject hG) j A₀
⊢ False

Tactic:
simpa [hasCardinalLT_iff_cardinal_mk_lt] using hJ.of_injective _ h

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean
lemma measurableSet_succ_memPartition (t : ℕ → Set α) (n : ℕ) {s : Set α}
    (hs : s ∈ memPartition t n) :
    MeasurableSet[generateFrom (memPartition t (n + 1))] s

Proof state:
case refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ s ∩ t n ∈ memPartition t (n + 1)

Tactic:
rw [memPartition_succ]

Result:
case refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ s ∩ t n ∈ {s | ∃ u ∈ memPartition t n, s = u ∩ t n ∨ s = u \ t n}

Proof state:
case refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ MeasurableSet (s ∩ t n)

Tactic:
refine measurableSet_generateFrom ?_

Result:
case refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ s ∩ t n ∈ memPartition t (n + 1)

Proof state:
case refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ s ∩ t n ∈ {s | ∃ u ∈ memPartition t n, s = u ∩ t n ∨ s = u \ t n}

Tactic:
exact ⟨s, hs, by simp⟩

Result:
no goals

Proof state:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ s ∩ t n = s ∩ t n ∨ s ∩ t n = s \ t n

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ MeasurableSet s

Tactic:
rw [← diff_union_inter s (t n)]

Result:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ MeasurableSet (s \ t n ∪ s ∩ t n)
-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
lemma coverMincard_finite_iff (T : X → X) (F : Set X) (U : Set (X × X)) (n : ℕ) :
    coverMincard T F U n < ⊤ ↔
    ∃ s : Finset X, IsDynCoverOf T F U n s ∧ s.card = coverMincard T F U n

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
⊢ coverMincard T F U n < ⊤ ↔ ∃ s, IsDynCoverOf T F U n ↑s ∧ ↑s.card = coverMincard T F U n

Tactic:
refine ⟨fun h_fin ↦ ?_, (fun ⟨s, _, s_coverMincard⟩ ↦ s_coverMincard ▸ WithTop.coe_lt_top s.card)⟩

Result:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
h_fin : coverMincard T F U n < ⊤
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ ↑s.card = coverMincard T F U n
-- Mathlib/Data/Real/Archimedean.lean
/-- As `sSup s = 0` when `s` is a set of reals that's unbounded above, it suffices to show that `s`
contains a nonnegative element to show that `0 ≤ sSup s`. -/
lemma sSup_nonneg' (hs : ∃ x ∈ s, 0 ≤ x) : 0 ≤ sSup s

Proof state:
s : Set ℝ
hs : ∃ x ∈ s, 0 ≤ x
⊢ 0 ≤ sSup s

Tactic:
obtain ⟨x, hxs, hx⟩ := hs

Result:
case intro.intro
s : Set ℝ
x : ℝ
hxs : x ∈ s
hx : 0 ≤ x
⊢ 0 ≤ sSup s

Proof state:
s : Set ℝ
hs : ∃ x ∈ s, 0 ≤ x
⊢ 0 ≤ sSup s

Tactic:
classical
obtain ⟨x, hxs, hx⟩ := hs
exact dite _ (fun h ↦ le_csSup_of_le h hxs hx) fun h ↦ (sSup_of_not_bddAbove h).ge

Result:
no goals

Proof state:
case intro.intro
s : Set ℝ
x : ℝ
hxs : x ∈ s
hx : 0 ≤ x
⊢ 0 ≤ sSup s

Tactic:
exact dite _ (fun h ↦ le_csSup_of_le h hxs hx) fun h ↦ (sSup_of_not_bddAbove h).ge

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem unary_relation_sSup_iff {α : Type*} (s : Set (α → Prop)) {a : α} :
    sSup s a ↔ ∃ r : α → Prop, r ∈ s ∧ r a

Proof state:
α : Type u_8
s : Set (α → Prop)
a : α
⊢ sSup s a ↔ ∃ r ∈ s, r a

Tactic:
rw [sSup_apply]

Result:
α : Type u_8
s : Set (α → Prop)
a : α
⊢ ⨆ f, ↑f a ↔ ∃ r ∈ s, r a

Proof state:
α : Type u_8
s : Set (α → Prop)
a : α
⊢ ⨆ f, ↑f a ↔ ∃ r ∈ s, r a

Tactic:
simp [← eq_iff_iff]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Tower.lean
theorem mvPolynomial_aeval_coe (S : Subalgebra R A) (x : σ → S) (p : MvPolynomial σ R) :
    aeval (fun i => (x i : A)) p = aeval x p

Proof state:
R : Type u_1
A : Type u_2
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
x : σ → ↥S
p : MvPolynomial σ R
⊢ (aeval fun i => ↑(x i)) p = ↑((aeval x) p)

Tactic:
convert aeval_algebraMap_apply A x p

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RefVecOperator/Zip.lean
theorem go_denote_mem_prefix {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len)
    (s : RefVec aig curr) (lhs rhs : RefVec aig len)
    (f : (aig : AIG α) → BinaryInput aig → Entrypoint α) [LawfulOperator α BinaryInput f]
    [chainable : LawfulZipOperator α f] (start : Nat) (hstart) :
    ⟦
      (go aig curr s hcurr lhs rhs f).aig,
      ⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
      assign
    ⟧
      =
    ⟦aig, ⟨start, hstart⟩, assign⟧

Proof state:
case hprefix
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
lhs rhs : aig.RefVec len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
start : Nat
hstart : start < aig.decls.size
⊢ IsPrefix { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls (go aig curr s hcurr lhs rhs f).aig.decls

Tactic:
apply IsPrefix.of

Result:
case hprefix.idx_eq
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
lhs rhs : aig.RefVec len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
start : Nat
hstart : start < aig.decls.size
⊢ ∀ (idx : Nat) (h : idx < { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls.size),
    (go aig curr s hcurr lhs rhs f).aig.decls[idx] =
      { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls[idx]

case hprefix.size_le
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
lhs rhs : aig.RefVec len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
start : Nat
hstart : start < aig.decls.size
⊢ { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls.size ≤
    (go aig curr s hcurr lhs rhs f).aig.decls.size
-- Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
theorem rightAdjointMate_comp_evaluation {X Y : C} [HasRightDual X] [HasRightDual Y] (f : X ⟶ Y) :
    (fᘁ ▷ X) ≫ ε_ X (Xᘁ) = ((Yᘁ) ◁ f) ≫ ε_ Y (Yᘁ)

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
⊢ fᘁ ▷ X ≫ ε_ X Xᘁ = Yᘁ ◁ f ≫ ε_ Y Yᘁ

Tactic:
apply_fun tensorRightHomEquiv _ X (Xᘁ) _

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
⊢ (tensorRightHomEquiv Yᘁ X Xᘁ (𝟙_ C)) (fᘁ ▷ X ≫ ε_ X Xᘁ) = (tensorRightHomEquiv Yᘁ X Xᘁ (𝟙_ C)) (Yᘁ ◁ f ≫ ε_ Y Yᘁ)

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
⊢ (tensorRightHomEquiv Yᘁ X Xᘁ (𝟙_ C)) (fᘁ ▷ X ≫ ε_ X Xᘁ) = (tensorRightHomEquiv Yᘁ X Xᘁ (𝟙_ C)) (Yᘁ ◁ f ≫ ε_ Y Yᘁ)

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem smul_eq_C_smul (x : RatFunc K) (r : K) : r • x = Polynomial.C r • x

Proof state:
case ofFractionRing.H
K : Type u
inst✝ : CommRing K
r : K
y✝ : K[X] × ↥K[X]⁰
⊢ r • { toFractionRing := Localization.mk y✝.1 y✝.2 } = Polynomial.C r • { toFractionRing := Localization.mk y✝.1 y✝.2 }

Tactic:
rw [← ofFractionRing_smul, ← ofFractionRing_smul, Localization.smul_mk,
  Localization.smul_mk, smul_eq_mul, Polynomial.smul_eq_C_mul]

Result:
no goals

Proof state:
case ofFractionRing
K : Type u
inst✝ : CommRing K
r : K
x : FractionRing K[X]
⊢ r • { toFractionRing := x } = Polynomial.C r • { toFractionRing := x }

Tactic:
induction x using Localization.induction_on

Result:
case ofFractionRing.H
K : Type u
inst✝ : CommRing K
r : K
y✝ : K[X] × ↥K[X]⁰
⊢ r • { toFractionRing := Localization.mk y✝.1 y✝.2 } = Polynomial.C r • { toFractionRing := Localization.mk y✝.1 y✝.2 }

Proof state:
K : Type u
inst✝ : CommRing K
x : RatFunc K
r : K
⊢ r • x = Polynomial.C r • x

Tactic:
obtain ⟨x⟩ := x

Result:
case ofFractionRing
K : Type u
inst✝ : CommRing K
r : K
x : FractionRing K[X]
⊢ r • { toFractionRing := x } = Polynomial.C r • { toFractionRing := x }
-- Mathlib/MeasureTheory/Function/L2Space.lean
theorem memLp_two_iff_integrable_sq_norm {f : α → F} (hf : AEStronglyMeasurable f μ) :
    MemLp f 2 μ ↔ Integrable (fun x => ‖f x‖ ^ 2) μ

Proof state:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
⊢ MemLp f 2 μ ↔ Integrable (fun x => ‖f x‖ ^ 2) μ

Tactic:
rw [← memLp_one_iff_integrable]

Result:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
⊢ MemLp f 2 μ ↔ MemLp (fun x => ‖f x‖ ^ 2) 1 μ

Proof state:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
⊢ MemLp f 2 μ ↔ MemLp (fun x => ‖f x‖ ^ 2) 1 μ

Tactic:
convert (memLp_norm_rpow_iff hf two_ne_zero ENNReal.ofNat_ne_top).symm

Result:
case h.e'_2.h.e'_6.h
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
x✝ : α
⊢ ‖f x✝‖ ^ 2 = ‖f x✝‖ ^ ENNReal.toReal 2

case h.e'_2.h.e'_7
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
⊢ 1 = 2 / 2

Proof state:
case h.e'_2.h.e'_7
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
⊢ 1 = 2 / 2

Tactic:
rw [div_eq_mul_inv, ENNReal.mul_inv_cancel two_ne_zero ENNReal.ofNat_ne_top]

Result:
no goals

Proof state:
case h.e'_2.h.e'_6.h
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
x✝ : α
⊢ ‖f x✝‖ ^ 2 = ‖f x✝‖ ^ ENNReal.toReal 2

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem _root_.map_finset_sup' [SemilatticeSup β] [FunLike F α β] [SupHomClass F α β]
    (f : F) {s : Finset ι} (hs) (g : ι → α) :
    f (s.sup' hs g) = s.sup' hs (f ∘ g)

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : F
s : Finset ι
hs : s.Nonempty
g : ι → α
⊢ f (s.sup' hs g) = s.sup' hs (⇑f ∘ g)

Tactic:
refine hs.cons_induction ?_ ?_ <;> intros <;> simp [*]

Result:
no goals
-- Mathlib/RingTheory/Ideal/GoingUp.lean
theorem comap_lt_comap_of_integral_mem_sdiff [Algebra R S] [hI : I.IsPrime] (hIJ : I ≤ J) {x : S}
    (mem : x ∈ (J : Set S) \ I) (integral : IsIntegral R x) :
    I.comap (algebraMap R S) < J.comap (algebraMap R S)

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
I J : Ideal S
inst✝ : Algebra R S
hI : I.IsPrime
hIJ : I ≤ J
x : S
mem : x ∈ ↑J \ ↑I
integral : IsIntegral R x
⊢ comap (algebraMap R S) I < comap (algebraMap R S) J

Tactic:
obtain ⟨p, p_monic, hpx⟩ := integral

Result:
case intro.intro
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
I J : Ideal S
inst✝ : Algebra R S
hI : I.IsPrime
hIJ : I ≤ J
x : S
mem : x ∈ ↑J \ ↑I
p : R[X]
p_monic : p.Monic
hpx : eval₂ (algebraMap R S) x p = 0
⊢ comap (algebraMap R S) I < comap (algebraMap R S) J

Proof state:
case intro.intro
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
I J : Ideal S
inst✝ : Algebra R S
hI : I.IsPrime
hIJ : I ≤ J
x : S
mem : x ∈ ↑J \ ↑I
p : R[X]
p_monic : p.Monic
hpx : eval₂ (algebraMap R S) x p = 0
⊢ eval₂ (algebraMap R S) x p ∈ I

Tactic:
convert I.zero_mem

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
I J : Ideal S
inst✝ : Algebra R S
hI : I.IsPrime
hIJ : I ≤ J
x : S
mem : x ∈ ↑J \ ↑I
p : R[X]
p_monic : p.Monic
hpx : eval₂ (algebraMap R S) x p = 0
⊢ comap (algebraMap R S) I < comap (algebraMap R S) J

Tactic:
refine comap_lt_comap_of_root_mem_sdiff hIJ mem (map_monic_ne_zero p_monic) ?_

Result:
case intro.intro
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
I J : Ideal S
inst✝ : Algebra R S
hI : I.IsPrime
hIJ : I ≤ J
x : S
mem : x ∈ ↑J \ ↑I
p : R[X]
p_monic : p.Monic
hpx : eval₂ (algebraMap R S) x p = 0
⊢ eval₂ (algebraMap R S) x p ∈ I
-- Mathlib/MeasureTheory/PiSystem.lean
theorem generateFrom_piiUnionInter_measurableSet (m : ι → MeasurableSpace α) (S : Set ι) :
    generateFrom (piiUnionInter (fun n => { s | MeasurableSet[m n] s }) S) = ⨆ i ∈ S, m i

Proof state:
case refine_2
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
i : ι
hi : i ∈ S
⊢ generateFrom {s | MeasurableSet s} ≤ generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S)

Tactic:
exact generateFrom_mono (mem_piiUnionInter_of_measurableSet m hi)

Result:
no goals

Proof state:
case refine_1
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
⊢ generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S) ≤ ⨆ i ∈ S, m i

Tactic:
rw [← @generateFrom_measurableSet α (⨆ i ∈ S, m i)]

Result:
case refine_1
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
⊢ generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S) ≤ generateFrom {s | MeasurableSet s}

Proof state:
case refine_1
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
⊢ generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S) ≤ generateFrom {s | MeasurableSet s}

Tactic:
exact generateFrom_mono (measurableSet_iSup_of_mem_piiUnionInter m S)

Result:
no goals

Proof state:
case refine_2
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
⊢ ⨆ i ∈ S, m i ≤ generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S)

Tactic:
refine iSup₂_le fun i hi => ?_

Result:
case refine_2
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
i : ι
hi : i ∈ S
⊢ m i ≤ generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S)

Proof state:
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
⊢ generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S) = ⨆ i ∈ S, m i

Tactic:
refine le_antisymm ?_ ?_

Result:
case refine_1
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
⊢ generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S) ≤ ⨆ i ∈ S, m i

case refine_2
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
⊢ ⨆ i ∈ S, m i ≤ generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S)

Proof state:
case refine_2
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
i : ι
hi : i ∈ S
⊢ m i ≤ generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S)

Tactic:
rw [← @generateFrom_measurableSet α (m i)]

Result:
case refine_2
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
i : ι
hi : i ∈ S
⊢ generateFrom {s | MeasurableSet s} ≤ generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S)
-- Mathlib/Analysis/Asymptotics/ExpGrowth.lean
lemma expGrowthInf_inv {u : ℕ → ℝ≥0∞} :
    expGrowthInf u⁻¹ = - expGrowthSup u

Proof state:
u : ℕ → ℝ≥0∞
⊢ expGrowthInf u⁻¹ = liminf (-fun n => (u n).log / ↑n) atTop

Tactic:
refine liminf_congr (Eventually.of_forall fun n ↦ ?_)

Result:
u : ℕ → ℝ≥0∞
n : ℕ
⊢ (u⁻¹ n).log / ↑n = (-fun n => (u n).log / ↑n) n

Proof state:
u : ℕ → ℝ≥0∞
⊢ expGrowthInf u⁻¹ = -expGrowthSup u

Tactic:
rw [expGrowthSup, ← liminf_neg]

Result:
u : ℕ → ℝ≥0∞
⊢ expGrowthInf u⁻¹ = liminf (-fun n => (u n).log / ↑n) atTop

Proof state:
u : ℕ → ℝ≥0∞
n : ℕ
⊢ (u⁻¹ n).log / ↑n = (-fun n => (u n).log / ↑n) n

Tactic:
rw [Pi.neg_apply, Pi.inv_apply, div_eq_mul_inv, div_eq_mul_inv, ← EReal.neg_mul, log_inv]

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/TransfiniteCompositionLifting.lean
lemma retracts_transfiniteComposition_pushouts_coproducts_le_llp_rlp :
    (transfiniteCompositions.{w} (coproducts.{w} W).pushouts).retracts ≤ W.rlp.llp

Proof state:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
⊢ transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} W).pushouts ≤ W.rlp.llp

Tactic:
apply transfiniteCompositions_pushouts_coproducts_le_llp_rlp

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
⊢ (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} W).pushouts).retracts ≤ W.rlp.llp

Tactic:
rw [le_llp_iff_le_rlp, rlp_retracts, ← le_llp_iff_le_rlp]

Result:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
⊢ transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} W).pushouts ≤ W.rlp.llp
-- Mathlib/Data/Setoid/Basic.lean
theorem sup_def {r s : Setoid α} : r ⊔ s = EqvGen.setoid (⇑r ⊔ ⇑s)

Proof state:
α : Type u_1
r s : Setoid α
⊢ (EqvGen.setoid fun x y => r x y ∨ s x y) = EqvGen.setoid (⇑r ⊔ ⇑s)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
r s : Setoid α
⊢ r ⊔ s = EqvGen.setoid (⇑r ⊔ ⇑s)

Tactic:
rw [sup_eq_eqvGen]

Result:
α : Type u_1
r s : Setoid α
⊢ (EqvGen.setoid fun x y => r x y ∨ s x y) = EqvGen.setoid (⇑r ⊔ ⇑s)
-- Mathlib/SetTheory/Cardinal/Finite.lean
theorem card_eq_zero_iff_empty (α : Type*) : card α = 0 ↔ IsEmpty α

Proof state:
α : Type u_3
⊢ card α = 0 ↔ #α = 0

Tactic:
simp [card]

Result:
no goals

Proof state:
α : Type u_3
⊢ card α = 0 ↔ IsEmpty α

Tactic:
rw [← Cardinal.mk_eq_zero_iff]

Result:
α : Type u_3
⊢ card α = 0 ↔ #α = 0
-- Mathlib/Data/Rat/Defs.lean
@[simp] lemma inv_mkRat (a : ℤ) (b : ℕ) : (mkRat a b)⁻¹ = b /. a

Proof state:
a : ℤ
b : ℕ
⊢ (mkRat a b)⁻¹ = ↑b /. a

Tactic:
rw [mkRat_eq_divInt, inv_divInt']

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Lemmas.lean
theorem getElem_insertIdx_loop_eq {as : Array α} {i : Nat} {j : Nat} {hj : j < as.size} {h} :
    (insertIdx.loop i as ⟨j, hj⟩)[i] = if i ≤ j then as[j] else as[i]'(by simpa using h)

Proof state:
case isFalse
α : Type u_1
as : Array α
i j : Nat
hj : j < as.size
h : i < (insertIdx.loop i as ⟨j, hj⟩).size
h₁✝ : ¬i < ↑⟨j, hj⟩
h₁ : j ≤ i
⊢ as[i] = if i ≤ j then as[j] else as[i]

Tactic:
by_cases h' : i = j

Result:
case pos
α : Type u_1
as : Array α
i j : Nat
hj : j < as.size
h : i < (insertIdx.loop i as ⟨j, hj⟩).size
h₁✝ : ¬i < ↑⟨j, hj⟩
h₁ : j ≤ i
h' : i = j
⊢ as[i] = if i ≤ j then as[j] else as[i]

case neg
α : Type u_1
as : Array α
i j : Nat
hj : j < as.size
h : i < (insertIdx.loop i as ⟨j, hj⟩).size
h₁✝ : ¬i < ↑⟨j, hj⟩
h₁ : j ≤ i
h' : ¬i = j
⊢ as[i] = if i ≤ j then as[j] else as[i]

Proof state:
α : Type u_1
as : Array α
i j : Nat
hj : j < as.size
h : i < (insertIdx.loop i as ⟨j, hj⟩).size
⊢ (if i < ↑⟨j, hj⟩ then
        let j' := ⟨↑⟨j, hj⟩ - 1, ⋯⟩;
        let as_1 := as.swap ↑j' ↑⟨j, hj⟩ ⋯ ⋯;
        insertIdx.loop i as_1 ⟨↑j', ⋯⟩
      else as)[i] =
    if i ≤ j then as[j] else as[i]

Tactic:
split <;> rename_i h₁

Result:
case isTrue
α : Type u_1
as : Array α
i j : Nat
hj : j < as.size
h : i < (insertIdx.loop i as ⟨j, hj⟩).size
h₁ : i < ↑⟨j, hj⟩
⊢ (let j' := ⟨↑⟨j, hj⟩ - 1, ⋯⟩;
      let as_1 := as.swap ↑j' ↑⟨j, hj⟩ ⋯ ⋯;
      insertIdx.loop i as_1 ⟨↑j', ⋯⟩)[i] =
    if i ≤ j then as[j] else as[i]

case isFalse
α : Type u_1
as : Array α
i j : Nat
hj : j < as.size
h : i < (insertIdx.loop i as ⟨j, hj⟩).size
h₁ : ¬i < ↑⟨j, hj⟩
⊢ as[i] = if i ≤ j then as[j] else as[i]
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem mk_smul_mk (r : R) (m : M) (s t : S) :
    Localization.mk r s • mk m t = mk (r • m) (s * t)

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
m : M
s t : ↥S
⊢ IsLocalization.mk' (Localization S) r s • mk m t = mk (r • m) (s * t)

Tactic:
exact mk'_smul_mk ..

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
m : M
s t : ↥S
⊢ Localization.mk r s • mk m t = mk (r • m) (s * t)

Tactic:
rw [Localization.mk_eq_mk']

Result:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
m : M
s t : ↥S
⊢ IsLocalization.mk' (Localization S) r s • mk m t = mk (r • m) (s * t)
-- Mathlib/LinearAlgebra/RootSystem/Reduced.lean
/-- See also `RootPairing.linearIndependent_iff_coxeterWeightIn_ne_four`. -/
lemma linearIndependent_iff_coxeterWeight_ne_four :
    LinearIndependent R ![P.root i, P.root j] ↔ P.coxeterWeight i j ≠ 4

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
i j : ι
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
this : NoZeroSMulDivisors ℤ M
h : ¬LinearIndependent R ![P.root j, P.root i]
h₁ : P.pairing j i • P.root i = 2 • P.root j
h₂ : P.pairing i j • P.root j = 2 • P.root i
⊢ P.coxeterWeight i j • P.root i = (P.pairing i j * P.pairing j i) • P.root i

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
i j : ι
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
this : NoZeroSMulDivisors ℤ M
h : ¬LinearIndependent R ![P.root j, P.root i]
h₁ : P.pairing j i • P.root i = 2 • P.root j
h₂ : P.pairing i j • P.root j = 2 • P.root i
⊢ (2 * 2) • P.root i = 4 • P.root i

Tactic:
norm_num

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
i j : ι
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
this : NoZeroSMulDivisors ℤ M
h : ¬LinearIndependent R ![P.root j, P.root i]
h₁ : P.pairing j i • P.root i = 2 • P.root j
⊢ P.coxeterWeight i j = 4

Tactic:
have h₂ := P.pairing_smul_root_eq_of_not_linInd h

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
i j : ι
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
this : NoZeroSMulDivisors ℤ M
h : ¬LinearIndependent R ![P.root j, P.root i]
h₁ : P.pairing j i • P.root i = 2 • P.root j
h₂ : P.pairing i j • P.root j = 2 • P.root i
⊢ P.coxeterWeight i j = 4
-- Mathlib/Data/Matrix/Mul.lean
theorem sumElim_dotProduct_sumElim : Sum.elim u x ⬝ᵥ Sum.elim v y = u ⬝ᵥ v + x ⬝ᵥ y

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
u v : m → α
x y : n → α
⊢ Sum.elim u x ⬝ᵥ Sum.elim v y = u ⬝ᵥ v + x ⬝ᵥ y

Tactic:
simp [dotProduct]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma negMap_of_Z_eq_zero {P : Fin 3 → F} (hP : W.Nonsingular P) (hPz : P z = 0) :
    W.negMap ⟦P⟧ = ⟦![0, 1, 0]⟧

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ W.negMap ⟦P⟧ = ⟦![0, 1, 0]⟧

Tactic:
rw [negMap_eq, neg_of_Z_eq_zero hP.left hPz, smul_eq _ (isUnit_Y_of_Z_eq_zero hP hPz).neg]

Result:
no goals