harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean
lemma distinguished_cocone_triangle {X Y : HomotopyCategory C (ComplexShape.up ℤ)} (f : X ⟶ Y) :
    ∃ (Z : HomotopyCategory C (ComplexShape.up ℤ)) (g : Y ⟶ Z) (h : Z ⟶ X⟦1⟧),
      Triangle.mk f g h ∈ distinguishedTriangles C

Proof state:
case mk.mk.intro
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : HomologicalComplex C (ComplexShape.up ℤ)
f : X ⟶ Y
⊢ ∃ Z g h, Triangle.mk ((quotient C (ComplexShape.up ℤ)).map f) g h ∈ distinguishedTriangles C

Tactic:
exact ⟨_, _, _, ⟨_, _, f, ⟨Iso.refl _⟩⟩⟩

Result:
no goals

Proof state:
case mk
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
Y : HomotopyCategory C (ComplexShape.up ℤ)
X : HomologicalComplex C (ComplexShape.up ℤ)
f : { as := X } ⟶ Y
⊢ ∃ Z g h, Triangle.mk f g h ∈ distinguishedTriangles C

Tactic:
obtain ⟨Y⟩ := Y

Result:
case mk.mk
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : HomologicalComplex C (ComplexShape.up ℤ)
f : { as := X } ⟶ { as := Y }
⊢ ∃ Z g h, Triangle.mk f g h ∈ distinguishedTriangles C

Proof state:
case mk.mk
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : HomologicalComplex C (ComplexShape.up ℤ)
f : { as := X } ⟶ { as := Y }
⊢ ∃ Z g h, Triangle.mk f g h ∈ distinguishedTriangles C

Tactic:
obtain ⟨f, rfl⟩ := (quotient _ _).map_surjective f

Result:
case mk.mk.intro
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : HomologicalComplex C (ComplexShape.up ℤ)
f : X ⟶ Y
⊢ ∃ Z g h, Triangle.mk ((quotient C (ComplexShape.up ℤ)).map f) g h ∈ distinguishedTriangles C

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : HomotopyCategory C (ComplexShape.up ℤ)
f : X ⟶ Y
⊢ ∃ Z g h, Triangle.mk f g h ∈ distinguishedTriangles C

Tactic:
obtain ⟨X⟩ := X

Result:
case mk
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
Y : HomotopyCategory C (ComplexShape.up ℤ)
X : HomologicalComplex C (ComplexShape.up ℤ)
f : { as := X } ⟶ Y
⊢ ∃ Z g h, Triangle.mk f g h ∈ distinguishedTriangles C
-- Mathlib/Order/Atoms.lean
theorem eq_bot_iff [∀ i, Bot (π i)] {f : ∀ i, π i} : f = ⊥ ↔ ∀ i, f i = ⊥ :=
  ⟨(· ▸ by simp), fun h => funext fun i => by simp [h]⟩

Proof state:
ι : Type u_4
π : ι → Type u
inst✝ : (i : ι) → Bot (π i)
f : (i : ι) → π i
x✝ : f = ⊥
⊢ ∀ (i : ι), ⊥ i = ⊥

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_4
π : ι → Type u
inst✝ : (i : ι) → Bot (π i)
f : (i : ι) → π i
h : ∀ (i : ι), f i = ⊥
i : ι
⊢ f i = ⊥ i

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Topology/Algebra/LinearTopology.lean
theorem tendsto_smul_zero [IsLinearTopology R M] {ι : Type*} {f : Filter ι}
    (a : ι → R) (m : ι → M) (ha : Tendsto m f (𝓝 0)) :
    Tendsto (a • m) f (𝓝 0)

Proof state:
R : Type u_1
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace M
inst✝ : IsLinearTopology R M
ι : Type u_4
f : Filter ι
a : ι → R
m : ι → M
ha : ∀ (i : Submodule R M), ↑i ∈ 𝓝 0 → ∀ᶠ (x : ι) in f, m x ∈ ↑i
I : Submodule R M
hI : ↑I ∈ 𝓝 0
⊢ ∀ᶠ (x : ι) in f, (a • m) x ∈ ↑I

Tactic:
filter_upwards [ha I hI] with i ai_mem

Result:
case h
R : Type u_1
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace M
inst✝ : IsLinearTopology R M
ι : Type u_4
f : Filter ι
a : ι → R
m : ι → M
ha : ∀ (i : Submodule R M), ↑i ∈ 𝓝 0 → ∀ᶠ (x : ι) in f, m x ∈ ↑i
I : Submodule R M
hI : ↑I ∈ 𝓝 0
i : ι
ai_mem : m i ∈ ↑I
⊢ (a • m) i ∈ ↑I

Proof state:
case h
R : Type u_1
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace M
inst✝ : IsLinearTopology R M
ι : Type u_4
f : Filter ι
a : ι → R
m : ι → M
ha : ∀ (i : Submodule R M), ↑i ∈ 𝓝 0 → ∀ᶠ (x : ι) in f, m x ∈ ↑i
I : Submodule R M
hI : ↑I ∈ 𝓝 0
i : ι
ai_mem : m i ∈ ↑I
⊢ (a • m) i ∈ ↑I

Tactic:
exact I.smul_mem _ ai_mem

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace M
inst✝ : IsLinearTopology R M
ι : Type u_4
f : Filter ι
a : ι → R
m : ι → M
ha : ∀ (i : Submodule R M), ↑i ∈ 𝓝 0 → ∀ᶠ (x : ι) in f, m x ∈ ↑i
⊢ ∀ (i : Submodule R M), ↑i ∈ 𝓝 0 → ∀ᶠ (x : ι) in f, (a • m) x ∈ ↑i

Tactic:
intro I hI

Result:
R : Type u_1
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace M
inst✝ : IsLinearTopology R M
ι : Type u_4
f : Filter ι
a : ι → R
m : ι → M
ha : ∀ (i : Submodule R M), ↑i ∈ 𝓝 0 → ∀ᶠ (x : ι) in f, m x ∈ ↑i
I : Submodule R M
hI : ↑I ∈ 𝓝 0
⊢ ∀ᶠ (x : ι) in f, (a • m) x ∈ ↑I

Proof state:
R : Type u_1
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace M
inst✝ : IsLinearTopology R M
ι : Type u_4
f : Filter ι
a : ι → R
m : ι → M
ha : Tendsto m f (𝓝 0)
⊢ Tendsto (a • m) f (𝓝 0)

Tactic:
rw [hasBasis_submodule R |>.tendsto_right_iff] at ha ⊢

Result:
R : Type u_1
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace M
inst✝ : IsLinearTopology R M
ι : Type u_4
f : Filter ι
a : ι → R
m : ι → M
ha : ∀ (i : Submodule R M), ↑i ∈ 𝓝 0 → ∀ᶠ (x : ι) in f, m x ∈ ↑i
⊢ ∀ (i : Submodule R M), ↑i ∈ 𝓝 0 → ∀ᶠ (x : ι) in f, (a • m) x ∈ ↑i
-- Mathlib/GroupTheory/Complement.lean
theorem equiv_fst_eq_one_of_mem_of_one_mem {g : G} (h1 : 1 ∈ S) (hg : g ∈ T) :
    (hST.equiv g).fst = ⟨1, h1⟩

Proof state:
case a
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
hg : g ∈ T
⊢ ↑(hST.equiv g).1 = ↑⟨1, h1⟩

Tactic:
rw [equiv_fst_eq_mul_inv, equiv_snd_eq_self_of_mem_of_one_mem _ h1 hg, mul_inv_cancel]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
hg : g ∈ T
⊢ (hST.equiv g).1 = ⟨1, h1⟩

Tactic:
ext

Result:
case a
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
hg : g ∈ T
⊢ ↑(hST.equiv g).1 = ↑⟨1, h1⟩
-- Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean
theorem continuous_transAssocReparamAux : Continuous transAssocReparamAux

Proof state:
case refine_9
x : ↑I
hx : ↑x = 1 / 4
⊢ 2 * ↑x = if ↑x ≤ 1 / 2 then ↑x + 1 / 4 else 1 / 2 * (↑x + 1)

Tactic:
norm_num [hx]

Result:
no goals

Proof state:
case refine_9

⊢ ∀ (x : ↑I), ↑x = 1 / 4 → 2 * ↑x = if ↑x ≤ 1 / 2 then ↑x + 1 / 4 else 1 / 2 * (↑x + 1)

Tactic:
intro x hx

Result:
case refine_9
x : ↑I
hx : ↑x = 1 / 4
⊢ 2 * ↑x = if ↑x ≤ 1 / 2 then ↑x + 1 / 4 else 1 / 2 * (↑x + 1)
-- Mathlib/CategoryTheory/ComposableArrows.lean
lemma map_comp {i j k : Fin (n + 1 + 1)} (hij : i ≤ j) (hjk : j ≤ k) :
    map F f i k (hij.trans hjk) = map F f i j hij ≫ map F f j k hjk

Proof state:
case mk.mk.mk.zero.succ.succ
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
k : ℕ
hk : k < n + 1 + 1
hi : 0 < n + 1 + 1
j : ℕ
hj : j + 1 + 1 < n + 1 + 1
hjk : ⟨j + 1 + 1, hj⟩ ≤ ⟨k, hk⟩
hij : ⟨0, hi⟩ ≤ ⟨j + 1 + 1, hj⟩
⊢ map F f ⟨0, hi⟩ ⟨k, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨j + 1 + 1, hj⟩ hij ≫ map F f ⟨j + 1 + 1, hj⟩ ⟨k, hk⟩ hjk

Tactic:
obtain _ | _ | k := k

Result:
case mk.mk.mk.zero.succ.succ.zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
hi : 0 < n + 1 + 1
j : ℕ
hj : j + 1 + 1 < n + 1 + 1
hij : ⟨0, hi⟩ ≤ ⟨j + 1 + 1, hj⟩
hk : 0 < n + 1 + 1
hjk : ⟨j + 1 + 1, hj⟩ ≤ ⟨0, hk⟩
⊢ map F f ⟨0, hi⟩ ⟨0, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨j + 1 + 1, hj⟩ hij ≫ map F f ⟨j + 1 + 1, hj⟩ ⟨0, hk⟩ hjk

case mk.mk.mk.zero.succ.succ.succ.zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
hi : 0 < n + 1 + 1
j : ℕ
hj : j + 1 + 1 < n + 1 + 1
hij : ⟨0, hi⟩ ≤ ⟨j + 1 + 1, hj⟩
hk : 0 + 1 < n + 1 + 1
hjk : ⟨j + 1 + 1, hj⟩ ≤ ⟨0 + 1, hk⟩
⊢ map F f ⟨0, hi⟩ ⟨0 + 1, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨j + 1 + 1, hj⟩ hij ≫ map F f ⟨j + 1 + 1, hj⟩ ⟨0 + 1, hk⟩ hjk

case mk.mk.mk.zero.succ.succ.succ.succ
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
hi : 0 < n + 1 + 1
j : ℕ
hj : j + 1 + 1 < n + 1 + 1
hij : ⟨0, hi⟩ ≤ ⟨j + 1 + 1, hj⟩
k : ℕ
hk : k + 1 + 1 < n + 1 + 1
hjk : ⟨j + 1 + 1, hj⟩ ≤ ⟨k + 1 + 1, hk⟩
⊢ map F f ⟨0, hi⟩ ⟨k + 1 + 1, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨j + 1 + 1, hj⟩ hij ≫ map F f ⟨j + 1 + 1, hj⟩ ⟨k + 1 + 1, hk⟩ hjk

Proof state:
case mk.mk.mk.zero.succ.succ.succ.zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
hi : 0 < n + 1 + 1
j : ℕ
hj : j + 1 + 1 < n + 1 + 1
hij : ⟨0, hi⟩ ≤ ⟨j + 1 + 1, hj⟩
hk : 0 + 1 < n + 1 + 1
hjk : ⟨j + 1 + 1, hj⟩ ≤ ⟨0 + 1, hk⟩
⊢ map F f ⟨0, hi⟩ ⟨0 + 1, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨j + 1 + 1, hj⟩ hij ≫ map F f ⟨j + 1 + 1, hj⟩ ⟨0 + 1, hk⟩ hjk

Tactic:
simp [Fin.le_def] at hjk

Result:
case mk.mk.mk.zero.succ.succ.succ.zero
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
hi : 0 < n + 1 + 1
j : ℕ
hj : j + 1 + 1 < n + 1 + 1
hij : ⟨0, hi⟩ ≤ ⟨j + 1 + 1, hj⟩
hk : 0 + 1 < n + 1 + 1
hjk✝ : ⟨j + 1 + 1, hj⟩ ≤ ⟨0 + 1, hk⟩
hjk : j + 1 + 1 ≤ 1
⊢ map F f ⟨0, hi⟩ ⟨0 + 1, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨j + 1 + 1, hj⟩ hij ≫ map F f ⟨j + 1 + 1, hj⟩ ⟨0 + 1, hk⟩ hjk✝
-- Mathlib/Computability/Primrec.lean
theorem prim_iff₁ {f : ℕ → ℕ} : (@Primrec' 1 fun v => f v.head) ↔ Primrec f :=
  prim_iff.trans
    ⟨fun h => (h.comp <| .vector_ofFn fun _ => .id).of_eq fun v => by simp, fun h =>
      h.comp .vector_head⟩

Proof state:
f : ℕ → ℕ
h : Primrec fun v => f v.head
v : ℕ
⊢ f (ofFn fun i => id v).head = f v

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Index.lean
@[to_additive]
lemma pow_mem_of_index_ne_zero_of_dvd (h : H.index ≠ 0) (a : G) {n : ℕ}
    (hn : ∀ m, 0 < m → m ≤ H.index → m ∣ n) : a ^ n ∈ H

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n : ℕ
hn : ∀ (m : ℕ), 0 < m → m ≤ H.index → m ∣ n
⊢ a ^ n ∈ H

Tactic:
rcases exists_pow_mem_of_index_ne_zero h a with ⟨m, hlt, hle, he⟩

Result:
case intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n : ℕ
hn : ∀ (m : ℕ), 0 < m → m ≤ H.index → m ∣ n
m : ℕ
hlt : 0 < m
hle : m ≤ H.index
he : a ^ m ∈ H
⊢ a ^ n ∈ H

Proof state:
case intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n : ℕ
hn : ∀ (m : ℕ), 0 < m → m ≤ H.index → m ∣ n
m : ℕ
hlt : 0 < m
hle : m ≤ H.index
he : a ^ m ∈ H
⊢ a ^ n ∈ H

Tactic:
rcases hn m hlt hle with ⟨k, rfl⟩

Result:
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
m : ℕ
hlt : 0 < m
hle : m ≤ H.index
he : a ^ m ∈ H
k : ℕ
hn : ∀ (m_1 : ℕ), 0 < m_1 → m_1 ≤ H.index → m_1 ∣ m * k
⊢ a ^ (m * k) ∈ H

Proof state:
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
m : ℕ
hlt : 0 < m
hle : m ≤ H.index
he : a ^ m ∈ H
k : ℕ
hn : ∀ (m_1 : ℕ), 0 < m_1 → m_1 ≤ H.index → m_1 ∣ m * k
⊢ (a ^ m) ^ k ∈ H

Tactic:
exact pow_mem he _

Result:
no goals

Proof state:
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
m : ℕ
hlt : 0 < m
hle : m ≤ H.index
he : a ^ m ∈ H
k : ℕ
hn : ∀ (m_1 : ℕ), 0 < m_1 → m_1 ≤ H.index → m_1 ∣ m * k
⊢ a ^ (m * k) ∈ H

Tactic:
rw [pow_mul]

Result:
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
m : ℕ
hlt : 0 < m
hle : m ≤ H.index
he : a ^ m ∈ H
k : ℕ
hn : ∀ (m_1 : ℕ), 0 < m_1 → m_1 ≤ H.index → m_1 ∣ m * k
⊢ (a ^ m) ^ k ∈ H
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma zpow_lt_one₀ (ha₀ : 0 < a) (ha₁ : a < 1) (hn : 0 < n) : a ^ n < 1

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulStrictMono G₀
n : ℤ
ha₀ : 0 < a
ha₁ : a < 1
hn : 0 < n
⊢ a ^ n < 1

Tactic:
simpa using zpow_right_strictAnti₀ ha₀ ha₁ hn

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem comapDomain'_zero [∀ i, Zero (β i)] (h : κ → ι) {h' : ι → κ}
    (hh' : Function.LeftInverse h' h) : comapDomain' h hh' (0 : Π₀ i, β i) = 0

Proof state:
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
⊢ comapDomain' h hh' 0 = 0

Tactic:
ext

Result:
case h
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
i✝ : κ
⊢ (comapDomain' h hh' 0) i✝ = 0 i✝

Proof state:
case h
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
i✝ : κ
⊢ (comapDomain' h hh' 0) i✝ = 0 i✝

Tactic:
rw [zero_apply, comapDomain'_apply, zero_apply]

Result:
no goals
-- Mathlib/Analysis/Calculus/VectorField.lean
lemma _root_.ContDiffAt.lieBracket_vectorField {m n : WithTop ℕ∞} (hV : ContDiffAt 𝕜 n V x)
    (hW : ContDiffAt 𝕜 n W x) (hmn : m + 1 ≤ n) :
    ContDiffAt 𝕜 m (lieBracket 𝕜 V W) x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
x : E
m n : WithTop ℕ∞
hV : ContDiffWithinAt 𝕜 n V univ x
hW : ContDiffWithinAt 𝕜 n W univ x
hmn : m + 1 ≤ n
⊢ ContDiffWithinAt 𝕜 m (lieBracket 𝕜 V W) univ x

Tactic:
simp_rw [← lieBracketWithin_univ]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
x : E
m n : WithTop ℕ∞
hV : ContDiffWithinAt 𝕜 n V univ x
hW : ContDiffWithinAt 𝕜 n W univ x
hmn : m + 1 ≤ n
⊢ ContDiffWithinAt 𝕜 m (lieBracketWithin 𝕜 V W univ) univ x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
x : E
m n : WithTop ℕ∞
hV : ContDiffWithinAt 𝕜 n V univ x
hW : ContDiffWithinAt 𝕜 n W univ x
hmn : m + 1 ≤ n
⊢ ContDiffWithinAt 𝕜 m (lieBracketWithin 𝕜 V W univ) univ x

Tactic:
exact hV.lieBracketWithin_vectorField hW uniqueDiffOn_univ hmn (mem_univ _)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
x : E
m n : WithTop ℕ∞
hV : ContDiffAt 𝕜 n V x
hW : ContDiffAt 𝕜 n W x
hmn : m + 1 ≤ n
⊢ ContDiffAt 𝕜 m (lieBracket 𝕜 V W) x

Tactic:
rw [← contDiffWithinAt_univ] at hV hW ⊢

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
x : E
m n : WithTop ℕ∞
hV : ContDiffWithinAt 𝕜 n V univ x
hW : ContDiffWithinAt 𝕜 n W univ x
hmn : m + 1 ≤ n
⊢ ContDiffWithinAt 𝕜 m (lieBracket 𝕜 V W) univ x
-- Mathlib/CategoryTheory/Generator/Preadditive.lean
theorem Preadditive.isSeparating_iff (𝒢 : Set C) :
    IsSeparating 𝒢 ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ G ∈ 𝒢, ∀ (h : G ⟶ X), h ≫ f = 0) → f = 0 :=
  ⟨fun h𝒢 X Y f hf => h𝒢 _ _ (by simpa only [Limits.comp_zero] using hf), fun h𝒢 X Y f g hfg =>
    sub_eq_zero.1 <| h𝒢 _ (by simpa only [Preadditive.comp_sub, sub_eq_zero] using hfg)⟩

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ G ∈ 𝒢, ∀ (h : G ⟶ X), h ≫ f = 0
⊢ ∀ G ∈ 𝒢, ∀ (h : G ⟶ X), h ≫ f = h ≫ 0

Tactic:
simpa only [Limits.comp_zero] using hf

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
𝒢 : Set C
h𝒢 : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ G ∈ 𝒢, ∀ (h : G ⟶ X), h ≫ f = 0) → f = 0
X Y : C
f g : X ⟶ Y
hfg : ∀ G ∈ 𝒢, ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ ∀ G ∈ 𝒢, ∀ (h : G ⟶ X), h ≫ (f - g) = 0

Tactic:
simpa only [Preadditive.comp_sub, sub_eq_zero] using hfg

Result:
no goals
-- Mathlib/RingTheory/Valuation/ValuationSubring.lean
theorem valuation_eq_one_iff (a : A) : IsUnit a ↔ A.valuation a = 1 :=
  ⟨fun h => A.valuation_unit h.unit, fun h => by
    have ha : (a : K) ≠ 0

Proof state:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
h : 0 = 1
c : ↑a = 0
⊢ False

Tactic:
exact zero_ne_one h

Result:
no goals

Proof state:
case a
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
h : A.valuation ↑a = 1
ha : ↑a ≠ 0
ha' : (↑a)⁻¹ ∈ A
⊢ ↑(a * ⟨(↑a)⁻¹, ha'⟩) = ↑1

Tactic:
field_simp

Result:
no goals

Proof state:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
h : A.valuation ↑a = 1
ha : ↑a ≠ 0
⊢ IsUnit a

Tactic:
have ha' : (a : K)⁻¹ ∈ A := by rw [← valuation_le_one_iff, map_inv₀, h, inv_one]

Result:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
h : A.valuation ↑a = 1
ha : ↑a ≠ 0
ha' : (↑a)⁻¹ ∈ A
⊢ IsUnit a

Proof state:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
h : A.valuation ↑a = 1
c : ↑a = 0
⊢ False

Tactic:
rw [c, A.valuation.map_zero] at h

Result:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
h : 0 = 1
c : ↑a = 0
⊢ False

Proof state:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
h : A.valuation ↑a = 1
ha : ↑a ≠ 0
⊢ (↑a)⁻¹ ∈ A

Tactic:
rw [← valuation_le_one_iff, map_inv₀, h, inv_one]

Result:
no goals

Proof state:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
h : A.valuation ↑a = 1
⊢ IsUnit a

Tactic:
have ha : (a : K) ≠ 0 := by
  intro c
  rw [c, A.valuation.map_zero] at h
  exact zero_ne_one h

Result:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
h : A.valuation ↑a = 1
ha : ↑a ≠ 0
⊢ IsUnit a

Proof state:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
h : A.valuation ↑a = 1
ha : ↑a ≠ 0
ha' : (↑a)⁻¹ ∈ A
⊢ IsUnit a

Tactic:
apply isUnit_of_mul_eq_one a ⟨a⁻¹, ha'⟩

Result:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
h : A.valuation ↑a = 1
ha : ↑a ≠ 0
ha' : (↑a)⁻¹ ∈ A
⊢ a * ⟨(↑a)⁻¹, ha'⟩ = 1

Proof state:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
h : A.valuation ↑a = 1
⊢ ↑a ≠ 0

Tactic:
intro c

Result:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
h : A.valuation ↑a = 1
c : ↑a = 0
⊢ False

Proof state:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
h : A.valuation ↑a = 1
ha : ↑a ≠ 0
ha' : (↑a)⁻¹ ∈ A
⊢ a * ⟨(↑a)⁻¹, ha'⟩ = 1

Tactic:
ext

Result:
case a
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
h : A.valuation ↑a = 1
ha : ↑a ≠ 0
ha' : (↑a)⁻¹ ∈ A
⊢ ↑(a * ⟨(↑a)⁻¹, ha'⟩) = ↑1
-- Mathlib/CategoryTheory/FiberedCategory/Cocartesian.lean
/-- When its possible to compare the two, the composition of two `IsStronglyCocartesian.map` will
also be given by a `IsStronglyCocartesian.map`. In other words, given diagrams
```
a --φ--> b        b'         b''
|        |        |          |
v        v        v          v
R --f--> S --g--> S' --g'--> S'
```
and
```
a --φ'--> b'
|         |
v         v
R --f'--> S'

```
and
```
a --φ''--> b''
|          |
v          v
R --f''--> S''
```
such that `φ` and `φ'` are strongly cocartesian morphisms, and such that `f' = f ≫ g` and
`f'' = f' ≫ g'`. Then composing the induced map from `b ⟶ b'` with the induced map from
`b' ⟶ b''` gives the induced map from `b ⟶ b''`. -/
@[reassoc (attr := simp)]
lemma map_comp_map {S' S'' : 𝒮} {b' b'' : 𝒳} {f' : R ⟶ S'} {f'' : R ⟶ S''} {g : S ⟶ S'}
    {g' : S' ⟶ S''} (H : f' = f ≫ g) (H' : f'' = f' ≫ g') (φ' : a ⟶ b') (φ'' : a ⟶ b'')
    [IsStronglyCocartesian p f' φ'] [IsHomLift p f'' φ''] :
    map p f φ H φ' ≫ map p f' φ' H' φ'' =
      map p f φ (show f'' = f ≫ (g ≫ g') by rwa [← assoc, ← H]) φ''

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝² : p.IsStronglyCocartesian f φ
S' S'' : 𝒮
b' b'' : 𝒳
f' : R ⟶ S'
f'' : R ⟶ S''
g : S ⟶ S'
g' : S' ⟶ S''
H : f' = f ≫ g
H' : f'' = f' ≫ g'
φ' : a ⟶ b'
φ'' : a ⟶ b''
inst✝¹ : p.IsStronglyCocartesian f' φ'
inst✝ : p.IsHomLift f'' φ''
⊢ map p f φ H φ' ≫ map p f' φ' H' φ'' = map p f φ ⋯ φ''

Tactic:
apply map_uniq p f φ

Result:
case hψ
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝² : p.IsStronglyCocartesian f φ
S' S'' : 𝒮
b' b'' : 𝒳
f' : R ⟶ S'
f'' : R ⟶ S''
g : S ⟶ S'
g' : S' ⟶ S''
H : f' = f ≫ g
H' : f'' = f' ≫ g'
φ' : a ⟶ b'
φ'' : a ⟶ b''
inst✝¹ : p.IsStronglyCocartesian f' φ'
inst✝ : p.IsHomLift f'' φ''
⊢ φ ≫ map p f φ H φ' ≫ map p f' φ' H' φ'' = φ''

Proof state:
case hψ
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝² : p.IsStronglyCocartesian f φ
S' S'' : 𝒮
b' b'' : 𝒳
f' : R ⟶ S'
f'' : R ⟶ S''
g : S ⟶ S'
g' : S' ⟶ S''
H : f' = f ≫ g
H' : f'' = f' ≫ g'
φ' : a ⟶ b'
φ'' : a ⟶ b''
inst✝¹ : p.IsStronglyCocartesian f' φ'
inst✝ : p.IsHomLift f'' φ''
⊢ φ ≫ map p f φ H φ' ≫ map p f' φ' H' φ'' = φ''

Tactic:
simp only [fac_assoc, fac]

Result:
no goals

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝² : p.IsStronglyCocartesian f φ
S' S'' : 𝒮
b' b'' : 𝒳
f' : R ⟶ S'
f'' : R ⟶ S''
g : S ⟶ S'
g' : S' ⟶ S''
H : f' = f ≫ g
H' : f'' = f' ≫ g'
φ' : a ⟶ b'
φ'' : a ⟶ b''
inst✝¹ : p.IsStronglyCocartesian f' φ'
inst✝ : p.IsHomLift f'' φ''
⊢ f'' = f ≫ g ≫ g'

Tactic:
rwa [← assoc, ← H]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean
lemma IsEquipartition.card_interedges_sparsePairs_le (hP : P.IsEquipartition) (hε : 0 ≤ ε) :
    #((P.sparsePairs G ε).biUnion fun (U, V) ↦ G.interedges U V) ≤ 4 * ε * #A ^ 2

Proof state:
case h.hab.bc.h
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ #P.parts ≤ #A

Tactic:
exact P.card_parts_le_card

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ ε * (↑(#A) + ↑(#P.parts)) ^ 2 ≤ ε * (↑(#A) + ↑(#A)) ^ 2

Tactic:
gcongr

Result:
case h.hab.bc.h
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ #P.parts ≤ #A

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ ↑(#((P.sparsePairs G ε).biUnion fun x =>
          match x with
          | (U, V) => G.interedges U V)) ≤
    4 * ε * ↑(#A) ^ 2

Tactic:
calc
  _ ≤ _ := hP.card_interedges_sparsePairs_le' hε
  _ ≤ ε * (#A + #A)^2 := by gcongr; exact P.card_parts_le_card
  _ = _ := by ring

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ ε * (↑(#A) + ↑(#A)) ^ 2 = 4 * ε * ↑(#A) ^ 2

Tactic:
ring

Result:
no goals
-- Mathlib/CategoryTheory/Category/Cat.lean
lemma leftUnitor_inv_app {B C : Cat} (F : B ⟶ C) (X : B) : (λ_ F).inv.app X = eqToHom (by simp) :=
  rfl

Proof state:
B C : Cat
F : B ⟶ C
X : ↑B
⊢ F.obj X = (𝟙 B ≫ F).obj X

Tactic:
simp

Result:
no goals