harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem dvd_out_iff (a : α) (b : Associates α) : a ∣ b.out ↔ Associates.mk a ≤ b :=
  Quotient.inductionOn b <| by
    simp [Associates.out_mk, Associates.quotient_mk_eq_mk, mk_le_mk_iff_dvd]

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
b : Associates α
⊢ ∀ (a_1 : α), a ∣ Associates.out ⟦a_1⟧ ↔ Associates.mk a ≤ ⟦a_1⟧

Tactic:
simp [Associates.out_mk, Associates.quotient_mk_eq_mk, mk_le_mk_iff_dvd]

Result:
no goals
-- Mathlib/Data/Matrix/Rank.lean
theorem rank_unit [StrongRankCondition R] [DecidableEq n] (A : (Matrix n n R)ˣ) :
    (A : Matrix n n R).rank = Fintype.card n

Proof state:
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : StrongRankCondition R
inst✝ : DecidableEq n
A : (Matrix n n R)ˣ
⊢ Fintype.card n ≤ (↑A).rank

Tactic:
have := rank_mul_le_left (A : Matrix n n R) (↑A⁻¹ : Matrix n n R)

Result:
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : StrongRankCondition R
inst✝ : DecidableEq n
A : (Matrix n n R)ˣ
this : (↑A * ↑A⁻¹).rank ≤ (↑A).rank
⊢ Fintype.card n ≤ (↑A).rank

Proof state:
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : StrongRankCondition R
inst✝ : DecidableEq n
A : (Matrix n n R)ˣ
this : (↑A * ↑A⁻¹).rank ≤ (↑A).rank
⊢ Fintype.card n ≤ (↑A).rank

Tactic:
rwa [← Units.val_mul, mul_inv_cancel, Units.val_one, rank_one] at this

Result:
no goals

Proof state:
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : StrongRankCondition R
inst✝ : DecidableEq n
A : (Matrix n n R)ˣ
⊢ (↑A).rank = Fintype.card n

Tactic:
apply le_antisymm (rank_le_card_width (A : Matrix n n R)) _

Result:
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : StrongRankCondition R
inst✝ : DecidableEq n
A : (Matrix n n R)ˣ
⊢ Fintype.card n ≤ (↑A).rank
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Erase.lean
theorem eraseIdx_append_of_lt_size {l : Vector α n} {k : Nat} (hk : k < n) (l' : Vector α n) (h) :
    eraseIdx (l ++ l') k = (eraseIdx l k ++ l').cast (by omega)

Proof state:
α : Type ?u.16797
n : Nat
l : Vector α n
k : Nat
hk : k < n
l' : Vector α n
h : k < n + n
⊢ n - 1 + n = n + n - 1

Tactic:
omega

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
n k : Nat
hk : k < n
h : k < n + n
l : Array α
size_toArray✝¹ : l.size = n
l' : Array α
size_toArray✝ : l'.size = n
⊢ ({ toArray := l, size_toArray := size_toArray✝¹ } ++ { toArray := l', size_toArray := size_toArray✝ }).eraseIdx k h =
    Vector.cast ⋯
      ({ toArray := l, size_toArray := size_toArray✝¹ }.eraseIdx k hk ++
        { toArray := l', size_toArray := size_toArray✝ })

Tactic:
simp [Array.eraseIdx_append_of_lt_size, *]

Result:
no goals

Proof state:
case mk
α : Type u_1
n k : Nat
hk : k < n
l' : Vector α n
h : k < n + n
l : Array α
size_toArray✝ : l.size = n
⊢ ({ toArray := l, size_toArray := size_toArray✝ } ++ l').eraseIdx k h =
    Vector.cast ⋯ ({ toArray := l, size_toArray := size_toArray✝ }.eraseIdx k hk ++ l')

Tactic:
rcases l' with ⟨l'⟩

Result:
case mk.mk
α : Type u_1
n k : Nat
hk : k < n
h : k < n + n
l : Array α
size_toArray✝¹ : l.size = n
l' : Array α
size_toArray✝ : l'.size = n
⊢ ({ toArray := l, size_toArray := size_toArray✝¹ } ++ { toArray := l', size_toArray := size_toArray✝ }).eraseIdx k h =
    Vector.cast ⋯
      ({ toArray := l, size_toArray := size_toArray✝¹ }.eraseIdx k hk ++
        { toArray := l', size_toArray := size_toArray✝ })

Proof state:
α : Type u_1
n : Nat
l : Vector α n
k : Nat
hk : k < n
l' : Vector α n
h : k < n + n
⊢ (l ++ l').eraseIdx k h = Vector.cast ⋯ (l.eraseIdx k hk ++ l')

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
n k : Nat
hk : k < n
l' : Vector α n
h : k < n + n
l : Array α
size_toArray✝ : l.size = n
⊢ ({ toArray := l, size_toArray := size_toArray✝ } ++ l').eraseIdx k h =
    Vector.cast ⋯ ({ toArray := l, size_toArray := size_toArray✝ }.eraseIdx k hk ++ l')
-- Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
theorem tangentBundle_model_space_chartAt (p : TangentBundle I H) :
    (chartAt (ModelProd H E) p).toPartialEquiv = (TotalSpace.toProd H E).toPartialEquiv

Proof state:
case hsymm
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
p : TangentBundle I H
x : ModelProd H E
⊢ ↑(chartAt (ModelProd H E) p).symm x = ↑(TotalSpace.toProd H E).toPartialEquiv.symm x

Tactic:
ext

Result:
case hsymm.proj
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
p : TangentBundle I H
x : ModelProd H E
⊢ (↑(chartAt (ModelProd H E) p).symm x).proj = (↑(TotalSpace.toProd H E).toPartialEquiv.symm x).proj

case hsymm.snd
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
p : TangentBundle I H
x : ModelProd H E
⊢ HEq (↑(chartAt (ModelProd H E) p).symm x).snd (↑(TotalSpace.toProd H E).toPartialEquiv.symm x).snd

Proof state:
case hsymm.snd.h
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
p : TangentBundle I H
x : ModelProd H E
⊢ (↑(chartAt (ModelProd H E) p).symm x).snd = (↑(TotalSpace.toProd H E).toPartialEquiv.symm x).snd

Tactic:
exact (tangentBundleCore I H).coordChange_self (achart _ x.1) x.1 (mem_achart_source H x.1) x.2

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/PartialAdjoint.lean
lemma partialLeftAdjointHomEquiv_comp {X : F.PartialLeftAdjointSource} {Y Y' : D}
    (f : F.partialLeftAdjointObj X ⟶ Y) (g : Y ⟶ Y') :
    F.partialLeftAdjointHomEquiv (f ≫ g) =
      F.partialLeftAdjointHomEquiv f ≫ F.map g

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
X : F.PartialLeftAdjointSource
Y Y' : D
f : F.partialLeftAdjointObj X ⟶ Y
g : Y ⟶ Y'
⊢ F.partialLeftAdjointHomEquiv (f ≫ g) = F.partialLeftAdjointHomEquiv f ≫ F.map g

Tactic:
apply CorepresentableBy.homEquiv_comp

Result:
no goals
-- Mathlib/NumberTheory/WellApproximable.lean
theorem smul_subset_of_coprime (han : (orderOf a).Coprime n) :
    a • approxOrderOf A n δ ⊆ approxOrderOf A (orderOf a * n) δ

Proof state:
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
han : (orderOf a).Coprime n
⊢ ⋃ i, ⋃ (_ : orderOf i = n), ball (a * i) δ ⊆ ⋃ x, ⋃ (_ : orderOf x = orderOf a * n), ball x δ

Tactic:
refine iUnion₂_subset_iff.mpr fun b hb c hc => ?_

Result:
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
han : (orderOf a).Coprime n
b : A
hb : orderOf b = n
c : A
hc : c ∈ ball (a * b) δ
⊢ c ∈ ⋃ x, ⋃ (_ : orderOf x = orderOf a * n), ball x δ

Proof state:
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
han : (orderOf a).Coprime n
b : A
hb : orderOf b = n
c : A
hc : c ∈ ball (a * b) δ
⊢ c ∈ ⋃ x, ⋃ (_ : orderOf x = orderOf a * n), ball x δ

Tactic:
simp only [mem_iUnion, exists_prop]

Result:
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
han : (orderOf a).Coprime n
b : A
hb : orderOf b = n
c : A
hc : c ∈ ball (a * b) δ
⊢ ∃ i, orderOf i = orderOf a * n ∧ c ∈ ball i δ

Proof state:
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
han : (orderOf a).Coprime n
b : A
hb : orderOf b = n
c : A
hc : c ∈ ball (a * b) δ
⊢ ∃ i, orderOf i = orderOf a * n ∧ c ∈ ball i δ

Tactic:
refine ⟨a * b, ?_, hc⟩

Result:
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
han : (orderOf a).Coprime n
b : A
hb : orderOf b = n
c : A
hc : c ∈ ball (a * b) δ
⊢ orderOf (a * b) = orderOf a * n

Proof state:
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
han : (orderOf a).Coprime n
⊢ a • approxOrderOf A n δ ⊆ approxOrderOf A (orderOf a * n) δ

Tactic:
simp_rw [approxOrderOf, thickening_eq_biUnion_ball, ← image_smul, image_iUnion₂, image_smul,
  smul_ball'', smul_eq_mul, mem_setOf_eq]

Result:
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
han : (orderOf a).Coprime n
⊢ ⋃ i, ⋃ (_ : orderOf i = n), ball (a * i) δ ⊆ ⋃ x, ⋃ (_ : orderOf x = orderOf a * n), ball x δ

Proof state:
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
b : A
han : (orderOf a).Coprime (orderOf b)
hb : orderOf b = n
c : A
hc : c ∈ ball (a * b) δ
⊢ orderOf (a * b) = orderOf a * orderOf b

Tactic:
exact (Commute.all a b).orderOf_mul_eq_mul_orderOf_of_coprime han

Result:
no goals

Proof state:
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
han : (orderOf a).Coprime n
b : A
hb : orderOf b = n
c : A
hc : c ∈ ball (a * b) δ
⊢ orderOf (a * b) = orderOf a * n

Tactic:
rw [← hb] at han ⊢

Result:
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
b : A
han : (orderOf a).Coprime (orderOf b)
hb : orderOf b = n
c : A
hc : c ∈ ball (a * b) δ
⊢ orderOf (a * b) = orderOf a * orderOf b
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem affineSpan_coe_preimage_eq_top (A : Set P) [Nonempty A] :
    affineSpan k (((↑) : affineSpan k A → P) ⁻¹' A) = ⊤

Proof state:
case mk.refine_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
A : Set P
inst✝ : Nonempty ↑A
x : P
hx : x ∈ affineSpan k A
c : k
u : P
hu : u ∈ affineSpan k A
v : P
hv : v ∈ affineSpan k A
w : P
hw : w ∈ affineSpan k A
⊢ ⟨u, hu⟩ ∈ ↑(affineSpan k (Subtype.val ⁻¹' A)) →
    ⟨v, hv⟩ ∈ ↑(affineSpan k (Subtype.val ⁻¹' A)) →
      ⟨w, hw⟩ ∈ ↑(affineSpan k (Subtype.val ⁻¹' A)) → ⟨c • (u -ᵥ v) +ᵥ w, ⋯⟩ ∈ ↑(affineSpan k (Subtype.val ⁻¹' A))

Tactic:
exact AffineSubspace.smul_vsub_vadd_mem _ _

Result:
no goals

Proof state:
case mk.refine_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
A : Set P
inst✝ : Nonempty ↑A
x : P
hx : x ∈ affineSpan k A
y : P
hy : y ∈ A
⊢ ⟨y, ⋯⟩ ∈ ↑(affineSpan k (Subtype.val ⁻¹' A))

Tactic:
exact subset_affineSpan _ _ hy

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
A : Set P
inst✝ : Nonempty ↑A
⊢ affineSpan k (Subtype.val ⁻¹' A) = ⊤

Tactic:
rw [eq_top_iff]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
A : Set P
inst✝ : Nonempty ↑A
⊢ ⊤ ≤ affineSpan k (Subtype.val ⁻¹' A)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
A : Set P
inst✝ : Nonempty ↑A
⊢ ⊤ ≤ affineSpan k (Subtype.val ⁻¹' A)

Tactic:
rintro ⟨x, hx⟩ -

Result:
case mk
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
A : Set P
inst✝ : Nonempty ↑A
x : P
hx : x ∈ affineSpan k A
⊢ ⟨x, hx⟩ ∈ ↑(affineSpan k (Subtype.val ⁻¹' A))

Proof state:
case mk
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
A : Set P
inst✝ : Nonempty ↑A
x : P
hx : x ∈ affineSpan k A
⊢ ⟨x, hx⟩ ∈ ↑(affineSpan k (Subtype.val ⁻¹' A))

Tactic:
refine affineSpan_induction' (fun y hy ↦ ?_) (fun c u hu v hv w hw ↦ ?_) hx

Result:
case mk.refine_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
A : Set P
inst✝ : Nonempty ↑A
x : P
hx : x ∈ affineSpan k A
y : P
hy : y ∈ A
⊢ ⟨y, ⋯⟩ ∈ ↑(affineSpan k (Subtype.val ⁻¹' A))

case mk.refine_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
A : Set P
inst✝ : Nonempty ↑A
x : P
hx : x ∈ affineSpan k A
c : k
u : P
hu : u ∈ affineSpan k A
v : P
hv : v ∈ affineSpan k A
w : P
hw : w ∈ affineSpan k A
⊢ ⟨u, hu⟩ ∈ ↑(affineSpan k (Subtype.val ⁻¹' A)) →
    ⟨v, hv⟩ ∈ ↑(affineSpan k (Subtype.val ⁻¹' A)) →
      ⟨w, hw⟩ ∈ ↑(affineSpan k (Subtype.val ⁻¹' A)) → ⟨c • (u -ᵥ v) +ᵥ w, ⋯⟩ ∈ ↑(affineSpan k (Subtype.val ⁻¹' A))
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem stronglyMeasurable_uncurry_of_continuous_of_stronglyMeasurable {α β ι : Type*}
    [TopologicalSpace ι] [MetrizableSpace ι] [MeasurableSpace ι] [SecondCountableTopology ι]
    [OpensMeasurableSpace ι] [TopologicalSpace β] [PseudoMetrizableSpace β] [MeasurableSpace α]
    {u : ι → α → β} (hu_cont : ∀ x, Continuous fun i => u i x) (h : ∀ i, StronglyMeasurable (u i)) :
    StronglyMeasurable (Function.uncurry u)

Proof state:
α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u ((t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p => u ((t_sf n) p.1) p.2
⊢ ∀ (x : ι × α), Tendsto (fun i => U i x) atTop (𝓝 (u x.1 x.2))

Tactic:
exact fun p => ht_sf p.fst p.snd

Result:
no goals

Proof state:
case intro
α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u ((t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p => u ((t_sf n) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun p => u p.1 p.2)
n : ℕ
h_str_meas : StronglyMeasurable fun p => u (↑p.1) p.2
⊢ StronglyMeasurable (U n)

Tactic:
have :
  (fun p : ι × α => u (t_sf n p.fst) p.snd) =
    (fun p : ↥(t_sf n).range × α => u p.fst p.snd) ∘ fun p : ι × α =>
      (⟨t_sf n p.fst, SimpleFunc.mem_range_self _ _⟩, p.snd) :=
  rfl

Result:
case intro
α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous fun i => u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u ((t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p => u ((t_sf n) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun p => u p.1 p.2)
n : ℕ
h_str_meas : StronglyMeasurable fun p => u (↑p.1) p.2
this : (fun p => u ((t_sf n) p.1) p.2) = (fun p => u (↑p.1) p.2) ∘ fun p => (⟨(t_sf n) p.1, ⋯⟩, p.2)
⊢ StronglyMeasurable (U n)
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Metrizable.lean
theorem aemeasurable_of_unif_approx {β} [MeasurableSpace β] [PseudoMetricSpace β] [BorelSpace β]
    {μ : Measure α} {g : α → β}
    (hf : ∀ ε > (0 : ℝ), ∃ f : α → β, AEMeasurable f μ ∧ ∀ᵐ x ∂μ, dist (f x) (g x) ≤ ε) :
    AEMeasurable g μ

Proof state:
α : Type u_1
inst✝³ : MeasurableSpace α
β : Type u_3
inst✝² : MeasurableSpace β
inst✝¹ : PseudoMetricSpace β
inst✝ : BorelSpace β
μ : Measure α
g : α → β
hf : ∀ ε > 0, ∃ f, AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
f : ℕ → α → β
Hf : ∀ (n : ℕ), AEMeasurable (f n) μ ∧ ∀ᵐ (x : α) ∂μ, dist (f n x) (g x) ≤ u n
this : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), dist (f n x) (g x) ≤ u n
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))

Tactic:
filter_upwards [this]

Result:
case h
α : Type u_1
inst✝³ : MeasurableSpace α
β : Type u_3
inst✝² : MeasurableSpace β
inst✝¹ : PseudoMetricSpace β
inst✝ : BorelSpace β
μ : Measure α
g : α → β
hf : ∀ ε > 0, ∃ f, AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
f : ℕ → α → β
Hf : ∀ (n : ℕ), AEMeasurable (f n) μ ∧ ∀ᵐ (x : α) ∂μ, dist (f n x) (g x) ≤ u n
this : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), dist (f n x) (g x) ≤ u n
⊢ ∀ (a : α), (∀ (n : ℕ), dist (f n a) (g a) ≤ u n) → Tendsto (fun n => f n a) atTop (𝓝 (g a))

Proof state:
case intro.intro.intro
α : Type u_1
inst✝³ : MeasurableSpace α
β : Type u_3
inst✝² : MeasurableSpace β
inst✝¹ : PseudoMetricSpace β
inst✝ : BorelSpace β
μ : Measure α
g : α → β
hf : ∀ ε > 0, ∃ f, AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
f : ℕ → α → β
Hf : ∀ (n : ℕ), AEMeasurable (f n) μ ∧ ∀ᵐ (x : α) ∂μ, dist (f n x) (g x) ≤ u n
this : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
⊢ AEMeasurable g μ

Tactic:
exact aemeasurable_of_tendsto_metrizable_ae' (fun n => (Hf n).1) this

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Basis.lean
theorem coord_apply [DecidableEq ι] (i j : ι) : b.coord i (b j) = if i = j then 1 else 0

Proof state:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : DecidableEq ι
i j : ι
⊢ (b.coord i) (b j) = if i = j then 1 else 0

Tactic:
rcases eq_or_ne i j with h | h <;> simp [h]

Result:
no goals
-- Mathlib/Combinatorics/HalesJewett.lean
@[simp] lemma reindex_isMono {eη : η ≃ η'} {eα : α ≃ α'} {eι : ι ≃ ι'} {C : (ι' → α') → κ} :
    (l.reindex eη eα eι).IsMono C ↔ l.IsMono fun x ↦ C <| eα ∘ x ∘ eι.symm

Proof state:
η : Type u_5
α : Type u_6
ι : Type u_7
κ : Type u_8
l : Subspace η α ι
η' : Type u_9
α' : Type u_10
ι' : Type u_11
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
C : (ι' → α') → κ
⊢ IsMono C (l.reindex eη eα eι) ↔ IsMono (fun x => C (⇑eα ∘ x ∘ ⇑eι.symm)) l

Tactic:
simp only [IsMono, funext (reindex_apply _ _ _ _ _), coe_apply]

Result:
η : Type u_5
α : Type u_6
ι : Type u_7
κ : Type u_8
l : Subspace η α ι
η' : Type u_9
α' : Type u_10
ι' : Type u_11
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
C : (ι' → α') → κ
⊢ (∃ c, ∀ (x : η' → α'), (C fun x_1 => eα (Sum.elim id (⇑eα.symm ∘ x ∘ ⇑eη) (l.idxFun (eι.symm x_1)))) = c) ↔
    ∃ c, ∀ (x : η → α), C (⇑eα ∘ ↑l x ∘ ⇑eι.symm) = c

Proof state:
η : Type u_5
α : Type u_6
ι : Type u_7
κ : Type u_8
l : Subspace η α ι
η' : Type u_9
α' : Type u_10
ι' : Type u_11
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
C : (ι' → α') → κ
⊢ (∃ c, ∀ (x : η' → α'), (C fun x_1 => eα (Sum.elim id (⇑eα.symm ∘ x ∘ ⇑eη) (l.idxFun (eι.symm x_1)))) = c) ↔
    ∃ c, ∀ (x : η → α), C (⇑eα ∘ ↑l x ∘ ⇑eι.symm) = c

Tactic:
exact exists_congr fun c ↦ (eη.arrowCongr eα).symm.forall_congr <| by aesop

Result:
no goals

Proof state:
η : Type u_5
α : Type u_6
ι : Type u_7
κ : Type u_8
l : Subspace η α ι
η' : Type u_9
α' : Type u_10
ι' : Type u_11
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
C : (ι' → α') → κ
c : κ
⊢ ∀ (a : η' → α'),
    (C fun x => eα (Sum.elim id (⇑eα.symm ∘ a ∘ ⇑eη) (l.idxFun (eι.symm x)))) = c ↔
      C (⇑eα ∘ ↑l ((eη.arrowCongr eα).symm a) ∘ ⇑eι.symm) = c

Tactic:
aesop

Result:
no goals
-- Mathlib/Computability/TuringMachine.lean
theorem addBottom_nth_snd (L : ListBlank (∀ k, Option (Γ k))) (n : ℕ) :
    ((addBottom L).nth n).2 = L.nth n

Proof state:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
⊢ ((addBottom L).nth n).2 = L.nth n

Tactic:
conv => rhs; rw [← addBottom_map L, ListBlank.nth_map]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem iff_self_and : (p ↔ p ∧ q) ↔ (p → q)

Proof state:
p q : Prop
⊢ (p ↔ p ∧ q) ↔ p → q

Tactic:
rw [@Iff.comm p, and_iff_left_iff_imp]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Gluing.lean
theorem dist_triangle (x y z : Σi, E i) : dist x z ≤ dist x y + dist y z

Proof state:
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
z : E i
hij : i ≠ j
⊢ dist x z ≤ dist x ⋯.some + 0 + 0 + (0 + 0 + dist ⋯.some z)

Tactic:
simpa only [zero_add, add_zero] using dist_triangle _ _ _

Result:
no goals

Proof state:
case mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
y z : (i : ι) × E i
i : ι
x : E i
⊢ dist ⟨i, x⟩ z ≤ dist ⟨i, x⟩ y + dist y z

Tactic:
rcases y with ⟨j, y⟩

Result:
case mk.mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
z : (i : ι) × E i
i : ι
x : E i
j : ι
y : E j
⊢ dist ⟨i, x⟩ z ≤ dist ⟨i, x⟩ ⟨j, y⟩ + dist ⟨j, y⟩ z

Proof state:
case mk.mk.mk.inr.inr.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
z : E j
hik : i ≠ j
⊢ dist x ⋯.some + 1 + dist ⋯.some z ≤ dist x ⋯.some + 1 + dist ⋯.some y + dist y z

Tactic:
calc
  dist x (Nonempty.some ⟨x⟩) + 1 + dist (Nonempty.some ⟨z⟩) z ≤
      dist x (Nonempty.some ⟨x⟩) + 1 + (dist (Nonempty.some ⟨z⟩) y + dist y z) := by
    apply_rules [add_le_add, le_rfl, dist_triangle]
  _ = _ := by abel

Result:
no goals

Proof state:
case mk.mk.mk.inr.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
k : ι
z : E k
hik : i ≠ k
y : E i
⊢ dist x ⋯.some + 1 + dist ⋯.some z ≤ dist x y + (dist y ⋯.some + 1 + dist ⋯.some z)

Tactic:
calc
  dist x (Nonempty.some ⟨x⟩) + 1 + dist (Nonempty.some ⟨z⟩) z ≤
      dist x y + dist y (Nonempty.some ⟨y⟩) + 1 + dist (Nonempty.some ⟨z⟩) z := by
    apply_rules [add_le_add, le_rfl, dist_triangle]
  _ = _ := by abel

Result:
no goals

Proof state:
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
k : ι
z : E k
hik : i ≠ k
y : E i
⊢ dist x ⋯.some + 1 + dist ⋯.some z ≤ dist x y + dist y ⋯.some + 1 + dist ⋯.some z

Tactic:
apply_rules [add_le_add, le_rfl, dist_triangle]

Result:
no goals

Proof state:
case mk.mk.mk.inr.inr.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
z : E j
hik : i ≠ j
⊢ dist ⟨i, x⟩ ⟨j, z⟩ ≤ dist ⟨i, x⟩ ⟨j, y⟩ + dist ⟨j, y⟩ ⟨j, z⟩

Tactic:
simp only [Sigma.dist_ne hij, Sigma.dist_same]

Result:
case mk.mk.mk.inr.inr.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
z : E j
hik : i ≠ j
⊢ dist x ⋯.some + 1 + dist ⋯.some z ≤ dist x ⋯.some + 1 + dist ⋯.some y + dist y z

Proof state:
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
z : E i
hij : i ≠ j
⊢ dist x ⋯.some + 0 + 0 + (0 + 0 + dist ⋯.some z) ≤
    dist x ⋯.some + 1 + dist ⋯.some y + (dist y ⋯.some + 1 + dist ⋯.some z)

Tactic:
apply_rules [add_le_add, le_rfl, dist_nonneg, zero_le_one]

Result:
no goals
-- Mathlib/Algebra/Divisibility/Units.lean
theorem dvd_mul_right (hu : IsUnit u) : a ∣ b * u ↔ a ∣ b

Proof state:
case intro
α : Type u_1
inst✝ : Monoid α
a b : α
u : αˣ
⊢ a ∣ b * ↑u ↔ a ∣ b

Tactic:
apply Units.dvd_mul_right

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Monoid α
a b u : α
hu : IsUnit u
⊢ a ∣ b * u ↔ a ∣ b

Tactic:
rcases hu with ⟨u, rfl⟩

Result:
case intro
α : Type u_1
inst✝ : Monoid α
a b : α
u : αˣ
⊢ a ∣ b * ↑u ↔ a ∣ b