harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem pmap_congr_left {p q : α → Prop} {f : ∀ a, p a → β} {g : ∀ a, q a → β} (l : Array α) {H₁ H₂}
    (h : ∀ a ∈ l, ∀ (h₁ h₂), f a h₁ = g a h₂) : pmap f l H₁ = pmap g l H₂

Proof state:
case mk
α : Type u_1
β : Type u_2
p q : α → Prop
f : (a : α) → p a → β
g : (a : α) → q a → β
toList✝ : List α
H₁ : ∀ (a : α), a ∈ { toList := toList✝ } → p a
H₂ : ∀ (a : α), a ∈ { toList := toList✝ } → q a
h : ∀ (a : α), a ∈ toList✝ → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂
⊢ pmap f { toList := toList✝ } H₁ = pmap g { toList := toList✝ } H₂

Tactic:
simp only [List.pmap_toArray, mk.injEq]

Result:
case mk
α : Type u_1
β : Type u_2
p q : α → Prop
f : (a : α) → p a → β
g : (a : α) → q a → β
toList✝ : List α
H₁ : ∀ (a : α), a ∈ { toList := toList✝ } → p a
H₂ : ∀ (a : α), a ∈ { toList := toList✝ } → q a
h : ∀ (a : α), a ∈ toList✝ → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂
⊢ List.pmap f toList✝ ⋯ = List.pmap g toList✝ ⋯

Proof state:
case mk
α : Type u_1
β : Type u_2
p q : α → Prop
f : (a : α) → p a → β
g : (a : α) → q a → β
toList✝ : List α
H₁ : ∀ (a : α), a ∈ { toList := toList✝ } → p a
H₂ : ∀ (a : α), a ∈ { toList := toList✝ } → q a
h : ∀ (a : α), a ∈ { toList := toList✝ } → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂
⊢ pmap f { toList := toList✝ } H₁ = pmap g { toList := toList✝ } H₂

Tactic:
simp only [mem_toArray] at h

Result:
case mk
α : Type u_1
β : Type u_2
p q : α → Prop
f : (a : α) → p a → β
g : (a : α) → q a → β
toList✝ : List α
H₁ : ∀ (a : α), a ∈ { toList := toList✝ } → p a
H₂ : ∀ (a : α), a ∈ { toList := toList✝ } → q a
h : ∀ (a : α), a ∈ toList✝ → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂
⊢ pmap f { toList := toList✝ } H₁ = pmap g { toList := toList✝ } H₂

Proof state:
case mk
α : Type u_1
β : Type u_2
p q : α → Prop
f : (a : α) → p a → β
g : (a : α) → q a → β
toList✝ : List α
H₁ : ∀ (a : α), a ∈ { toList := toList✝ } → p a
H₂ : ∀ (a : α), a ∈ { toList := toList✝ } → q a
h : ∀ (a : α), a ∈ toList✝ → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂
⊢ List.pmap f toList✝ ⋯ = List.pmap g toList✝ ⋯

Tactic:
rw [List.pmap_congr_left _ h]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p q : α → Prop
f : (a : α) → p a → β
g : (a : α) → q a → β
l : Array α
H₁ : ∀ (a : α), a ∈ l → p a
H₂ : ∀ (a : α), a ∈ l → q a
h : ∀ (a : α), a ∈ l → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂
⊢ pmap f l H₁ = pmap g l H₂

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
p q : α → Prop
f : (a : α) → p a → β
g : (a : α) → q a → β
toList✝ : List α
H₁ : ∀ (a : α), a ∈ { toList := toList✝ } → p a
H₂ : ∀ (a : α), a ∈ { toList := toList✝ } → q a
h : ∀ (a : α), a ∈ { toList := toList✝ } → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂
⊢ pmap f { toList := toList✝ } H₁ = pmap g { toList := toList✝ } H₂
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
theorem singularPart_add (μ₁ μ₂ ν : Measure α) [HaveLebesgueDecomposition μ₁ ν]
    [HaveLebesgueDecomposition μ₂ ν] :
    (μ₁ + μ₂).singularPart ν = μ₁.singularPart ν + μ₂.singularPart ν

Proof state:
α : Type u_1
m : MeasurableSpace α
μ₁ μ₂ ν : Measure α
inst✝¹ : μ₁.HaveLebesgueDecomposition ν
inst✝ : μ₂.HaveLebesgueDecomposition ν
⊢ (μ₁ + μ₂).singularPart ν = μ₁.singularPart ν + μ₂.singularPart ν

Tactic:
refine (eq_singularPart ((measurable_rnDeriv μ₁ ν).add (measurable_rnDeriv μ₂ ν))
  ((mutuallySingular_singularPart _ _).add_left (mutuallySingular_singularPart _ _)) ?_).symm

Result:
α : Type u_1
m : MeasurableSpace α
μ₁ μ₂ ν : Measure α
inst✝¹ : μ₁.HaveLebesgueDecomposition ν
inst✝ : μ₂.HaveLebesgueDecomposition ν
⊢ μ₁ + μ₂ = μ₁.singularPart ν + μ₂.singularPart ν + ν.withDensity fun a => μ₁.rnDeriv ν a + μ₂.rnDeriv ν a

Proof state:
α : Type u_1
m : MeasurableSpace α
μ₁ μ₂ ν : Measure α
inst✝¹ : μ₁.HaveLebesgueDecomposition ν
inst✝ : μ₂.HaveLebesgueDecomposition ν
⊢ μ₁ + μ₂ = μ₁.singularPart ν + μ₂.singularPart ν + (ν.withDensity (μ₁.rnDeriv ν) + ν.withDensity (μ₂.rnDeriv ν))

Tactic:
conv_rhs => rw [add_assoc, add_comm (μ₂.singularPart ν), ← add_assoc, ← add_assoc]

Result:
α : Type u_1
m : MeasurableSpace α
μ₁ μ₂ ν : Measure α
inst✝¹ : μ₁.HaveLebesgueDecomposition ν
inst✝ : μ₂.HaveLebesgueDecomposition ν
⊢ μ₁ + μ₂ = μ₁.singularPart ν + ν.withDensity (μ₁.rnDeriv ν) + ν.withDensity (μ₂.rnDeriv ν) + μ₂.singularPart ν

Proof state:
α : Type u_1
m : MeasurableSpace α
μ₁ μ₂ ν : Measure α
inst✝¹ : μ₁.HaveLebesgueDecomposition ν
inst✝ : μ₂.HaveLebesgueDecomposition ν
⊢ μ₁ + μ₂ = μ₁.singularPart ν + μ₂.singularPart ν + ν.withDensity fun a => μ₁.rnDeriv ν a + μ₂.rnDeriv ν a

Tactic:
erw [withDensity_add_left (measurable_rnDeriv μ₁ ν)]

Result:
α : Type u_1
m : MeasurableSpace α
μ₁ μ₂ ν : Measure α
inst✝¹ : μ₁.HaveLebesgueDecomposition ν
inst✝ : μ₂.HaveLebesgueDecomposition ν
⊢ μ₁ + μ₂ = μ₁.singularPart ν + μ₂.singularPart ν + (ν.withDensity (μ₁.rnDeriv ν) + ν.withDensity (μ₂.rnDeriv ν))

Proof state:
α : Type u_1
m : MeasurableSpace α
μ₁ μ₂ ν : Measure α
inst✝¹ : μ₁.HaveLebesgueDecomposition ν
inst✝ : μ₂.HaveLebesgueDecomposition ν
⊢ μ₁ + μ₂ = μ₁.singularPart ν + ν.withDensity (μ₁.rnDeriv ν) + ν.withDensity (μ₂.rnDeriv ν) + μ₂.singularPart ν

Tactic:
rw [← haveLebesgueDecomposition_add μ₁ ν, add_assoc, add_comm (ν.withDensity (μ₂.rnDeriv ν)),
  ← haveLebesgueDecomposition_add μ₂ ν]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem map_mkArray : (mkArray n a).map f = mkArray n (f a)

Proof state:
case h
n : Nat
α✝¹ : Type u_1
a : α✝¹
α✝ : Type u_2
f : α✝¹ → α✝
⊢ (map f (mkArray n a)).toList = (mkArray n (f a)).toList

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
α✝¹ : Type u_1
a : α✝¹
α✝ : Type u_2
f : α✝¹ → α✝
⊢ map f (mkArray n a) = mkArray n (f a)

Tactic:
apply Array.ext'

Result:
case h
n : Nat
α✝¹ : Type u_1
a : α✝¹
α✝ : Type u_2
f : α✝¹ → α✝
⊢ (map f (mkArray n a)).toList = (mkArray n (f a)).toList
-- Mathlib/Algebra/ContinuedFractions/ContinuantsRecurrence.lean
theorem conts_recurrence {gp ppred pred : Pair K} (succ_nth_s_eq : g.s.get? (n + 1) = some gp)
    (nth_conts_eq : g.conts n = ppred) (succ_nth_conts_eq : g.conts (n + 1) = pred) :
    g.conts (n + 2) = ⟨gp.b * pred.a + gp.a * ppred.a, gp.b * pred.b + gp.a * ppred.b⟩

Proof state:
K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp ppred pred : Pair K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
nth_conts_eq : g.contsAux (n + 1) = ppred
succ_nth_conts_eq : g.contsAux (n + 1 + 1) = pred
⊢ g.conts (n + 2) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }

Tactic:
exact conts_recurrenceAux succ_nth_s_eq nth_conts_eq succ_nth_conts_eq

Result:
no goals

Proof state:
K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp ppred pred : Pair K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
nth_conts_eq : g.conts n = ppred
succ_nth_conts_eq : g.conts (n + 1) = pred
⊢ g.conts (n + 2) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }

Tactic:
rw [nth_cont_eq_succ_nth_contAux] at nth_conts_eq succ_nth_conts_eq

Result:
K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp ppred pred : Pair K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
nth_conts_eq : g.contsAux (n + 1) = ppred
succ_nth_conts_eq : g.contsAux (n + 1 + 1) = pred
⊢ g.conts (n + 2) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
/-- In a flatten, taking the first elements up to an index which is the sum of the lengths of the
first `i` sublists, is the same as taking the flatten of the first `i` sublists. -/
lemma take_sum_flatten (L : List (List α)) (i : ℕ) :
    L.flatten.take ((L.map length).take i).sum = (L.take i).flatten

Proof state:
case nil
α : Type u_2
i : ℕ
⊢ take (take i (map length [])).sum [].flatten = (take i []).flatten

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
L : List (List α)
i : ℕ
⊢ take (take i (map length L)).sum L.flatten = (take i L).flatten

Tactic:
induction L generalizing i

Result:
case nil
α : Type u_2
i : ℕ
⊢ take (take i (map length [])).sum [].flatten = (take i []).flatten

case cons
α : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), take (take i (map length tail✝)).sum tail✝.flatten = (take i tail✝).flatten
i : ℕ
⊢ take (take i (map length (head✝ :: tail✝))).sum (head✝ :: tail✝).flatten = (take i (head✝ :: tail✝)).flatten

Proof state:
case cons
α : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), take (take i (map length tail✝)).sum tail✝.flatten = (take i tail✝).flatten
i : ℕ
⊢ take (take i (map length (head✝ :: tail✝))).sum (head✝ :: tail✝).flatten = (take i (head✝ :: tail✝)).flatten

Tactic:
cases i <;> simp [take_append, *]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem IsNClique.mono (h : G ≤ H) : G.IsNClique n s → H.IsNClique n s

Proof state:
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
h : G ≤ H
⊢ G.IsNClique n s → H.IsNClique n s

Tactic:
simp_rw [isNClique_iff]

Result:
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
h : G ≤ H
⊢ G.IsClique ↑s ∧ #s = n → H.IsClique ↑s ∧ #s = n

Proof state:
α : Type u_1
G H : SimpleGraph α
n : ℕ
s : Finset α
h : G ≤ H
⊢ G.IsClique ↑s ∧ #s = n → H.IsClique ↑s ∧ #s = n

Tactic:
exact And.imp_left (IsClique.mono h)

Result:
no goals
-- Mathlib/CategoryTheory/Limits/ConcreteCategory/WithAlgebraicStructures.lean
theorem colimit_rep_eq_zero
    (F : J ⥤ ModuleCat.{max t w} R) [PreservesColimit F (forget (ModuleCat R))] [IsFiltered J]
    [HasColimit F] (j : J) (x : F.obj j) (hx : colimit.ι F j x = 0) :
    ∃ (j' : J) (i : j ⟶ j'), (F.map i).hom x = 0

Proof state:
case intro.intro.intro
R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
j : J
x : ↑(F.obj j)
j' : J
i y : j ⟶ j'
g : (ConcreteCategory.hom (F.map i)) x = (ConcreteCategory.hom (F.map y)) 0
⊢ ∃ j' i, (ModuleCat.Hom.hom (F.map i)) x = 0

Tactic:
exact ⟨j', i, g ▸ by simp⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
j : J
x : ↑(F.obj j)
hx : (ConcreteCategory.hom (colimit.ι F j)) x = 0
⊢ ∃ j' i, (ModuleCat.Hom.hom (F.map i)) x = 0

Tactic:
rw [show 0 = colimit.ι F j 0 by simp, colimit_rep_eq_iff_exists] at hx

Result:
R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
j : J
x : ↑(F.obj j)
hx : ∃ k f g, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) 0
⊢ ∃ j' i, (ModuleCat.Hom.hom (F.map i)) x = 0

Proof state:
R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
j : J
x : ↑(F.obj j)
j' : J
i y : j ⟶ j'
g : (ConcreteCategory.hom (F.map i)) x = (ConcreteCategory.hom (F.map y)) 0
⊢ (ConcreteCategory.hom (F.map y)) 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
j : J
x : ↑(F.obj j)
hx : ∃ k f g, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) 0
⊢ ∃ j' i, (ModuleCat.Hom.hom (F.map i)) x = 0

Tactic:
obtain ⟨j', i, y, g⟩ := hx

Result:
case intro.intro.intro
R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
j : J
x : ↑(F.obj j)
j' : J
i y : j ⟶ j'
g : (ConcreteCategory.hom (F.map i)) x = (ConcreteCategory.hom (F.map y)) 0
⊢ ∃ j' i, (ModuleCat.Hom.hom (F.map i)) x = 0

Proof state:
R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
j : J
x : ↑(F.obj j)
hx : (ConcreteCategory.hom (colimit.ι F j)) x = 0
⊢ 0 = (ConcreteCategory.hom (colimit.ι F j)) 0

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
theorem filter_dvd_eq_divisors (h : n ≠ 0) : {d ∈ range n.succ | d ∣ n} = n.divisors

Proof state:
case h
n : ℕ
h : n ≠ 0
a✝ : ℕ
⊢ a✝ ∈ filter (fun d => d ∣ n) (range n.succ) ↔ a✝ ∈ n.divisors

Tactic:
simp only [divisors, mem_filter, mem_range, mem_Ico, and_congr_left_iff, iff_and_self]

Result:
case h
n : ℕ
h : n ≠ 0
a✝ : ℕ
⊢ a✝ ∣ n → a✝ < n.succ → 1 ≤ a✝

Proof state:
case h
n : ℕ
h : n ≠ 0
a✝ : ℕ
⊢ a✝ ∣ n → a✝ < n.succ → 1 ≤ a✝

Tactic:
exact fun ha _ => succ_le_iff.mpr (pos_of_dvd_of_pos ha h.bot_lt)

Result:
no goals

Proof state:
n : ℕ
h : n ≠ 0
⊢ filter (fun d => d ∣ n) (range n.succ) = n.divisors

Tactic:
ext

Result:
case h
n : ℕ
h : n ≠ 0
a✝ : ℕ
⊢ a✝ ∈ filter (fun d => d ∣ n) (range n.succ) ↔ a✝ ∈ n.divisors
-- Mathlib/Data/Finset/NAry.lean
theorem image_image₂_distrib_right {g : γ → δ} {f' : α → β' → δ} {g' : β → β'}
    (h_distrib : ∀ a b, g (f a b) = f' a (g' b)) :
    (image₂ f s t).image g = image₂ f' s (t.image g') :=
  coe_injective <| by
    push_cast
    exact image_image2_distrib_right h_distrib

Proof state:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq β'
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
g : γ → δ
f' : α → β' → δ
g' : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)
⊢ g '' image2 f ↑s ↑t = image2 f' (↑s) (g' '' ↑t)

Tactic:
exact image_image2_distrib_right h_distrib

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq β'
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
g : γ → δ
f' : α → β' → δ
g' : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)
⊢ ↑(image g (image₂ f s t)) = ↑(image₂ f' s (image g' t))

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq β'
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
g : γ → δ
f' : α → β' → δ
g' : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)
⊢ g '' image2 f ↑s ↑t = image2 f' (↑s) (g' '' ↑t)
-- Mathlib/MeasureTheory/SetSemiring.lean
lemma pairwiseDisjoint_insert_disjointOfDiff (hC : IsSetSemiring C) (hs : s ∈ C)
    (ht : t ∈ C) :
    PairwiseDisjoint (insert t (hC.disjointOfDiff hs ht) : Set (Set α)) id

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
h : (↑(hC.disjointOfDiff hs ht)).PairwiseDisjoint id
u : Set α
hu : u ∈ ↑(hC.disjointOfDiff hs ht)
⊢ Disjoint t u

Tactic:
refine Disjoint.mono_right ?_ (hC.disjoint_sUnion_disjointOfDiff hs ht)

Result:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
h : (↑(hC.disjointOfDiff hs ht)).PairwiseDisjoint id
u : Set α
hu : u ∈ ↑(hC.disjointOfDiff hs ht)
⊢ u ≤ ⋃₀ ↑(hC.disjointOfDiff hs ht)

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
h : (↑(hC.disjointOfDiff hs ht)).PairwiseDisjoint id
⊢ (insert t ↑(hC.disjointOfDiff hs ht)).PairwiseDisjoint id

Tactic:
refine PairwiseDisjoint.insert_of_not_mem h (hC.nmem_disjointOfDiff hs ht) fun u hu ↦ ?_

Result:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
h : (↑(hC.disjointOfDiff hs ht)).PairwiseDisjoint id
u : Set α
hu : u ∈ ↑(hC.disjointOfDiff hs ht)
⊢ Disjoint (id t) (id u)

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
h : (↑(hC.disjointOfDiff hs ht)).PairwiseDisjoint id
u : Set α
hu : u ∈ ↑(hC.disjointOfDiff hs ht)
⊢ u ≤ ⋃₀ ↑(hC.disjointOfDiff hs ht)

Tactic:
simp only [Set.le_eq_subset]

Result:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
h : (↑(hC.disjointOfDiff hs ht)).PairwiseDisjoint id
u : Set α
hu : u ∈ ↑(hC.disjointOfDiff hs ht)
⊢ u ⊆ ⋃₀ ↑(hC.disjointOfDiff hs ht)

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ (insert t ↑(hC.disjointOfDiff hs ht)).PairwiseDisjoint id

Tactic:
have h := hC.pairwiseDisjoint_disjointOfDiff hs ht

Result:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
h : (↑(hC.disjointOfDiff hs ht)).PairwiseDisjoint id
⊢ (insert t ↑(hC.disjointOfDiff hs ht)).PairwiseDisjoint id

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
h : (↑(hC.disjointOfDiff hs ht)).PairwiseDisjoint id
u : Set α
hu : u ∈ ↑(hC.disjointOfDiff hs ht)
⊢ u ⊆ ⋃₀ ↑(hC.disjointOfDiff hs ht)

Tactic:
exact subset_sUnion_of_mem hu

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
h : (↑(hC.disjointOfDiff hs ht)).PairwiseDisjoint id
u : Set α
hu : u ∈ ↑(hC.disjointOfDiff hs ht)
⊢ Disjoint (id t) (id u)

Tactic:
simp_rw [id]

Result:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
h : (↑(hC.disjointOfDiff hs ht)).PairwiseDisjoint id
u : Set α
hu : u ∈ ↑(hC.disjointOfDiff hs ht)
⊢ Disjoint t u
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem insert_setBlack {t : RBNode α} :
    (t.insert cmp v).setBlack = (t.ins cmp v).setBlack

Proof state:
α : Type u_1
cmp : α → α → Ordering
v : α
t : RBNode α
⊢ (match t.isRed with
      | red => (ins cmp v t).setBlack
      | black => ins cmp v t).setBlack =
    (ins cmp v t).setBlack

Tactic:
split <;> simp [setBlack_idem]

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
v : α
t : RBNode α
⊢ (insert cmp t v).setBlack = (ins cmp v t).setBlack

Tactic:
unfold insert

Result:
α : Type u_1
cmp : α → α → Ordering
v : α
t : RBNode α
⊢ (match t.isRed with
      | red => (ins cmp v t).setBlack
      | black => ins cmp v t).setBlack =
    (ins cmp v t).setBlack
-- Mathlib/Data/DFinsupp/NeLocus.lean
theorem neLocus_zero_right : f.neLocus 0 = f.support

Proof state:
case h
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → Zero (N a)
f : Π₀ (a : α), N a
a✝ : α
⊢ a✝ ∈ f.neLocus 0 ↔ a✝ ∈ f.support

Tactic:
rw [mem_neLocus, mem_support_iff, coe_zero, Pi.zero_apply]

Result:
no goals

Proof state:
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → Zero (N a)
f : Π₀ (a : α), N a
⊢ f.neLocus 0 = f.support

Tactic:
ext

Result:
case h
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → Zero (N a)
f : Π₀ (a : α), N a
a✝ : α
⊢ a✝ ∈ f.neLocus 0 ↔ a✝ ∈ f.support
-- Mathlib/AlgebraicGeometry/Pullbacks.lean
theorem p_comm : p1 𝒰 f g ≫ f = p2 𝒰 f g ≫ g

Proof state:
case h
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
⊢ ∀ (b : (MultispanShape.prod (gluing 𝒰 f g).J).R),
    Multicoequalizer.π (gluing 𝒰 f g).diagram b ≫ p1 𝒰 f g ≫ f =
      Multicoequalizer.π (gluing 𝒰 f g).diagram b ≫ p2 𝒰 f g ≫ g

Tactic:
simp [p1, p2, pullback.condition]

Result:
no goals

Proof state:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
⊢ p1 𝒰 f g ≫ f = p2 𝒰 f g ≫ g

Tactic:
apply Multicoequalizer.hom_ext

Result:
case h
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
⊢ ∀ (b : (MultispanShape.prod (gluing 𝒰 f g).J).R),
    Multicoequalizer.π (gluing 𝒰 f g).diagram b ≫ p1 𝒰 f g ≫ f =
      Multicoequalizer.π (gluing 𝒰 f g).diagram b ≫ p2 𝒰 f g ≫ g
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem Products.lt_nil_empty {I} [LinearOrder I] : { m : Products I | m < Products.nil } = ∅

Proof state:
case h.mk
I : Type u_1
inst✝ : LinearOrder I
m : List I
hm : List.Chain' (fun x1 x2 => x1 > x2) m
⊢ ⟨m, hm⟩ ∈ {m | m < nil} ↔ ⟨m, hm⟩ ∈ ∅

Tactic:
refine ⟨fun h ↦ ?_, by tauto⟩

Result:
case h.mk
I : Type u_1
inst✝ : LinearOrder I
m : List I
hm : List.Chain' (fun x1 x2 => x1 > x2) m
h : ⟨m, hm⟩ ∈ {m | m < nil}
⊢ ⟨m, hm⟩ ∈ ∅

Proof state:
case h.mk
I : Type u_1
inst✝ : LinearOrder I
m : List I
hm : List.Chain' (fun x1 x2 => x1 > x2) m
h : ⟨m, hm⟩ ∈ {m | m < nil}
⊢ ⟨m, hm⟩ ∈ ∅

Tactic:
simp only [Set.mem_setOf_eq, lt_iff_lex_lt, nil, List.not_lex_nil] at h

Result:
no goals

Proof state:
I : Type u_1
inst✝ : LinearOrder I
⊢ {m | m < nil} = ∅

Tactic:
ext ⟨m, hm⟩

Result:
case h.mk
I : Type u_1
inst✝ : LinearOrder I
m : List I
hm : List.Chain' (fun x1 x2 => x1 > x2) m
⊢ ⟨m, hm⟩ ∈ {m | m < nil} ↔ ⟨m, hm⟩ ∈ ∅

Proof state:
I : Type u_1
inst✝ : LinearOrder I
m : List I
hm : List.Chain' (fun x1 x2 => x1 > x2) m
⊢ ⟨m, hm⟩ ∈ ∅ → ⟨m, hm⟩ ∈ {m | m < nil}

Tactic:
tauto

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Basic.lean
theorem integralSum_smul (c : ℝ) (f : ℝⁿ → E) (vol : ι →ᵇᵃ E →L[ℝ] F) (π : TaggedPrepartition I) :
    integralSum (c • f) vol π = c • integralSum f vol π

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I : Box ι
c : ℝ
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : TaggedPrepartition I
⊢ integralSum (c • f) vol π = c • integralSum f vol π

Tactic:
simp only [integralSum, Finset.smul_sum, Pi.smul_apply, ContinuousLinearMap.map_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head_append_of_ne_nil {l : List α} {w₁} (w₂) :
    head (l ++ l') w₁ = head l w₂

Proof state:
α : Type u_1
l' l✝ : List α
w₂ : l✝ ≠ []
a : α
l : List α
x✝ : a :: l ≠ []
w₁ : a :: l ++ l' ≠ []
⊢ (a :: l ++ l').head w₁ = (a :: l).head x✝

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
l' l : List α
w₁ : l ++ l' ≠ []
w₂ : l ≠ []
⊢ (l ++ l').head w₁ = l.head w₂

Tactic:
match l, w₂ with
| a :: l, _ => rfl

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Operations.lean
theorem map_comap_of_surjective {β} {f : α → β} (hf : Surjective f) (m : OuterMeasure β) :
    map f (comap f m) = m :=
  ext fun s => by rw [map_apply, comap_apply, hf.image_preimage]

Proof state:
α : Type u_1
β : Type u_3
f : α → β
hf : Surjective f
m : OuterMeasure β
s : Set β
⊢ ((map f) ((comap f) m)) s = m s

Tactic:
rw [map_apply, comap_apply, hf.image_preimage]

Result:
no goals
-- Mathlib/Algebra/Order/Hom/Monoid.lean
theorem toMulEquiv_injective : Injective (toMulEquiv : _ → α ≃* β) := fun f g h =>
  ext <| by convert DFunLike.ext_iff.1 h using 0

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Mul α
inst✝ : Mul β
f g : α ≃*o β
h : f.toMulEquiv = g.toMulEquiv
⊢ ∀ (a : α), f a = g a

Tactic:
convert DFunLike.ext_iff.1 h using 0

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem inv_eq_of_mul_eq_one_left {a : α} (h : a * u = 1) : ↑u⁻¹ = a :=
  calc
    ↑u⁻¹ = 1 * ↑u⁻¹

Proof state:
α : Type u
inst✝ : Monoid α
u : αˣ
a : α
h : a * ↑u = 1
⊢ 1 * ↑u⁻¹ = a

Tactic:
rw [← h, mul_inv_cancel_right]

Result:
no goals

Proof state:
α : Type u
inst✝ : Monoid α
u : αˣ
a : α
h : a * ↑u = 1
⊢ ↑u⁻¹ = 1 * ↑u⁻¹

Tactic:
rw [one_mul]

Result:
no goals