harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_def (f : α → M) [Decidable (mulSupport f).Finite] :
    ∏ᶠ i : α, f i = if h : (mulSupport f).Finite then ∏ i ∈ h.toFinset, f i else 1

Proof state:
case neg
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Decidable (mulSupport f).Finite
h : ¬(mulSupport f).Finite
⊢ ∏ᶠ (i : α), f i = 1

Tactic:
rw [finprod, dif_neg]

Result:
case neg.hnc
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Decidable (mulSupport f).Finite
h : ¬(mulSupport f).Finite
⊢ ¬(mulSupport ((fun i => f i) ∘ PLift.down)).Finite

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Decidable (mulSupport f).Finite
⊢ ∏ᶠ (i : α), f i = if h : (mulSupport f).Finite then ∏ i ∈ h.toFinset, f i else 1

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Decidable (mulSupport f).Finite
h : (mulSupport f).Finite
⊢ ∏ᶠ (i : α), f i = ∏ i ∈ h.toFinset, f i

case neg
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Decidable (mulSupport f).Finite
h : ¬(mulSupport f).Finite
⊢ ∏ᶠ (i : α), f i = 1

Proof state:
case pos
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Decidable (mulSupport f).Finite
h : (mulSupport f).Finite
⊢ ∏ᶠ (i : α), f i = ∏ i ∈ h.toFinset, f i

Tactic:
exact finprod_eq_prod_of_mulSupport_toFinset_subset _ h (Finset.Subset.refl _)

Result:
no goals

Proof state:
case neg.hnc
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Decidable (mulSupport f).Finite
h : ¬(mulSupport f).Finite
⊢ ¬(PLift.down ⁻¹' mulSupport fun i => f i).Finite

Tactic:
exact mt (fun hf => hf.of_preimage Equiv.plift.surjective) h

Result:
no goals

Proof state:
case neg.hnc
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Decidable (mulSupport f).Finite
h : ¬(mulSupport f).Finite
⊢ ¬(mulSupport ((fun i => f i) ∘ PLift.down)).Finite

Tactic:
rw [mulSupport_comp_eq_preimage]

Result:
case neg.hnc
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Decidable (mulSupport f).Finite
h : ¬(mulSupport f).Finite
⊢ ¬(PLift.down ⁻¹' mulSupport fun i => f i).Finite
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem splits_map_iff (j : L →+* F) {f : K[X]} : Splits j (f.map i) ↔ Splits (j.comp i) f

Proof state:
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
j : L →+* F
f : K[X]
⊢ Splits j (map i f) ↔ Splits (j.comp i) f

Tactic:
simp [Splits, Polynomial.map_map]

Result:
no goals
-- Mathlib/Data/Real/Cardinality.lean
theorem cantorFunctionAux_true (h : f n = true) : cantorFunctionAux c f n = c ^ n

Proof state:
c : ℝ
f : ℕ → Bool
n : ℕ
h : f n = true
⊢ cantorFunctionAux c f n = c ^ n

Tactic:
simp [cantorFunctionAux, h]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem ae_bdd_liminf_atTop_rpow_of_eLpNorm_bdd {p : ℝ≥0∞} {f : ℕ → α → E}
    (hfmeas : ∀ n, Measurable (f n)) (hbdd : ∀ n, eLpNorm (f n) p μ ≤ R) :
    ∀ᵐ x ∂μ, liminf (fun n => ((‖f n x‖ₑ) ^ p.toReal : ℝ≥0∞)) atTop < ∞

Proof state:
case pos.h
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : p.toReal = 0
a✝ : α
⊢ 1 < ⊤

Tactic:
exact ENNReal.one_lt_top

Result:
no goals

Proof state:
case neg
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : ¬p.toReal = 0
hp : p ≠ 0
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => ‖f n x‖ₑ ^ p.toReal) atTop < ⊤

Tactic:
have hp' : p ≠ ∞ := fun h => by simp [h] at hp0

Result:
case neg
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : ¬p.toReal = 0
hp : p ≠ 0
hp' : p ≠ ⊤
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => ‖f n x‖ₑ ^ p.toReal) atTop < ⊤

Proof state:
case pos.h
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : p.toReal = 0
a✝ : α
⊢ liminf (fun n => 1) atTop < ⊤

Tactic:
rw [liminf_const (1 : ℝ≥0∞)]

Result:
case pos.h
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : p.toReal = 0
a✝ : α
⊢ 1 < ⊤
-- Mathlib/Topology/EMetricSpace/Defs.lean
theorem EMetricSpace.ext
    {α : Type*} {m m' : EMetricSpace α} (h : m.toEDist = m'.toEDist) : m = m'

Proof state:
case mk.mk.e_toPseudoEMetricSpace
α : Type u_2
toPseudoEMetricSpace✝¹ : PseudoEMetricSpace α
eq_of_edist_eq_zero✝¹ : ∀ {x y : α}, edist x y = 0 → x = y
toPseudoEMetricSpace✝ : PseudoEMetricSpace α
eq_of_edist_eq_zero✝ : ∀ {x y : α}, edist x y = 0 → x = y
h : PseudoEMetricSpace.toEDist = PseudoEMetricSpace.toEDist
⊢ toPseudoEMetricSpace✝¹ = toPseudoEMetricSpace✝

Tactic:
ext1

Result:
case mk.mk.e_toPseudoEMetricSpace.h
α : Type u_2
toPseudoEMetricSpace✝¹ : PseudoEMetricSpace α
eq_of_edist_eq_zero✝¹ : ∀ {x y : α}, edist x y = 0 → x = y
toPseudoEMetricSpace✝ : PseudoEMetricSpace α
eq_of_edist_eq_zero✝ : ∀ {x y : α}, edist x y = 0 → x = y
h : PseudoEMetricSpace.toEDist = PseudoEMetricSpace.toEDist
⊢ PseudoEMetricSpace.toEDist = PseudoEMetricSpace.toEDist

Proof state:
case mk.mk.e_toPseudoEMetricSpace.h
α : Type u_2
toPseudoEMetricSpace✝¹ : PseudoEMetricSpace α
eq_of_edist_eq_zero✝¹ : ∀ {x y : α}, edist x y = 0 → x = y
toPseudoEMetricSpace✝ : PseudoEMetricSpace α
eq_of_edist_eq_zero✝ : ∀ {x y : α}, edist x y = 0 → x = y
h : PseudoEMetricSpace.toEDist = PseudoEMetricSpace.toEDist
⊢ PseudoEMetricSpace.toEDist = PseudoEMetricSpace.toEDist

Tactic:
assumption

Result:
no goals

Proof state:
case mk.mk
α : Type u_2
toPseudoEMetricSpace✝¹ : PseudoEMetricSpace α
eq_of_edist_eq_zero✝¹ : ∀ {x y : α}, edist x y = 0 → x = y
toPseudoEMetricSpace✝ : PseudoEMetricSpace α
eq_of_edist_eq_zero✝ : ∀ {x y : α}, edist x y = 0 → x = y
h : PseudoEMetricSpace.toEDist = PseudoEMetricSpace.toEDist
⊢ mk eq_of_edist_eq_zero✝¹ = mk eq_of_edist_eq_zero✝

Tactic:
congr

Result:
case mk.mk.e_toPseudoEMetricSpace
α : Type u_2
toPseudoEMetricSpace✝¹ : PseudoEMetricSpace α
eq_of_edist_eq_zero✝¹ : ∀ {x y : α}, edist x y = 0 → x = y
toPseudoEMetricSpace✝ : PseudoEMetricSpace α
eq_of_edist_eq_zero✝ : ∀ {x y : α}, edist x y = 0 → x = y
h : PseudoEMetricSpace.toEDist = PseudoEMetricSpace.toEDist
⊢ toPseudoEMetricSpace✝¹ = toPseudoEMetricSpace✝

Proof state:
α : Type u_2
m m' : EMetricSpace α
h : PseudoEMetricSpace.toEDist = PseudoEMetricSpace.toEDist
⊢ m = m'

Tactic:
cases m

Result:
case mk
α : Type u_2
m' : EMetricSpace α
toPseudoEMetricSpace✝ : PseudoEMetricSpace α
eq_of_edist_eq_zero✝ : ∀ {x y : α}, edist x y = 0 → x = y
h : PseudoEMetricSpace.toEDist = PseudoEMetricSpace.toEDist
⊢ mk eq_of_edist_eq_zero✝ = m'

Proof state:
case mk
α : Type u_2
m' : EMetricSpace α
toPseudoEMetricSpace✝ : PseudoEMetricSpace α
eq_of_edist_eq_zero✝ : ∀ {x y : α}, edist x y = 0 → x = y
h : PseudoEMetricSpace.toEDist = PseudoEMetricSpace.toEDist
⊢ mk eq_of_edist_eq_zero✝ = m'

Tactic:
cases m'

Result:
case mk.mk
α : Type u_2
toPseudoEMetricSpace✝¹ : PseudoEMetricSpace α
eq_of_edist_eq_zero✝¹ : ∀ {x y : α}, edist x y = 0 → x = y
toPseudoEMetricSpace✝ : PseudoEMetricSpace α
eq_of_edist_eq_zero✝ : ∀ {x y : α}, edist x y = 0 → x = y
h : PseudoEMetricSpace.toEDist = PseudoEMetricSpace.toEDist
⊢ mk eq_of_edist_eq_zero✝¹ = mk eq_of_edist_eq_zero✝
-- Mathlib/RingTheory/Ideal/Norm/RelNorm.lean
theorem map_spanIntNorm (I : Ideal S) {T : Type*} [CommRing T] (f : R →+* T) :
    map f (spanNorm R I) = span (f ∘ Algebra.intNorm R S '' (I : Set S))

Proof state:
R : Type u_1
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
S : Type u_3
inst✝⁸ : CommRing S
inst✝⁷ : IsDomain S
inst✝⁶ : IsIntegrallyClosed R
inst✝⁵ : IsIntegrallyClosed S
inst✝⁴ : Algebra R S
inst✝³ : Module.Finite R S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
I : Ideal S
T : Type u_4
inst✝ : CommRing T
f : R →+* T
⊢ map f (spanNorm R I) = span (⇑f ∘ ⇑(Algebra.intNorm R S) '' ↑I)

Tactic:
rw [spanNorm]

Result:
R : Type u_1
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
S : Type u_3
inst✝⁸ : CommRing S
inst✝⁷ : IsDomain S
inst✝⁶ : IsIntegrallyClosed R
inst✝⁵ : IsIntegrallyClosed S
inst✝⁴ : Algebra R S
inst✝³ : Module.Finite R S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
I : Ideal S
T : Type u_4
inst✝ : CommRing T
f : R →+* T
⊢ map f (map (Algebra.intNorm R S) I) = span (⇑f ∘ ⇑(Algebra.intNorm R S) '' ↑I)

Proof state:
R : Type u_1
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
S : Type u_3
inst✝⁸ : CommRing S
inst✝⁷ : IsDomain S
inst✝⁶ : IsIntegrallyClosed R
inst✝⁵ : IsIntegrallyClosed S
inst✝⁴ : Algebra R S
inst✝³ : Module.Finite R S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
I : Ideal S
T : Type u_4
inst✝ : CommRing T
f : R →+* T
⊢ map f (map (Algebra.intNorm R S) I) = span (⇑f ∘ ⇑(Algebra.intNorm R S) '' ↑I)

Tactic:
nth_rw 2 [map]

Result:
R : Type u_1
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
S : Type u_3
inst✝⁸ : CommRing S
inst✝⁷ : IsDomain S
inst✝⁶ : IsIntegrallyClosed R
inst✝⁵ : IsIntegrallyClosed S
inst✝⁴ : Algebra R S
inst✝³ : Module.Finite R S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
I : Ideal S
T : Type u_4
inst✝ : CommRing T
f : R →+* T
⊢ map f (span (⇑(Algebra.intNorm R S) '' ↑I)) = span (⇑f ∘ ⇑(Algebra.intNorm R S) '' ↑I)

Proof state:
R : Type u_1
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
S : Type u_3
inst✝⁸ : CommRing S
inst✝⁷ : IsDomain S
inst✝⁶ : IsIntegrallyClosed R
inst✝⁵ : IsIntegrallyClosed S
inst✝⁴ : Algebra R S
inst✝³ : Module.Finite R S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
I : Ideal S
T : Type u_4
inst✝ : CommRing T
f : R →+* T
⊢ map f (span (⇑(Algebra.intNorm R S) '' ↑I)) = span (⇑f ∘ ⇑(Algebra.intNorm R S) '' ↑I)

Tactic:
simp [map_span, Set.image_image]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean
/-- The composition of the derivative of the inverse of `extChartAt` with the derivative of
`extChartAt` gives the identity.
Version where the basepoint belongs to `(extChartAt I x).source`. -/
lemma mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt'
    {y : M} (hy : y ∈ (extChartAt I x).source) :
    (mfderivWithin 𝓘(𝕜, E) I (extChartAt I x).symm (range I) (extChartAt I x y)) ∘L
      (mfderiv I 𝓘(𝕜, E) (extChartAt I x) y)
      = ContinuousLinearMap.id _ _

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x y : M
hy : y ∈ (extChartAt I x).source
this : y = ↑(extChartAt I x).symm (↑(extChartAt I x) y)
⊢ (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) y)).comp
      (mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) y) =
    ContinuousLinearMap.id 𝕜 (TangentSpace I y)

Tactic:
convert mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt ((extChartAt I x).map_source hy)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x y : M
hy : y ∈ (extChartAt I x).source
⊢ (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) y)).comp
      (mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) y) =
    ContinuousLinearMap.id 𝕜 (TangentSpace I y)

Tactic:
have : y = (extChartAt I x).symm (extChartAt I x y) := ((extChartAt I x).left_inv hy).symm

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x y : M
hy : y ∈ (extChartAt I x).source
this : y = ↑(extChartAt I x).symm (↑(extChartAt I x) y)
⊢ (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) y)).comp
      (mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) y) =
    ContinuousLinearMap.id 𝕜 (TangentSpace I y)
-- Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean
lemma isHomological_of_localization (L : C ⥤ D)
    [L.CommShift ℤ] [L.IsTriangulated] [L.mapArrow.EssSurj] (F : D ⥤ A)
    (G : C ⥤ A) (e : L ⋙ F ≅ G) [G.IsHomological] :
    F.IsHomological

Proof state:
C : Type u_1
D : Type u_2
A : Type u_3
inst✝¹⁷ : Category.{u_4, u_1} C
inst✝¹⁶ : HasShift C ℤ
inst✝¹⁵ : Category.{u_5, u_2} D
inst✝¹⁴ : HasZeroObject D
inst✝¹³ : HasShift D ℤ
inst✝¹² : Preadditive D
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹⁰ : Pretriangulated D
inst✝⁹ : Category.{u_6, u_3} A
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Abelian A
L : C ⥤ D
inst✝³ : L.CommShift ℤ
inst✝² : L.IsTriangulated
inst✝¹ : L.mapArrow.EssSurj
F : D ⥤ A
G : C ⥤ A
e : L ⋙ F ≅ G
inst✝ : G.IsHomological
⊢ F.IsHomological

Tactic:
have : F.PreservesZeroMorphisms := preservesZeroMorphisms_of_map_zero_object
  (F.mapIso L.mapZeroObject.symm ≪≫ e.app _ ≪≫ G.mapZeroObject)

Result:
C : Type u_1
D : Type u_2
A : Type u_3
inst✝¹⁷ : Category.{u_4, u_1} C
inst✝¹⁶ : HasShift C ℤ
inst✝¹⁵ : Category.{u_5, u_2} D
inst✝¹⁴ : HasZeroObject D
inst✝¹³ : HasShift D ℤ
inst✝¹² : Preadditive D
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹⁰ : Pretriangulated D
inst✝⁹ : Category.{u_6, u_3} A
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Abelian A
L : C ⥤ D
inst✝³ : L.CommShift ℤ
inst✝² : L.IsTriangulated
inst✝¹ : L.mapArrow.EssSurj
F : D ⥤ A
G : C ⥤ A
e : L ⋙ F ≅ G
inst✝ : G.IsHomological
this : F.PreservesZeroMorphisms
⊢ F.IsHomological
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem EuclideanSpace.orthonormal_single :
    Orthonormal 𝕜 fun i : ι => EuclideanSpace.single i (1 : 𝕜)

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ Orthonormal 𝕜 fun i => single i 1

Tactic:
simp_rw [orthonormal_iff_ite, EuclideanSpace.inner_single_left, map_one, one_mul,
  EuclideanSpace.single_apply]

Result:
ι : Type u_1
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ ι → ι → True

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ ι → ι → True

Tactic:
intros

Result:
ι : Type u_1
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i✝ j✝ : ι
⊢ True

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i✝ j✝ : ι
⊢ True

Tactic:
trivial

Result:
no goals
-- Mathlib/Analysis/Normed/Module/FiniteDimension.lean
theorem LipschitzOnWith.extend_finite_dimension {α : Type*} [PseudoMetricSpace α] {E' : Type*}
    [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {s : Set α} {f : α → E'}
    {K : ℝ≥0} (hf : LipschitzOnWith K f s) :
    ∃ g : α → E', LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ EqOn f g s

Proof state:
case intro.intro.refine_1
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv
LA : LipschitzWith ‖↑A‖₊ ⇑A
L : LipschitzOnWith (‖↑A‖₊ * K) (⇑A ∘ f) s
g : α → ι → ℝ
hg : LipschitzWith (‖↑A‖₊ * K) g
gs : EqOn (⇑A ∘ f) g s
LAsymm : LipschitzWith ‖↑A.symm‖₊ ⇑A.symm
⊢ ‖↑A.symm‖₊ * (‖↑A‖₊ * K) ≤ lipschitzExtensionConstant E' * K

Tactic:
rw [lipschitzExtensionConstant, ← mul_assoc]

Result:
case intro.intro.refine_1
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv
LA : LipschitzWith ‖↑A‖₊ ⇑A
L : LipschitzOnWith (‖↑A‖₊ * K) (⇑A ∘ f) s
g : α → ι → ℝ
hg : LipschitzWith (‖↑A‖₊ * K) g
gs : EqOn (⇑A ∘ f) g s
LAsymm : LipschitzWith ‖↑A.symm‖₊ ⇑A.symm
⊢ ‖↑A.symm‖₊ * ‖↑A‖₊ * K ≤
    (let A := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv;
      ‖↑A.symm‖₊ * ‖↑A‖₊ ⊔ 1) *
      K
-- Mathlib/Combinatorics/Colex.lean
/-- `s < {a}` in colex iff all elements of `s` are strictly less than `a`. -/
lemma toColex_lt_singleton : toColex s < toColex {a} ↔ ∀ b ∈ s, b < a

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
⊢ { ofColex := s } < { ofColex := {a} } ↔ ∀ b ∈ s, b < a

Tactic:
rw [lt_iff_le_and_ne, toColex_le_singleton, toColex_ne_toColex]

Result:
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
⊢ (∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)) ∧ s ≠ {a} ↔ ∀ b ∈ s, b < a

Proof state:
case refine_1
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
b : α
hb : b ∈ s
h : (∀ b_1 ∈ s, b_1 ≤ b ∧ (b ∈ s → b_1 = b)) ∧ s ≠ {b}
⊢ False

Tactic:
refine h.2 <| eq_singleton_iff_unique_mem.2 ⟨hb, fun c hc ↦ (h.1 _ hc).2 hb⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
⊢ (∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)) ∧ s ≠ {a} ↔ ∀ b ∈ s, b < a

Tactic:
refine ⟨fun h b hb ↦ (h.1 _ hb).1.lt_of_ne ?_,
  fun h ↦ ⟨fun b hb ↦ ⟨(h _ hb).le, fun ha ↦ (lt_irrefl _ <| h _ ha).elim⟩, ?_⟩⟩ <;> rintro rfl

Result:
case refine_1
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
b : α
hb : b ∈ s
h : (∀ b_1 ∈ s, b_1 ≤ b ∧ (b ∈ s → b_1 = b)) ∧ s ≠ {b}
⊢ False

case refine_2
α : Type u_1
inst✝ : PartialOrder α
a : α
h : ∀ b ∈ {a}, b < a
⊢ False

Proof state:
case refine_2
α : Type u_1
inst✝ : PartialOrder α
a : α
h : ∀ b ∈ {a}, b < a
⊢ False

Tactic:
simp at h

Result:
no goals
-- Mathlib/NumberTheory/LucasLehmer.lean
lemma testFalseHelper (p : ℕ) (hp : Nat.blt 1 p = true)
    (h : Nat.ble 1 (sModNatTR (2 ^ p - 1) (p - 2))) : ¬ LucasLehmerTest p

Proof state:
p : ℕ
hp : 1 < p
h : Nat.ble 1 (sModNatTR (2 ^ p - 1) (p - 2)) = true
⊢ ¬LucasLehmerTest p

Tactic:
rw [Nat.ble_eq, Nat.succ_le, Nat.pos_iff_ne_zero] at h

Result:
p : ℕ
hp : 1 < p
h : sModNatTR (2 ^ p - 1) (p - 2) ≠ 0
⊢ ¬LucasLehmerTest p

Proof state:
p : ℕ
hp : Nat.blt 1 p = true
h : Nat.ble 1 (sModNatTR (2 ^ p - 1) (p - 2)) = true
⊢ ¬LucasLehmerTest p

Tactic:
rw [Nat.blt_eq] at hp

Result:
p : ℕ
hp : 1 < p
h : Nat.ble 1 (sModNatTR (2 ^ p - 1) (p - 2)) = true
⊢ ¬LucasLehmerTest p

Proof state:
p : ℕ
hp : 1 < p
h : sModNatTR (2 ^ p - 1) (p - 2) ≠ 0
⊢ ¬LucasLehmerTest p

Tactic:
rw [LucasLehmerTest, LucasLehmer.residue_eq_zero_iff_sMod_eq_zero p hp, ← sModNat_eq_sMod p _ hp,
  ← sModNatTR_eq_sModNat]

Result:
p : ℕ
hp : 1 < p
h : sModNatTR (2 ^ p - 1) (p - 2) ≠ 0
⊢ ¬↑(sModNatTR (2 ^ p - 1) (p - 2)) = 0

Proof state:
p : ℕ
hp : 1 < p
h : sModNatTR (2 ^ p - 1) (p - 2) ≠ 0
⊢ ¬↑(sModNatTR (2 ^ p - 1) (p - 2)) = 0

Tactic:
simpa using h

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/Construction.lean
@[reassoc (attr := simp)]
lemma ιFunctorObj_naturality :
    ιFunctorObj f πX ≫ functorMap f τ = τ.left ≫ ιFunctorObj f πY

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S T X Y : C
πX : X ⟶ S
πY : Y ⟶ T
τ : Arrow.mk πX ⟶ Arrow.mk πY
inst✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝² : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C
inst✝¹ : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
inst✝ : HasPushout (functorObjTop f πY) (functorObjLeft f πY)
⊢ ιFunctorObj f πX ≫ functorMap f τ = τ.left ≫ ιFunctorObj f πY

Tactic:
simp [ιFunctorObj, functorMap]

Result:
no goals
-- Mathlib/LinearAlgebra/DFinsupp.lean
theorem iSup_range_lsingle : ⨆ i, LinearMap.range (lsingle (R := R) (M := M) i) = ⊤ :=
  top_le_iff.mp fun m _ ↦ by
    rw [← LinearMap.id_apply (R := R) m, ← lsum_lsingle ℕ]
    exact dfinsupp_sumAddHom_mem _ _ _ fun i _ ↦ Submodule.mem_iSup_of_mem i ⟨_, rfl⟩

Proof state:
ι : Type u_1
R : Type u_2
M : ι → Type u_4
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
m : Π₀ (i : ι), M i
x✝ : m ∈ ⊤
⊢ m ∈ ⨆ i, LinearMap.range (lsingle i)

Tactic:
rw [← LinearMap.id_apply (R := R) m, ← lsum_lsingle ℕ]

Result:
ι : Type u_1
R : Type u_2
M : ι → Type u_4
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
m : Π₀ (i : ι), M i
x✝ : m ∈ ⊤
⊢ ((lsum ℕ) lsingle) m ∈ ⨆ i, LinearMap.range (lsingle i)

Proof state:
ι : Type u_1
R : Type u_2
M : ι → Type u_4
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
m : Π₀ (i : ι), M i
x✝ : m ∈ ⊤
⊢ ((lsum ℕ) lsingle) m ∈ ⨆ i, LinearMap.range (lsingle i)

Tactic:
exact dfinsupp_sumAddHom_mem _ _ _ fun i _ ↦ Submodule.mem_iSup_of_mem i ⟨_, rfl⟩

Result:
no goals