harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Bitwise.lean
lemma and_two_pow (n i : ℕ) : n &&& 2 ^ i = (n.testBit i).toNat * 2 ^ i

Proof state:
n i : ℕ
⊢ n &&& 2 ^ i = (n.testBit i).toNat * 2 ^ i

Tactic:
refine eq_of_testBit_eq fun j => ?_

Result:
n i j : ℕ
⊢ (n &&& 2 ^ i).testBit j = ((n.testBit i).toNat * 2 ^ i).testBit j

Proof state:
case inl.false
n i : ℕ
h : n.testBit i = false
⊢ (n &&& 2 ^ i).testBit i = (false.toNat * 2 ^ i).testBit i

Tactic:
simp [h]

Result:
no goals

Proof state:
case inl.true
n i : ℕ
h : n.testBit i = true
⊢ (n &&& 2 ^ i).testBit i = (true.toNat * 2 ^ i).testBit i

Tactic:
simp [h]

Result:
no goals

Proof state:
case inr.true
n i j : ℕ
hij : i ≠ j
h : n.testBit i = true
⊢ (n &&& 2 ^ i).testBit j = (true.toNat * 2 ^ i).testBit j

Tactic:
simp [h, testBit_two_pow_of_ne hij]

Result:
no goals

Proof state:
n i j : ℕ
⊢ (n &&& 2 ^ i).testBit j = ((n.testBit i).toNat * 2 ^ i).testBit j

Tactic:
obtain rfl | hij := Decidable.eq_or_ne i j <;> cases h : n.testBit i

Result:
case inl.false
n i : ℕ
h : n.testBit i = false
⊢ (n &&& 2 ^ i).testBit i = (false.toNat * 2 ^ i).testBit i

case inl.true
n i : ℕ
h : n.testBit i = true
⊢ (n &&& 2 ^ i).testBit i = (true.toNat * 2 ^ i).testBit i

case inr.false
n i j : ℕ
hij : i ≠ j
h : n.testBit i = false
⊢ (n &&& 2 ^ i).testBit j = (false.toNat * 2 ^ i).testBit j

case inr.true
n i j : ℕ
hij : i ≠ j
h : n.testBit i = true
⊢ (n &&& 2 ^ i).testBit j = (true.toNat * 2 ^ i).testBit j

Proof state:
case inr.false
n i j : ℕ
hij : i ≠ j
h : n.testBit i = false
⊢ (n &&& 2 ^ i).testBit j = (false.toNat * 2 ^ i).testBit j

Tactic:
simp [h, testBit_two_pow_of_ne hij]

Result:
no goals
-- Mathlib/Topology/FiberBundle/Constructions.lean
theorem Prod.right_inv {x : B × F₁ × F₂}
    (h : x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ (univ : Set (F₁ × F₂))) :
    Prod.toFun' e₁ e₂ (Prod.invFun' e₁ e₂ x) = x

Proof state:
case mk.mk
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
x : B
w₁ : F₁
w₂ : F₂
h : (x, w₁, w₂) ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ
⊢ toFun' e₁ e₂ (invFun' e₁ e₂ (x, w₁, w₂)) = (x, w₁, w₂)

Tactic:
obtain ⟨⟨h₁ : x ∈ e₁.baseSet, h₂ : x ∈ e₂.baseSet⟩, -⟩ := h

Result:
case mk.mk.intro.intro
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
x : B
w₁ : F₁
w₂ : F₂
h₁ : x ∈ e₁.baseSet
h₂ : x ∈ e₂.baseSet
⊢ toFun' e₁ e₂ (invFun' e₁ e₂ (x, w₁, w₂)) = (x, w₁, w₂)

Proof state:
case mk.mk.intro.intro
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
x : B
w₁ : F₁
w₂ : F₂
h₁ : x ∈ e₁.baseSet
h₂ : x ∈ e₂.baseSet
⊢ toFun' e₁ e₂ (invFun' e₁ e₂ (x, w₁, w₂)) = (x, w₁, w₂)

Tactic:
simp only [Prod.toFun', Prod.invFun', apply_mk_symm, h₁, h₂]

Result:
no goals

Proof state:
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
x : B × F₁ × F₂
h : x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ
⊢ toFun' e₁ e₂ (invFun' e₁ e₂ x) = x

Tactic:
obtain ⟨x, w₁, w₂⟩ := x

Result:
case mk.mk
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
x : B
w₁ : F₁
w₂ : F₂
h : (x, w₁, w₂) ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ
⊢ toFun' e₁ e₂ (invFun' e₁ e₂ (x, w₁, w₂)) = (x, w₁, w₂)
-- Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean
theorem tendsto_log_gamma {x : ℝ} (hx : 0 < x) :
    Tendsto (logGammaSeq x) atTop (𝓝 <| log (Gamma x))

Proof state:
x : ℝ
hx : 0 < x
⊢ log (Gamma x) = (log ∘ Gamma) x - (log ∘ Gamma) 1

Tactic:
simp_rw [Function.comp_apply, Gamma_one, log_one, sub_zero]

Result:
no goals

Proof state:
x : ℝ
hx : 0 < x
this : log (Gamma x) = (log ∘ Gamma) x - (log ∘ Gamma) 1
y : ℝ
hy : 0 < y
⊢ (log ∘ Gamma) (y + 1) = (log ∘ Gamma) y + log y

Tactic:
rw [Function.comp_apply, Gamma_add_one hy.ne', log_mul hy.ne' (Gamma_pos_of_pos hy).ne', add_comm,
  Function.comp_apply]

Result:
no goals

Proof state:
x : ℝ
hx : 0 < x
this : log (Gamma x) = (log ∘ Gamma) x - (log ∘ Gamma) 1
⊢ Tendsto (logGammaSeq x) atTop (𝓝 ((log ∘ Gamma) x - (log ∘ Gamma) 1))

Tactic:
refine BohrMollerup.tendsto_logGammaSeq convexOn_log_Gamma (fun {y} hy => ?_) hx

Result:
x : ℝ
hx : 0 < x
this : log (Gamma x) = (log ∘ Gamma) x - (log ∘ Gamma) 1
y : ℝ
hy : 0 < y
⊢ (log ∘ Gamma) (y + 1) = (log ∘ Gamma) y + log y

Proof state:
x : ℝ
hx : 0 < x
this : log (Gamma x) = (log ∘ Gamma) x - (log ∘ Gamma) 1
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (log (Gamma x)))

Tactic:
rw [this]

Result:
x : ℝ
hx : 0 < x
this : log (Gamma x) = (log ∘ Gamma) x - (log ∘ Gamma) 1
⊢ Tendsto (logGammaSeq x) atTop (𝓝 ((log ∘ Gamma) x - (log ∘ Gamma) 1))

Proof state:
x : ℝ
hx : 0 < x
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (log (Gamma x)))

Tactic:
have : log (Gamma x) = (log ∘ Gamma) x - (log ∘ Gamma) 1 := by
  simp_rw [Function.comp_apply, Gamma_one, log_one, sub_zero]

Result:
x : ℝ
hx : 0 < x
this : log (Gamma x) = (log ∘ Gamma) x - (log ∘ Gamma) 1
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (log (Gamma x)))
-- Mathlib/Data/List/TakeDrop.lean
lemma drop_length_sub_one {l : List α} (h : l ≠ []) : l.drop (l.length - 1) = [l.getLast h]

Proof state:
case neg
α : Type u
a : α
l : List α
ih : ∀ (h : l ≠ []), drop (l.length - 1) l = [l.getLast h]
h : a :: l ≠ []
hl : ¬l = []
⊢ drop ((a :: l).length - 1) (a :: l) = [(a :: l).getLast h]

Tactic:
rw [length_cons, Nat.add_one_sub_one, List.drop_length_cons hl a]

Result:
case neg
α : Type u
a : α
l : List α
ih : ∀ (h : l ≠ []), drop (l.length - 1) l = [l.getLast h]
h : a :: l ≠ []
hl : ¬l = []
⊢ [l.getLast hl] = [(a :: l).getLast h]

Proof state:
case cons
α : Type u
a : α
l : List α
ih : ∀ (h : l ≠ []), drop (l.length - 1) l = [l.getLast h]
h : a :: l ≠ []
⊢ drop ((a :: l).length - 1) (a :: l) = [(a :: l).getLast h]

Tactic:
by_cases hl : l = []

Result:
case pos
α : Type u
a : α
l : List α
ih : ∀ (h : l ≠ []), drop (l.length - 1) l = [l.getLast h]
h : a :: l ≠ []
hl : l = []
⊢ drop ((a :: l).length - 1) (a :: l) = [(a :: l).getLast h]

case neg
α : Type u
a : α
l : List α
ih : ∀ (h : l ≠ []), drop (l.length - 1) l = [l.getLast h]
h : a :: l ≠ []
hl : ¬l = []
⊢ drop ((a :: l).length - 1) (a :: l) = [(a :: l).getLast h]

Proof state:
case pos
α : Type u
a : α
l : List α
ih : ∀ (h : l ≠ []), drop (l.length - 1) l = [l.getLast h]
h : a :: l ≠ []
hl : l = []
⊢ drop ((a :: l).length - 1) (a :: l) = [(a :: l).getLast h]

Tactic:
aesop

Result:
no goals

Proof state:
case nil
α : Type u
h : [] ≠ []
⊢ drop ([].length - 1) [] = [[].getLast h]

Tactic:
aesop

Result:
no goals

Proof state:
case neg
α : Type u
a : α
l : List α
ih : ∀ (h : l ≠ []), drop (l.length - 1) l = [l.getLast h]
h : a :: l ≠ []
hl : ¬l = []
⊢ [l.getLast hl] = [(a :: l).getLast h]

Tactic:
simp [getLast_cons, hl]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean
lemma in₂₁_iff' :
    (graph t).Adj (in₂ c) (in₁ b) ↔ ∃ x : α × β × γ, x ∈ t ∧ x.2.2 = c ∧ x.2.1 = b where
  mp

Proof state:
case intro.mk.mk.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (graph t).Adj (in₂ (a, b, c).2.2) (in₁ (a, b, c).2.1)

Tactic:
constructor

Result:
case intro.mk.mk.intro.intro.a
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (?intro.mk.mk.intro.intro.a, (a, b, c).2.1, (a, b, c).2.2) ∈ t

case intro.mk.mk.intro.intro.a
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ α

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b : β
c : γ
⊢ (graph t).Adj (in₂ c) (in₁ b) → ∃ x ∈ t, x.2.2 = c ∧ x.2.1 = b

Tactic:
rintro ⟨⟩

Result:
case in₂₁
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b : β
c : γ
a✝¹ : α
a✝ : (a✝¹, b, c) ∈ t
⊢ ∃ x ∈ t, x.2.2 = c ∧ x.2.1 = b

Proof state:
case in₂₁
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b : β
c : γ
a✝¹ : α
a✝ : (a✝¹, b, c) ∈ t
⊢ ∃ x ∈ t, x.2.2 = c ∧ x.2.1 = b

Tactic:
exact ⟨_, ‹_›, by simp⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b : β
c : γ
⊢ (∃ x ∈ t, x.2.2 = c ∧ x.2.1 = b) → (graph t).Adj (in₂ c) (in₁ b)

Tactic:
rintro ⟨⟨a, b, c⟩, h, rfl, rfl⟩

Result:
case intro.mk.mk.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (graph t).Adj (in₂ (a, b, c).2.2) (in₁ (a, b, c).2.1)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b : β
c : γ
a✝¹ : α
a✝ : (a✝¹, b, c) ∈ t
⊢ (a✝¹, b, c).2.2 = c ∧ (a✝¹, b, c).2.1 = b

Tactic:
simp

Result:
no goals

Proof state:
case intro.mk.mk.intro.intro.a
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (?intro.mk.mk.intro.intro.a, (a, b, c).2.1, (a, b, c).2.2) ∈ t

case intro.mk.mk.intro.intro.a
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ α

Tactic:
assumption

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Pairwise.lean
theorem pairwise_extract {as : Array α} (h : as.Pairwise R) (start stop) :
    (as.extract start stop).Pairwise R

Proof state:
case a
α : Type u_1
R : α → α → Prop
as : Array α
start stop : Nat
h : ∀ (i j : Nat) (x : i < as.size) (x_1 : j < as.size), i < j → R as[i] as[j]
i✝ j✝ : Nat
x✝¹ : i✝ < min stop as.size - start
x✝ : j✝ < min stop as.size - start
hlt : i✝ < j✝
⊢ start + i✝ < start + j✝

Tactic:
exact Nat.add_lt_add_left hlt start

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
as : Array α
start stop : Nat
h : ∀ (i j : Nat) (x : i < as.size) (x_1 : j < as.size), i < j → R as[i] as[j]
i✝ j✝ : Nat
x✝¹ : i✝ < min stop as.size - start
x✝ : j✝ < min stop as.size - start
hlt : i✝ < j✝
⊢ R as[start + i✝] as[start + j✝]

Tactic:
apply h

Result:
case a
α : Type u_1
R : α → α → Prop
as : Array α
start stop : Nat
h : ∀ (i j : Nat) (x : i < as.size) (x_1 : j < as.size), i < j → R as[i] as[j]
i✝ j✝ : Nat
x✝¹ : i✝ < min stop as.size - start
x✝ : j✝ < min stop as.size - start
hlt : i✝ < j✝
⊢ start + i✝ < start + j✝

Proof state:
α : Type u_1
R : α → α → Prop
as : Array α
start stop : Nat
h : ∀ (i j : Nat) (x : i < as.size) (x_1 : j < as.size), i < j → R as[i] as[j]
⊢ ∀ (i j : Nat) (x : i < min stop as.size - start) (x_1 : j < min stop as.size - start),
    i < j → R as[start + i] as[start + j]

Tactic:
intro _ _ _ _ hlt

Result:
α : Type u_1
R : α → α → Prop
as : Array α
start stop : Nat
h : ∀ (i j : Nat) (x : i < as.size) (x_1 : j < as.size), i < j → R as[i] as[j]
i✝ j✝ : Nat
x✝¹ : i✝ < min stop as.size - start
x✝ : j✝ < min stop as.size - start
hlt : i✝ < j✝
⊢ R as[start + i✝] as[start + j✝]

Proof state:
α : Type u_1
R : α → α → Prop
as : Array α
h : Pairwise R as
start stop : Nat
⊢ Pairwise R (as.extract start stop)

Tactic:
simp only [pairwise_iff_getElem, getElem_extract, size_extract] at h ⊢

Result:
α : Type u_1
R : α → α → Prop
as : Array α
start stop : Nat
h : ∀ (i j : Nat) (x : i < as.size) (x_1 : j < as.size), i < j → R as[i] as[j]
⊢ ∀ (i j : Nat) (x : i < min stop as.size - start) (x_1 : j < min stop as.size - start),
    i < j → R as[start + i] as[start + j]
-- Mathlib/Probability/Independence/Kernel.lean
lemma indepSets_congr (h : κ =ᵐ[μ] η) : IndepSets s1 s2 κ μ ↔ IndepSets s1 s2 η μ

Proof state:
case h
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
s1 s2 : Set (Set Ω)
h : ⇑κ =ᶠ[ae μ] ⇑η
a✝³ a✝² : Set Ω
a✝¹ : a✝³ ∈ s1
a✝ : a✝² ∈ s2
h' : ∀ᵐ (a : α) ∂μ, (η a) (a✝³ ∩ a✝²) = (η a) a✝³ * (η a) a✝²
a : α
ha : κ a = η a
h'a : (η a) (a✝³ ∩ a✝²) = (η a) a✝³ * (η a) a✝²
⊢ (κ a) (a✝³ ∩ a✝²) = (κ a) a✝³ * (κ a) a✝²

Tactic:
simpa [ha] using h'a

Result:
no goals

Proof state:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
s1 s2 : Set (Set Ω)
h : ⇑κ =ᶠ[ae μ] ⇑η
⊢ IndepSets s1 s2 κ μ ↔ IndepSets s1 s2 η μ

Tactic:
peel 4

Result:
case h.h.h.h
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
s1 s2 : Set (Set Ω)
h : ⇑κ =ᶠ[ae μ] ⇑η
a✝³ a✝² : Set Ω
a✝¹ : a✝³ ∈ s1
a✝ : a✝² ∈ s2
⊢ (∀ᵐ (a : α) ∂μ, (κ a) (a✝³ ∩ a✝²) = (κ a) a✝³ * (κ a) a✝²) ↔ ∀ᵐ (a : α) ∂μ, (η a) (a✝³ ∩ a✝²) = (η a) a✝³ * (η a) a✝²

Proof state:
case h.h.h.h.refine_2
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
s1 s2 : Set (Set Ω)
h : ⇑κ =ᶠ[ae μ] ⇑η
a✝³ a✝² : Set Ω
a✝¹ : a✝³ ∈ s1
a✝ : a✝² ∈ s2
h' : ∀ᵐ (a : α) ∂μ, (η a) (a✝³ ∩ a✝²) = (η a) a✝³ * (η a) a✝²
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (a✝³ ∩ a✝²) = (κ a) a✝³ * (κ a) a✝²

Tactic:
filter_upwards [h, h'] with a ha h'a

Result:
case h
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
s1 s2 : Set (Set Ω)
h : ⇑κ =ᶠ[ae μ] ⇑η
a✝³ a✝² : Set Ω
a✝¹ : a✝³ ∈ s1
a✝ : a✝² ∈ s2
h' : ∀ᵐ (a : α) ∂μ, (η a) (a✝³ ∩ a✝²) = (η a) a✝³ * (η a) a✝²
a : α
ha : κ a = η a
h'a : (η a) (a✝³ ∩ a✝²) = (η a) a✝³ * (η a) a✝²
⊢ (κ a) (a✝³ ∩ a✝²) = (κ a) a✝³ * (κ a) a✝²
-- Mathlib/CategoryTheory/Subpresheaf/Sieves.lean
theorem family_of_elements_compatible {U : Cᵒᵖ} (s : F.obj U) :
    (G.familyOfElementsOfSection s).Compatible

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
U : Cᵒᵖ
s : F.obj U
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ unop U
f₂ : Y₂ ⟶ unop U
h₁ : (G.sieveOfSection s).arrows f₁
h₂ : (G.sieveOfSection s).arrows f₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ G.toPresheaf.map g₁.op (G.familyOfElementsOfSection s f₁ h₁) =
    G.toPresheaf.map g₂.op (G.familyOfElementsOfSection s f₂ h₂)

Tactic:
refine Subtype.ext ?_

Result:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
U : Cᵒᵖ
s : F.obj U
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ unop U
f₂ : Y₂ ⟶ unop U
h₁ : (G.sieveOfSection s).arrows f₁
h₂ : (G.sieveOfSection s).arrows f₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ ↑(G.toPresheaf.map g₁.op (G.familyOfElementsOfSection s f₁ h₁)) =
    ↑(G.toPresheaf.map g₂.op (G.familyOfElementsOfSection s f₂ h₂))

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
U : Cᵒᵖ
s : F.obj U
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ unop U
f₂ : Y₂ ⟶ unop U
h₁ : (G.sieveOfSection s).arrows f₁
h₂ : (G.sieveOfSection s).arrows f₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ ↑(G.toPresheaf.map g₁.op (G.familyOfElementsOfSection s f₁ h₁)) =
    ↑(G.toPresheaf.map g₂.op (G.familyOfElementsOfSection s f₂ h₂))

Tactic:
change F.map g₁.op (F.map f₁.op s) = F.map g₂.op (F.map f₂.op s)

Result:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
U : Cᵒᵖ
s : F.obj U
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ unop U
f₂ : Y₂ ⟶ unop U
h₁ : (G.sieveOfSection s).arrows f₁
h₂ : (G.sieveOfSection s).arrows f₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ F.map g₁.op (F.map f₁.op s) = F.map g₂.op (F.map f₂.op s)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
U : Cᵒᵖ
s : F.obj U
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ unop U
f₂ : Y₂ ⟶ unop U
h₁ : (G.sieveOfSection s).arrows f₁
h₂ : (G.sieveOfSection s).arrows f₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ F.map g₁.op (F.map f₁.op s) = F.map g₂.op (F.map f₂.op s)

Tactic:
rw [← FunctorToTypes.map_comp_apply, ← FunctorToTypes.map_comp_apply, ← op_comp, ← op_comp, e]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
U : Cᵒᵖ
s : F.obj U
⊢ (G.familyOfElementsOfSection s).Compatible

Tactic:
intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ e

Result:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
U : Cᵒᵖ
s : F.obj U
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ unop U
f₂ : Y₂ ⟶ unop U
h₁ : (G.sieveOfSection s).arrows f₁
h₂ : (G.sieveOfSection s).arrows f₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ G.toPresheaf.map g₁.op (G.familyOfElementsOfSection s f₁ h₁) =
    G.toPresheaf.map g₂.op (G.familyOfElementsOfSection s f₂ h₂)
-- Mathlib/CategoryTheory/Sites/Closed.lean
theorem classifier_isSheaf : Presieve.IsSheaf J₁ (Functor.closedSieves J₁)

Proof state:
case refine_1.mk.mk.a.h.mp
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.unop (Opposite.op X))
hM : J₁.IsClosed M
N : Sieve (Opposite.unop (Opposite.op X))
hN : J₁.IsClosed N
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : J₁.Covers M f
⊢ Sieve.pullback f (M ⊓ S) ∈ J₁ Y

Tactic:
apply J₁.arrow_intersect f M S hf (J₁.pullback_stable _ hS)

Result:
no goals

Proof state:
case refine_1.mk.mk.a.h.mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.unop (Opposite.op X))
hM : J₁.IsClosed M
N : Sieve (Opposite.unop (Opposite.op X))
hN : J₁.IsClosed N
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
⊢ J₁.Covers N f → J₁.Covers M f

Tactic:
intro hf

Result:
case refine_1.mk.mk.a.h.mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
M : Sieve (Opposite.unop (Opposite.op X))
hM : J₁.IsClosed M
N : Sieve (Opposite.unop (Opposite.op X))
hN : J₁.IsClosed N
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : J₁.Covers N f
⊢ J₁.Covers M f

Proof state:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : x.SieveCompatible
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
this : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : S.arrows f), Sieve.pullback f M = ↑(x f hf)
⊢ ∃ t, x.IsAmalgamation t

Tactic:
refine ⟨⟨_, J₁.close_isClosed M⟩, ?_⟩

Result:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁) S.arrows
hx : x.SieveCompatible
M : Sieve X := Sieve.bind S.arrows fun Y f hf => ↑(x f hf)
this : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : S.arrows f), Sieve.pullback f M = ↑(x f hf)
⊢ x.IsAmalgamation ⟨J₁.close M, ⋯⟩
-- Mathlib/Logic/Function/Iterate.lean
lemma iterate_cancel (hf : Injective f) (ha : f^[m] a = f^[n] a) : f^[m - n] a = a

Proof state:
α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : n ≤ m
⊢ f^[m - n + ?m.8006] a = f^[?m.8006] a

Tactic:
rwa [Nat.sub_add_cancel h]

Result:
no goals

Proof state:
case inr
α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : n ≤ m
⊢ f^[m - n] a = a

Tactic:
{ exact iterate_cancel_of_add hf (by rwa [Nat.sub_add_cancel h]) }

Result:
no goals

Proof state:
case inl
α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : m ≤ n
⊢ f^[m - n] a = a

Tactic:
simp [Nat.sub_eq_zero_of_le h]

Result:
no goals

Proof state:
α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
⊢ f^[m - n] a = a

Tactic:
obtain h | h := Nat.le_total m n

Result:
case inl
α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : m ≤ n
⊢ f^[m - n] a = a

case inr
α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : n ≤ m
⊢ f^[m - n] a = a

Proof state:
case inl
α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : m ≤ n
⊢ f^[m - n] a = a

case inr
α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : n ≤ m
⊢ f^[m - n] a = a

Tactic:
{ simp [Nat.sub_eq_zero_of_le h] }

Result:
case inr
α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : n ≤ m
⊢ f^[m - n] a = a

Proof state:
case inr
α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : n ≤ m
⊢ f^[m - n] a = a

Tactic:
exact iterate_cancel_of_add hf (by rwa [Nat.sub_add_cancel h])

Result:
no goals