harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Compactness/Lindelof.lean
theorem IsLindelof.elim_countable_subfamily_closed {ι : Type v} (hs : IsLindelof s)
    (t : ι → Set X) (htc : ∀ i, IsClosed (t i)) (hst : (s ∩ ⋂ i, t i) = ∅) :
    ∃ u : Set ι, u.Countable ∧ (s ∩ ⋂ i ∈ u, t i) = ∅

Proof state:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed (t i)
hst : s ∩ ⋂ i, t i = ∅
U : ι → Set X := tᶜ
hUo : ∀ (i : ι), IsOpen (U i)
hsU : s ⊆ ⋃ i, U i
u : Set ι
hucount : u.Countable
husub : s ⊆ ⋃ i ∈ u, U i
⊢ ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅

Tactic:
use u, hucount

Result:
case right
X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed (t i)
hst : s ∩ ⋂ i, t i = ∅
U : ι → Set X := tᶜ
hUo : ∀ (i : ι), IsOpen (U i)
hsU : s ⊆ ⋃ i, U i
u : Set ι
hucount : u.Countable
husub : s ⊆ ⋃ i ∈ u, U i
⊢ s ∩ ⋂ i ∈ u, t i = ∅

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed (t i)
hst : s ∩ ⋂ i, t i = ∅
U : ι → Set X := tᶜ
⊢ ∀ (i : ι), IsClosed (t i)

Tactic:
exact htc

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed (t i)
hst : s ∩ ⋂ i, t i = ∅
⊢ ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅

Tactic:
let U := tᶜ

Result:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed (t i)
hst : s ∩ ⋂ i, t i = ∅
U : ι → Set X := tᶜ
⊢ ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅
-- Mathlib/RingTheory/Spectrum/Maximal/Localization.lean
theorem mapPiLocalization_bijective (hf : Function.Bijective f) :
    Function.Bijective (mapPiLocalization f)

Proof state:
case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ (mapPiLocalization ↑f.symm).comp (mapPiLocalization ↑f) = RingHom.id (PiLocalization R)

Tactic:
rw [← mapPiLocalization_comp, RingEquiv.symm_comp, mapPiLocalization_id]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ Function.Bijective ⇑(mapPiLocalization f✝)

Tactic:
let e := RingEquiv.ofRingHom (mapPiLocalization (f : R →+* S)) (mapPiLocalization f.symm) ?_ ?_

Result:
case refine_3
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
e : PiLocalization R ≃+* PiLocalization S :=
  RingEquiv.ofRingHom (mapPiLocalization ↑f) (mapPiLocalization ↑f.symm) ?refine_1 ?refine_2
⊢ Function.Bijective ⇑(mapPiLocalization f✝)

case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ (mapPiLocalization ↑f).comp (mapPiLocalization ↑f.symm) = RingHom.id (PiLocalization S)

case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ (mapPiLocalization ↑f.symm).comp (mapPiLocalization ↑f) = RingHom.id (PiLocalization R)

Proof state:
case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ (mapPiLocalization ↑f).comp (mapPiLocalization ↑f.symm) = RingHom.id (PiLocalization S)

Tactic:
rw [← mapPiLocalization_comp, RingEquiv.comp_symm, mapPiLocalization_id]

Result:
no goals

Proof state:
case refine_3
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
e : PiLocalization R ≃+* PiLocalization S :=
  RingEquiv.ofRingHom (mapPiLocalization ↑f) (mapPiLocalization ↑f.symm) ?refine_1 ?refine_2
⊢ Function.Bijective ⇑(mapPiLocalization f✝)

Tactic:
exact e.bijective

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Bijective ⇑f
⊢ Function.Bijective ⇑(mapPiLocalization f)

Tactic:
let f := RingEquiv.ofBijective f hf

Result:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ Function.Bijective ⇑(mapPiLocalization f✝)
-- Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean
theorem IsIntegral.algebraMap [Algebra A B] [IsScalarTower R A B] {x : A}
    (h : IsIntegral R x) : IsIntegral R (algebraMap A B x)

Proof state:
case intro.intro
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
x : A
f : R[X]
hf : f.Monic
hx : eval₂ (algebraMap R A) x f = 0
⊢ IsIntegral R ((algebraMap A B) x)

Tactic:
use f, hf

Result:
case right
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
x : A
f : R[X]
hf : f.Monic
hx : eval₂ (algebraMap R A) x f = 0
⊢ eval₂ (algebraMap R B) ((algebraMap A B) x) f = 0

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
x : A
h : IsIntegral R x
⊢ IsIntegral R ((algebraMap A B) x)

Tactic:
rcases h with ⟨f, hf, hx⟩

Result:
case intro.intro
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
x : A
f : R[X]
hf : f.Monic
hx : eval₂ (algebraMap R A) x f = 0
⊢ IsIntegral R ((algebraMap A B) x)

Proof state:
case right
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
x : A
f : R[X]
hf : f.Monic
hx : eval₂ (algebraMap R A) x f = 0
⊢ eval₂ (algebraMap R B) ((algebraMap A B) x) f = 0

Tactic:
rw [IsScalarTower.algebraMap_eq R A B, ← hom_eval₂, hx, RingHom.map_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem pairwise_le_range' s n (step := 1) :
    Pairwise (· ≤ ·) (range' s n step) :=
  match s, n, step with
  | _, 0, _ => Pairwise.nil
  | s, n + 1, step => by
    simp only [range'_succ, pairwise_cons]
    constructor
    · intros n m
      rw [mem_range'] at m
      omega
    · exact pairwise_le_range' (s + step) n step

Proof state:
case right
s✝ n✝ : Nat
step✝ : optParam Nat 1
s n : Nat
step : optParam Nat 1
⊢ Pairwise (fun x1 x2 => x1 ≤ x2) (range' (s + step) n step)

Tactic:
exact pairwise_le_range' (s + step) n step

Result:
no goals

Proof state:
case left
s✝ n✝ : Nat
step✝ : optParam Nat 1
s n : Nat
step : optParam Nat 1
⊢ ∀ (a' : Nat), a' ∈ range' (s + step) n step → s ≤ a'

Tactic:
intros n m

Result:
case left
s✝ n✝¹ : Nat
step✝ : optParam Nat 1
s n✝ : Nat
step : optParam Nat 1
n : Nat
m : n ∈ range' (s + step) n✝ step
⊢ s ≤ n

Proof state:
s✝ n✝ : Nat
step✝ : optParam Nat 1
s n : Nat
step : optParam Nat 1
⊢ Pairwise (fun x1 x2 => x1 ≤ x2) (range' s (n + 1) step)

Tactic:
simp only [range'_succ, pairwise_cons]

Result:
s✝ n✝ : Nat
step✝ : optParam Nat 1
s n : Nat
step : optParam Nat 1
⊢ (∀ (a' : Nat), a' ∈ range' (s + step) n step → s ≤ a') ∧ Pairwise (fun x1 x2 => x1 ≤ x2) (range' (s + step) n step)

Proof state:
case left
s✝ n✝¹ : Nat
step✝ : optParam Nat 1
s n✝ : Nat
step : optParam Nat 1
n : Nat
m : n ∈ range' (s + step) n✝ step
⊢ s ≤ n

Tactic:
rw [mem_range'] at m

Result:
case left
s✝ n✝¹ : Nat
step✝ : optParam Nat 1
s n✝ : Nat
step : optParam Nat 1
n : Nat
m : ∃ i, i < n✝ ∧ n = s + step + step * i
⊢ s ≤ n

Proof state:
s✝ n✝ : Nat
step✝ : optParam Nat 1
s n : Nat
step : optParam Nat 1
⊢ (∀ (a' : Nat), a' ∈ range' (s + step) n step → s ≤ a') ∧ Pairwise (fun x1 x2 => x1 ≤ x2) (range' (s + step) n step)

Tactic:
constructor

Result:
case left
s✝ n✝ : Nat
step✝ : optParam Nat 1
s n : Nat
step : optParam Nat 1
⊢ ∀ (a' : Nat), a' ∈ range' (s + step) n step → s ≤ a'

case right
s✝ n✝ : Nat
step✝ : optParam Nat 1
s n : Nat
step : optParam Nat 1
⊢ Pairwise (fun x1 x2 => x1 ≤ x2) (range' (s + step) n step)

Proof state:
case left
s✝ n✝¹ : Nat
step✝ : optParam Nat 1
s n✝ : Nat
step : optParam Nat 1
n : Nat
m : ∃ i, i < n✝ ∧ n = s + step + step * i
⊢ s ≤ n

Tactic:
omega

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean
theorem Basis.prod_addHaar (v : Basis ι ℝ E) (w : Basis ι' ℝ F) :
    (v.prod w).addHaar = v.addHaar.prod w.addHaar

Proof state:
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹⁰ : Fintype ι
inst✝⁹ : Fintype ι'
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : SecondCountableTopologyEither E F
v : Basis ι ℝ E
w : Basis ι' ℝ F
⊢ (v.prod w).addHaar = v.addHaar.prod w.addHaar

Tactic:
have : FiniteDimensional ℝ E := FiniteDimensional.of_fintype_basis v

Result:
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹⁰ : Fintype ι
inst✝⁹ : Fintype ι'
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : SecondCountableTopologyEither E F
v : Basis ι ℝ E
w : Basis ι' ℝ F
this : FiniteDimensional ℝ E
⊢ (v.prod w).addHaar = v.addHaar.prod w.addHaar

Proof state:
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹⁰ : Fintype ι
inst✝⁹ : Fintype ι'
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : SecondCountableTopologyEither E F
v : Basis ι ℝ E
w : Basis ι' ℝ F
this✝ : FiniteDimensional ℝ E
this : FiniteDimensional ℝ F
⊢ (v.prod w).addHaar = v.addHaar.prod w.addHaar

Tactic:
simp [(v.prod w).addHaar_eq_iff, Basis.prod_parallelepiped, Basis.addHaar_self]

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹⁰ : Fintype ι
inst✝⁹ : Fintype ι'
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : SecondCountableTopologyEither E F
v : Basis ι ℝ E
w : Basis ι' ℝ F
this : FiniteDimensional ℝ E
⊢ (v.prod w).addHaar = v.addHaar.prod w.addHaar

Tactic:
have : FiniteDimensional ℝ F := FiniteDimensional.of_fintype_basis w

Result:
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹⁰ : Fintype ι
inst✝⁹ : Fintype ι'
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : SecondCountableTopologyEither E F
v : Basis ι ℝ E
w : Basis ι' ℝ F
this✝ : FiniteDimensional ℝ E
this : FiniteDimensional ℝ F
⊢ (v.prod w).addHaar = v.addHaar.prod w.addHaar
-- Mathlib/Topology/Algebra/FilterBasis.lean
theorem N_one (B : GroupFilterBasis G) : B.N 1 = B.toFilterBasis.filter

Proof state:
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ B.N 1 = toFilterBasis.filter

Tactic:
simp only [N, one_mul, map_id']

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem log_pow (x : ℝ) (n : ℕ) : log (x ^ n) = n * log x

Proof state:
case succ.inr
x : ℝ
n : ℕ
ih : log (x ^ n) = ↑n * log x
hx : x ≠ 0
⊢ log (x ^ (n + 1)) = ↑(n + 1) * log x

Tactic:
rw [pow_succ, log_mul (pow_ne_zero _ hx) hx, ih, Nat.cast_succ, add_mul, one_mul]

Result:
no goals

Proof state:
case zero
x : ℝ
⊢ log (x ^ 0) = ↑0 * log x

Tactic:
simp

Result:
no goals

Proof state:
case succ.inl
n : ℕ
ih : log (0 ^ n) = ↑n * log 0
⊢ log (0 ^ (n + 1)) = ↑(n + 1) * log 0

Tactic:
simp

Result:
no goals

Proof state:
case succ
x : ℝ
n : ℕ
ih : log (x ^ n) = ↑n * log x
⊢ log (x ^ (n + 1)) = ↑(n + 1) * log x

Tactic:
rcases eq_or_ne x 0 with (rfl | hx)

Result:
case succ.inl
n : ℕ
ih : log (0 ^ n) = ↑n * log 0
⊢ log (0 ^ (n + 1)) = ↑(n + 1) * log 0

case succ.inr
x : ℝ
n : ℕ
ih : log (x ^ n) = ↑n * log x
hx : x ≠ 0
⊢ log (x ^ (n + 1)) = ↑(n + 1) * log x
-- Mathlib/Algebra/Order/Archimedean/Basic.lean
lemma exists_nat_one_div_lt (hε : 0 < ε) : ∃ n : ℕ, 1 / (n + 1 : α) < ε

Proof state:
case h
α : Type u_1
inst✝¹ : LinearOrderedSemifield α
inst✝ : Archimedean α
ε : α
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ 1 / (↑n + 1) < ε

Tactic:
rw [div_lt_iff₀, ← div_lt_iff₀' hε]

Result:
case h
α : Type u_1
inst✝¹ : LinearOrderedSemifield α
inst✝ : Archimedean α
ε : α
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ 1 / ε < ↑n + 1

case h
α : Type u_1
inst✝¹ : LinearOrderedSemifield α
inst✝ : Archimedean α
ε : α
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ 0 < ↑n + 1

Proof state:
case h
α : Type u_1
inst✝¹ : LinearOrderedSemifield α
inst✝ : Archimedean α
ε : α
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ 1 / ε < ↑n + 1

Tactic:
apply hn.trans

Result:
case h
α : Type u_1
inst✝¹ : LinearOrderedSemifield α
inst✝ : Archimedean α
ε : α
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ ↑n < ↑n + 1

Proof state:
case h
α : Type u_1
inst✝¹ : LinearOrderedSemifield α
inst✝ : Archimedean α
ε : α
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ 0 < ↑n + 1

Tactic:
exact n.cast_add_one_pos

Result:
no goals

Proof state:
case intro
α : Type u_1
inst✝¹ : LinearOrderedSemifield α
inst✝ : Archimedean α
ε : α
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ ∃ n, 1 / (↑n + 1) < ε

Tactic:
use n

Result:
case h
α : Type u_1
inst✝¹ : LinearOrderedSemifield α
inst✝ : Archimedean α
ε : α
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ 1 / (↑n + 1) < ε

Proof state:
case h
α : Type u_1
inst✝¹ : LinearOrderedSemifield α
inst✝ : Archimedean α
ε : α
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ ↑n < ↑n + 1

Tactic:
simp [zero_lt_one]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedSemifield α
inst✝ : Archimedean α
ε : α
hε : 0 < ε
⊢ ∃ n, 1 / (↑n + 1) < ε

Tactic:
obtain ⟨n, hn⟩ := exists_nat_gt (1 / ε)

Result:
case intro
α : Type u_1
inst✝¹ : LinearOrderedSemifield α
inst✝ : Archimedean α
ε : α
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ ∃ n, 1 / (↑n + 1) < ε
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tendsto_nhds_of_Icc {f : Filter α} {u : α → ℝ≥0∞} {a : ℝ≥0∞}
    (h : ∀ ε > 0, ∀ᶠ x in f, u x ∈ Icc (a - ε) (a + ε)) : Tendsto u f (𝓝 a)

Proof state:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
h : ∀ ε > 0, ∀ᶠ (x : α) in f, u x ∈ Icc (a - ε) (a + ε)
⊢ Tendsto u f (𝓝 a)

Tactic:
refine Tendsto.mono_right ?_ (biInf_le_nhds _)

Result:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
h : ∀ ε > 0, ∀ᶠ (x : α) in f, u x ∈ Icc (a - ε) (a + ε)
⊢ Tendsto u f (⨅ ε, ⨅ (_ : ε > 0), 𝓟 (Icc (a - ε) (a + ε)))

Proof state:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
h : ∀ ε > 0, ∀ᶠ (x : α) in f, u x ∈ Icc (a - ε) (a + ε)
⊢ Tendsto u f (⨅ ε, ⨅ (_ : ε > 0), 𝓟 (Icc (a - ε) (a + ε)))

Tactic:
simpa only [tendsto_iInf, tendsto_principal]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Convolution.lean
lemma toArithmeticFunction_congr {R : Type*} [Zero R] {f f' : ℕ → R}
    (h : ∀ {n}, n ≠ 0 → f n = f' n) :
    toArithmeticFunction f = toArithmeticFunction f'

Proof state:
R : Type u_1
inst✝ : Zero R
f f' : ℕ → R
h : ∀ {n : ℕ}, n ≠ 0 → f n = f' n
⊢ toArithmeticFunction f = toArithmeticFunction f'

Tactic:
ext

Result:
case h
R : Type u_1
inst✝ : Zero R
f f' : ℕ → R
h : ∀ {n : ℕ}, n ≠ 0 → f n = f' n
x✝ : ℕ
⊢ (toArithmeticFunction f) x✝ = (toArithmeticFunction f') x✝

Proof state:
case h
R : Type u_1
inst✝ : Zero R
f f' : ℕ → R
h : ∀ {n : ℕ}, n ≠ 0 → f n = f' n
x✝ : ℕ
⊢ (toArithmeticFunction f) x✝ = (toArithmeticFunction f') x✝

Tactic:
simp_all [toArithmeticFunction]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem sum_coe_finset (s : Finset ι) (μ : ι → Measure α) :
    (sum fun i : s => μ i) = ∑ i ∈ s, μ i

Proof state:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
s : Finset ι
μ : ι → Measure α
⊢ (sum fun i => μ ↑i) = ∑ i ∈ s, μ i

Tactic:
rw [sum_fintype, Finset.sum_coe_sort s μ]

Result:
no goals
-- Mathlib/Data/ENNReal/Order.lean
theorem lt_add_of_sub_lt_left (h : a ≠ ∞ ∨ b ≠ ∞) : a - b < c → a < b + c

Proof state:
case inl
a c : ℝ≥0∞
h : a ≠ ⊤ ∨ ⊤ ≠ ⊤
⊢ a - ⊤ < c → a ≠ ⊤

Tactic:
exact fun _ => h.resolve_right (Classical.not_not.2 rfl)

Result:
no goals

Proof state:
a b c : ℝ≥0∞
h : a ≠ ⊤ ∨ b ≠ ⊤
⊢ a - b < c → a < b + c

Tactic:
obtain rfl | hb := eq_or_ne b ∞

Result:
case inl
a c : ℝ≥0∞
h : a ≠ ⊤ ∨ ⊤ ≠ ⊤
⊢ a - ⊤ < c → a < ⊤ + c

case inr
a b c : ℝ≥0∞
h : a ≠ ⊤ ∨ b ≠ ⊤
hb : b ≠ ⊤
⊢ a - b < c → a < b + c

Proof state:
case inl
a c : ℝ≥0∞
h : a ≠ ⊤ ∨ ⊤ ≠ ⊤
⊢ a - ⊤ < c → a < ⊤ + c

Tactic:
rw [top_add, lt_top_iff_ne_top]

Result:
case inl
a c : ℝ≥0∞
h : a ≠ ⊤ ∨ ⊤ ≠ ⊤
⊢ a - ⊤ < c → a ≠ ⊤

Proof state:
case inr
a b c : ℝ≥0∞
h : a ≠ ⊤ ∨ b ≠ ⊤
hb : b ≠ ⊤
⊢ a - b < c → a < b + c

Tactic:
exact (cancel_of_ne hb).lt_add_of_tsub_lt_left

Result:
no goals
-- Mathlib/Data/Set/Subsingleton.lean
theorem Nontrivial.exists_ne (hs : s.Nontrivial) (z) : ∃ x ∈ s, x ≠ z

Proof state:
α : Type u
s : Set α
hs : s.Nontrivial
z : α
H : ∀ x ∈ s, x = z
⊢ False

Tactic:
rcases hs with ⟨x, hx, y, hy, hxy⟩

Result:
case intro.intro.intro.intro
α : Type u
s : Set α
z : α
H : ∀ x ∈ s, x = z
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
⊢ False

Proof state:
case intro.intro.intro.intro
α : Type u
s : Set α
z : α
H : ∀ x ∈ s, x = z
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : z ≠ z
⊢ False

Tactic:
exact hxy rfl

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u
s : Set α
z : α
H : ∀ x ∈ s, x = z
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
⊢ False

Tactic:
rw [H x hx, H y hy] at hxy

Result:
case intro.intro.intro.intro
α : Type u
s : Set α
z : α
H : ∀ x ∈ s, x = z
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : z ≠ z
⊢ False

Proof state:
α : Type u
s : Set α
hs : s.Nontrivial
z : α
⊢ ∃ x ∈ s, x ≠ z

Tactic:
by_contra! H

Result:
α : Type u
s : Set α
hs : s.Nontrivial
z : α
H : ∀ x ∈ s, x = z
⊢ False
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean
lemma FarFromTriangleFree.lt_half (hG : G.FarFromTriangleFree ε) : ε < 2⁻¹

Proof state:
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hG : G.FarFromTriangleFree ε
hε : 2⁻¹ ≤ ε
hε₀ : 0 < ε
⊢ ε * ↑(Fintype.card α) ^ 2 < ε * ↑(Fintype.card α) ^ 2

Tactic:
rw [inv_le_iff_one_le_mul₀ (zero_lt_two' 𝕜)] at hε

Result:
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hG : G.FarFromTriangleFree ε
hε : 1 ≤ ε * 2
hε₀ : 0 < ε
⊢ ε * ↑(Fintype.card α) ^ 2 < ε * ↑(Fintype.card α) ^ 2
-- Mathlib/LinearAlgebra/Dimension/Basic.lean
theorem lift_rank_range_le (f : M →ₗ[R] M') : Cardinal.lift.{v}
    (Module.rank R (LinearMap.range f)) ≤ Cardinal.lift.{v'} (Module.rank R M)

Proof state:
case h.mk.a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥(LinearMap.range f)
li : LinearIndepOn R id s
⊢ ?h.mk.b ≤ lift.{v', v} (⨆ ι, #↑↑ι)

Tactic:
apply Cardinal.lift_le.mpr

Result:
case h.mk.a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥(LinearMap.range f)
li : LinearIndepOn R id s
⊢ ?m.65965 ≤ ⨆ ι, #↑↑ι

R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥(LinearMap.range f)
li : LinearIndepOn R id s
⊢ Cardinal.{v}
-- Mathlib/MeasureTheory/Group/Action.lean
theorem measure_isOpen_pos_of_smulInvariant_of_compact_ne_zero (hK : IsCompact K) (hμK : μ K ≠ 0)
    (hU : IsOpen U) (hne : U.Nonempty) : 0 < μ U :=
  let ⟨t, ht⟩ := hK.exists_finite_cover_smul G hU hne
  pos_iff_ne_zero.2 fun hμU =>
    hμK <|
      measure_mono_null ht <|
        (measure_biUnion_null_iff t.countable_toSet).2 fun _ _ => by rwa [measure_smul]

Proof state:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
μ : Measure α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousConstSMul G α
inst✝ : MulAction.IsMinimal G α
K U : Set α
hK : IsCompact K
hμK : μ K ≠ 0
hU : IsOpen U
hne : U.Nonempty
t : Finset G
ht : K ⊆ ⋃ g ∈ t, g • U
hμU : μ U = 0
x✝¹ : G
x✝ : x✝¹ ∈ ↑t
⊢ μ (x✝¹ • U) = 0

Tactic:
rwa [measure_smul]

Result:
no goals
-- Mathlib/SetTheory/Game/Birthday.lean
theorem birthday_natCast : ∀ n : ℕ, birthday n = n
  | 0 => birthday_zero
  | n + 1 => by simp [birthday_natCast]

Proof state:
n : ℕ
⊢ (↑(n + 1)).birthday = ↑(n + 1)

Tactic:
simp [birthday_natCast]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem nonsing_inv_eq_ring_inverse : A⁻¹ = Ring.inverse A

Proof state:
case neg
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h_det : ¬IsUnit A.det
⊢ A⁻¹ = Ring.inverse A

Tactic:
have h := mt A.isUnit_iff_isUnit_det.mp h_det

Result:
case neg
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h_det : ¬IsUnit A.det
h : ¬IsUnit A
⊢ A⁻¹ = Ring.inverse A

Proof state:
case neg
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h_det : ¬IsUnit A.det
h : ¬IsUnit A
⊢ A⁻¹ = Ring.inverse A

Tactic:
rw [Ring.inverse_non_unit _ h, nonsing_inv_apply_not_isUnit A h_det]

Result:
no goals

Proof state:
case pos.intro
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h_det : IsUnit A.det
val✝ : Invertible A
⊢ A⁻¹ = Ring.inverse A

Tactic:
rw [← invOf_eq_nonsing_inv, Ring.inverse_invertible]

Result:
no goals

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
⊢ A⁻¹ = Ring.inverse A

Tactic:
by_cases h_det : IsUnit A.det

Result:
case pos
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h_det : IsUnit A.det
⊢ A⁻¹ = Ring.inverse A

case neg
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h_det : ¬IsUnit A.det
⊢ A⁻¹ = Ring.inverse A

Proof state:
case pos
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h_det : IsUnit A.det
⊢ A⁻¹ = Ring.inverse A

Tactic:
cases (A.isUnit_iff_isUnit_det.mpr h_det).nonempty_invertible

Result:
case pos.intro
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h_det : IsUnit A.det
val✝ : Invertible A
⊢ A⁻¹ = Ring.inverse A