harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem map_surjective_of_surjective (hg : Surjective g) (k : LocalizationMap (S.map g) Q) :
    Surjective (map f (apply_coe_mem_map g S) k) := fun z ↦ by
  obtain ⟨y, ⟨y', s, hs, rfl⟩, rfl⟩ := k.mk'_surjective z
  obtain ⟨x, rfl⟩ := hg y
  use f.mk' x ⟨s, hs⟩
  rw [map_mk']

Proof state:
case h
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
Q : Type u_4
inst✝ : CommMonoid Q
hg : Surjective ⇑g
k : (Submonoid.map g S).LocalizationMap Q
s : M
hs : s ∈ ↑S
x : M
⊢ (f.map ⋯ k) (f.mk' x ⟨s, hs⟩) = k.mk' (g x) ⟨g s, ⋯⟩

Tactic:
rw [map_mk']

Result:
no goals

Proof state:
case intro.intro.mk.intro.intro
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
Q : Type u_4
inst✝ : CommMonoid Q
hg : Surjective ⇑g
k : (Submonoid.map g S).LocalizationMap Q
y : P
s : M
hs : s ∈ ↑S
⊢ ∃ a, (f.map ⋯ k) a = k.mk' y ⟨g s, ⋯⟩

Tactic:
obtain ⟨x, rfl⟩ := hg y

Result:
case intro.intro.mk.intro.intro.intro
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
Q : Type u_4
inst✝ : CommMonoid Q
hg : Surjective ⇑g
k : (Submonoid.map g S).LocalizationMap Q
s : M
hs : s ∈ ↑S
x : M
⊢ ∃ a, (f.map ⋯ k) a = k.mk' (g x) ⟨g s, ⋯⟩

Proof state:
case intro.intro.mk.intro.intro.intro
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
Q : Type u_4
inst✝ : CommMonoid Q
hg : Surjective ⇑g
k : (Submonoid.map g S).LocalizationMap Q
s : M
hs : s ∈ ↑S
x : M
⊢ ∃ a, (f.map ⋯ k) a = k.mk' (g x) ⟨g s, ⋯⟩

Tactic:
use f.mk' x ⟨s, hs⟩

Result:
case h
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
Q : Type u_4
inst✝ : CommMonoid Q
hg : Surjective ⇑g
k : (Submonoid.map g S).LocalizationMap Q
s : M
hs : s ∈ ↑S
x : M
⊢ (f.map ⋯ k) (f.mk' x ⟨s, hs⟩) = k.mk' (g x) ⟨g s, ⋯⟩

Proof state:
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
Q : Type u_4
inst✝ : CommMonoid Q
hg : Surjective ⇑g
k : (Submonoid.map g S).LocalizationMap Q
z : Q
⊢ ∃ a, (f.map ⋯ k) a = z

Tactic:
obtain ⟨y, ⟨y', s, hs, rfl⟩, rfl⟩ := k.mk'_surjective z

Result:
case intro.intro.mk.intro.intro
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
Q : Type u_4
inst✝ : CommMonoid Q
hg : Surjective ⇑g
k : (Submonoid.map g S).LocalizationMap Q
y : P
s : M
hs : s ∈ ↑S
⊢ ∃ a, (f.map ⋯ k) a = k.mk' y ⟨g s, ⋯⟩
-- Mathlib/Topology/Order/LeftRightNhds.lean
theorem nhds_basis_abs_sub_lt [NoMaxOrder α] (a : α) :
    (𝓝 a).HasBasis (fun ε : α => (0 : α) < ε) fun ε => { b | |b - a| < ε }

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrderedAddCommGroup α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
a : α
⊢ (𝓝 a).HasBasis (fun ε => 0 < ε) fun ε => {b | |b - a| < ε}

Tactic:
simp only [nhds_eq_iInf_abs_sub, abs_sub_comm (a := a)]

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrderedAddCommGroup α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
a : α
⊢ (⨅ r, ⨅ (_ : r > 0), 𝓟 {b | |b - a| < r}).HasBasis (fun ε => 0 < ε) fun ε => {b | |b - a| < ε}

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrderedAddCommGroup α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
a : α
⊢ (⨅ r, ⨅ (_ : r > 0), 𝓟 {b | |b - a| < r}).HasBasis (fun ε => 0 < ε) fun ε => {b | |b - a| < ε}

Tactic:
refine hasBasis_biInf_principal' (fun x hx y hy => ?_) (exists_gt _)

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrderedAddCommGroup α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
a x : α
hx : x > 0
y : α
hy : y > 0
⊢ ∃ k > 0, {b | |b - a| < k} ⊆ {b | |b - a| < x} ∧ {b | |b - a| < k} ⊆ {b | |b - a| < y}

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrderedAddCommGroup α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
a x : α
hx : x > 0
y : α
hy : y > 0
⊢ ∃ k > 0, {b | |b - a| < k} ⊆ {b | |b - a| < x} ∧ {b | |b - a| < k} ⊆ {b | |b - a| < y}

Tactic:
exact ⟨min x y, lt_min hx hy, fun _ hz => hz.trans_le (min_le_left _ _),
  fun _ hz => hz.trans_le (min_le_right _ _)⟩

Result:
no goals
-- Mathlib/Data/List/Sort.lean
theorem Sorted.insertionSort_eq : ∀ {l : List α}, Sorted r l → insertionSort r l = l
  | [], _ => rfl
  | [_], _ => rfl
  | a :: b :: l, h => by
    rw [insertionSort, Sorted.insertionSort_eq, orderedInsert, if_pos]
    exacts [rel_of_sorted_cons h _ (mem_cons_self _ _), h.tail]

Proof state:
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
h : Sorted r (a :: b :: l)
⊢ insertionSort r (a :: b :: l) = a :: b :: l

Tactic:
rw [insertionSort, Sorted.insertionSort_eq, orderedInsert, if_pos]

Result:
case hc
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
h : Sorted r (a :: b :: l)
⊢ r a b

α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
h : Sorted r (a :: b :: l)
⊢ Sorted r (b :: l)

Proof state:
case hc
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
h : Sorted r (a :: b :: l)
⊢ r a b

α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
h : Sorted r (a :: b :: l)
⊢ Sorted r (b :: l)

Tactic:
exacts [rel_of_sorted_cons h _ (mem_cons_self _ _), h.tail]

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Basic.lean
theorem inter_subset_inter {x y s t : Finset α} (h : x ⊆ y) (h' : s ⊆ t) : x ∩ s ⊆ y ∩ t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x y s t : Finset α
h : x ⊆ y
h' : s ⊆ t
⊢ x ∩ s ⊆ y ∩ t

Tactic:
intro a a_in

Result:
α : Type u_1
inst✝ : DecidableEq α
x y s t : Finset α
h : x ⊆ y
h' : s ⊆ t
a : α
a_in : a ∈ x ∩ s
⊢ a ∈ y ∩ t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x y s t : Finset α
h : x ⊆ y
h' : s ⊆ t
a : α
a_in : a ∈ x ∧ a ∈ s
⊢ a ∈ y ∧ a ∈ t

Tactic:
exact ⟨h a_in.1, h' a_in.2⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x y s t : Finset α
h : x ⊆ y
h' : s ⊆ t
a : α
a_in : a ∈ x ∩ s
⊢ a ∈ y ∩ t

Tactic:
rw [Finset.mem_inter] at a_in ⊢

Result:
α : Type u_1
inst✝ : DecidableEq α
x y s t : Finset α
h : x ⊆ y
h' : s ⊆ t
a : α
a_in : a ∈ x ∧ a ∈ s
⊢ a ∈ y ∧ a ∈ t
-- Mathlib/Data/Finset/Lattice/Fold.lean
@[simp] lemma mem_inf' (hs) : a ∈ s.inf' hs f ↔ ∀ i ∈ s, a ∈ f i

Proof state:
α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
hs : s.Nonempty
⊢ a ∈ s.inf' hs f ↔ ∀ i ∈ s, a ∈ f i

Tactic:
induction' hs using Nonempty.cons_induction <;> simp [*]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem div_lt_div_iff_left (a : α) : a / b < a / c ↔ c < b

Proof state:
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
b c a : α
⊢ a / b < a / c ↔ c < b

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, ← mul_lt_mul_iff_left a⁻¹, inv_mul_cancel_left,
  inv_mul_cancel_left, inv_lt_inv_iff]

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
theorem not_specializes_iff_exists_open : ¬x ⤳ y ↔ ∃ S : Set X, IsOpen S ∧ y ∈ S ∧ x ∉ S

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ (¬∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s) ↔ ∃ S, IsOpen S ∧ y ∈ S ∧ x ∉ S

Tactic:
push_neg

Result:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ (∃ s, IsOpen s ∧ y ∈ s ∧ x ∉ s) ↔ ∃ S, IsOpen S ∧ y ∈ S ∧ x ∉ S

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ ¬x ⤳ y ↔ ∃ S, IsOpen S ∧ y ∈ S ∧ x ∉ S

Tactic:
rw [specializes_iff_forall_open]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ (¬∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s) ↔ ∃ S, IsOpen S ∧ y ∈ S ∧ x ∉ S

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ (∃ s, IsOpen s ∧ y ∈ s ∧ x ∉ s) ↔ ∃ S, IsOpen S ∧ y ∈ S ∧ x ∉ S

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem areaForm_map {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F]
    [hF : Fact (finrank ℝ F = 2)] (φ : E ≃ₗᵢ[ℝ] F) (x y : F) :
    (Orientation.map (Fin 2) φ.toLinearEquiv o).areaForm x y =
    o.areaForm (φ.symm x) (φ.symm y)

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
this : ⇑φ.symm ∘ ![x, y] = ![φ.symm x, φ.symm y]
⊢ (((map (Fin 2) φ.toLinearEquiv) o).areaForm x) y = (o.areaForm (φ.symm x)) (φ.symm y)

Tactic:
simp [areaForm_to_volumeForm, volumeForm_map, this]

Result:
no goals

Proof state:
case h
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
i : Fin (Nat.succ 0).succ
⊢ (⇑φ.symm ∘ ![x, y]) i = ![φ.symm x, φ.symm y] i

Tactic:
fin_cases i <;> rfl

Result:
no goals

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
⊢ ⇑φ.symm ∘ ![x, y] = ![φ.symm x, φ.symm y]

Tactic:
ext i

Result:
case h
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
i : Fin (Nat.succ 0).succ
⊢ (⇑φ.symm ∘ ![x, y]) i = ![φ.symm x, φ.symm y] i

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
⊢ (((map (Fin 2) φ.toLinearEquiv) o).areaForm x) y = (o.areaForm (φ.symm x)) (φ.symm y)

Tactic:
have : φ.symm ∘ ![x, y] = ![φ.symm x, φ.symm y] := by
  ext i
  fin_cases i <;> rfl

Result:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
this : ⇑φ.symm ∘ ![x, y] = ![φ.symm x, φ.symm y]
⊢ (((map (Fin 2) φ.toLinearEquiv) o).areaForm x) y = (o.areaForm (φ.symm x)) (φ.symm y)
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
@[simp]
lemma map_addZ (P Q : Fin 3 → R) : addZ (f ∘ P) (f ∘ Q) = f (addZ P Q)

Proof state:
R : Type r
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
P Q : Fin 3 → R
⊢ addZ (⇑f ∘ P) (⇑f ∘ Q) = f (addZ P Q)

Tactic:
simp only [addZ]

Result:
R : Type r
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
P Q : Fin 3 → R
⊢ (⇑f ∘ P) x * (⇑f ∘ Q) z ^ 2 - (⇑f ∘ Q) x * (⇑f ∘ P) z ^ 2 = f (P x * Q z ^ 2 - Q x * P z ^ 2)

Proof state:
R : Type r
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
P Q : Fin 3 → R
⊢ (⇑f ∘ P) x * (⇑f ∘ Q) z ^ 2 - (⇑f ∘ Q) x * (⇑f ∘ P) z ^ 2 = f (P x * Q z ^ 2 - Q x * P z ^ 2)

Tactic:
map_simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean
theorem hom_refl (C : G.ComponentCompl L) : C.hom (subset_refl L) = C

Proof state:
V : Type u
G : SimpleGraph V
L : Set V
C : G.ComponentCompl L
⊢ hom ⋯ C = C

Tactic:
change C.map _ = C

Result:
V : Type u
G : SimpleGraph V
L : Set V
C : G.ComponentCompl L
⊢ ConnectedComponent.map (induceHom Hom.id ⋯) C = C

Proof state:
V : Type u
G : SimpleGraph V
L : Set V
C : G.ComponentCompl L
⊢ ConnectedComponent.map (induceHom Hom.id ⋯) C = C

Tactic:
rw [induceHom_id G Lᶜ, ConnectedComponent.map_id]

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem Subgroup.is_normal_topologicalClosure {G : Type*} [TopologicalSpace G] [Group G]
    [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] :
    (Subgroup.topologicalClosure N).Normal where
  conj_mem n hn g

Proof state:
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
N : Subgroup G
inst✝ : N.Normal
n : G
hn : n ∈ N.topologicalClosure
g : G
⊢ MapsTo (fun h => g * h * g⁻¹) ↑N ↑N

Tactic:
exact fun m hm => Subgroup.Normal.conj_mem inferInstance m hm g

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
N : Subgroup G
inst✝ : N.Normal
n : G
hn : n ∈ N.topologicalClosure
g : G
⊢ g * n * g⁻¹ ∈ N.topologicalClosure

Tactic:
apply map_mem_closure (IsTopologicalGroup.continuous_conj g) hn

Result:
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
N : Subgroup G
inst✝ : N.Normal
n : G
hn : n ∈ N.topologicalClosure
g : G
⊢ MapsTo (fun h => g * h * g⁻¹) ↑N ↑N
-- Mathlib/Deprecated/Cardinal/Finite.lean
theorem _root_.Cardinal.toPartENat_le_natCast_iff {c : Cardinal} {n : ℕ} :
    toPartENat c ≤ n ↔ c ≤ n

Proof state:
c : Cardinal.{u_1}
n : ℕ
⊢ toPartENat c ≤ ↑n ↔ c ≤ ↑n

Tactic:
rw [← toPartENat_natCast n, toPartENat_le_iff_of_lt_aleph0 (nat_lt_aleph0 n)]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
theorem Matrix.toLinearMap₂_basisFun :
    Matrix.toLinearMap₂ (Pi.basisFun R n) (Pi.basisFun R m) =
      Matrix.toLinearMap₂' R (N₂ := N₂)

Proof state:
R : Type u_1
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : Module R N₂
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Fintype m
⊢ toLinearMap₂ (Pi.basisFun R n) (Pi.basisFun R m) = toLinearMap₂' R

Tactic:
ext M

Result:
case h.h.h.h.h
R : Type u_1
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : Module R N₂
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Fintype m
M : Matrix n m N₂
i✝¹ : n
i✝ : m
⊢ (((toLinearMap₂ (Pi.basisFun R n) (Pi.basisFun R m)) M ∘ₗ single R (fun i => R) i✝¹) 1 ∘ₗ single R (fun i => R) i✝)
      1 =
    (((toLinearMap₂' R) M ∘ₗ single R (fun i => R) i✝¹) 1 ∘ₗ single R (fun i => R) i✝) 1

Proof state:
case h.h.h.h.h
R : Type u_1
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : Module R N₂
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Fintype m
M : Matrix n m N₂
i✝¹ : n
i✝ : m
⊢ (((toLinearMap₂ (Pi.basisFun R n) (Pi.basisFun R m)) M ∘ₗ single R (fun i => R) i✝¹) 1 ∘ₗ single R (fun i => R) i✝)
      1 =
    (((toLinearMap₂' R) M ∘ₗ single R (fun i => R) i✝¹) 1 ∘ₗ single R (fun i => R) i✝) 1

Tactic:
simp only [coe_comp, coe_single, Function.comp_apply, toLinearMap₂_apply, Pi.basisFun_repr,
  toLinearMap₂'_apply]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem isLittleO_const_log_atTop {c : ℝ} : (fun _ => c) =o[atTop] log

Proof state:
c : ℝ
⊢ (fun x => c) =o[atTop] log

Tactic:
refine Asymptotics.isLittleO_of_tendsto' ?_
  <| Tendsto.div_atTop (a := c) (by simp) tendsto_log_atTop

Result:
c : ℝ
⊢ ∀ᶠ (x : ℝ) in atTop, log x = 0 → c = 0

Proof state:
case h
c x : ℝ
hx : 1 < x
⊢ log x = 0 → c = 0

Tactic:
aesop (add safe forward log_pos)

Result:
no goals

Proof state:
c : ℝ
⊢ ∀ᶠ (x : ℝ) in atTop, log x = 0 → c = 0

Tactic:
filter_upwards [eventually_gt_atTop 1] with x hx

Result:
case h
c x : ℝ
hx : 1 < x
⊢ log x = 0 → c = 0

Proof state:
c : ℝ
⊢ Tendsto (fun x => c) atTop (𝓝 c)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[reassoc (attr := simp)]
lemma op_pOpcycles_opcyclesOpIso_hom [S.HasLeftHomology] :
    S.op.pOpcycles ≫ S.opcyclesOpIso.hom = S.iCycles.op

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasLeftHomology
⊢ S.op.pOpcycles ≫ S.opcyclesOpIso.hom = S.iCycles.op

Tactic:
dsimp [opcyclesOpIso]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasLeftHomology
⊢ S.op.pOpcycles ≫ S.leftHomologyData.op.opcyclesIso.hom = S.iCycles.op

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasLeftHomology
⊢ S.op.pOpcycles ≫ S.leftHomologyData.op.opcyclesIso.hom = S.iCycles.op

Tactic:
rw [← S.leftHomologyData.op.p_comp_opcyclesIso_inv, assoc,
  Iso.inv_hom_id, comp_id]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasLeftHomology
⊢ S.leftHomologyData.op.p = S.iCycles.op

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasLeftHomology
⊢ S.leftHomologyData.op.p = S.iCycles.op

Tactic:
rfl

Result:
no goals
-- Mathlib/SetTheory/Surreal/Dyadic.lean
theorem nsmul_pow_two_powHalf' (n k : ℕ) : 2 ^ n * powHalf (n + k) = powHalf k

Proof state:
n k : ℕ
⊢ 2 ^ n * powHalf (n + k) = powHalf k

Tactic:
induction' k with k hk

Result:
case zero
n : ℕ
⊢ 2 ^ n * powHalf (n + 0) = powHalf 0

case succ
n k : ℕ
hk : 2 ^ n * powHalf (n + k) = powHalf k
⊢ 2 ^ n * powHalf (n + (k + 1)) = powHalf (k + 1)

Proof state:
case succ
n k : ℕ
hk : 2 * (2 ^ n * powHalf (n + k + 1)) = 2 * powHalf (k + 1)
⊢ 2 ^ n * powHalf (n + (k + 1)) = powHalf (k + 1)

Tactic:
rw [← zsmul_eq_zsmul_iff' two_ne_zero]

Result:
case succ
n k : ℕ
hk : 2 * (2 ^ n * powHalf (n + k + 1)) = 2 * powHalf (k + 1)
⊢ 2 • (2 ^ n * powHalf (n + (k + 1))) = 2 • powHalf (k + 1)

Proof state:
case succ
n k : ℕ
hk : 2 ^ n * powHalf (n + k) = powHalf k
⊢ 2 ^ n * powHalf (n + (k + 1)) = powHalf (k + 1)

Tactic:
rw [← double_powHalf_succ_eq_powHalf (n + k), ← double_powHalf_succ_eq_powHalf k,
  ← mul_assoc, mul_comm (2 ^ n) 2, mul_assoc] at hk

Result:
case succ
n k : ℕ
hk : 2 * (2 ^ n * powHalf (n + k + 1)) = 2 * powHalf (k + 1)
⊢ 2 ^ n * powHalf (n + (k + 1)) = powHalf (k + 1)

Proof state:
case zero
n : ℕ
⊢ 2 ^ n * powHalf (n + 0) = powHalf 0

Tactic:
simp only [add_zero, Surreal.nsmul_pow_two_powHalf, eq_self_iff_true,
  Surreal.powHalf_zero]

Result:
no goals

Proof state:
case succ
n k : ℕ
hk : 2 * (2 ^ n * powHalf (n + k + 1)) = 2 * powHalf (k + 1)
⊢ 2 • (2 ^ n * powHalf (n + (k + 1))) = 2 • powHalf (k + 1)

Tactic:
simpa only [zsmul_eq_mul, Int.cast_ofNat]

Result:
no goals
-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean
theorem _root_.BoundedVariationOn.dist_le {E : Type*} [PseudoMetricSpace E] {f : α → E}
    {s : Set α} (h : BoundedVariationOn f s) {x y : α} (hx : x ∈ s) (hy : y ∈ s) :
    dist (f x) (f y) ≤ (eVariationOn f s).toReal

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_3
inst✝ : PseudoMetricSpace E
f : α → E
s : Set α
h : BoundedVariationOn f s
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ edist (f x) (f y) ≤ eVariationOn f s

Tactic:
exact edist_le f hx hy

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_3
inst✝ : PseudoMetricSpace E
f : α → E
s : Set α
h : BoundedVariationOn f s
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ dist (f x) (f y) ≤ (eVariationOn f s).toReal

Tactic:
rw [← ENNReal.ofReal_le_ofReal_iff ENNReal.toReal_nonneg, ENNReal.ofReal_toReal h, ← edist_dist]

Result:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_3
inst✝ : PseudoMetricSpace E
f : α → E
s : Set α
h : BoundedVariationOn f s
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ edist (f x) (f y) ≤ eVariationOn f s
-- Mathlib/Data/Nat/Choose/Factorization.lean
theorem factorization_centralBinom_of_two_mul_self_lt_three_mul (n_big : 2 < n) (p_le_n : p ≤ n)
    (big : 2 * n < 3 * p) : (centralBinom n).factorization p = 0

Proof state:
case refine_2
p n : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
⊢ n ≤ 2 * n - n

Tactic:
rw [two_mul, add_tsub_cancel_left]

Result:
no goals

Proof state:
case refine_1
p n : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
⊢ p ≠ 2

Tactic:
omega

Result:
no goals

Proof state:
p n : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
⊢ n.centralBinom.factorization p = 0

Tactic:
refine factorization_choose_of_lt_three_mul ?_ p_le_n (p_le_n.trans ?_) big

Result:
case refine_1
p n : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
⊢ p ≠ 2

case refine_2
p n : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
⊢ n ≤ 2 * n - n
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem ppow_succ' {f : ArithmeticFunction R} {k : ℕ} : f.ppow (k + 1) = f.pmul (f.ppow k)

Proof state:
case h
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k x : ℕ
⊢ (f.ppow (k + 1)) x = (f.pmul (f.ppow k)) x

Tactic:
rw [ppow_apply (Nat.succ_pos k), _root_.pow_succ']

Result:
case h
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k x : ℕ
⊢ f x * f x ^ k = (f.pmul (f.ppow k)) x

Proof state:
case h
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k x : ℕ
⊢ f x * f x ^ k = (f.pmul (f.ppow k)) x

Tactic:
induction k <;> simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k : ℕ
⊢ f.ppow (k + 1) = f.pmul (f.ppow k)

Tactic:
ext x

Result:
case h
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k x : ℕ
⊢ (f.ppow (k + 1)) x = (f.pmul (f.ppow k)) x
-- Mathlib/Analysis/Seminorm.lean
theorem finset_sup_apply (p : ι → Seminorm 𝕜 E) (s : Finset ι) (x : E) :
    s.sup p x = ↑(s.sup fun i => ⟨p i x, apply_nonneg (p i) x⟩ : ℝ≥0)

Proof state:
case h₁
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
x : E
⊢ 0 = ↑0

Tactic:
norm_cast

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
⊢ (s.sup p) x = ↑(s.sup fun i => ⟨(p i) x, ⋯⟩)

Tactic:
induction' s using Finset.cons_induction_on with a s ha ih

Result:
case h₁
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
x : E
⊢ (∅.sup p) x = ↑(∅.sup fun i => ⟨(p i) x, ⋯⟩)

case h₂
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
x : E
a : ι
s : Finset ι
ha : a ∉ s
ih : (s.sup p) x = ↑(s.sup fun i => ⟨(p i) x, ⋯⟩)
⊢ ((Finset.cons a s ha).sup p) x = ↑((Finset.cons a s ha).sup fun i => ⟨(p i) x, ⋯⟩)

Proof state:
case h₁
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
x : E
⊢ (∅.sup p) x = ↑(∅.sup fun i => ⟨(p i) x, ⋯⟩)

Tactic:
rw [Finset.sup_empty, Finset.sup_empty, coe_bot, _root_.bot_eq_zero, Pi.zero_apply]

Result:
case h₁
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
x : E
⊢ 0 = ↑0

Proof state:
case h₂
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
x : E
a : ι
s : Finset ι
ha : a ∉ s
ih : (s.sup p) x = ↑(s.sup fun i => ⟨(p i) x, ⋯⟩)
⊢ ((Finset.cons a s ha).sup p) x = ↑((Finset.cons a s ha).sup fun i => ⟨(p i) x, ⋯⟩)

Tactic:
rw [Finset.sup_cons, Finset.sup_cons, coe_sup, Pi.sup_apply, NNReal.coe_max, NNReal.coe_mk, ih]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
protected lemma Connected.nonempty {H : G.Subgraph} (h : H.Connected) : H.verts.Nonempty

Proof state:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Connected
⊢ H.verts.Nonempty

Tactic:
rw [H.connected_iff] at h

Result:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Preconnected ∧ H.verts.Nonempty
⊢ H.verts.Nonempty

Proof state:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Preconnected ∧ H.verts.Nonempty
⊢ H.verts.Nonempty

Tactic:
exact h.2

Result:
no goals