harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Ring/SmoothingSeminorm.lean
theorem μ_bddAbove (hμ1 : μ 1 ≤ 1) {s : ℕ → ℕ} (hs : ∀ n : ℕ, s n ≤ n) (x : R)
    (ψ : ℕ → ℕ) : BddAbove (Set.range fun n : ℕ => μ (x ^ s (ψ n)) ^ (1 / (ψ n : ℝ)))

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : μ x ≤ 1
⊢ ∀ (x_1 : ℝ) (x_2 : ℕ), μ (x ^ s (ψ x_2)) ^ (1 / ↑(ψ x_2)) = x_1 → x_1 ≤ 1

Tactic:
rintro _ n rfl

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : μ x ≤ 1
n : ℕ
⊢ μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n)) ≤ 1

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : μ x ≤ 1
n : ℕ
⊢ μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n)) ≤ 1

Tactic:
apply le_trans (rpow_le_rpow (apply_nonneg _ _) (map_pow_le_pow' hμ1 _ _) (hψ n))

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : μ x ≤ 1
n : ℕ
⊢ (μ x ^ s (ψ n)) ^ (1 / ↑(ψ n)) ≤ 1
-- Mathlib/Analysis/Seminorm.lean
theorem finset_sup_apply_lt {p : ι → Seminorm 𝕜 E} {s : Finset ι} {x : E} {a : ℝ} (ha : 0 < a)
    (h : ∀ i, i ∈ s → p i x < a) : s.sup p x < a

Proof state:
case intro
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
a : ℝ≥0
ha : 0 < ↑a
h : ∀ i ∈ s, (p i) x < ↑a
⊢ ⊥ < a

Tactic:
exact NNReal.coe_pos.mpr ha

Result:
no goals

Proof state:
case intro
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
a : ℝ≥0
ha : 0 < ↑a
h : ∀ i ∈ s, (p i) x < ↑a
⊢ ∀ b ∈ s, ⟨(p b) x, ⋯⟩ < a

Tactic:
exact h

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
a : ℝ
ha : 0 < a
h : ∀ i ∈ s, (p i) x < a
⊢ (s.sup p) x < a

Tactic:
lift a to ℝ≥0 using ha.le

Result:
case intro
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
a : ℝ≥0
ha : 0 < ↑a
h : ∀ i ∈ s, (p i) x < ↑a
⊢ (s.sup p) x < ↑a

Proof state:
case intro
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
a : ℝ≥0
ha : 0 < ↑a
h : ∀ i ∈ s, (p i) x < ↑a
⊢ (s.sup p) x < ↑a

Tactic:
rw [finset_sup_apply, NNReal.coe_lt_coe, Finset.sup_lt_iff]

Result:
case intro
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
a : ℝ≥0
ha : 0 < ↑a
h : ∀ i ∈ s, (p i) x < ↑a
⊢ ∀ b ∈ s, ⟨(p b) x, ⋯⟩ < a

case intro
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
a : ℝ≥0
ha : 0 < ↑a
h : ∀ i ∈ s, (p i) x < ↑a
⊢ ⊥ < a
-- Mathlib/CategoryTheory/Abelian/RightDerived.lean
/-- A component of the natural transformation between right-derived functors can be computed
using a chosen injective resolution. -/
lemma rightDerived_app_eq
    {F G : C ⥤ D} [F.Additive] [G.Additive] (α : F ⟶ G) {X : C} (P : InjectiveResolution X)
    (n : ℕ) : (NatTrans.rightDerived α n).app X =
      (P.isoRightDerivedObj F n).hom ≫
        (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map
        ((NatTrans.mapHomologicalComplex α _).app P.cocomplex) ≫
        (P.isoRightDerivedObj G n).inv

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{u_2, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : InjectiveResolution X
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
            ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)) ≫
        (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj G).inv =
    (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.quotient D (ComplexShape.up ℕ) ⋙ HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex) ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app
            ((G.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex) ≫
          (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).inv.app
              ((G.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex) ≫
            (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
              (P.isoRightDerivedToHomotopyCategoryObj G).inv

Tactic:
simp only [Functor.comp_map, Iso.hom_inv_id_app_assoc]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean
theorem QuasiSeparated.of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [QuasiSeparated (f ≫ g)] :
    QuasiSeparated f

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
𝒰 : Scheme.Cover (@IsOpenImmersion) Y :=
  (Scheme.Cover.pullbackCover Z.affineCover g).bind fun x =>
    ((Scheme.Cover.pullbackCover Z.affineCover g).obj x).affineCover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
⊢ ∀
    (i :
      ((Scheme.Cover.pullbackCover Z.affineCover g).bind fun x =>
          ((Scheme.Cover.pullbackCover Z.affineCover g).obj x).affineCover).1),
    QuasiSeparatedSpace
      ↑↑((((Scheme.Cover.pullbackCover Z.affineCover g).bind fun x =>
                      ((Scheme.Cover.pullbackCover Z.affineCover g).obj x).affineCover).pullbackCover
                  f).obj
              i).toPresheafedSpace

Tactic:
rintro ⟨i, j⟩

Result:
case mk
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
𝒰 : Scheme.Cover (@IsOpenImmersion) Y :=
  (Scheme.Cover.pullbackCover Z.affineCover g).bind fun x =>
    ((Scheme.Cover.pullbackCover Z.affineCover g).obj x).affineCover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
i : (Scheme.Cover.pullbackCover Z.affineCover g).J
j : ((fun x => ((Scheme.Cover.pullbackCover Z.affineCover g).obj x).affineCover) i).J
⊢ QuasiSeparatedSpace
    ↑↑((((Scheme.Cover.pullbackCover Z.affineCover g).bind fun x =>
                    ((Scheme.Cover.pullbackCover Z.affineCover g).obj x).affineCover).pullbackCover
                f).obj
            ⟨i, j⟩).toPresheafedSpace

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
𝒰 : Scheme.Cover (@IsOpenImmersion) Y :=
  (Scheme.Cover.pullbackCover Z.affineCover g).bind fun x =>
    ((Scheme.Cover.pullbackCover Z.affineCover g).obj x).affineCover
⊢ QuasiSeparated f

Tactic:
have (i) : IsAffine (𝒰.obj i) := by dsimp [𝒰]; infer_instance

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
𝒰 : Scheme.Cover (@IsOpenImmersion) Y :=
  (Scheme.Cover.pullbackCover Z.affineCover g).bind fun x =>
    ((Scheme.Cover.pullbackCover Z.affineCover g).obj x).affineCover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
⊢ QuasiSeparated f

Proof state:
case mk.refine_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
𝒰 : Scheme.Cover (@IsOpenImmersion) Y :=
  (Scheme.Cover.pullbackCover Z.affineCover g).bind fun x =>
    ((Scheme.Cover.pullbackCover Z.affineCover g).obj x).affineCover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
i : Z.affineCover.J
j : (pullback g (Z.affineCover.map i)).affineCover.J
⊢ (((Scheme.Cover.pullbackCover Z.affineCover g).bind fun x =>
              ((Scheme.Cover.pullbackCover Z.affineCover g).obj x).affineCover).pullbackCover
          f).obj
      ⟨i, j⟩ ⟶
    pullback (f ≫ g) (Z.affineCover.map i)

Tactic:
exact pullback.map _ _ _ _ (𝟙 _) _ _ (by simp) (Category.comp_id _) ≫
  (pullbackRightPullbackFstIso g (Z.affineCover.map i) f).hom

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean
lemma reduce_of_not_pos {A : Δ m} (hc : (A.1 1 0) = 0) (ha : ¬ 0 < A.1 0 0) :
    reduce A = (T ^ (-(-A.1 0 1 / -A.1 1 1))) • (S • (S • A))

Proof state:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : ↑A 1 0 = 0
ha : ¬0 < ↑A 0 0
⊢ (if ↑A 1 0 = 0 then if 0 < ↑A 0 0 then T ^ (-(↑A 0 1 / ↑A 1 1)) • A else T ^ (-(-↑A 0 1 / -↑A 1 1)) • S • S • A
    else reduce (reduceStep A)) =
    T ^ (-(-↑A 0 1 / -↑A 1 1)) • S • S • A

Tactic:
simp only [abs_eq_zero, zpow_neg, Int.ediv_neg, neg_neg] at *

Result:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : ↑A 1 0 = 0
ha : ¬0 < ↑A 0 0
⊢ (if ↑A 1 0 = 0 then if 0 < ↑A 0 0 then (T ^ (↑A 0 1 / ↑A 1 1))⁻¹ • A else T ^ (-↑A 0 1 / ↑A 1 1) • S • S • A
    else reduce (reduceStep A)) =
    T ^ (-↑A 0 1 / ↑A 1 1) • S • S • A

Proof state:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : ↑A 1 0 = 0
ha : ¬0 < ↑A 0 0
⊢ reduce A = T ^ (-(-↑A 0 1 / -↑A 1 1)) • S • S • A

Tactic:
rw [reduce]

Result:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : ↑A 1 0 = 0
ha : ¬0 < ↑A 0 0
⊢ (if ↑A 1 0 = 0 then if 0 < ↑A 0 0 then T ^ (-(↑A 0 1 / ↑A 1 1)) • A else T ^ (-(-↑A 0 1 / -↑A 1 1)) • S • S • A
    else reduce (reduceStep A)) =
    T ^ (-(-↑A 0 1 / -↑A 1 1)) • S • S • A

Proof state:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : ↑A 1 0 = 0
ha : ¬0 < ↑A 0 0
⊢ (if ↑A 1 0 = 0 then if 0 < ↑A 0 0 then (T ^ (↑A 0 1 / ↑A 1 1))⁻¹ • A else T ^ (-↑A 0 1 / ↑A 1 1) • S • S • A
    else reduce (reduceStep A)) =
    T ^ (-↑A 0 1 / ↑A 1 1) • S • S • A

Tactic:
simp_rw [if_pos hc, if_neg ha]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem nextCoeff_X_add_C [Semiring S] (c : S) : nextCoeff (X + C c) = c

Proof state:
S : Type v
inst✝ : Semiring S
c : S
⊢ (X + C c).nextCoeff = c

Tactic:
nontriviality S

Result:
S : Type v
inst✝ : Semiring S
c : S
a✝ : Nontrivial S
⊢ (X + C c).nextCoeff = c

Proof state:
S : Type v
inst✝ : Semiring S
c : S
a✝ : Nontrivial S
⊢ (X + C c).nextCoeff = c

Tactic:
simp [nextCoeff_of_natDegree_pos]

Result:
no goals
-- Mathlib/Data/Nat/PrimeFin.lean
lemma mem_primeFactors_iff_mem_primeFactorsList : p ∈ n.primeFactors ↔ p ∈ n.primeFactorsList

Proof state:
n p : ℕ
⊢ p ∈ n.primeFactors ↔ p ∈ n.primeFactorsList

Tactic:
simp only [primeFactors, List.mem_toFinset]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Marginal.lean
theorem lmarginal_empty (f : (∀ i, π i) → ℝ≥0∞) : ∫⋯∫⁻_∅, f ∂μ = f

Proof state:
case h
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
f : ((i : δ) → π i) → ℝ≥0∞
x : (i : δ) → π i
⊢ (∫⁻ (y : (i : { x // x ∈ ∅ }) → π ↑i), f (updateFinset x ∅ y) ∂Measure.dirac fun a => isEmptyElim a) = f x

Tactic:
apply lintegral_dirac'

Result:
case h.hf
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
f : ((i : δ) → π i) → ℝ≥0∞
x : (i : δ) → π i
⊢ Measurable fun a => f (updateFinset x ∅ a)

Proof state:
case h
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
f : ((i : δ) → π i) → ℝ≥0∞
x : (i : δ) → π i
⊢ (∫⋯∫⁻_∅, f ∂μ) x = f x

Tactic:
simp_rw [lmarginal, Measure.pi_of_empty fun i : (∅ : Finset δ) => μ i]

Result:
case h
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
f : ((i : δ) → π i) → ℝ≥0∞
x : (i : δ) → π i
⊢ (∫⁻ (y : (i : { x // x ∈ ∅ }) → π ↑i), f (updateFinset x ∅ y) ∂Measure.dirac fun a => isEmptyElim a) = f x

Proof state:
case h.hf
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
f : ((i : δ) → π i) → ℝ≥0∞
x : (i : δ) → π i
⊢ Measurable fun a => f (updateFinset x ∅ a)

Tactic:
exact Subsingleton.measurable

Result:
no goals

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
f : ((i : δ) → π i) → ℝ≥0∞
⊢ ∫⋯∫⁻_∅, f ∂μ = f

Tactic:
ext1 x

Result:
case h
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
f : ((i : δ) → π i) → ℝ≥0∞
x : (i : δ) → π i
⊢ (∫⋯∫⁻_∅, f ∂μ) x = f x
-- Mathlib/Probability/Kernel/Composition/CompProd.lean
theorem compProdFun_eq_tsum (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel (α × β) γ)
    [IsSFiniteKernel η] (a : α) (hs : MeasurableSet s) :
    compProdFun κ η a s = ∑' (n) (m), compProdFun (seq κ n) (seq η m) a s

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
⊢ κ.compProdFun η a s = ∑' (n : ℕ) (m : ℕ), (κ.seq n).compProdFun (η.seq m) a s

Tactic:
simp_rw [compProdFun_tsum_left κ η a s, compProdFun_tsum_right _ η a hs]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/QuasiIso.lean
lemma quasiIso_unopMap {S₁ S₂ : ShortComplex Cᵒᵖ} [S₁.HasHomology] [S₂.HasHomology]
    [S₁.unop.HasHomology] [S₂.unop.HasHomology]
    (φ : S₁ ⟶ S₂) [QuasiIso φ] : QuasiIso (unopMap φ)

Proof state:
C : Type u_1
inst✝⁶ : Category.{u_2, u_1} C
inst✝⁵ : HasZeroMorphisms C
S₁ S₂ : ShortComplex Cᵒᵖ
inst✝⁴ : S₁.HasHomology
inst✝³ : S₂.HasHomology
inst✝² : S₁.unop.HasHomology
inst✝¹ : S₂.unop.HasHomology
φ : S₁ ⟶ S₂
inst✝ : QuasiIso φ
⊢ QuasiIso (opMap (unopMap φ))

Tactic:
change QuasiIso φ

Result:
C : Type u_1
inst✝⁶ : Category.{u_2, u_1} C
inst✝⁵ : HasZeroMorphisms C
S₁ S₂ : ShortComplex Cᵒᵖ
inst✝⁴ : S₁.HasHomology
inst✝³ : S₂.HasHomology
inst✝² : S₁.unop.HasHomology
inst✝¹ : S₂.unop.HasHomology
φ : S₁ ⟶ S₂
inst✝ : QuasiIso φ
⊢ QuasiIso φ

Proof state:
C : Type u_1
inst✝⁶ : Category.{u_2, u_1} C
inst✝⁵ : HasZeroMorphisms C
S₁ S₂ : ShortComplex Cᵒᵖ
inst✝⁴ : S₁.HasHomology
inst✝³ : S₂.HasHomology
inst✝² : S₁.unop.HasHomology
inst✝¹ : S₂.unop.HasHomology
φ : S₁ ⟶ S₂
inst✝ : QuasiIso φ
⊢ QuasiIso (unopMap φ)

Tactic:
rw [← quasiIso_opMap_iff]

Result:
C : Type u_1
inst✝⁶ : Category.{u_2, u_1} C
inst✝⁵ : HasZeroMorphisms C
S₁ S₂ : ShortComplex Cᵒᵖ
inst✝⁴ : S₁.HasHomology
inst✝³ : S₂.HasHomology
inst✝² : S₁.unop.HasHomology
inst✝¹ : S₂.unop.HasHomology
φ : S₁ ⟶ S₂
inst✝ : QuasiIso φ
⊢ QuasiIso (opMap (unopMap φ))

Proof state:
C : Type u_1
inst✝⁶ : Category.{u_2, u_1} C
inst✝⁵ : HasZeroMorphisms C
S₁ S₂ : ShortComplex Cᵒᵖ
inst✝⁴ : S₁.HasHomology
inst✝³ : S₂.HasHomology
inst✝² : S₁.unop.HasHomology
inst✝¹ : S₂.unop.HasHomology
φ : S₁ ⟶ S₂
inst✝ : QuasiIso φ
⊢ QuasiIso φ

Tactic:
infer_instance

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Hom.lean
@[simp]
lemma weightMap_weightEquiv_symm (e : RootPairing.Equiv P Q) (m : M₂) :
    e.toHom.weightMap ((weightEquiv P Q e).symm m) = m

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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
e : P.Equiv Q
m : M₂
⊢ (↑e).weightMap ((weightEquiv P Q e).symm m) = m

Tactic:
rw [← weightEquiv_apply]

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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
e : P.Equiv Q
m : M₂
⊢ (weightEquiv P Q e) ((weightEquiv P Q e).symm m) = m

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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
e : P.Equiv Q
m : M₂
⊢ (weightEquiv P Q e) ((weightEquiv P Q e).symm m) = m

Tactic:
exact LinearEquiv.apply_symm_apply (weightEquiv P Q e) m

Result:
no goals
-- Mathlib/Data/Nat/Fib/Zeckendorf.lean
@[simp] lemma greatestFib_eq_zero : greatestFib n = 0 ↔ n = 0 :=
  ⟨fun h ↦ by simpa using findGreatest_eq_zero_iff.1 h zero_lt_one le_add_self, by rintro rfl; rfl⟩

Proof state:
⊢ greatestFib 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
h : n.greatestFib = 0
⊢ n = 0

Tactic:
simpa using findGreatest_eq_zero_iff.1 h zero_lt_one le_add_self

Result:
no goals

Proof state:
n : ℕ
⊢ n = 0 → n.greatestFib = 0

Tactic:
rintro rfl

Result:
⊢ greatestFib 0 = 0
-- Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
theorem sup_toSubsemiring (S T : Subalgebra R A) :
    (S ⊔ T).toSubsemiring = S.toSubsemiring ⊔ T.toSubsemiring

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ (S ⊔ T).toSubsemiring = Subsemiring.closure (↑S.toSubsemiring ∪ ↑T.toSubsemiring)

Tactic:
simp_rw [sup_def, adjoin_toSubsemiring, Subalgebra.coe_toSubsemiring]

Result:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ Subsemiring.closure (Set.range ⇑(algebraMap R A) ∪ (↑S ∪ ↑T)) = Subsemiring.closure (↑S ∪ ↑T)

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ Subsemiring.closure (Set.range ⇑(algebraMap R A) ∪ (↑S ∪ ↑T)) = Subsemiring.closure (↑S ∪ ↑T)

Tactic:
congr 1

Result:
case e_s
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ Set.range ⇑(algebraMap R A) ∪ (↑S ∪ ↑T) = ↑S ∪ ↑T

Proof state:
case e_s
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ Set.range ⇑(algebraMap R A) ⊆ ↑S ∪ ↑T

Tactic:
rintro _ ⟨x, rfl⟩

Result:
case e_s.intro
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x : R
⊢ (algebraMap R A) x ∈ ↑S ∪ ↑T

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ (S ⊔ T).toSubsemiring = S.toSubsemiring ⊔ T.toSubsemiring

Tactic:
rw [← S.toSubsemiring.closure_eq, ← T.toSubsemiring.closure_eq, ← Subsemiring.closure_union]

Result:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ (S ⊔ T).toSubsemiring = Subsemiring.closure (↑S.toSubsemiring ∪ ↑T.toSubsemiring)

Proof state:
case e_s
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ Set.range ⇑(algebraMap R A) ∪ (↑S ∪ ↑T) = ↑S ∪ ↑T

Tactic:
rw [Set.union_eq_right]

Result:
case e_s
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ Set.range ⇑(algebraMap R A) ⊆ ↑S ∪ ↑T

Proof state:
case e_s.intro
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x : R
⊢ (algebraMap R A) x ∈ ↑S ∪ ↑T

Tactic:
exact Set.mem_union_left _ (algebraMap_mem S x)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Char/Basic.lean
theorem isValidChar_of_isValidCharNat (n : Nat) (h : isValidCharNat n) : isValidChar (UInt32.ofNat' n (isValidUInt32 n h)) :=
  match h with
  | Or.inl h =>
    Or.inl (UInt32.ofNat'_lt_of_lt _ (by decide) h)
  | Or.inr ⟨h₁, h₂⟩ =>
    Or.inr ⟨UInt32.lt_ofNat'_of_lt _ (by decide) h₁, UInt32.ofNat'_lt_of_lt _ (by decide) h₂⟩

Proof state:
n : Nat
h : isValidCharNat n
h₁ : 57343 < n
h₂ : n < 1114112
⊢ 57343 < UInt32.size

Tactic:
decide

Result:
no goals

Proof state:
n : Nat
h : isValidCharNat n
h₁ : 57343 < n
h₂ : n < 1114112
⊢ 1114112 < UInt32.size

Tactic:
decide

Result:
no goals

Proof state:
n : Nat
h✝ : isValidCharNat n
h : n < 55296
⊢ 55296 < UInt32.size

Tactic:
decide

Result:
no goals
-- Mathlib/Analysis/Asymptotics/ExpGrowth.lean
lemma expGrowthSup_le_of_eventually_le {u v : ℕ → ℝ≥0∞} {C : ℝ≥0∞} (hC : C ≠ ∞)
    (h : ∀ᶠ n in atTop, u n ≤ C * v n) :
    expGrowthSup u ≤ expGrowthSup v

Proof state:
case inr
u v : ℕ → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ C * v n
C_pos : 0 < C
⊢ (expGrowthSup fun x => C * v x) ≤ expGrowthSup v

Tactic:
apply (expGrowthSup_mul_le _ _).trans_eq <;> rw [expGrowthSup_const C_pos.ne' hC]

Result:
case inr
u v : ℕ → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ C * v n
C_pos : 0 < C
⊢ 0 + expGrowthSup v = expGrowthSup v

u v : ℕ → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ C * v n
C_pos : 0 < C
⊢ 0 ≠ ⊥ ∨ expGrowthSup v ≠ ⊤

u v : ℕ → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ C * v n
C_pos : 0 < C
⊢ 0 ≠ ⊤ ∨ expGrowthSup v ≠ ⊥

Proof state:
case inr
u v : ℕ → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ C * v n
C_pos : 0 < C
⊢ 0 + expGrowthSup v = expGrowthSup v

Tactic:
exact zero_add (expGrowthSup v)

Result:
no goals

Proof state:
case inl
u v : ℕ → ℝ≥0∞
hC : 0 ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ 0 * v n
⊢ (expGrowthSup fun x => 0 * v x) ≤ expGrowthSup v

Tactic:
simp only [zero_mul, ← Pi.zero_def, expGrowthSup_zero, bot_le]

Result:
no goals

Proof state:
u v : ℕ → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ C * v n
⊢ expGrowthSup u ≤ expGrowthSup v

Tactic:
apply (expGrowthSup_eventually_monotone h).trans

Result:
u v : ℕ → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ C * v n
⊢ (expGrowthSup fun x => C * v x) ≤ expGrowthSup v

Proof state:
u v : ℕ → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ C * v n
C_pos : 0 < C
⊢ 0 ≠ ⊤ ∨ expGrowthSup v ≠ ⊥

Tactic:
exact Or.inl EReal.zero_ne_top

Result:
no goals

Proof state:
u v : ℕ → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ C * v n
C_pos : 0 < C
⊢ 0 ≠ ⊥ ∨ expGrowthSup v ≠ ⊤

Tactic:
exact Or.inl EReal.zero_ne_bot

Result:
no goals

Proof state:
u v : ℕ → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ C * v n
⊢ (expGrowthSup fun x => C * v x) ≤ expGrowthSup v

Tactic:
rcases eq_zero_or_pos C with rfl | C_pos

Result:
case inl
u v : ℕ → ℝ≥0∞
hC : 0 ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ 0 * v n
⊢ (expGrowthSup fun x => 0 * v x) ≤ expGrowthSup v

case inr
u v : ℕ → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ C * v n
C_pos : 0 < C
⊢ (expGrowthSup fun x => C * v x) ≤ expGrowthSup v
-- Mathlib/Algebra/Order/Monoid/Unbundled/MinMax.lean
theorem lt_or_le_of_mul_le_mul [MulLeftStrictMono α] [MulRightMono α] {a₁ a₂ b₁ b₂ : α} :
    a₁ * b₁ ≤ a₂ * b₂ → a₁ < a₂ ∨ b₁ ≤ b₂

Proof state:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : Mul α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightMono α
a₁ a₂ b₁ b₂ : α
⊢ a₂ ≤ a₁ ∧ b₂ < b₁ → a₂ * b₂ < a₁ * b₁

Tactic:
exact fun h => mul_lt_mul_of_le_of_lt h.1 h.2

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : Mul α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightMono α
a₁ a₂ b₁ b₂ : α
⊢ a₁ * b₁ ≤ a₂ * b₂ → a₁ < a₂ ∨ b₁ ≤ b₂

Tactic:
contrapose!

Result:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : Mul α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightMono α
a₁ a₂ b₁ b₂ : α
⊢ a₂ ≤ a₁ ∧ b₂ < b₁ → a₂ * b₂ < a₁ * b₁