harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/batteries/Batteries/Data/HashMap/WF.lean
theorem WF.filterMap {α β γ} {f : α → β → Option γ} [BEq α] [Hashable α]
    {m : Imp α β} (H : WF m) : WF (filterMap f m)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → Option γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : m.WF
g₁ : AssocList α β → List (α × γ) :=
  fun l => List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList
H1 :
  ∀ (l : AssocList α β) (n : ULift Nat) (acc : AssocList α γ),
    filterMap.go f acc l n = (((g₁ l).reverse ++ acc.toList).toAssocList, { down := n.down + (g₁ l).length })
g : AssocList α β → AssocList α γ := fun l => (g₁ l).reverse.toAssocList
M : Type (max u_3 u_1) → Type (max u_3 u_1) := StateT (ULift Nat) Id
H2 :
  ∀ (l : List (AssocList α β)) (n : ULift Nat),
    List.mapM (filterMap.go f AssocList.nil) l n =
      (List.map g l, { down := n.down + (List.map (fun x => x.toList.length) (List.map g l)).sum })
H3 :
  ∀ (l : List (α × β)),
    (List.map (fun a => a.fst)
          (List.filterMap
            (fun x =>
              match x with
              | (a, b) => Option.map (fun x => (a, x)) (f a b))
            l)).Sublist
      (List.map (fun x => x.fst) l)
⊢ ∀ (bk : List (AssocList α γ)) (sz : Nat) (h : 0 < bk.length),
    Array.mapM (filterMap.go f AssocList.nil) m.buckets.val { down := 0 } = ({ toList := bk }, { down := sz }) →
      { size := sz, buckets := ⟨{ toList := bk }, h⟩ }.WF

Tactic:
simp only [Array.mapM_eq_mapM_toList, Functor.map, StateT.map, H2, List.map_map, Nat.zero_add, g]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → Option γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : m.WF
g₁ : AssocList α β → List (α × γ) :=
  fun l => List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList
H1 :
  ∀ (l : AssocList α β) (n : ULift Nat) (acc : AssocList α γ),
    filterMap.go f acc l n = (((g₁ l).reverse ++ acc.toList).toAssocList, { down := n.down + (g₁ l).length })
g : AssocList α β → AssocList α γ := fun l => (g₁ l).reverse.toAssocList
M : Type (max u_3 u_1) → Type (max u_3 u_1) := StateT (ULift Nat) Id
H2 :
  ∀ (l : List (AssocList α β)) (n : ULift Nat),
    List.mapM (filterMap.go f AssocList.nil) l n =
      (List.map g l, { down := n.down + (List.map (fun x => x.toList.length) (List.map g l)).sum })
H3 :
  ∀ (l : List (α × β)),
    (List.map (fun a => a.fst)
          (List.filterMap
            (fun x =>
              match x with
              | (a, b) => Option.map (fun x => (a, x)) (f a b))
            l)).Sublist
      (List.map (fun x => x.fst) l)
⊢ ∀ (bk : List (AssocList α γ)) (sz : Nat) (h : 0 < bk.length),
    (do
          let __discr ←
            (List.map (fun l => (g₁ l).reverse.toAssocList) m.buckets.val.toList,
                {
                  down :=
                    (List.map ((fun x => x.toList.length) ∘ fun l => (g₁ l).reverse.toAssocList)
                        m.buckets.val.toList).sum })
          pure (__discr.fst.toArray, __discr.snd)) =
        ({ toList := bk }, { down := sz }) →
      { size := sz, buckets := ⟨{ toList := bk }, h⟩ }.WF
-- Mathlib/.lake/packages/batteries/Batteries/Data/HashMap/WF.lean
theorem WF.filterMap {α β γ} {f : α → β → Option γ} [BEq α] [Hashable α]
    {m : Imp α β} (H : WF m) : WF (filterMap f m)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → Option γ
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
H : m.WF
g₁ : AssocList α β → List (α × γ) :=
  fun l => List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList
H1 :
  ∀ (l : AssocList α β) (n : ULift Nat) (acc : AssocList α γ),
    filterMap.go f acc l n = (((g₁ l).reverse ++ acc.toList).toAssocList, { down := n.down + (g₁ l).length })
g : AssocList α β → AssocList α γ := fun l => (g₁ l).reverse.toAssocList
M : Type (max u_3 u_1) → Type (max u_3 u_1) := StateT (ULift Nat) Id
l : List (AssocList α β)
n : ULift Nat
⊢ List.mapM (filterMap.go f AssocList.nil) l n =
    (List.map g l, { down := n.down + (List.map (fun x => x.toList.length) (List.map g l)).sum })

Tactic:
induction l generalizing n with
| nil => rfl
| cons l L IH => simp [bind, StateT.bind, IH, H1, Nat.add_assoc, g]; rfl

Result:
no goals

Proof state:
case refl.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → Option γ
inst✝³ : BEq α
inst✝² : Hashable α
m : Imp α β
H : m.WF
g₁ : AssocList α β → List (α × γ) :=
  fun l => List.filterMap (fun x => Option.map (fun x_1 => (x.fst, x_1)) (f x.fst x.snd)) l.toList
H1 :
  ∀ (l : AssocList α β) (n : ULift Nat) (acc : AssocList α γ),
    filterMap.go f acc l n = (((g₁ l).reverse ++ acc.toList).toAssocList, { down := n.down + (g₁ l).length })
g : AssocList α β → AssocList α γ := fun l => (g₁ l).reverse.toAssocList
M : Type (max u_3 u_1) → Type (max u_3 u_1) := StateT (ULift Nat) Id
H2 :
  ∀ (l : List (AssocList α β)) (n : ULift Nat),
    List.mapM (filterMap.go f AssocList.nil) l n =
      (List.map g l, { down := n.down + (List.map (fun x => x.toList.length) (List.map g l)).sum })
H3 :
  ∀ (l : List (α × β)),
    (List.map (fun a => a.fst)
          (List.filterMap
            (fun x =>
              match x with
              | (a, b) => Option.map (fun x => (a, x)) (f a b))
            l)).Sublist
      (List.map (fun x => x.fst) l)
h✝ :
  0 <
    (List.map (fun l => (g₁ l).reverse.toAssocList) m.buckets.val.toList,
          {
            down :=
              (List.map ((fun x => x.toList.length) ∘ fun l => (g₁ l).reverse.toAssocList)
                  m.buckets.val.toList).sum }).fst.length
inst✝¹ : LawfulHashable α
inst✝ : PartialEquivBEq α
l : AssocList α β
h : l ∈ m.buckets.val.toList
this : List.Pairwise (fun x1 x2 => ¬(x1 == x2) = true) (List.map Prod.fst l.toList)
⊢ List.Pairwise (fun x1 x2 => ¬(x1 == x2) = true) (List.map Prod.fst (g₁ l))

Tactic:
exact this.sublist (H3 l.toList)

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/Basic.lean
theorem gradedMonoid_eq_of_cast {Γ : Subgroup SL(2, ℤ)} {a b : GradedMonoid (ModularForm Γ)}
    (h : a.fst = b.fst) (h2 : mcast h a.snd = b.snd) : a = b

Proof state:
case mk.mk
Γ : Subgroup SL(2, ℤ)
i : ℤ
a : ModularForm Γ i
j : ℤ
b : ModularForm Γ j
h : ⟨i, a⟩.fst = ⟨j, b⟩.fst
h2 : mcast h ⟨i, a⟩.snd = ⟨j, b⟩.snd
⊢ ⟨i, a⟩ = ⟨j, b⟩

Tactic:
cases h

Result:
case mk.mk.refl
Γ : Subgroup SL(2, ℤ)
i : ℤ
a b : ModularForm Γ i
h2 : mcast ⋯ ⟨i, a⟩.snd = ⟨i, b⟩.snd
⊢ ⟨i, a⟩ = ⟨i, b⟩

Proof state:
Γ : Subgroup SL(2, ℤ)
a b : GradedMonoid (ModularForm Γ)
h : a.fst = b.fst
h2 : mcast h a.snd = b.snd
⊢ a = b

Tactic:
obtain ⟨i, a⟩ := a

Result:
case mk
Γ : Subgroup SL(2, ℤ)
b : GradedMonoid (ModularForm Γ)
i : ℤ
a : ModularForm Γ i
h : ⟨i, a⟩.fst = b.fst
h2 : mcast h ⟨i, a⟩.snd = b.snd
⊢ ⟨i, a⟩ = b

Proof state:
case mk
Γ : Subgroup SL(2, ℤ)
b : GradedMonoid (ModularForm Γ)
i : ℤ
a : ModularForm Γ i
h : ⟨i, a⟩.fst = b.fst
h2 : mcast h ⟨i, a⟩.snd = b.snd
⊢ ⟨i, a⟩ = b

Tactic:
obtain ⟨j, b⟩ := b

Result:
case mk.mk
Γ : Subgroup SL(2, ℤ)
i : ℤ
a : ModularForm Γ i
j : ℤ
b : ModularForm Γ j
h : ⟨i, a⟩.fst = ⟨j, b⟩.fst
h2 : mcast h ⟨i, a⟩.snd = ⟨j, b⟩.snd
⊢ ⟨i, a⟩ = ⟨j, b⟩

Proof state:
case mk.mk.refl
Γ : Subgroup SL(2, ℤ)
i : ℤ
a b : ModularForm Γ i
h2 : mcast ⋯ ⟨i, a⟩.snd = ⟨i, b⟩.snd
⊢ ⟨i, a⟩ = ⟨i, b⟩

Tactic:
exact congr_arg _ h2

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_erase_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
    get? (m.erase k) k = none

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k : α
⊢ get? (m.erase k) k = none

Tactic:
simp_to_raw using Raw₀.Const.get?_erase_self

Result:
no goals
-- Mathlib/Data/Real/Basic.lean
theorem ofCauchy_sub (a b) : (⟨a - b⟩ : ℝ) = ⟨a⟩ - ⟨b⟩

Proof state:
a b : Cauchy abs
⊢ { cauchy := a - b } = { cauchy := a } - { cauchy := b }

Tactic:
rw [sub_eq_add_neg, ofCauchy_add, ofCauchy_neg]

Result:
a b : Cauchy abs
⊢ { cauchy := a } + -{ cauchy := b } = { cauchy := a } - { cauchy := b }

Proof state:
a b : Cauchy abs
⊢ { cauchy := a } + -{ cauchy := b } = { cauchy := a } - { cauchy := b }

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem image_sUnion {f : α → β} {s : Set (Set α)} : (f '' ⋃₀ s) = ⋃₀ (image f '' s)

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → β
s : Set (Set α)
b : β
⊢ b ∈ f '' ⋃₀ s ↔ b ∈ ⋃₀ (image f '' s)

Tactic:
simp only [mem_image, mem_sUnion, exists_prop, sUnion_image, mem_iUnion]

Result:
case h
α : Type u_1
β : Type u_2
f : α → β
s : Set (Set α)
b : β
⊢ (∃ x, (∃ t ∈ s, x ∈ t) ∧ f x = b) ↔ ∃ i ∈ s, ∃ x ∈ i, f x = b

Proof state:
case h.mpr
α : Type u_1
β : Type u_2
f : α → β
s : Set (Set α)
b : β
⊢ (∃ i ∈ s, ∃ x ∈ i, f x = b) → ∃ x, (∃ t ∈ s, x ∈ t) ∧ f x = b

Tactic:
rintro ⟨t, ht₁, a, ht₂, rfl⟩

Result:
case h.mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
s : Set (Set α)
t : Set α
ht₁ : t ∈ s
a : α
ht₂ : a ∈ t
⊢ ∃ x, (∃ t ∈ s, x ∈ t) ∧ f x = f a

Proof state:
case h.mp
α : Type u_1
β : Type u_2
f : α → β
s : Set (Set α)
b : β
⊢ (∃ x, (∃ t ∈ s, x ∈ t) ∧ f x = b) → ∃ i ∈ s, ∃ x ∈ i, f x = b

Tactic:
rintro ⟨a, ⟨t, ht₁, ht₂⟩, rfl⟩

Result:
case h.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
s : Set (Set α)
a : α
t : Set α
ht₁ : t ∈ s
ht₂ : a ∈ t
⊢ ∃ i ∈ s, ∃ x ∈ i, f x = f a

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set (Set α)
⊢ f '' ⋃₀ s = ⋃₀ (image f '' s)

Tactic:
ext b

Result:
case h
α : Type u_1
β : Type u_2
f : α → β
s : Set (Set α)
b : β
⊢ b ∈ f '' ⋃₀ s ↔ b ∈ ⋃₀ (image f '' s)

Proof state:
case h.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
s : Set (Set α)
a : α
t : Set α
ht₁ : t ∈ s
ht₂ : a ∈ t
⊢ ∃ i ∈ s, ∃ x ∈ i, f x = f a

Tactic:
exact ⟨t, ht₁, a, ht₂, rfl⟩

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → β
s : Set (Set α)
b : β
⊢ (∃ x, (∃ t ∈ s, x ∈ t) ∧ f x = b) ↔ ∃ i ∈ s, ∃ x ∈ i, f x = b

Tactic:
constructor

Result:
case h.mp
α : Type u_1
β : Type u_2
f : α → β
s : Set (Set α)
b : β
⊢ (∃ x, (∃ t ∈ s, x ∈ t) ∧ f x = b) → ∃ i ∈ s, ∃ x ∈ i, f x = b

case h.mpr
α : Type u_1
β : Type u_2
f : α → β
s : Set (Set α)
b : β
⊢ (∃ i ∈ s, ∃ x ∈ i, f x = b) → ∃ x, (∃ t ∈ s, x ∈ t) ∧ f x = b

Proof state:
case h.mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
s : Set (Set α)
t : Set α
ht₁ : t ∈ s
a : α
ht₂ : a ∈ t
⊢ ∃ x, (∃ t ∈ s, x ∈ t) ∧ f x = f a

Tactic:
exact ⟨a, ⟨t, ht₁, ht₂⟩, rfl⟩

Result:
no goals
-- Mathlib/Data/Complex/Norm.lean
theorem norm_neg' (z : ℂ) : ‖-z‖ = ‖z‖

Proof state:
z : ℂ
⊢ ‖-z‖ = ‖z‖

Tactic:
rw [Complex.norm_def, norm_def, normSq_neg]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Hasse.lean
theorem pathGraph_two_eq_top : pathGraph 2 = ⊤

Proof state:
case Adj.h.h.a
u v : Fin 2
⊢ (pathGraph 2).Adj u v ↔ ⊤.Adj u v

Tactic:
fin_cases u <;> fin_cases v <;> simp [pathGraph, ← Fin.coe_covBy_iff, covBy_iff_add_one_eq]

Result:
no goals

Proof state:
⊢ pathGraph 2 = ⊤

Tactic:
ext u v

Result:
case Adj.h.h.a
u v : Fin 2
⊢ (pathGraph 2).Adj u v ↔ ⊤.Adj u v
-- Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean
theorem integral2_divergence_prod_of_hasFDerivWithinAt_off_countable (f g : ℝ × ℝ → E)
    (f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E) (a₁ a₂ b₁ b₂ : ℝ) (s : Set (ℝ × ℝ)) (hs : s.Countable)
    (Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]]))
    (Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]]))
    (Hdf : ∀ x ∈ Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Ioo (min a₂ b₂) (max a₂ b₂) \ s,
      HasFDerivAt f (f' x) x)
    (Hdg : ∀ x ∈ Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Ioo (min a₂ b₂) (max a₂ b₂) \ s,
      HasFDerivAt g (g' x) x)
    (Hi : IntegrableOn (fun x => f' x (1, 0) + g' x (0, 1)) ([[a₁, b₁]] ×ˢ [[a₂, b₂]])) :
    (∫ x in a₁..b₁, ∫ y in a₂..b₂, f' (x, y) (1, 0) + g' (x, y) (0, 1)) =
      (((∫ x in a₁..b₁, g (x, b₂)) - ∫ x in a₁..b₁, g (x, a₂)) + ∫ y in a₂..b₂, f (b₁, y)) -
        ∫ y in a₂..b₂, f (a₁, y)

Proof state:
case inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a₂ b₂ : ℝ
s : Set (ℝ × ℝ)
hs : s.Countable
a₁ b₁ : ℝ
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ x ∈ Set.Ioo (a₁ ⊓ b₁) (a₁ ⊔ b₁) ×ˢ Set.Ioo (a₂ ⊓ b₂) (a₂ ⊔ b₂) \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo (a₁ ⊓ b₁) (a₁ ⊔ b₁) ×ˢ Set.Ioo (a₂ ⊓ b₂) (a₂ ⊔ b₂) \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) volume
h₁ : a₁ ≤ b₁
h₂ : ¬a₂ ≤ b₂
this :
  ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
    ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
      (∀ x ∈ Set.Ioo (a₁ ⊓ b₁) (a₁ ⊔ b₁) ×ˢ Set.Ioo (a₂ ⊓ b₂) (a₂ ⊔ b₂) \ s, HasFDerivAt f (f' x) x) →
        (∀ x ∈ Set.Ioo (a₁ ⊓ b₁) (a₁ ⊔ b₁) ×ˢ Set.Ioo (a₂ ⊓ b₂) (a₂ ⊔ b₂) \ s, HasFDerivAt g (g' x) x) →
          IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) volume →
            b₂ ≤ a₂ →
              ∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in b₂..a₂, (f' (x, y)) (1, 0) + (g' (x, y)) (0, 1) =
                (((∫ (x : ℝ) in a₁..b₁, g (x, a₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, b₂)) + ∫ (y : ℝ) in b₂..a₂, f (b₁, y)) -
                  ∫ (y : ℝ) in b₂..a₂, f (a₁, y)
⊢ -((((∫ (x : ℝ) in a₁..b₁, g (x, a₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, b₂)) + ∫ (y : ℝ) in b₂..a₂, f (b₁, y)) -
        ∫ (y : ℝ) in b₂..a₂, f (a₁, y)) =
    (((∫ (x : ℝ) in a₁..b₁, g (x, b₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, a₂)) + -∫ (y : ℝ) in b₂..a₂, f (b₁, y)) -
      -∫ (y : ℝ) in b₂..a₂, f (a₁, y)

Tactic:
abel

Result:
no goals
-- Mathlib/AlgebraicGeometry/Pullbacks.lean
lemma diagonalCover_map (I) : (diagonalCover f 𝒰 𝒱).map I =
    pullback.map _ _ _ _
    ((𝒱 I.fst).map _ ≫ pullback.fst _ _) ((𝒱 I.fst).map _ ≫ pullback.fst _ _) (𝒰.map _)
    (by simp)
    (by simp)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.J), HasPullback (𝒰✝.map i ≫ f✝) g
s : PullbackCone f✝ g
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : (Cover.pullbackCover 𝒰 f).J) → ((Cover.pullbackCover 𝒰 f).obj i).OpenCover
I : (diagonalCover f 𝒰 𝒱).J
⊢ ((𝒱 I.fst).map I.snd.2 ≫ Cover.pullbackHom 𝒰 f I.fst) ≫ 𝒰.map I.fst =
    ((𝒱 I.fst).map I.snd.2 ≫ pullback.fst f (𝒰.map I.fst)) ≫ f

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.J), HasPullback (𝒰✝.map i ≫ f✝) g
s : PullbackCone f✝ g
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : (Cover.pullbackCover 𝒰 f).J) → ((Cover.pullbackCover 𝒰 f).obj i).OpenCover
I : (diagonalCover f 𝒰 𝒱).J
⊢ ((𝒱 I.fst).map I.snd.1 ≫ Cover.pullbackHom 𝒰 f I.fst) ≫ 𝒰.map I.fst =
    ((𝒱 I.fst).map I.snd.1 ≫ pullback.fst f (𝒰.map I.fst)) ≫ f

Tactic:
simp

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : (Cover.pullbackCover 𝒰 f).J) → ((Cover.pullbackCover 𝒰 f).obj i).OpenCover
I : (diagonalCover f 𝒰 𝒱).J
⊢ (diagonalCover f 𝒰 𝒱).map I =
    pullback.map ((𝒱 I.fst).map I.snd.1 ≫ Cover.pullbackHom 𝒰 f I.fst)
      ((𝒱 I.fst).map I.snd.2 ≫ Cover.pullbackHom 𝒰 f I.fst) f f ((𝒱 I.fst).map I.snd.1 ≫ pullback.fst f (𝒰.map I.fst))
      ((𝒱 I.fst).map I.snd.2 ≫ pullback.fst f (𝒰.map I.fst)) (𝒰.map I.fst) ⋯ ⋯

Tactic:
ext1 <;> simp [diagonalCover, Cover.pullbackHom]

Result:
no goals
-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
theorem eq_top_iff {S : NonUnitalStarSubalgebra R A} : S = ⊤ ↔ ∀ x : A, x ∈ S :=
  ⟨fun h x => by rw [h]; exact mem_top,
    fun h => by ext x; exact ⟨fun _ => mem_top, fun _ => h x⟩⟩

Proof state:
case h
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
S : NonUnitalStarSubalgebra R A
h : ∀ (x : A), x ∈ S
x : A
⊢ x ∈ S ↔ x ∈ ⊤

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

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
S : NonUnitalStarSubalgebra R A
h : S = ⊤
x : A
⊢ x ∈ S

Tactic:
rw [h]

Result:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
S : NonUnitalStarSubalgebra R A
h : S = ⊤
x : A
⊢ x ∈ ⊤

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
S : NonUnitalStarSubalgebra R A
h : ∀ (x : A), x ∈ S
⊢ S = ⊤

Tactic:
ext x

Result:
case h
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
S : NonUnitalStarSubalgebra R A
h : ∀ (x : A), x ∈ S
x : A
⊢ x ∈ S ↔ x ∈ ⊤

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
S : NonUnitalStarSubalgebra R A
h : S = ⊤
x : A
⊢ x ∈ ⊤

Tactic:
exact mem_top

Result:
no goals
-- Mathlib/Order/Cover.lean
lemma covBy_iff_exists_sdiff_singleton : s ⋖ t ↔ ∃ a ∈ t, t \ {a} = s :=
  ⟨CovBy.exists_set_sdiff_singleton, by rintro ⟨a, ha, rfl⟩; exact sdiff_singleton_covBy ha⟩

Proof state:
case intro.intro
α : Type u_1
t : Set α
a : α
ha : a ∈ t
⊢ t \ {a} ⋖ t

Tactic:
exact sdiff_singleton_covBy ha

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
⊢ (∃ a ∈ t, t \ {a} = s) → s ⋖ t

Tactic:
rintro ⟨a, ha, rfl⟩

Result:
case intro.intro
α : Type u_1
t : Set α
a : α
ha : a ∈ t
⊢ t \ {a} ⋖ t
-- Mathlib/GroupTheory/GroupAction/ConjAct.lean
theorem fixedPoints_eq_center : fixedPoints (ConjAct G) G = center G

Proof state:
case h
G : Type u_3
inst✝ : Group G
x : G
⊢ x ∈ fixedPoints (ConjAct G) G ↔ x ∈ ↑(center G)

Tactic:
simp [mem_center_iff, smul_def, mul_inv_eq_iff_eq_mul]

Result:
no goals

Proof state:
G : Type u_3
inst✝ : Group G
⊢ fixedPoints (ConjAct G) G = ↑(center G)

Tactic:
ext x

Result:
case h
G : Type u_3
inst✝ : Group G
x : G
⊢ x ∈ fixedPoints (ConjAct G) G ↔ x ∈ ↑(center G)
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
lemma isoSpec_hom_base_apply (x : U) :
    hU.isoSpec.hom.base x = (Spec.map (X.presheaf.germ U x x.2)).base (closedPoint _)

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ (TopCat.Hom.hom (Spec.map (X.presheaf.map (eqToHom ⋯).op)).base)
      ((ConcreteCategory.hom (Spec.map ((↑U).presheaf.germ ⊤ x trivial)).base) (closedPoint ↑((↑U).presheaf.stalk x))) =
    (ConcreteCategory.hom (Spec.map (X.presheaf.germ U ↑x ⋯)).base) (closedPoint ↑(X.presheaf.stalk ↑x))

Tactic:
rw [← Scheme.comp_base_apply, ← Spec.map_comp,
  (Iso.eq_comp_inv _).mpr (Scheme.Opens.germ_stalkIso_hom U (V := ⊤) x trivial),
  X.presheaf.germ_res_assoc, Spec.map_comp, Scheme.comp_base_apply]

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ (ConcreteCategory.hom (Spec.map (X.presheaf.germ U ↑x ⋯)).base)
      ((ConcreteCategory.hom (Spec.map (U.stalkIso x).inv).base) (closedPoint ↑((↑U).presheaf.stalk x))) =
    (ConcreteCategory.hom (Spec.map (X.presheaf.germ U ↑x ⋯)).base) (closedPoint ↑(X.presheaf.stalk ↑x))

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ (ConcreteCategory.hom hU.isoSpec.hom.base) x =
    (ConcreteCategory.hom (Spec.map (X.presheaf.germ U ↑x ⋯)).base) (closedPoint ↑(X.presheaf.stalk ↑x))

Tactic:
dsimp [IsAffineOpen.isoSpec_hom, Scheme.isoSpec_hom, Scheme.toSpecΓ_base, Scheme.Opens.toSpecΓ]

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ (TopCat.Hom.hom (Spec.map (X.presheaf.map (eqToHom ⋯).op)).base)
      ((ConcreteCategory.hom (Spec.map ((↑U).presheaf.germ ⊤ x trivial)).base) (closedPoint ↑((↑U).presheaf.stalk x))) =
    (ConcreteCategory.hom (Spec.map (X.presheaf.germ U ↑x ⋯)).base) (closedPoint ↑(X.presheaf.stalk ↑x))

Proof state:
case h.e_6.h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ (ConcreteCategory.hom (Spec.map (U.stalkIso x).inv).base) (closedPoint ↑((↑U).presheaf.stalk x)) =
    closedPoint ↑(X.presheaf.stalk ↑x)

Tactic:
exact IsLocalRing.comap_closedPoint (U.stalkIso x).inv.hom

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ (ConcreteCategory.hom (Spec.map (X.presheaf.germ U ↑x ⋯)).base)
      ((ConcreteCategory.hom (Spec.map (U.stalkIso x).inv).base) (closedPoint ↑((↑U).presheaf.stalk x))) =
    (ConcreteCategory.hom (Spec.map (X.presheaf.germ U ↑x ⋯)).base) (closedPoint ↑(X.presheaf.stalk ↑x))

Tactic:
congr 1

Result:
case h.e_6.h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ (ConcreteCategory.hom (Spec.map (U.stalkIso x).inv).base) (closedPoint ↑((↑U).presheaf.stalk x)) =
    closedPoint ↑(X.presheaf.stalk ↑x)
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem isIndepSet_neighborSet_of_triangleFree [DecidableEq α] (h: G.CliqueFree 3) (v : α) :
    G.IsIndepSet (G.neighborSet v)

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableEq α
h : G.CliqueFree 3
v j : α
avj : G.Adj v j
k : α
avk : G.Adj v k
left✝ : j ≠ k
ajk : G.Adj j k
⊢ G.Adj v j ∧ G.Adj v k ∧ G.Adj j k

Tactic:
simp [avj, avk, ajk]

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableEq α
h : G.CliqueFree 3
v : α
⊢ G.IsIndepSet (G.neighborSet v)

Tactic:
by_contra nind

Result:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableEq α
h : G.CliqueFree 3
v : α
nind : ¬G.IsIndepSet (G.neighborSet v)
⊢ False

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableEq α
h : G.CliqueFree 3
v : α
nind : ∃ x, G.Adj v x ∧ ∃ y, G.Adj v y ∧ x ≠ y ∧ G.Adj x y
⊢ False

Tactic:
obtain ⟨j, avj, k, avk, _, ajk⟩ := nind

Result:
case intro.intro.intro.intro.intro
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableEq α
h : G.CliqueFree 3
v j : α
avj : G.Adj v j
k : α
avk : G.Adj v k
left✝ : j ≠ k
ajk : G.Adj j k
⊢ False

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableEq α
h : G.CliqueFree 3
v : α
nind : ¬G.IsIndepSet (G.neighborSet v)
⊢ False

Tactic:
rw [IsIndepSet, Set.Pairwise] at nind

Result:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableEq α
h : G.CliqueFree 3
v : α
nind : ¬∀ ⦃x : α⦄, x ∈ G.neighborSet v → ∀ ⦃y : α⦄, y ∈ G.neighborSet v → x ≠ y → ¬G.Adj x y
⊢ False

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableEq α
h : G.CliqueFree 3
v : α
nind : ∃ x ∈ G.neighborSet v, ∃ y ∈ G.neighborSet v, x ≠ y ∧ G.Adj x y
⊢ False

Tactic:
simp_rw [mem_neighborSet] at nind

Result:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableEq α
h : G.CliqueFree 3
v : α
nind : ∃ x, G.Adj v x ∧ ∃ y, G.Adj v y ∧ x ≠ y ∧ G.Adj x y
⊢ False

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableEq α
h : G.CliqueFree 3
v j : α
avj : G.Adj v j
k : α
avk : G.Adj v k
left✝ : j ≠ k
ajk : G.Adj j k
⊢ False

Tactic:
exact h {v, j, k} (is3Clique_triple_iff.mpr (by simp [avj, avk, ajk]))

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableEq α
h : G.CliqueFree 3
v : α
nind : ¬∀ ⦃x : α⦄, x ∈ G.neighborSet v → ∀ ⦃y : α⦄, y ∈ G.neighborSet v → x ≠ y → ¬G.Adj x y
⊢ False

Tactic:
push_neg at nind

Result:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableEq α
h : G.CliqueFree 3
v : α
nind : ∃ x ∈ G.neighborSet v, ∃ y ∈ G.neighborSet v, x ≠ y ∧ G.Adj x y
⊢ False