harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Convex/Intrinsic.lean
theorem intrinsicClosure_eq_closure : intrinsicClosure 𝕜 s = closure s

Proof state:
case h
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
⊢ (∃ y, (∀ (o : Set ↥(affineSpan 𝕜 s)), IsOpen o → y ∈ o → (o ∩ Subtype.val ⁻¹' s).Nonempty) ∧ ↑y = x) ↔
    ∀ (o : Set P), IsOpen o → x ∈ o → (o ∩ s).Nonempty

Tactic:
refine ⟨?_, fun h => ⟨⟨x, _⟩, ?_, Subtype.coe_mk _ ?_⟩⟩

Result:
case h.refine_1
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
⊢ (∃ y, (∀ (o : Set ↥(affineSpan 𝕜 s)), IsOpen o → y ∈ o → (o ∩ Subtype.val ⁻¹' s).Nonempty) ∧ ↑y = x) →
    ∀ (o : Set P), IsOpen o → x ∈ o → (o ∩ s).Nonempty

case h.refine_2
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
h : ∀ (o : Set P), IsOpen o → x ∈ o → (o ∩ s).Nonempty
⊢ ∀ (o : Set ↥(affineSpan 𝕜 s)), IsOpen o → ⟨x, ?h.refine_3⟩ ∈ o → (o ∩ Subtype.val ⁻¹' s).Nonempty

case h.refine_3
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
h : ∀ (o : Set P), IsOpen o → x ∈ o → (o ∩ s).Nonempty
⊢ x ∈ affineSpan 𝕜 s

Proof state:
case h.refine_2.intro.intro.intro.intro
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
h : ∀ (o : Set P), IsOpen o → x ∈ o → (o ∩ s).Nonempty
t : Set P
ht : IsOpen t
hx : ⟨x, ?h.refine_3⟩ ∈ Subtype.val ⁻¹' t
y : P
hyt : y ∈ t
hys : y ∈ s
⊢ (Subtype.val ⁻¹' t ∩ Subtype.val ⁻¹' s).Nonempty

Tactic:
exact ⟨⟨_, subset_affineSpan 𝕜 s hys⟩, hyt, hys⟩

Result:
no goals

Proof state:
case h.refine_3.intro.intro
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
h : ∀ (o : Set P), IsOpen o → x ∈ o → (o ∩ s).Nonempty
hc : x ∉ affineSpan 𝕜 s
z : P
hz₁ : z ∈ (↑(affineSpan 𝕜 s))ᶜ
hz₂ : z ∈ s
⊢ False

Tactic:
exact hz₁ (subset_affineSpan 𝕜 s hz₂)

Result:
no goals
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem limit.lift_map {F G : J ⥤ C} [HasLimit F] [HasLimit G] (c : Cone F) (α : F ⟶ G) :
    limit.lift F c ≫ limMap α = limit.lift G ((Cones.postcompose α).obj c)

Proof state:
case w
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
F G : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : HasLimit G
c : Cone F
α : F ⟶ G
j✝ : J
⊢ c.π.app j✝ ≫ α.app j✝ = ((Cones.postcompose α).obj c).π.app j✝

Tactic:
rfl

Result:
no goals

Proof state:
case w
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
F G : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : HasLimit G
c : Cone F
α : F ⟶ G
j✝ : J
⊢ (lift F c ≫ limMap α) ≫ π G j✝ = lift G ((Cones.postcompose α).obj c) ≫ π G j✝

Tactic:
rw [assoc, limMap_π, limit.lift_π_assoc, limit.lift_π]

Result:
case w
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
F G : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : HasLimit G
c : Cone F
α : F ⟶ G
j✝ : J
⊢ c.π.app j✝ ≫ α.app j✝ = ((Cones.postcompose α).obj c).π.app j✝

Proof state:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
F G : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : HasLimit G
c : Cone F
α : F ⟶ G
⊢ lift F c ≫ limMap α = lift G ((Cones.postcompose α).obj c)

Tactic:
ext

Result:
case w
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
F G : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : HasLimit G
c : Cone F
α : F ⟶ G
j✝ : J
⊢ (lift F c ≫ limMap α) ≫ π G j✝ = lift G ((Cones.postcompose α).obj c) ≫ π G j✝
-- Mathlib/GroupTheory/GroupExtension/Basic.lean
theorem symm {s₁ s₂ : S.Splitting} (h : S.IsConj s₁ s₂) : S.IsConj s₂ s₁

Proof state:
case intro
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
s₁ s₂ : S.Splitting
n : N
hn : ⇑s₁ = fun g => S.inl n * s₂ g * (S.inl n)⁻¹
⊢ S.IsConj s₂ s₁

Tactic:
exact ⟨n⁻¹, by simp only [hn, map_inv]; group⟩

Result:
no goals

Proof state:
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
s₁ s₂ : S.Splitting
n : N
hn : ⇑s₁ = fun g => S.inl n * s₂ g * (S.inl n)⁻¹
⊢ ⇑s₂ = fun g => S.inl n⁻¹ * s₁ g * (S.inl n⁻¹)⁻¹

Tactic:
simp only [hn, map_inv]

Result:
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
s₁ s₂ : S.Splitting
n : N
hn : ⇑s₁ = fun g => S.inl n * s₂ g * (S.inl n)⁻¹
⊢ ⇑s₂ = fun g => (S.inl n)⁻¹ * (S.inl n * s₂ g * (S.inl n)⁻¹) * (S.inl n)⁻¹⁻¹

Proof state:
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
s₁ s₂ : S.Splitting
n : N
hn : ⇑s₁ = fun g => S.inl n * s₂ g * (S.inl n)⁻¹
⊢ ⇑s₂ = fun g => (S.inl n)⁻¹ * (S.inl n * s₂ g * (S.inl n)⁻¹) * (S.inl n)⁻¹⁻¹

Tactic:
group

Result:
no goals

Proof state:
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
s₁ s₂ : S.Splitting
h : S.IsConj s₁ s₂
⊢ S.IsConj s₂ s₁

Tactic:
obtain ⟨n, hn⟩ := h

Result:
case intro
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
s₁ s₂ : S.Splitting
n : N
hn : ⇑s₁ = fun g => S.inl n * s₂ g * (S.inl n)⁻¹
⊢ S.IsConj s₂ s₁
-- Mathlib/Order/Cofinal.lean
theorem IsCofinal.mem_of_isMax {s : Set α} {a : α} (ha : IsMax a) (hs : IsCofinal s) : a ∈ s

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s : Set α
a : α
ha : IsMax a
hs : IsCofinal s
⊢ a ∈ s

Tactic:
obtain ⟨b, hb, hb'⟩ := hs a

Result:
case intro.intro
α : Type u_1
inst✝ : PartialOrder α
s : Set α
a : α
ha : IsMax a
hs : IsCofinal s
b : α
hb : b ∈ s
hb' : a ≤ b
⊢ a ∈ s

Proof state:
case intro.intro
α : Type u_1
inst✝ : PartialOrder α
s : Set α
a : α
ha : IsMax a
hs : IsCofinal s
b : α
hb : b ∈ s
hb' : a ≤ b
⊢ a ∈ s

Tactic:
rwa [ha.eq_of_ge hb'] at hb

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem eventually_mul_pow_lt_factorial_sub (a c d : ℕ) :
    ∀ᶠ n in atTop, a * c ^ n < (n - d)!

Proof state:
a c d : ℕ
⊢ ∀ᶠ (n : ℕ) in atTop, a * c ^ n < (n - d)!

Tactic:
filter_upwards [Nat.eventually_pow_lt_factorial_sub (a * c) d, Filter.eventually_gt_atTop 0]
  with n hn hn0

Result:
case h
a c d n : ℕ
hn : (a * c) ^ n < (n - d)!
hn0 : 0 < n
⊢ a * c ^ n < (n - d)!

Proof state:
case h
a c d n : ℕ
hn : a ^ n * c ^ n < (n - d)!
hn0 : 0 < n
⊢ a * c ^ n < (n - d)!

Tactic:
exact (Nat.mul_le_mul_right _ (Nat.le_self_pow hn0.ne' _)).trans_lt hn

Result:
no goals

Proof state:
case h
a c d n : ℕ
hn : (a * c) ^ n < (n - d)!
hn0 : 0 < n
⊢ a * c ^ n < (n - d)!

Tactic:
rw [mul_pow] at hn

Result:
case h
a c d n : ℕ
hn : a ^ n * c ^ n < (n - d)!
hn0 : 0 < n
⊢ a * c ^ n < (n - d)!
-- Mathlib/Data/Part.lean
theorem mem_toOption {o : Part α} [Decidable o.Dom] {a : α} : a ∈ toOption o ↔ a ∈ o

Proof state:
case pos
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
a : α
h : o.Dom
⊢ o.get ⋯ = a ↔ a ∈ o

Tactic:
exact ⟨fun h => ⟨_, h⟩, fun ⟨_, h⟩ => h⟩

Result:
no goals

Proof state:
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
a : α
⊢ a ∈ o.toOption ↔ a ∈ o

Tactic:
unfold toOption

Result:
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
a : α
⊢ (a ∈ if h : o.Dom then Option.some (o.get h) else Option.none) ↔ a ∈ o

Proof state:
case neg
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
a : α
h : ¬o.Dom
⊢ a ∉ o

Tactic:
exact mt Exists.fst h

Result:
no goals

Proof state:
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
a : α
⊢ (a ∈ if h : o.Dom then Option.some (o.get h) else Option.none) ↔ a ∈ o

Tactic:
by_cases h : o.Dom <;> simp [h]

Result:
case pos
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
a : α
h : o.Dom
⊢ o.get ⋯ = a ↔ a ∈ o

case neg
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
a : α
h : ¬o.Dom
⊢ a ∉ o
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
/-- The main proof of the upper bound part of the Akra-Bazzi theorem. The factor
`1 - ε n` does not change the asymptotic order, but is needed for the induction step to go
through. -/
lemma T_isBigO_smoothingFn_mul_asympBound :
    T =O[atTop] (fun n => (1 - ε n) * asympBound g a b n)

Proof state:
case h₂
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
h_smoothing_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < 1 - ε ↑y
h_smoothing_gt_half : ∀ (y : ℕ), n₀ ≤ y → 1 / 2 < 1 - ε ↑y
h_asympBound_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < asympBound g a b y
h_asympBound_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < asympBound g a b (r i y)
h_asympBound_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < asympBound g a b y
n₀_pos : 0 < n₀
h_smoothing_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < 1 - ε ↑(r i y)
bound1 : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), ↑(r i y) ^ p a b * (1 - ε ↑(r i y)) ≤ b i ^ p a b * ↑y ^ p a b * (1 - ε ↑y)
h_smoothingFn_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < 1 - ε ↑y
h_sumTransform : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), c₁ * g ↑y ≤ sumTransform (p a b) g (r i y) y
h_bi_le_r : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), b (min_bi b) / 2 * ↑y ≤ ↑(r i y)
h_base_nonempty : (Ico ⌊b (min_bi b) / 2 * ↑n₀⌋₊ n₀).Nonempty
base_max : ℝ := (Ico ⌊b' * ↑n₀⌋₊ n₀).sup' h_base_nonempty fun n => T n / ((1 - ε ↑n) * asympBound g a b n)
C : ℝ := 2 * c₁⁻¹ ⊔ base_max
hC : C = 2 * c₁⁻¹ ⊔ base_max
h_base : ∀ n ∈ Ico ⌊b' * ↑n₀⌋₊ n₀, T n ≤ C * ((1 - ε ↑n) * asympBound g a b n)
n : ℕ
h_ind : ∀ m < n, m ≥ n₀ → 0 < asympBound g a b m → 0 < 1 - ε ↑m → T m ≤ C * ((1 - ε ↑m) * asympBound g a b m)
hn : n ≥ n₀
h_asympBound_pos' : 0 < asympBound g a b n
h_one_sub_smoothingFn_pos' : 0 < 1 - ε ↑n
b_mul_n₀_le_ri : ∀ (i : α), ⌊b' * ↑n₀⌋₊ ≤ r i n
g_pos : 0 ≤ g ↑n
⊢ 1 / 2 ≤ 1 - ε ↑n

Tactic:
exact le_of_lt <| h_smoothing_gt_half n hn

Result:
no goals
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
/-- The main proof of the upper bound part of the Akra-Bazzi theorem. The factor
`1 - ε n` does not change the asymptotic order, but is needed for the induction step to go
through. -/
lemma T_isBigO_smoothingFn_mul_asympBound :
    T =O[atTop] (fun n => (1 - ε n) * asympBound g a b n)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
h_smoothing_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < 1 - ε ↑y
h_smoothing_gt_half : ∀ (y : ℕ), n₀ ≤ y → 1 / 2 < 1 - ε ↑y
h_asympBound_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < asympBound g a b y
h_asympBound_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < asympBound g a b (r i y)
h_asympBound_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < asympBound g a b y
n₀_pos : 0 < n₀
h_smoothing_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < 1 - ε ↑(r i y)
bound1 : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), ↑(r i y) ^ p a b * (1 - ε ↑(r i y)) ≤ b i ^ p a b * ↑y ^ p a b * (1 - ε ↑y)
h_smoothingFn_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < 1 - ε ↑y
h_sumTransform : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), c₁ * g ↑y ≤ sumTransform (p a b) g (r i y) y
h_bi_le_r : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), b (min_bi b) / 2 * ↑y ≤ ↑(r i y)
h_base_nonempty : (Ico ⌊b (min_bi b) / 2 * ↑n₀⌋₊ n₀).Nonempty
base_max : ℝ := (Ico ⌊b' * ↑n₀⌋₊ n₀).sup' h_base_nonempty fun n => T n / ((1 - ε ↑n) * asympBound g a b n)
C : ℝ := 2 * c₁⁻¹ ⊔ base_max
hC : C = 2 * c₁⁻¹ ⊔ base_max
h_base : ∀ n ∈ Ico ⌊b' * ↑n₀⌋₊ n₀, T n ≤ C * ((1 - ε ↑n) * asympBound g a b n)
n : ℕ
h_ind : ∀ m < n, m ≥ n₀ → 0 < asympBound g a b m → 0 < 1 - ε ↑m → T m ≤ C * ((1 - ε ↑m) * asympBound g a b m)
hn : n ≥ n₀
h_asympBound_pos' : 0 < asympBound g a b n
h_one_sub_smoothingFn_pos' : 0 < 1 - ε ↑n
b_mul_n₀_le_ri : ∀ (i : α), ⌊b' * ↑n₀⌋₊ ≤ r i n
g_pos : 0 ≤ g ↑n
⊢ C * (1 - ε ↑n) * asympBound g a b n + 0 = C * ((1 - ε ↑n) * asympBound g a b n)

Tactic:
ring

Result:
no goals
-- Mathlib/CategoryTheory/Filtered/Basic.lean
theorem tulip {j₁ j₂ j₃ k₁ k₂ l : C} (f₁ : j₁ ⟶ k₁) (f₂ : j₂ ⟶ k₁) (f₃ : j₂ ⟶ k₂) (f₄ : j₃ ⟶ k₂)
    (g₁ : j₁ ⟶ l) (g₂ : j₃ ⟶ l) :
    ∃ (s : C) (α : k₁ ⟶ s) (β : l ⟶ s) (γ : k₂ ⟶ s),
      f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = f₃ ≫ γ ∧ f₄ ≫ γ = g₂ ≫ β

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ j₃ k₁ k₂ l : C
f₁ : j₁ ⟶ k₁
f₂ : j₂ ⟶ k₁
f₃ : j₂ ⟶ k₂
f₄ : j₃ ⟶ k₂
g₁ : j₁ ⟶ l
g₂ : j₃ ⟶ l
⊢ ∃ s α β γ, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = f₃ ≫ γ ∧ f₄ ≫ γ = g₂ ≫ β

Tactic:
obtain ⟨l', k₁l, k₂l, hl⟩ := span f₂ f₃

Result:
case intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ j₃ k₁ k₂ l : C
f₁ : j₁ ⟶ k₁
f₂ : j₂ ⟶ k₁
f₃ : j₂ ⟶ k₂
f₄ : j₃ ⟶ k₂
g₁ : j₁ ⟶ l
g₂ : j₃ ⟶ l
l' : C
k₁l : k₁ ⟶ l'
k₂l : k₂ ⟶ l'
hl : f₂ ≫ k₁l = f₃ ≫ k₂l
⊢ ∃ s α β γ, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = f₃ ≫ γ ∧ f₄ ≫ γ = g₂ ≫ β

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ j₃ k₁ k₂ l : C
f₁ : j₁ ⟶ k₁
f₂ : j₂ ⟶ k₁
f₃ : j₂ ⟶ k₂
f₄ : j₃ ⟶ k₂
g₁ : j₁ ⟶ l
g₂ : j₃ ⟶ l
l' : C
k₁l : k₁ ⟶ l'
k₂l : k₂ ⟶ l'
hl : f₂ ≫ k₁l = f₃ ≫ k₂l
s : C
ls : l ⟶ s
l's : l' ⟶ s
hs₁ : g₁ ≫ ls = (f₁ ≫ k₁l) ≫ l's
hs₂ : g₂ ≫ ls = (f₄ ≫ k₂l) ≫ l's
⊢ f₂ ≫ k₁l ≫ l's = f₃ ≫ k₂l ≫ l's

Tactic:
simp only [← Category.assoc, hl]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ j₃ k₁ k₂ l : C
f₁ : j₁ ⟶ k₁
f₂ : j₂ ⟶ k₁
f₃ : j₂ ⟶ k₂
f₄ : j₃ ⟶ k₂
g₁ : j₁ ⟶ l
g₂ : j₃ ⟶ l
l' : C
k₁l : k₁ ⟶ l'
k₂l : k₂ ⟶ l'
hl : f₂ ≫ k₁l = f₃ ≫ k₂l
s : C
ls : l ⟶ s
l's : l' ⟶ s
hs₁ : g₁ ≫ ls = (f₁ ≫ k₁l) ≫ l's
hs₂ : g₂ ≫ ls = (f₄ ≫ k₂l) ≫ l's
⊢ ∃ s α β γ, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = f₃ ≫ γ ∧ f₄ ≫ γ = g₂ ≫ β

Tactic:
refine ⟨s, k₁l ≫ l's, ls, k₂l ≫ l's, ?_, by simp only [← Category.assoc, hl], ?_⟩ <;>
  simp only [hs₁, hs₂, Category.assoc]

Result:
no goals

Proof state:
case intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ j₃ k₁ k₂ l : C
f₁ : j₁ ⟶ k₁
f₂ : j₂ ⟶ k₁
f₃ : j₂ ⟶ k₂
f₄ : j₃ ⟶ k₂
g₁ : j₁ ⟶ l
g₂ : j₃ ⟶ l
l' : C
k₁l : k₁ ⟶ l'
k₂l : k₂ ⟶ l'
hl : f₂ ≫ k₁l = f₃ ≫ k₂l
⊢ ∃ s α β γ, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = f₃ ≫ γ ∧ f₄ ≫ γ = g₂ ≫ β

Tactic:
obtain ⟨s, ls, l's, hs₁, hs₂⟩ := bowtie g₁ (f₁ ≫ k₁l) g₂ (f₄ ≫ k₂l)

Result:
case intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ j₃ k₁ k₂ l : C
f₁ : j₁ ⟶ k₁
f₂ : j₂ ⟶ k₁
f₃ : j₂ ⟶ k₂
f₄ : j₃ ⟶ k₂
g₁ : j₁ ⟶ l
g₂ : j₃ ⟶ l
l' : C
k₁l : k₁ ⟶ l'
k₂l : k₂ ⟶ l'
hl : f₂ ≫ k₁l = f₃ ≫ k₂l
s : C
ls : l ⟶ s
l's : l' ⟶ s
hs₁ : g₁ ≫ ls = (f₁ ≫ k₁l) ≫ l's
hs₂ : g₂ ≫ ls = (f₄ ≫ k₂l) ≫ l's
⊢ ∃ s α β γ, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = f₃ ≫ γ ∧ f₄ ≫ γ = g₂ ≫ β
-- Mathlib/RingTheory/LocalRing/Quotient.lean
theorem quotient_span_eq_top_iff_span_eq_top (s : Set S) :
    span (R ⧸ p) ((Ideal.Quotient.mk (I := pS)) '' s) = ⊤ ↔ span R s = ⊤

Proof state:
case mp.hNN
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) = map (IsScalarTower.toAlgHom R S (S ⧸ pS)) (span R s)
hs : span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤
⊢ ⊤ ≤ span R s ⊔ p • ⊤

Tactic:
rw [Ideal.smul_top_eq_map]

Result:
case mp.hNN
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) = map (IsScalarTower.toAlgHom R S (S ⧸ pS)) (span R s)
hs : span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤
⊢ ⊤ ≤ span R s ⊔ restrictScalars R pS

Proof state:
case mp
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) = map (IsScalarTower.toAlgHom R S (S ⧸ pS)) (span R s)
⊢ span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤ → span R s = ⊤

Tactic:
intro hs

Result:
case mp
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) = map (IsScalarTower.toAlgHom R S (S ⧸ pS)) (span R s)
hs : span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤
⊢ span R s = ⊤
-- Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
/-- `P` can be checked locally around points of the source. -/
lemma iff_exists_appLE
    (hQ : StableUnderCompositionWithLocalizationAwaySource Q) : P f ↔
    ∀ (x : X), ∃ (U : Y.affineOpens) (V : X.affineOpens) (_ : x ∈ V.1) (e : V.1 ≤ f ⁻¹ᵁ U.1),
      Q (f.appLE U V e).hom

Proof state:
case hQi
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => Q
inst : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] => Q
this✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] => Locally fun {R S} [CommRing R] [CommRing S] => Q
this : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] => Q
⊢ RespectsIso fun {R S} [CommRing R] [CommRing S] => Q

Tactic:
apply (isLocal_ringHomProperty P (Q := Q)).respectsIso

Result:
no goals
-- Mathlib/Data/Int/Order/Basic.lean
theorem nonneg_or_nonpos_of_mul_nonneg {a b : ℤ} : 0 ≤ a * b → 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Proof state:
case pos
a b : ℤ
h : 0 ≤ a * b
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Tactic:
exact .inl ⟨ha, hb⟩

Result:
no goals

Proof state:
case neg
a b : ℤ
h : 0 ≤ a * b
ha : ¬0 ≤ a
hb : ¬0 ≤ b
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Tactic:
exact .inr ⟨le_of_not_ge ha, le_of_not_ge hb⟩

Result:
no goals

Proof state:
case pos
a b : ℤ
h : 0 ≤ a * b
ha : ¬0 ≤ a
hb : 0 ≤ b
⊢ b ≤ 0

Tactic:
obtain _ | _ := Int.mul_eq_zero.mp <|
  Int.le_antisymm (Int.mul_nonpos_of_nonpos_of_nonneg (le_of_not_le ha) hb) h

Result:
case pos.inl
a b : ℤ
h : 0 ≤ a * b
ha : ¬0 ≤ a
hb : 0 ≤ b
h✝ : a = 0
⊢ b ≤ 0

case pos.inr
a b : ℤ
h : 0 ≤ a * b
ha : ¬0 ≤ a
hb : 0 ≤ b
h✝ : b = 0
⊢ b ≤ 0

Proof state:
case neg.inl
a b : ℤ
h : 0 ≤ a * b
ha : 0 ≤ a
hb : ¬0 ≤ b
h✝ : a = 0
⊢ a ≤ 0

case neg.inr
a b : ℤ
h : 0 ≤ a * b
ha : 0 ≤ a
hb : ¬0 ≤ b
h✝ : b = 0
⊢ a ≤ 0

Tactic:
all_goals omega

Result:
no goals

Proof state:
case neg
a b : ℤ
h : 0 ≤ a * b
ha : 0 ≤ a
hb : ¬0 ≤ b
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Tactic:
refine .inr ⟨?_, le_of_not_le hb⟩

Result:
case neg
a b : ℤ
h : 0 ≤ a * b
ha : 0 ≤ a
hb : ¬0 ≤ b
⊢ a ≤ 0

Proof state:
a b : ℤ
h : 0 ≤ a * b
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Tactic:
by_cases ha : 0 ≤ a <;> by_cases hb : 0 ≤ b

Result:
case pos
a b : ℤ
h : 0 ≤ a * b
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

case neg
a b : ℤ
h : 0 ≤ a * b
ha : 0 ≤ a
hb : ¬0 ≤ b
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

case pos
a b : ℤ
h : 0 ≤ a * b
ha : ¬0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

case neg
a b : ℤ
h : 0 ≤ a * b
ha : ¬0 ≤ a
hb : ¬0 ≤ b
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Proof state:
case pos.inr
a b : ℤ
h : 0 ≤ a * b
ha : ¬0 ≤ a
hb : 0 ≤ b
h✝ : b = 0
⊢ b ≤ 0

Tactic:
omega

Result:
no goals

Proof state:
a b : ℤ
⊢ 0 ≤ a * b → 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Tactic:
intro h

Result:
a b : ℤ
h : 0 ≤ a * b
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Proof state:
case neg
a b : ℤ
h : 0 ≤ a * b
ha : 0 ≤ a
hb : ¬0 ≤ b
⊢ a ≤ 0

Tactic:
obtain _ | _ := Int.mul_eq_zero.mp <|
  Int.le_antisymm (Int.mul_nonpos_of_nonneg_of_nonpos ha <| le_of_not_le hb) h

Result:
case neg.inl
a b : ℤ
h : 0 ≤ a * b
ha : 0 ≤ a
hb : ¬0 ≤ b
h✝ : a = 0
⊢ a ≤ 0

case neg.inr
a b : ℤ
h : 0 ≤ a * b
ha : 0 ≤ a
hb : ¬0 ≤ b
h✝ : b = 0
⊢ a ≤ 0

Proof state:
case neg.inr
a b : ℤ
h : 0 ≤ a * b
ha : 0 ≤ a
hb : ¬0 ≤ b
h✝ : b = 0
⊢ a ≤ 0

Tactic:
omega

Result:
no goals

Proof state:
case pos
a b : ℤ
h : 0 ≤ a * b
ha : ¬0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Tactic:
refine .inr ⟨le_of_not_le ha, ?_⟩

Result:
case pos
a b : ℤ
h : 0 ≤ a * b
ha : ¬0 ≤ a
hb : 0 ≤ b
⊢ b ≤ 0

Proof state:
case pos.inl
a b : ℤ
h : 0 ≤ a * b
ha : ¬0 ≤ a
hb : 0 ≤ b
h✝ : a = 0
⊢ b ≤ 0

case pos.inr
a b : ℤ
h : 0 ≤ a * b
ha : ¬0 ≤ a
hb : 0 ≤ b
h✝ : b = 0
⊢ b ≤ 0

Tactic:
all_goals omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem ediv_eq_iff_eq_mul_left {a b c : Int}
    (H : b ≠ 0) (H' : b ∣ a) : a / b = c ↔ a = c * b

Proof state:
a b c : Int
H : b ≠ 0
H' : b ∣ a
⊢ a / b = c ↔ a = b * c

Tactic:
exact Int.ediv_eq_iff_eq_mul_right H H'

Result:
no goals

Proof state:
a b c : Int
H : b ≠ 0
H' : b ∣ a
⊢ a / b = c ↔ a = c * b

Tactic:
rw [Int.mul_comm]

Result:
a b c : Int
H : b ≠ 0
H' : b ∣ a
⊢ a / b = c ↔ a = b * c
-- Mathlib/Topology/Connected/LocallyConnected.lean
theorem connectedComponentIn_mem_nhds [LocallyConnectedSpace α] {F : Set α} {x : α} (h : F ∈ 𝓝 x) :
    connectedComponentIn F x ∈ 𝓝 x

Proof state:
case intro.intro.intro.intro
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
s : Set α
hsF : id s ⊆ F
h1s : IsOpen s
hxs : x ∈ s
h2s : IsConnected s
⊢ connectedComponentIn F x ∈ 𝓝 x

Tactic:
exact mem_nhds_iff.mpr ⟨s, h2s.isPreconnected.subset_connectedComponentIn hxs hsF, h1s, hxs⟩

Result:
no goals

Proof state:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
h : F ∈ 𝓝 x
⊢ connectedComponentIn F x ∈ 𝓝 x

Tactic:
rw [(LocallyConnectedSpace.open_connected_basis x).mem_iff] at h

Result:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
h : ∃ i, (IsOpen i ∧ x ∈ i ∧ IsConnected i) ∧ id i ⊆ F
⊢ connectedComponentIn F x ∈ 𝓝 x

Proof state:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
h : ∃ i, (IsOpen i ∧ x ∈ i ∧ IsConnected i) ∧ id i ⊆ F
⊢ connectedComponentIn F x ∈ 𝓝 x

Tactic:
rcases h with ⟨s, ⟨h1s, hxs, h2s⟩, hsF⟩

Result:
case intro.intro.intro.intro
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
s : Set α
hsF : id s ⊆ F
h1s : IsOpen s
hxs : x ∈ s
h2s : IsConnected s
⊢ connectedComponentIn F x ∈ 𝓝 x