harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem cons_subset_cons {l₁ l₂ : List α} (a : α) (s : l₁ ⊆ l₂) : a :: l₁ ⊆ a :: l₂ :=
  fun _ => by simp only [mem_cons]; exact Or.imp_right (@s _)

Proof state:
α : Type u_1
l₁ l₂ : List α
a : α
s : l₁ ⊆ l₂
x✝ : α
⊢ x✝ ∈ a :: l₁ → x✝ ∈ a :: l₂

Tactic:
simp only [mem_cons]

Result:
α : Type u_1
l₁ l₂ : List α
a : α
s : l₁ ⊆ l₂
x✝ : α
⊢ x✝ = a ∨ x✝ ∈ l₁ → x✝ = a ∨ x✝ ∈ l₂

Proof state:
α : Type u_1
l₁ l₂ : List α
a : α
s : l₁ ⊆ l₂
x✝ : α
⊢ x✝ = a ∨ x✝ ∈ l₁ → x✝ = a ∨ x✝ ∈ l₂

Tactic:
exact Or.imp_right (@s _)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem unattach_attach {l : List α} : l.attach.unattach = l

Proof state:
α : Type u_1
l : List α
⊢ l.attach.unattach = l

Tactic:
unfold unattach

Result:
α : Type u_1
l : List α
⊢ map (fun x => x.val) l.attach = l

Proof state:
case cons
α : Type u_1
a : α
l : List α
ih : map (fun x => x.val) l.attach = l
⊢ map (fun x => x.val) (a :: l).attach = a :: l

Tactic:
simp [ih, Function.comp_def]

Result:
no goals

Proof state:
case nil
α : Type u_1
⊢ map (fun x => x.val) [].attach = []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : List α
⊢ map (fun x => x.val) l.attach = l

Tactic:
induction l with
| nil => simp
| cons a l ih => simp [ih, Function.comp_def]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
@[simp] lemma valuation_zero : valuation (0 : ℤ_[p]) = 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ valuation 0 = 0

Tactic:
simp [valuation]

Result:
no goals
-- Mathlib/Analysis/Normed/Field/InfiniteSum.lean
theorem hasSum_sum_range_mul_of_summable_norm [CompleteSpace R] {f g : ℕ → R}
    (hf : Summable fun x => ‖f x‖) (hg : Summable fun x => ‖g x‖) :
    HasSum (fun n ↦ ∑ k ∈ range (n + 1), f k * g (n - k)) ((∑' n, f n) * ∑' n, g n)

Proof state:
case h.e'_6
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (b : ℕ), ∑ k ∈ range (b + 1), f k * g (b - k)

Tactic:
exact tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm hf hg

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
⊢ HasSum (fun n => ∑ k ∈ range (n + 1), f k * g (n - k)) ((∑' (n : ℕ), f n) * ∑' (n : ℕ), g n)

Tactic:
convert (summable_norm_sum_mul_range_of_summable_norm hf hg).of_norm.hasSum

Result:
case h.e'_6
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (b : ℕ), ∑ k ∈ range (b + 1), f k * g (b - k)
-- Mathlib/Data/ENNReal/Inv.lean
theorem top_div_of_ne_top (h : a ≠ ∞) : ∞ / a = ∞

Proof state:
a : ℝ≥0∞
h : a ≠ ⊤
⊢ ⊤ / a = ⊤

Tactic:
simp [top_div, h]

Result:
no goals
-- Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
lemma Set.EqOn.iteratedDeriv_of_isOpen (hfg : Set.EqOn f g s) (hs : IsOpen s) (n : ℕ) :
    Set.EqOn (iteratedDeriv n f) (iteratedDeriv n g) s

Proof state:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
f g : 𝕜 → F
hfg : EqOn f g s
hs : IsOpen s
n : ℕ
x : 𝕜
hx : x ∈ s
a : 𝕜
ha : a ∈ s
⊢ f a = g a

Tactic:
exact hfg ha

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
f g : 𝕜 → F
hfg : EqOn f g s
hs : IsOpen s
n : ℕ
⊢ EqOn (iteratedDeriv n f) (iteratedDeriv n g) s

Tactic:
refine fun x hx ↦ Filter.EventuallyEq.iteratedDeriv_eq n ?_

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
f g : 𝕜 → F
hfg : EqOn f g s
hs : IsOpen s
n : ℕ
x : 𝕜
hx : x ∈ s
⊢ f =ᶠ[nhds x] g

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
f g : 𝕜 → F
hfg : EqOn f g s
hs : IsOpen s
n : ℕ
x : 𝕜
hx : x ∈ s
⊢ f =ᶠ[nhds x] g

Tactic:
filter_upwards [IsOpen.mem_nhds hs hx] with a ha

Result:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
f g : 𝕜 → F
hfg : EqOn f g s
hs : IsOpen s
n : ℕ
x : 𝕜
hx : x ∈ s
a : 𝕜
ha : a ∈ s
⊢ f a = g a
-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem lift.range_le {s : Subgroup β} (H : Set.range f ⊆ s) : (lift f).range ≤ s

Proof state:
α : Type u
β : Type v
inst✝ : Group β
f : α → β
s : Subgroup β
H : Set.range f ⊆ ↑s
w✝ : FreeGroup α
L : List (α × Bool)
x✝ : α × Bool
tl : List (α × Bool)
ih : (lift f) (Quot.mk Red.Step tl) ∈ s
x : α
b : Bool
⊢ (lift f) (Quot.mk Red.Step ((x, true) :: tl)) ∈ s

Tactic:
simpa using s.mul_mem (H ⟨x, rfl⟩) ih

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝ : Group β
f : α → β
s : Subgroup β
H : Set.range f ⊆ ↑s
⊢ (lift f).range ≤ s

Tactic:
rintro _ ⟨⟨L⟩, rfl⟩

Result:
case intro.mk
α : Type u
β : Type v
inst✝ : Group β
f : α → β
s : Subgroup β
H : Set.range f ⊆ ↑s
w✝ : FreeGroup α
L : List (α × Bool)
⊢ (lift f) (Quot.mk Red.Step L) ∈ s

Proof state:
case intro.mk
α : Type u
β : Type v
inst✝ : Group β
f : α → β
s : Subgroup β
H : Set.range f ⊆ ↑s
w✝ : FreeGroup α
L : List (α × Bool)
⊢ (lift f) (Quot.mk Red.Step L) ∈ s

Tactic:
exact List.recOn L s.one_mem fun ⟨x, b⟩ tl ih ↦
  Bool.recOn b (by simpa using s.mul_mem (s.inv_mem <| H ⟨x, rfl⟩) ih)
    (by simpa using s.mul_mem (H ⟨x, rfl⟩) ih)

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝ : Group β
f : α → β
s : Subgroup β
H : Set.range f ⊆ ↑s
w✝ : FreeGroup α
L : List (α × Bool)
x✝ : α × Bool
tl : List (α × Bool)
ih : (lift f) (Quot.mk Red.Step tl) ∈ s
x : α
b : Bool
⊢ (lift f) (Quot.mk Red.Step ((x, false) :: tl)) ∈ s

Tactic:
simpa using s.mul_mem (s.inv_mem <| H ⟨x, rfl⟩) ih

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
lemma exists_isNilRegular_of_finrank_le_card (h : finrank R M ≤ #R) :
    ∃ x : L, IsNilRegular φ x

Proof state:
case intro
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Finite R L
inst✝¹ : Free R L
inst✝ : IsDomain R
h : ↑(finrank R M) ≤ #R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
bₘ : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
n : ℕ := Fintype.card (ChooseBasisIndex R M)
aux : ((φ.polyCharpoly b).coeff φ.nilRank).IsHomogeneous (n - φ.nilRank)
x : ChooseBasisIndex R L → R
hx : (eval x) ((φ.polyCharpoly b).coeff φ.nilRank) ≠ 0
c : ChooseBasisIndex R L →₀ R := Finsupp.equivFunOnFinite.symm x
⊢ ∃ x, φ.IsNilRegular x

Tactic:
use b.repr.symm c

Result:
case h
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Finite R L
inst✝¹ : Free R L
inst✝ : IsDomain R
h : ↑(finrank R M) ≤ #R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
bₘ : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
n : ℕ := Fintype.card (ChooseBasisIndex R M)
aux : ((φ.polyCharpoly b).coeff φ.nilRank).IsHomogeneous (n - φ.nilRank)
x : ChooseBasisIndex R L → R
hx : (eval x) ((φ.polyCharpoly b).coeff φ.nilRank) ≠ 0
c : ChooseBasisIndex R L →₀ R := Finsupp.equivFunOnFinite.symm x
⊢ φ.IsNilRegular (b.repr.symm c)
-- Mathlib/MeasureTheory/Group/Measure.lean
theorem eventually_div_right_iff (μ : Measure G) [IsMulRightInvariant μ] (t : G) {p : G → Prop} :
    (∀ᵐ x ∂μ, p (x / t)) ↔ ∀ᵐ x ∂μ, p x

Proof state:
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
t : G
p : G → Prop
⊢ (∀ᵐ (x : G) ∂μ, p (x / t)) ↔ {x | p x} ∈ Filter.map (fun t_1 => t_1 / t) (ae μ)

Tactic:
rfl

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
t : G
p : G → Prop
⊢ (∀ᵐ (x : G) ∂μ, p (x / t)) ↔ ∀ᵐ (x : G) ∂μ, p x

Tactic:
conv_rhs => rw [Filter.Eventually, ← map_div_right_ae μ t]

Result:
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
t : G
p : G → Prop
⊢ (∀ᵐ (x : G) ∂μ, p (x / t)) ↔ {x | p x} ∈ Filter.map (fun t_1 => t_1 / t) (ae μ)
-- Mathlib/Data/Real/Sqrt.lean
theorem real_sqrt_lt_nat_sqrt_succ {a : ℕ} : √(a : ℝ) < Nat.sqrt a + 1

Proof state:
a : ℕ
⊢ a < (a.sqrt + 1) ^ 2

Tactic:
exact Nat.lt_succ_sqrt' a

Result:
no goals

Proof state:
a : ℕ
⊢ 0 ≤ a.sqrt + 1

Tactic:
exact Nat.le_add_left 0 (Nat.sqrt a + 1)

Result:
no goals

Proof state:
a : ℕ
⊢ √↑a < ↑a.sqrt + 1

Tactic:
rw [sqrt_lt (by simp)] <;> norm_cast

Result:
a : ℕ
⊢ a < (a.sqrt + 1) ^ 2

a : ℕ
⊢ 0 ≤ a.sqrt + 1

Proof state:
a : ℕ
⊢ 0 ≤ ↑a

Tactic:
simp

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem sup_limsup [NeBot f] (a : α) : a ⊔ limsup u f = limsup (fun x => a ⊔ u x) f

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
⊢ ⨅ i ∈ f, a ⊔ ⨆ a ∈ i, u a = ⨅ s ∈ f, (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x

Tactic:
congr

Result:
case e_s
α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
⊢ (fun i => ⨅ (_ : i ∈ f), a ⊔ ⨆ a ∈ i, u a) = fun s => ⨅ (_ : s ∈ f), (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
⊢ a ⊔ limsup u f = limsup (fun x => a ⊔ u x) f

Tactic:
simp only [limsup_eq_iInf_iSup, iSup_sup_eq, sup_iInf₂_eq]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
⊢ ⨅ i ∈ f, a ⊔ ⨆ a ∈ i, u a = ⨅ s ∈ f, (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x

Proof state:
case e_s.h.e_s.h.e_a
α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
s : Set β
hs : s ∈ f
⊢ a = ⨆ x ∈ s, a

Tactic:
exact (biSup_const (nonempty_of_mem hs)).symm

Result:
no goals

Proof state:
case e_s.h.e_s
α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
s : Set β
⊢ (fun j => a ⊔ ⨆ a ∈ s, u a) = fun x => (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x

Tactic:
ext hs

Result:
case e_s.h.e_s.h
α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
s : Set β
hs : s ∈ f
⊢ a ⊔ ⨆ a ∈ s, u a = (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x

Proof state:
case e_s
α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
⊢ (fun i => ⨅ (_ : i ∈ f), a ⊔ ⨆ a ∈ i, u a) = fun s => ⨅ (_ : s ∈ f), (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x

Tactic:
ext s

Result:
case e_s.h
α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
s : Set β
⊢ ⨅ (_ : s ∈ f), a ⊔ ⨆ a ∈ s, u a = ⨅ (_ : s ∈ f), (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x

Proof state:
case e_s.h
α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
s : Set β
⊢ ⨅ (_ : s ∈ f), a ⊔ ⨆ a ∈ s, u a = ⨅ (_ : s ∈ f), (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x

Tactic:
congr

Result:
case e_s.h.e_s
α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
s : Set β
⊢ (fun j => a ⊔ ⨆ a ∈ s, u a) = fun x => (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x

Proof state:
case e_s.h.e_s.h
α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
s : Set β
hs : s ∈ f
⊢ a ⊔ ⨆ a ∈ s, u a = (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x

Tactic:
congr

Result:
case e_s.h.e_s.h.e_a
α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
s : Set β
hs : s ∈ f
⊢ a = ⨆ x ∈ s, a
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem one_lt_rpow_of_pos_of_lt_one_of_neg {x : ℝ≥0∞} {z : ℝ} (hx1 : 0 < x) (hx2 : x < 1)
    (hz : z < 0) : 1 < x ^ z

Proof state:
case intro
z : ℝ
hz : z < 0
x : ℝ≥0
hx1 : 0 < x
hx2 : x < 1
⊢ 1 < ↑x ^ z

Tactic:
simp [← coe_rpow_of_ne_zero (ne_of_gt hx1), NNReal.one_lt_rpow_of_pos_of_lt_one_of_neg hx1 hx2 hz]

Result:
no goals

Proof state:
x : ℝ≥0∞
z : ℝ
hx1 : 0 < x
hx2 : x < 1
hz : z < 0
⊢ 1 < x ^ z

Tactic:
lift x to ℝ≥0 using ne_of_lt (lt_of_lt_of_le hx2 le_top)

Result:
case intro
z : ℝ
hz : z < 0
x : ℝ≥0
hx1 : 0 < ↑x
hx2 : ↑x < 1
⊢ 1 < ↑x ^ z

Proof state:
case intro
z : ℝ
hz : z < 0
x : ℝ≥0
hx1 : 0 < ↑x
hx2 : ↑x < 1
⊢ 1 < ↑x ^ z

Tactic:
simp only [coe_lt_one_iff, coe_pos] at hx1 hx2 ⊢

Result:
case intro
z : ℝ
hz : z < 0
x : ℝ≥0
hx1 : 0 < x
hx2 : x < 1
⊢ 1 < ↑x ^ z
-- Mathlib/CategoryTheory/FiberedCategory/Cocartesian.lean
/-- The universal property of a strongly cocartesian morphism.

This lemma is more flexible with respect to non-definitional equalities than the field
`universal_property'` of `IsStronglyCocartesian`. -/
lemma universal_property {S' : 𝒮} {b' : 𝒳} (g : S ⟶ S') (f' : R ⟶ S') (hf' : f' = f ≫ g)
    (φ' : a ⟶ b') [IsHomLift p f' φ'] : ∃! χ : b ⟶ b', IsHomLift p g χ ∧ φ ≫ χ = φ'

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' : 𝒮
b' : 𝒳
g : S ⟶ S'
f' : R ⟶ S'
hf' : f' = f ≫ g
φ' : a ⟶ b'
inst✝ : p.IsHomLift f' φ'
⊢ ∃! χ, p.IsHomLift g χ ∧ φ ≫ χ = φ'

Tactic:
subst_hom_lift p f' φ'

Result:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
S✝ : 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
b' : 𝒳
φ' : a✝ ⟶ b'
R S : 𝒮
a b : 𝒳
f : p.obj a✝ ⟶ S✝
inst✝¹ : p.IsStronglyCocartesian f φ
g : S✝ ⟶ p.obj b'
hf' : p.map φ' = f ≫ g
inst✝ : p.IsHomLift (p.map φ') φ'
⊢ ∃! χ, p.IsHomLift g χ ∧ φ ≫ χ = φ'

Proof state:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
S : 𝒮
a b : 𝒳
φ : a ⟶ b
b' : 𝒳
φ' : a ⟶ b'
f : p.obj a ⟶ S
inst✝¹ : p.IsStronglyCocartesian f φ
g : S ⟶ p.obj b'
hf' : p.map φ' = f ≫ g
inst✝ : p.IsHomLift (p.map φ') φ'
this : p.IsHomLift (f ≫ g) φ'
⊢ ∃! χ, p.IsHomLift g χ ∧ φ ≫ χ = φ'

Tactic:
apply IsStronglyCocartesian.universal_property' f

Result:
no goals

Proof state:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
S✝ : 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
b' : 𝒳
φ' : a✝ ⟶ b'
R S : 𝒮
a b : 𝒳
f : p.obj a✝ ⟶ S✝
inst✝¹ : p.IsStronglyCocartesian f φ
g : S✝ ⟶ p.obj b'
hf' : p.map φ' = f ≫ g
inst✝ : p.IsHomLift (p.map φ') φ'
⊢ ∃! χ, p.IsHomLift g χ ∧ φ ≫ χ = φ'

Tactic:
clear a b R S

Result:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
S : 𝒮
a b : 𝒳
φ : a ⟶ b
b' : 𝒳
φ' : a ⟶ b'
f : p.obj a ⟶ S
inst✝¹ : p.IsStronglyCocartesian f φ
g : S ⟶ p.obj b'
hf' : p.map φ' = f ≫ g
inst✝ : p.IsHomLift (p.map φ') φ'
⊢ ∃! χ, p.IsHomLift g χ ∧ φ ≫ χ = φ'

Proof state:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
S : 𝒮
a b : 𝒳
φ : a ⟶ b
b' : 𝒳
φ' : a ⟶ b'
f : p.obj a ⟶ S
inst✝¹ : p.IsStronglyCocartesian f φ
g : S ⟶ p.obj b'
hf' : p.map φ' = f ≫ g
inst✝ : p.IsHomLift (p.map φ') φ'
⊢ ∃! χ, p.IsHomLift g χ ∧ φ ≫ χ = φ'

Tactic:
have : p.IsHomLift (f ≫ g) φ' := (hf' ▸ inferInstance)

Result:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
S : 𝒮
a b : 𝒳
φ : a ⟶ b
b' : 𝒳
φ' : a ⟶ b'
f : p.obj a ⟶ S
inst✝¹ : p.IsStronglyCocartesian f φ
g : S ⟶ p.obj b'
hf' : p.map φ' = f ≫ g
inst✝ : p.IsHomLift (p.map φ') φ'
this : p.IsHomLift (f ≫ g) φ'
⊢ ∃! χ, p.IsHomLift g χ ∧ φ ≫ χ = φ'
-- Mathlib/.lake/packages/batteries/Batteries/Data/HashMap/Lemmas.lean
theorem empty_buckets :
    (empty : Imp α β).buckets = ⟨mkArray 8 AssocList.nil, by simp⟩ := rfl

Proof state:
α : Type ?u.21
β : Type ?u.20
⊢ 0 < (mkArray 8 AssocList.nil).size

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Sites/LocallyFullyFaithful.lean
theorem IsLocallyFaithful.ext [G.IsLocallyFaithful K] (ℱ : Sheaf K (Type _))
    {X Y : C} (i₁ i₂ : X ⟶ Y) (e : G.map i₁ = G.map i₂)
    {s t : ℱ.val.obj (op (G.obj X))}
    (h : ∀ ⦃Z : C⦄ (j : Z ⟶ X), j ≫ i₁ = j ≫ i₂ →
      ℱ.1.map (G.map j).op s = ℱ.1.map (G.map j).op t) : s = t

Proof state:
C : Type uC
inst✝² : Category.{vC, uC} C
D : Type uD
inst✝¹ : Category.{vD, uD} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_2)
X Y : C
i₁ i₂ : X ⟶ Y
e : G.map i₁ = G.map i₂
s t : ℱ.val.obj (op (G.obj X))
h : ∀ ⦃Z : C⦄ (j : Z ⟶ X), j ≫ i₁ = j ≫ i₂ → ℱ.val.map (G.map j).op s = ℱ.val.map (G.map j).op t
⊢ ∀ ⦃Y_1 : D⦄ ⦃f : Y_1 ⟶ G.obj X⦄,
    (Sieve.functorPushforward G (Sieve.equalizer i₁ i₂)).arrows f → ℱ.val.map f.op s = ℱ.val.map f.op t

Tactic:
rintro Z _ ⟨W, iWX, iZW, hiWX, rfl⟩

Result:
case intro.intro.intro.intro
C : Type uC
inst✝² : Category.{vC, uC} C
D : Type uD
inst✝¹ : Category.{vD, uD} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_2)
X Y : C
i₁ i₂ : X ⟶ Y
e : G.map i₁ = G.map i₂
s t : ℱ.val.obj (op (G.obj X))
h : ∀ ⦃Z : C⦄ (j : Z ⟶ X), j ≫ i₁ = j ≫ i₂ → ℱ.val.map (G.map j).op s = ℱ.val.map (G.map j).op t
Z : D
W : C
iWX : W ⟶ X
iZW : Z ⟶ G.obj W
hiWX : (Sieve.equalizer i₁ i₂).arrows iWX
⊢ ℱ.val.map (iZW ≫ G.map iWX).op s = ℱ.val.map (iZW ≫ G.map iWX).op t

Proof state:
C : Type uC
inst✝² : Category.{vC, uC} C
D : Type uD
inst✝¹ : Category.{vD, uD} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_2)
X Y : C
i₁ i₂ : X ⟶ Y
e : G.map i₁ = G.map i₂
s t : ℱ.val.obj (op (G.obj X))
h : ∀ ⦃Z : C⦄ (j : Z ⟶ X), j ≫ i₁ = j ≫ i₂ → ℱ.val.map (G.map j).op s = ℱ.val.map (G.map j).op t
⊢ s = t

Tactic:
apply (((isSheaf_iff_isSheaf_of_type _ _).1 ℱ.cond) _
  (G.functorPushforward_equalizer_mem K i₁ i₂ e)).isSeparatedFor.ext

Result:
C : Type uC
inst✝² : Category.{vC, uC} C
D : Type uD
inst✝¹ : Category.{vD, uD} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_2)
X Y : C
i₁ i₂ : X ⟶ Y
e : G.map i₁ = G.map i₂
s t : ℱ.val.obj (op (G.obj X))
h : ∀ ⦃Z : C⦄ (j : Z ⟶ X), j ≫ i₁ = j ≫ i₂ → ℱ.val.map (G.map j).op s = ℱ.val.map (G.map j).op t
⊢ ∀ ⦃Y_1 : D⦄ ⦃f : Y_1 ⟶ G.obj X⦄,
    (Sieve.functorPushforward G (Sieve.equalizer i₁ i₂)).arrows f → ℱ.val.map f.op s = ℱ.val.map f.op t

Proof state:
case intro.intro.intro.intro
C : Type uC
inst✝² : Category.{vC, uC} C
D : Type uD
inst✝¹ : Category.{vD, uD} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_2)
X Y : C
i₁ i₂ : X ⟶ Y
e : G.map i₁ = G.map i₂
s t : ℱ.val.obj (op (G.obj X))
h : ∀ ⦃Z : C⦄ (j : Z ⟶ X), j ≫ i₁ = j ≫ i₂ → ℱ.val.map (G.map j).op s = ℱ.val.map (G.map j).op t
Z : D
W : C
iWX : W ⟶ X
iZW : Z ⟶ G.obj W
hiWX : (Sieve.equalizer i₁ i₂).arrows iWX
⊢ ℱ.val.map (iZW ≫ G.map iWX).op s = ℱ.val.map (iZW ≫ G.map iWX).op t

Tactic:
simp [h iWX hiWX]

Result:
no goals
-- Mathlib/Order/OrderIsoNat.lean
theorem Subtype.orderIsoOfNat_apply [dP : DecidablePred (· ∈ s)] {n : ℕ} :
    Subtype.orderIsoOfNat s n = Subtype.ofNat s n

Proof state:
s : Set ℕ
inst✝ : Infinite ↑s
dP : DecidablePred fun x => x ∈ s
n : ℕ
⊢ ofNat s n = ofNat s n

Tactic:
congr!

Result:
no goals

Proof state:
s : Set ℕ
inst✝ : Infinite ↑s
dP : DecidablePred fun x => x ∈ s
n : ℕ
⊢ (orderIsoOfNat s) n = ofNat s n

Tactic:
simp [orderIsoOfNat]

Result:
s : Set ℕ
inst✝ : Infinite ↑s
dP : DecidablePred fun x => x ∈ s
n : ℕ
⊢ ofNat s n = ofNat s n
-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem exp_neg_two_mul_le {x : ℝ} (hx : 0 < x) : exp (-2 * x) < exp (2 - ⌈x⌉₊) / ⌈x⌉₊

Proof state:
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
h₂ : 1 - x ≤ 2 - ↑⌈x⌉₊
⊢ rexp (-2 * x) < rexp (2 - ↑⌈x⌉₊) / ↑⌈x⌉₊

Tactic:
calc
  _ ≤ exp (1 - x) / (x + 1) := ?_
  _ ≤ exp (2 - ⌈x⌉₊) / (x + 1) := by gcongr
  _ < _ := by gcongr

Result:
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
h₂ : 1 - x ≤ 2 - ↑⌈x⌉₊
⊢ rexp (-2 * x) ≤ rexp (1 - x) / (x + 1)

Proof state:
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
h₂ : 1 - x ≤ 2 - ↑⌈x⌉₊
⊢ rexp (2 - ↑⌈x⌉₊) / (x + 1) < rexp (2 - ↑⌈x⌉₊) / ↑⌈x⌉₊

Tactic:
gcongr

Result:
no goals

Proof state:
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
h₂ : 1 - x ≤ 2 - ↑⌈x⌉₊
⊢ rexp (-2 * x) ≤ rexp (1 - x) / (x + 1)

Tactic:
rw [le_div_iff₀  (add_pos hx zero_lt_one), ← le_div_iff₀' (exp_pos _), ← exp_sub, neg_mul,
  sub_neg_eq_add, two_mul, sub_add_add_cancel, add_comm _ x]

Result:
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
h₂ : 1 - x ≤ 2 - ↑⌈x⌉₊
⊢ x + 1 ≤ rexp (x + 1)

Proof state:
x : ℝ
hx : 0 < x
⊢ rexp (-2 * x) < rexp (2 - ↑⌈x⌉₊) / ↑⌈x⌉₊

Tactic:
have h₁ := ceil_lt_add_one hx.le

Result:
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
⊢ rexp (-2 * x) < rexp (2 - ↑⌈x⌉₊) / ↑⌈x⌉₊

Proof state:
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
⊢ rexp (-2 * x) < rexp (2 - ↑⌈x⌉₊) / ↑⌈x⌉₊

Tactic:
have h₂ : 1 - x ≤ 2 - ⌈x⌉₊ := by linarith

Result:
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
h₂ : 1 - x ≤ 2 - ↑⌈x⌉₊
⊢ rexp (-2 * x) < rexp (2 - ↑⌈x⌉₊) / ↑⌈x⌉₊

Proof state:
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
⊢ 1 - x ≤ 2 - ↑⌈x⌉₊

Tactic:
linarith

Result:
no goals

Proof state:
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
h₂ : 1 - x ≤ 2 - ↑⌈x⌉₊
⊢ rexp (1 - x) / (x + 1) ≤ rexp (2 - ↑⌈x⌉₊) / (x + 1)

Tactic:
gcongr

Result:
no goals

Proof state:
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
h₂ : 1 - x ≤ 2 - ↑⌈x⌉₊
⊢ x + 1 ≤ rexp (x + 1)

Tactic:
exact le_trans (le_add_of_nonneg_right zero_le_one) (add_one_le_exp _)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean
theorem posLog_mul {a b : ℝ} :
    log⁺ (a * b) ≤ log⁺ a + log⁺ b

Proof state:
a b : ℝ
⊢ log⁺ (a * b) ≤ log⁺ a + log⁺ b

Tactic:
by_cases ha : a = 0

Result:
case pos
a b : ℝ
ha : a = 0
⊢ log⁺ (a * b) ≤ log⁺ a + log⁺ b

case neg
a b : ℝ
ha : ¬a = 0
⊢ log⁺ (a * b) ≤ log⁺ a + log⁺ b

Proof state:
case pos
a b : ℝ
ha : ¬a = 0
hb : b = 0
⊢ log⁺ (a * b) ≤ log⁺ a + log⁺ b

Tactic:
simp [hb, posLog]

Result:
no goals

Proof state:
case neg
a b : ℝ
ha : ¬a = 0
hb : ¬b = 0
⊢ (0 + 0) ⊔ (log a + log b) ≤ 0 ⊔ log a + 0 ⊔ log b

Tactic:
exact max_add_add_le_max_add_max

Result:
no goals

Proof state:
case neg
a b : ℝ
ha : ¬a = 0
hb : ¬b = 0
⊢ 0 ⊔ log (a * b) ≤ 0 ⊔ log a + 0 ⊔ log b

Tactic:
nth_rw 1 [← add_zero 0, log_mul ha hb]

Result:
case neg
a b : ℝ
ha : ¬a = 0
hb : ¬b = 0
⊢ (0 + 0) ⊔ (log a + log b) ≤ 0 ⊔ log a + 0 ⊔ log b

Proof state:
case neg
a b : ℝ
ha : ¬a = 0
⊢ log⁺ (a * b) ≤ log⁺ a + log⁺ b

Tactic:
by_cases hb : b = 0

Result:
case pos
a b : ℝ
ha : ¬a = 0
hb : b = 0
⊢ log⁺ (a * b) ≤ log⁺ a + log⁺ b

case neg
a b : ℝ
ha : ¬a = 0
hb : ¬b = 0
⊢ log⁺ (a * b) ≤ log⁺ a + log⁺ b

Proof state:
case pos
a b : ℝ
ha : a = 0
⊢ log⁺ (a * b) ≤ log⁺ a + log⁺ b

Tactic:
simp [ha, posLog]

Result:
no goals

Proof state:
case neg
a b : ℝ
ha : ¬a = 0
hb : ¬b = 0
⊢ log⁺ (a * b) ≤ log⁺ a + log⁺ b

Tactic:
unfold posLog

Result:
case neg
a b : ℝ
ha : ¬a = 0
hb : ¬b = 0
⊢ 0 ⊔ log (a * b) ≤ 0 ⊔ log a + 0 ⊔ log b
-- Mathlib/AlgebraicGeometry/Scheme.lean
theorem app_eq {X Y : Scheme} (f : X ⟶ Y) {U V : Y.Opens} (e : U = V) :
    f.app U =
      Y.presheaf.map (eqToHom e.symm).op ≫
        f.app V ≫
          X.presheaf.map (eqToHom (congr_arg (Opens.map f.base).obj e)).op

Proof state:
case refl
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ Hom.app f U ≫ X.presheaf.map ((Opens.map f.base).map (inv (eqToHom ⋯).op).unop).op =
    Hom.app f U ≫ X.presheaf.map (eqToHom ⋯).op

Tactic:
rfl

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
U V : Y.Opens
e : U = V
⊢ Hom.app f U = Y.presheaf.map (eqToHom ⋯).op ≫ Hom.app f V ≫ X.presheaf.map (eqToHom ⋯).op

Tactic:
rw [← IsIso.inv_comp_eq, ← Functor.map_inv, f.naturality]

Result:
X Y : Scheme
f : X ⟶ Y
U V : Y.Opens
e : U = V
⊢ Hom.app f V ≫ X.presheaf.map ((Opens.map f.base).map (inv (eqToHom ⋯).op).unop).op =
    Hom.app f V ≫ X.presheaf.map (eqToHom ⋯).op

Proof state:
X Y : Scheme
f : X ⟶ Y
U V : Y.Opens
e : U = V
⊢ Hom.app f V ≫ X.presheaf.map ((Opens.map f.base).map (inv (eqToHom ⋯).op).unop).op =
    Hom.app f V ≫ X.presheaf.map (eqToHom ⋯).op

Tactic:
cases e

Result:
case refl
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ Hom.app f U ≫ X.presheaf.map ((Opens.map f.base).map (inv (eqToHom ⋯).op).unop).op =
    Hom.app f U ≫ X.presheaf.map (eqToHom ⋯).op