harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem nhds_nhds_eq_uniformity_uniformity_prod {a b : α} :
    𝓝 a ×ˢ 𝓝 b = (𝓤 α).lift fun s : Set (α × α) =>
      (𝓤 α).lift' fun t => { y : α | (y, a) ∈ s } ×ˢ { y : α | (b, y) ∈ t }

Proof state:
α : Type ua
inst✝ : UniformSpace α
a b : α
⊢ ((𝓤 α).lift fun s => (𝓤 α).lift' fun t => {y | (y, a) ∈ s} ×ˢ ball b t) =
    (𝓤 α).lift fun s => (𝓤 α).lift' fun t => {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}

case hg₁
α : Type ua
inst✝ : UniformSpace α
a b : α
⊢ Monotone fun s => {y | (y, a) ∈ s}

case hg₂
α : Type ua
inst✝ : UniformSpace α
a b : α
⊢ Monotone (ball b)

Tactic:
exacts [rfl, monotone_preimage, monotone_preimage]

Result:
no goals

Proof state:
α : Type ua
inst✝ : UniformSpace α
a b : α
⊢ 𝓝 a ×ˢ 𝓝 b = (𝓤 α).lift fun s => (𝓤 α).lift' fun t => {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}

Tactic:
rw [nhds_eq_uniformity', nhds_eq_uniformity, prod_lift'_lift']

Result:
α : Type ua
inst✝ : UniformSpace α
a b : α
⊢ ((𝓤 α).lift fun s => (𝓤 α).lift' fun t => {y | (y, a) ∈ s} ×ˢ ball b t) =
    (𝓤 α).lift fun s => (𝓤 α).lift' fun t => {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}

case hg₁
α : Type ua
inst✝ : UniformSpace α
a b : α
⊢ Monotone fun s => {y | (y, a) ∈ s}

case hg₂
α : Type ua
inst✝ : UniformSpace α
a b : α
⊢ Monotone (ball b)
-- Mathlib/Data/Real/ConjExponents.lean
lemma top_one : IsConjExponent ∞ 1 := ⟨by simp⟩

Proof state:
⊢ ⊤⁻¹ + 1⁻¹ = 1

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem HasDerivWithinAt.comp_of_eq (hh₂ : HasDerivWithinAt h₂ h₂' s' y)
    (hh : HasDerivWithinAt h h' s x) (hst : MapsTo h s s') (hy : y = h x) :
    HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
hh₂ : HasDerivWithinAt h₂ h₂' s' y
hh : HasDerivWithinAt h h' s x
hst : MapsTo h s s'
hy : y = h x
⊢ HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x

Tactic:
rw [hy] at hh₂

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
hh₂ : HasDerivWithinAt h₂ h₂' s' (h x)
hh : HasDerivWithinAt h h' s x
hst : MapsTo h s s'
hy : y = h x
⊢ HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
hh₂ : HasDerivWithinAt h₂ h₂' s' (h x)
hh : HasDerivWithinAt h h' s x
hst : MapsTo h s s'
hy : y = h x
⊢ HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x

Tactic:
exact hh₂.comp x hh hst

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Divisibility.lean
theorem ne_zero_of_dvd_ne_zero {p q : α} (h₁ : q ≠ 0) (h₂ : p ∣ q) : p ≠ 0

Proof state:
case intro
α : Type u_1
inst✝ : MonoidWithZero α
p u : α
h₁ : p * u ≠ 0
⊢ p ≠ 0

Tactic:
exact left_ne_zero_of_mul h₁

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MonoidWithZero α
p q : α
h₁ : q ≠ 0
h₂ : p ∣ q
⊢ p ≠ 0

Tactic:
rcases h₂ with ⟨u, rfl⟩

Result:
case intro
α : Type u_1
inst✝ : MonoidWithZero α
p u : α
h₁ : p * u ≠ 0
⊢ p ≠ 0
-- Mathlib/Logic/IsEmpty.lean
theorem isEmpty_fun : IsEmpty (α → β) ↔ Nonempty α ∧ IsEmpty β

Proof state:
α : Sort u_1
β : Sort u_2
⊢ IsEmpty (α → β) ↔ Nonempty α ∧ IsEmpty β

Tactic:
rw [isEmpty_pi, ← exists_true_iff_nonempty, ← exists_and_right, true_and]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem getElem?_eraseIdx_of_lt (l : Array α) (i : Nat) (h : i < l.size) (j : Nat) (h' : j < i) :
    (l.eraseIdx i)[j]? = l[j]?

Proof state:
α : Type u_1
l : Array α
i : Nat
h : i < l.size
j : Nat
h' : j < i
⊢ (l.eraseIdx i h)[j]? = l[j]?

Tactic:
rw [getElem?_eraseIdx]

Result:
α : Type u_1
l : Array α
i : Nat
h : i < l.size
j : Nat
h' : j < i
⊢ (if j < i then l[j]? else l[j + 1]?) = l[j]?

Proof state:
α : Type u_1
l : Array α
i : Nat
h : i < l.size
j : Nat
h' : j < i
⊢ (if j < i then l[j]? else l[j + 1]?) = l[j]?

Tactic:
simp [h']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lex.lean
theorem lex_eq_true_iff_exists [BEq α] (lt : α → α → Bool) :
    lex l₁ l₂ lt = true ↔
      (l₁.isEqv (l₂.take l₁.length) (· == ·) ∧ l₁.length < l₂.length) ∨
        (∃ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length),
          (∀ j, (hj : j < i) →
            l₁[j]'(Nat.lt_trans hj h₁) == l₂[j]'(Nat.lt_trans hj h₂)) ∧ lt l₁[i] l₂[i])

Proof state:
case cons.cons.mpr.inr.intro.intro.intro.intro.succ
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
a : α
l₁ : List α
ih :
  ∀ {l₂ : List α},
    l₁.lex l₂ lt = true ↔
      (l₁.isEqv (take l₁.length l₂) fun x1 x2 => x1 == x2) = true ∧ l₁.length < l₂.length ∨
        ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₁[i] l₂[i] = true
b : α
l₂ : List α
i : Nat
h₁ : i + 1 < l₁.length + 1
h₂ : i + 1 < l₂.length + 1
w₁ : ∀ (j : Nat) (hj : j < i + 1), ((a :: l₁)[j] == (b :: l₂)[j]) = true
w₂ : lt (a :: l₁)[i + 1] (b :: l₂)[i + 1] = true
⊢ lt a b = true ∨
    (a == b) = true ∧
      ((l₁.isEqv (take l₁.length l₂) fun x1 x2 => x1 == x2) = true ∧ l₁.length < l₂.length ∨
        ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₁[i] l₂[i] = true)

Tactic:
right

Result:
case cons.cons.mpr.inr.intro.intro.intro.intro.succ.h
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
a : α
l₁ : List α
ih :
  ∀ {l₂ : List α},
    l₁.lex l₂ lt = true ↔
      (l₁.isEqv (take l₁.length l₂) fun x1 x2 => x1 == x2) = true ∧ l₁.length < l₂.length ∨
        ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₁[i] l₂[i] = true
b : α
l₂ : List α
i : Nat
h₁ : i + 1 < l₁.length + 1
h₂ : i + 1 < l₂.length + 1
w₁ : ∀ (j : Nat) (hj : j < i + 1), ((a :: l₁)[j] == (b :: l₂)[j]) = true
w₂ : lt (a :: l₁)[i + 1] (b :: l₂)[i + 1] = true
⊢ (a == b) = true ∧
    ((l₁.isEqv (take l₁.length l₂) fun x1 x2 => x1 == x2) = true ∧ l₁.length < l₂.length ∨
      ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₁[i] l₂[i] = true)
-- Mathlib/Order/Filter/Prod.lean
theorem map_swap4_prod {h : Filter γ} {k : Filter δ} :
    map (fun p : (α × β) × γ × δ => ((p.1.1, p.2.1), (p.1.2, p.2.2))) ((f ×ˢ g) ×ˢ (h ×ˢ k)) =
      (f ×ˢ h) ×ˢ (g ×ˢ k)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : Filter α
g : Filter β
h : Filter γ
k : Filter δ
⊢ comap ((Prod.fst ∘ Prod.fst) ∘ fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) f ⊓
        comap ((Prod.snd ∘ Prod.fst) ∘ fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) g ⊓
      (comap ((Prod.fst ∘ Prod.snd) ∘ fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) h ⊓
        comap ((Prod.snd ∘ Prod.snd) ∘ fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) k) =
    comap (Prod.fst ∘ Prod.fst) f ⊓ comap (Prod.snd ∘ Prod.fst) h ⊓
      (comap (Prod.fst ∘ Prod.snd) g ⊓ comap (Prod.snd ∘ Prod.snd) k)

Tactic:
ac_rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : Filter α
g : Filter β
h : Filter γ
k : Filter δ
⊢ map (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ((f ×ˢ g) ×ˢ h ×ˢ k) = (f ×ˢ h) ×ˢ g ×ˢ k

Tactic:
simp_rw [map_swap4_eq_comap, prod_eq_inf, comap_inf, comap_comap]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : Filter α
g : Filter β
h : Filter γ
k : Filter δ
⊢ comap ((Prod.fst ∘ Prod.fst) ∘ fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) f ⊓
        comap ((Prod.snd ∘ Prod.fst) ∘ fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) g ⊓
      (comap ((Prod.fst ∘ Prod.snd) ∘ fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) h ⊓
        comap ((Prod.snd ∘ Prod.snd) ∘ fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) k) =
    comap (Prod.fst ∘ Prod.fst) f ⊓ comap (Prod.snd ∘ Prod.fst) h ⊓
      (comap (Prod.fst ∘ Prod.snd) g ⊓ comap (Prod.snd ∘ Prod.snd) k)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Monadic.lean
theorem foldlM_map [Monad m] (f : β₁ → β₂) (g : α → β₂ → m α) (l : Array β₁) (init : α) (w : stop = l.size) :
    (l.map f).foldlM g init 0 stop = l.foldlM (fun x y => g x (f y)) init 0 stop

Proof state:
m : Type u_1 → Type u_2
β₁ : Type u_3
β₂ : Type u_4
α : Type u_1
stop : Nat
inst✝ : Monad m
f : β₁ → β₂
g : α → β₂ → m α
l : Array β₁
init : α
w : stop = l.size
⊢ foldlM g init (map f l) 0 stop = foldlM (fun x y => g x (f y)) init l 0 stop

Tactic:
subst w

Result:
m : Type u_1 → Type u_2
β₁ : Type u_3
β₂ : Type u_4
α : Type u_1
inst✝ : Monad m
f : β₁ → β₂
g : α → β₂ → m α
l : Array β₁
init : α
⊢ foldlM g init (map f l) 0 l.size = foldlM (fun x y => g x (f y)) init l

Proof state:
case mk
m : Type u_1 → Type u_2
β₁ : Type u_3
β₂ : Type u_4
α : Type u_1
inst✝ : Monad m
f : β₁ → β₂
g : α → β₂ → m α
init : α
toList✝ : List β₁
⊢ foldlM g init (map f { toList := toList✝ }) 0 { toList := toList✝ }.size =
    foldlM (fun x y => g x (f y)) init { toList := toList✝ }

Tactic:
simp [List.foldlM_map]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
β₁ : Type u_3
β₂ : Type u_4
α : Type u_1
inst✝ : Monad m
f : β₁ → β₂
g : α → β₂ → m α
l : Array β₁
init : α
⊢ foldlM g init (map f l) 0 l.size = foldlM (fun x y => g x (f y)) init l

Tactic:
cases l

Result:
case mk
m : Type u_1 → Type u_2
β₁ : Type u_3
β₂ : Type u_4
α : Type u_1
inst✝ : Monad m
f : β₁ → β₂
g : α → β₂ → m α
init : α
toList✝ : List β₁
⊢ foldlM g init (map f { toList := toList✝ }) 0 { toList := toList✝ }.size =
    foldlM (fun x y => g x (f y)) init { toList := toList✝ }
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem exists_of_mem_mapFinIdx {b : β} {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β}
    (h : b ∈ l.mapFinIdx f) : ∃ (i : Nat) (h : i < l.length), f i l[i] h = b

Proof state:
case intro.intro.intro
β : Type u_1
α : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
b : α
i : Nat
h✝ : l[i]? = some b
h : ∃ h, l[i] = b
⊢ ∃ i_1 h, f i_1 l[i_1] h = f i b ⋯

Tactic:
obtain ⟨h', rfl⟩ := h

Result:
case intro.intro.intro.intro
β : Type u_1
α : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
i : Nat
h' : i < l.length
h : l[i]? = some l[i]
⊢ ∃ i_1 h_1, f i_1 l[i_1] h_1 = f i l[i] ⋯

Proof state:
case intro.intro.intro
β : Type u_1
α : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
b : α
i : Nat
h : l[i]? = some b
⊢ ∃ i_1 h_1, f i_1 l[i_1] h_1 = f i b ⋯

Tactic:
rw [getElem?_eq_some_iff] at h

Result:
case intro.intro.intro
β : Type u_1
α : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
b : α
i : Nat
h✝ : l[i]? = some b
h : ∃ h, l[i] = b
⊢ ∃ i_1 h, f i_1 l[i_1] h = f i b ⋯

Proof state:
β : Type u_1
α : Type u_2
b : β
l : List α
f : (i : Nat) → α → i < l.length → β
h : ∃ a b_1 h, f b_1 a ⋯ = b
⊢ ∃ i h, f i l[i] h = b

Tactic:
obtain ⟨b, i, h, rfl⟩ := h

Result:
case intro.intro.intro
β : Type u_1
α : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
b : α
i : Nat
h : l[i]? = some b
⊢ ∃ i_1 h_1, f i_1 l[i_1] h_1 = f i b ⋯

Proof state:
β : Type u_1
α : Type u_2
b : β
l : List α
f : (i : Nat) → α → i < l.length → β
h : b ∈ l.mapFinIdx f
⊢ ∃ i h, f i l[i] h = b

Tactic:
rw [mapFinIdx_eq_zipIdx_map] at h

Result:
β : Type u_1
α : Type u_2
b : β
l : List α
f : (i : Nat) → α → i < l.length → β
h :
  b ∈
    map
      (fun x =>
        match x with
        | ⟨(x, i), m⟩ => f i x ⋯)
      l.zipIdx.attach
⊢ ∃ i h, f i l[i] h = b

Proof state:
β : Type u_1
α : Type u_2
b : β
l : List α
f : (i : Nat) → α → i < l.length → β
h :
  ∃ a,
    a ∈ l.zipIdx.attach ∧
      (match a with
        | ⟨(x, i), m⟩ => f i x ⋯) =
        b
⊢ ∃ i h, f i l[i] h = b

Tactic:
simp only [mem_attach, true_and, Subtype.exists, Prod.exists, mk_mem_zipIdx_iff_getElem?] at h

Result:
β : Type u_1
α : Type u_2
b : β
l : List α
f : (i : Nat) → α → i < l.length → β
h : ∃ a b_1 h, f b_1 a ⋯ = b
⊢ ∃ i h, f i l[i] h = b

Proof state:
case intro.intro.intro.intro
β : Type u_1
α : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
i : Nat
h' : i < l.length
h : l[i]? = some l[i]
⊢ ∃ i_1 h_1, f i_1 l[i_1] h_1 = f i l[i] ⋯

Tactic:
exact ⟨i, h', rfl⟩

Result:
no goals

Proof state:
β : Type u_1
α : Type u_2
b : β
l : List α
f : (i : Nat) → α → i < l.length → β
h :
  b ∈
    map
      (fun x =>
        match x with
        | ⟨(x, i), m⟩ => f i x ⋯)
      l.zipIdx.attach
⊢ ∃ i h, f i l[i] h = b

Tactic:
replace h := exists_of_mem_map h

Result:
β : Type u_1
α : Type u_2
b : β
l : List α
f : (i : Nat) → α → i < l.length → β
h :
  ∃ a,
    a ∈ l.zipIdx.attach ∧
      (match a with
        | ⟨(x, i), m⟩ => f i x ⋯) =
        b
⊢ ∃ i h, f i l[i] h = b
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem blsub_lt_ord_lift {o : Ordinal.{u}} {f : ∀ a < o, Ordinal} {c : Ordinal}
    (ho : Cardinal.lift.{v, u} o.card < c.cof) (hf : ∀ i hi, f i hi < c) : blsub.{u, v} o f < c :=
  lt_of_le_of_ne (blsub_le hf) fun h =>
    ho.not_le (by simpa [← iSup_ord, hf, h] using cof_blsub_le_lift.{u, v} f)

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
c : Ordinal.{max u v}
ho : Cardinal.lift.{v, u} o.card < c.cof
hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c
h : o.blsub f = c
⊢ c.cof ≤ Cardinal.lift.{v, u} o.card

Tactic:
simpa [← iSup_ord, hf, h] using cof_blsub_le_lift.{u, v} f

Result:
no goals
-- Mathlib/Algebra/Homology/TotalComplex.lean
@[reassoc (attr := simp)]
lemma d₁_mapMap (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) :
    K.d₁ c₁₂ i₁ i₂ i₁₂ ≫ GradedObject.mapMap (toGradedObjectMap φ) _ i₁₂ =
    (φ.f i₁).f i₂ ≫ L.d₁ c₁₂ i₁ i₂ i₁₂

Proof state:
case pos
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
c₁₂ : ComplexShape I₁₂
inst✝³ : TotalComplexShape c₁ c₂ c₁₂
inst✝² : DecidableEq I₁₂
inst✝¹ : K.HasTotal c₁₂
inst✝ : L.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : c₁.Rel i₁ (c₁.next i₁)
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂ ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ = (φ.f i₁).f i₂ ≫ L.d₁ c₁₂ i₁ i₂ i₁₂

Tactic:
simp [totalAux.d₁_eq' _ c₁₂ h]

Result:
no goals

Proof state:
case neg
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
c₁₂ : ComplexShape I₁₂
inst✝³ : TotalComplexShape c₁ c₂ c₁₂
inst✝² : DecidableEq I₁₂
inst✝¹ : K.HasTotal c₁₂
inst✝ : L.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : ¬c₁.Rel i₁ (c₁.next i₁)
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂ ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ = (φ.f i₁).f i₂ ≫ L.d₁ c₁₂ i₁ i₂ i₁₂

Tactic:
simp [d₁_eq_zero _ c₁₂ i₁ i₂ i₁₂ h]

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
c₁₂ : ComplexShape I₁₂
inst✝³ : TotalComplexShape c₁ c₂ c₁₂
inst✝² : DecidableEq I₁₂
inst✝¹ : K.HasTotal c₁₂
inst✝ : L.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂ ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ = (φ.f i₁).f i₂ ≫ L.d₁ c₁₂ i₁ i₂ i₁₂

Tactic:
by_cases h : c₁.Rel i₁ (c₁.next i₁)

Result:
case pos
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
c₁₂ : ComplexShape I₁₂
inst✝³ : TotalComplexShape c₁ c₂ c₁₂
inst✝² : DecidableEq I₁₂
inst✝¹ : K.HasTotal c₁₂
inst✝ : L.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : c₁.Rel i₁ (c₁.next i₁)
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂ ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ = (φ.f i₁).f i₂ ≫ L.d₁ c₁₂ i₁ i₂ i₁₂

case neg
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
c₁₂ : ComplexShape I₁₂
inst✝³ : TotalComplexShape c₁ c₂ c₁₂
inst✝² : DecidableEq I₁₂
inst✝¹ : K.HasTotal c₁₂
inst✝ : L.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : ¬c₁.Rel i₁ (c₁.next i₁)
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂ ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ = (φ.f i₁).f i₂ ≫ L.d₁ c₁₂ i₁ i₂ i₁₂
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem mem_dite_nil_right {x : α} [Decidable p] {l : p → List α} :
    (x ∈ if h : p then l h else []) ↔ ∃ h : p, x ∈ l h

Proof state:
α : Type u_1
p : Prop
x : α
inst✝ : Decidable p
l : p → List α
⊢ (x ∈ if h : p then l h else []) ↔ ∃ h, x ∈ l h

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_add_adjacent_intervals (hab : IntervalIntegrable f μ a b)
    (hbc : IntervalIntegrable f μ b c) :
    ((∫ x in a..b, f x ∂μ) + ∫ x in b..c, f x ∂μ) = ∫ x in a..c, f x ∂μ

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
⊢ ∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in b..c, f x ∂μ = ∫ (x : ℝ) in a..c, f x ∂μ

Tactic:
rw [← add_neg_eq_zero, ← integral_symm, integral_add_adjacent_intervals_cancel hab hbc]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem map_map [CommSemiring S₂] (g : S₁ →+* S₂) (p : MvPolynomial σ R) :
    map g (map f p) = map (g.comp f) p :=
  (eval₂_comp_left (map g) (C.comp f) X p).trans <| by
    congr
    · ext1 a
      simp only [map_C, comp_apply, RingHom.coe_comp]
    · ext1 n
      simp only [map_X, comp_apply]

Proof state:
case e_g.h
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
f : R →+* S₁
inst✝ : CommSemiring S₂
g : S₁ →+* S₂
p : MvPolynomial σ R
n : σ
⊢ (⇑(map g) ∘ X) n = X n

Tactic:
simp only [map_X, comp_apply]

Result:
no goals

Proof state:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
f : R →+* S₁
inst✝ : CommSemiring S₂
g : S₁ →+* S₂
p : MvPolynomial σ R
⊢ eval₂ ((map g).comp (C.comp f)) (⇑(map g) ∘ X) p = (map (g.comp f)) p

Tactic:
congr

Result:
case e_f
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
f : R →+* S₁
inst✝ : CommSemiring S₂
g : S₁ →+* S₂
p : MvPolynomial σ R
⊢ (map g).comp (C.comp f) = C.comp (g.comp f)

case e_g
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
f : R →+* S₁
inst✝ : CommSemiring S₂
g : S₁ →+* S₂
p : MvPolynomial σ R
⊢ ⇑(map g) ∘ X = X

Proof state:
case e_g
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
f : R →+* S₁
inst✝ : CommSemiring S₂
g : S₁ →+* S₂
p : MvPolynomial σ R
⊢ ⇑(map g) ∘ X = X

Tactic:
ext1 n

Result:
case e_g.h
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
f : R →+* S₁
inst✝ : CommSemiring S₂
g : S₁ →+* S₂
p : MvPolynomial σ R
n : σ
⊢ (⇑(map g) ∘ X) n = X n

Proof state:
case e_f.a
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
f : R →+* S₁
inst✝ : CommSemiring S₂
g : S₁ →+* S₂
p : MvPolynomial σ R
a : R
⊢ ((map g).comp (C.comp f)) a = (C.comp (g.comp f)) a

Tactic:
simp only [map_C, comp_apply, RingHom.coe_comp]

Result:
no goals

Proof state:
case e_f
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
f : R →+* S₁
inst✝ : CommSemiring S₂
g : S₁ →+* S₂
p : MvPolynomial σ R
⊢ (map g).comp (C.comp f) = C.comp (g.comp f)

Tactic:
ext1 a

Result:
case e_f.a
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
f : R →+* S₁
inst✝ : CommSemiring S₂
g : S₁ →+* S₂
p : MvPolynomial σ R
a : R
⊢ ((map g).comp (C.comp f)) a = (C.comp (g.comp f)) a
-- Mathlib/Order/SuccPred/Relation.lean
theorem reflTransGen_of_succ_of_ge (r : α → α → Prop) {n m : α} (h : ∀ i ∈ Ico m n, r (succ i) i)
    (hmn : m ≤ n) : ReflTransGen r n m

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
h : ∀ i ∈ Ico m n, r (succ i) i
hmn : m ≤ n
⊢ ReflTransGen r n m

Tactic:
rw [← reflTransGen_swap]

Result:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
h : ∀ i ∈ Ico m n, r (succ i) i
hmn : m ≤ n
⊢ ReflTransGen (swap r) m n

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
h : ∀ i ∈ Ico m n, r (succ i) i
hmn : m ≤ n
⊢ ReflTransGen (swap r) m n

Tactic:
exact reflTransGen_of_succ_of_le (swap r) h hmn

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem GoodProducts.span [WellFoundedLT I] (hC : IsClosed C) :
    ⊤ ≤ Submodule.span ℤ (Set.range (eval C))

Proof state:
case intro.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
hC : IsClosed C
K : Finset I
f' : LocallyConstant ↑(π C fun x => x ∈ K) ℤ
a✝ : (πJ C K) f' ∈ ⊤
⊢ (πJ C K) f' ∈ Submodule.span ℤ (Set.range (Products.eval C))

Tactic:
refine Submodule.span_mono ?_ <| Submodule.apply_mem_span_image_of_mem_span (πJ C K) <|
  spanFin C K (Submodule.mem_top : f' ∈ ⊤)

Result:
case intro.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
hC : IsClosed C
K : Finset I
f' : LocallyConstant ↑(π C fun x => x ∈ K) ℤ
a✝ : (πJ C K) f' ∈ ⊤
⊢ ⇑(πJ C K) '' Set.range (eval (π C fun x => x ∈ K)) ⊆ Set.range (Products.eval C)

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
hC : IsClosed C
⊢ ⊤ ≤ Submodule.span ℤ (Set.range (eval C))

Tactic:
rw [span_iff_products]

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
hC : IsClosed C
⊢ ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))

Proof state:
case intro.intro.intro.intro.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
hC : IsClosed C
K : Finset I
f' : LocallyConstant ↑(π C fun x => x ∈ K) ℤ
a✝ : (πJ C K) f' ∈ ⊤
m : { l // Products.isGood (π C fun x => x ∈ K) l }
⊢ (πJ C K) (eval (π C fun x => x ∈ K) m) ∈ Set.range (Products.eval C)

Tactic:
exact ⟨m.val, eval_eq_πJ C K m.val m.prop⟩

Result:
no goals

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
hC : IsClosed C
⊢ ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))

Tactic:
intro f _

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
hC : IsClosed C
f : LocallyConstant ↑C ℤ
a✝ : f ∈ ⊤
⊢ f ∈ Submodule.span ℤ (Set.range (Products.eval C))

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
hC : IsClosed C
f : LocallyConstant ↑C ℤ
a✝ : f ∈ ⊤
⊢ f ∈ Submodule.span ℤ (Set.range (Products.eval C))

Tactic:
obtain ⟨K, f', rfl⟩ : ∃ K f', f = πJ C K f' := fin_comap_jointlySurjective C hC f

Result:
case intro.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
hC : IsClosed C
K : Finset I
f' : LocallyConstant ↑(π C fun x => x ∈ K) ℤ
a✝ : (πJ C K) f' ∈ ⊤
⊢ (πJ C K) f' ∈ Submodule.span ℤ (Set.range (Products.eval C))

Proof state:
case intro.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
hC : IsClosed C
K : Finset I
f' : LocallyConstant ↑(π C fun x => x ∈ K) ℤ
a✝ : (πJ C K) f' ∈ ⊤
⊢ ⇑(πJ C K) '' Set.range (eval (π C fun x => x ∈ K)) ⊆ Set.range (Products.eval C)

Tactic:
rintro l ⟨y, ⟨m, rfl⟩, rfl⟩

Result:
case intro.intro.intro.intro.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
hC : IsClosed C
K : Finset I
f' : LocallyConstant ↑(π C fun x => x ∈ K) ℤ
a✝ : (πJ C K) f' ∈ ⊤
m : { l // Products.isGood (π C fun x => x ∈ K) l }
⊢ (πJ C K) (eval (π C fun x => x ∈ K) m) ∈ Set.range (Products.eval C)