harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/Stalk.lean
@[reassoc (attr := simp)]
lemma Opens.fromSpecStalkOfMem_toSpecΓ {X : Scheme.{u}} (U : X.Opens) (x : X) (hxU : x ∈ U) :
    U.fromSpecStalkOfMem x hxU ≫ U.toSpecΓ = Spec.map (X.presheaf.germ U x hxU)

Proof state:
case e_f
X : Scheme
U : X.Opens
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
⊢ (↑U).presheaf.germ ⊤ ⟨x, hxU⟩ trivial = U.topIso.hom ≫ X.presheaf.germ U x hxU ≫ Hom.stalkMap U.ι ⟨x, hxU⟩

Tactic:
erw [stalkMap_germ U.ι U ⟨x, hxU⟩]

Result:
case e_f
X : Scheme
U : X.Opens
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
⊢ (↑U).presheaf.germ ⊤ ⟨x, hxU⟩ trivial = U.topIso.hom ≫ Hom.app U.ι U ≫ (↑U).presheaf.germ (U.ι ⁻¹ᵁ U) ⟨x, hxU⟩ hxU

Proof state:
case e_f
X : Scheme
U : X.Opens
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
⊢ (↑U).presheaf.germ ⊤ ⟨x, hxU⟩ trivial = U.topIso.hom ≫ Hom.app U.ι U ≫ (↑U).presheaf.germ (U.ι ⁻¹ᵁ U) ⟨x, hxU⟩ hxU

Tactic:
rw [Opens.ι_app, Opens.topIso_hom, ← Functor.map_comp_assoc]

Result:
case e_f
X : Scheme
U : X.Opens
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
⊢ (↑U).presheaf.germ ⊤ ⟨x, hxU⟩ trivial =
    X.presheaf.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op) ≫ (↑U).presheaf.germ (U.ι ⁻¹ᵁ U) ⟨x, hxU⟩ hxU

Proof state:
case e_f
X : Scheme
U : X.Opens
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
⊢ (U.topIso.inv ≫ (↑U).presheaf.germ ⊤ ⟨x, hxU⟩ trivial) ≫ inv (Hom.stalkMap U.ι ⟨x, hxU⟩) = X.presheaf.germ U x hxU

Tactic:
rw [IsIso.comp_inv_eq, Iso.inv_comp_eq]

Result:
case e_f
X : Scheme
U : X.Opens
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
⊢ (↑U).presheaf.germ ⊤ ⟨x, hxU⟩ trivial = U.topIso.hom ≫ X.presheaf.germ U x hxU ≫ Hom.stalkMap U.ι ⟨x, hxU⟩

Proof state:
X : Scheme
U : X.Opens
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
⊢ U.fromSpecStalkOfMem x hxU ≫ U.toSpecΓ = Spec.map (X.presheaf.germ U x hxU)

Tactic:
rw [fromSpecStalkOfMem, Opens.toSpecΓ, Category.assoc, fromSpecStalk_toSpecΓ_assoc,
  ← Spec.map_comp, ← Spec.map_comp]

Result:
X : Scheme
U : X.Opens
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
⊢ Spec.map ((U.topIso.inv ≫ (↑U).presheaf.germ ⊤ ⟨x, hxU⟩ trivial) ≫ inv (Hom.stalkMap U.ι ⟨x, hxU⟩)) =
    Spec.map (X.presheaf.germ U x hxU)

Proof state:
case e_f
X : Scheme
U : X.Opens
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
⊢ (↑U).presheaf.germ ⊤ ⟨x, hxU⟩ trivial =
    X.presheaf.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op) ≫ (↑U).presheaf.germ (U.ι ⁻¹ᵁ U) ⟨x, hxU⟩ hxU

Tactic:
exact (U.toScheme.presheaf.germ_res (homOfLE le_top) ⟨x, hxU⟩ (U := U.ι ⁻¹ᵁ U) hxU).symm

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
⊢ Spec.map ((U.topIso.inv ≫ (↑U).presheaf.germ ⊤ ⟨x, hxU⟩ trivial) ≫ inv (Hom.stalkMap U.ι ⟨x, hxU⟩)) =
    Spec.map (X.presheaf.germ U x hxU)

Tactic:
congr 1

Result:
case e_f
X : Scheme
U : X.Opens
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
⊢ (U.topIso.inv ≫ (↑U).presheaf.germ ⊤ ⟨x, hxU⟩ trivial) ≫ inv (Hom.stalkMap U.ι ⟨x, hxU⟩) = X.presheaf.germ U x hxU
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem cos_angle_mul_norm_mul_norm (x y : V) : Real.cos (angle x y) * (‖x‖ * ‖y‖) = ⟪x, y⟫

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ ‖x‖ * ‖y‖ = 0 → inner x y = 0

Tactic:
simp +contextual [or_imp]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ cos (angle x y) * (‖x‖ * ‖y‖) = inner x y

Tactic:
rw [cos_angle, div_mul_cancel_of_imp]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ ‖x‖ * ‖y‖ = 0 → inner x y = 0
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem transPartialEquiv_trans (e : α ≃ β) (f' : PartialEquiv β γ) (f'' : PartialEquiv γ δ) :
    (e.transPartialEquiv f').trans f'' = e.transPartialEquiv (f'.trans f'')

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
f' : PartialEquiv β γ
f'' : PartialEquiv γ δ
⊢ (e.transPartialEquiv f').trans f'' = e.transPartialEquiv (f'.trans f'')

Tactic:
simp only [transPartialEquiv_eq_trans, PartialEquiv.trans_assoc]

Result:
no goals
-- Mathlib/RingTheory/Localization/NormTrace.lean
theorem Algebra.map_leftMulMatrix_localization {ι : Type*} [Fintype ι] [DecidableEq ι]
    (b : Basis ι R S) (a : S) :
    (algebraMap R Rₘ).mapMatrix (leftMulMatrix b a) =
    leftMulMatrix (b.localizationLocalization Rₘ M Sₘ) (algebraMap S Sₘ a)

Proof state:
case a
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
a : S
i j : ι
⊢ (algebraMap R Rₘ).mapMatrix ((leftMulMatrix b) a) i j =
    (leftMulMatrix (Basis.localizationLocalization Rₘ M Sₘ b)) ((algebraMap S Sₘ) a) i j

Tactic:
simp only [Matrix.map_apply, RingHom.mapMatrix_apply, leftMulMatrix_eq_repr_mul, ← map_mul,
  Basis.localizationLocalization_apply, Basis.localizationLocalization_repr_algebraMap]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
a : S
⊢ (algebraMap R Rₘ).mapMatrix ((leftMulMatrix b) a) =
    (leftMulMatrix (Basis.localizationLocalization Rₘ M Sₘ b)) ((algebraMap S Sₘ) a)

Tactic:
ext i j

Result:
case a
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
a : S
i j : ι
⊢ (algebraMap R Rₘ).mapMatrix ((leftMulMatrix b) a) i j =
    (leftMulMatrix (Basis.localizationLocalization Rₘ M Sₘ b)) ((algebraMap S Sₘ) a) i j
-- Mathlib/Analysis/Normed/Group/AddCircle.lean
theorem le_add_order_smul_norm_of_isOfFinAddOrder {u : AddCircle p} (hu : IsOfFinAddOrder u)
    (hu' : u ≠ 0) : p ≤ addOrderOf u • ‖u‖

Proof state:
case intro
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
hu : ↑(addOrderOf u) ≠ 0
hu' : n = 0
⊢ u = 0

Tactic:
simpa only [hu', Nat.cast_zero, zero_div, mul_zero, norm_eq_zero] using hn

Result:
no goals

Proof state:
case intro
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
⊢ p ≤ addOrderOf u • ‖u‖

Tactic:
replace hu : (addOrderOf u : ℝ) ≠ 0 := by
  norm_cast
  exact (addOrderOf_pos_iff.mpr hu).ne'

Result:
case intro
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
hu : ↑(addOrderOf u) ≠ 0
⊢ p ≤ addOrderOf u • ‖u‖

Proof state:
case intro
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
hu : ↑(addOrderOf u) ≠ 0
⊢ p * 1 ≤ addOrderOf u • ‖u‖

Tactic:
rw [hn, nsmul_eq_mul, ← mul_assoc, mul_comm _ p, mul_assoc, mul_div_cancel₀ _ hu,
  mul_le_mul_left hp.out, Nat.one_le_cast, Nat.one_le_iff_ne_zero]

Result:
case intro
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
hu : ↑(addOrderOf u) ≠ 0
⊢ n ≠ 0

Proof state:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
hu' : u ≠ 0
⊢ p ≤ addOrderOf u • ‖u‖

Tactic:
obtain ⟨n, hn⟩ := exists_norm_eq_of_isOfFinAddOrder hu

Result:
case intro
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
⊢ p ≤ addOrderOf u • ‖u‖

Proof state:
case intro
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
hu : ↑(addOrderOf u) ≠ 0
⊢ n ≠ 0

Tactic:
contrapose! hu'

Result:
case intro
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
hu : ↑(addOrderOf u) ≠ 0
hu' : n = 0
⊢ u = 0

Proof state:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
⊢ ¬addOrderOf u = 0

Tactic:
exact (addOrderOf_pos_iff.mpr hu).ne'

Result:
no goals

Proof state:
case intro
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
hu : ↑(addOrderOf u) ≠ 0
⊢ p ≤ addOrderOf u • ‖u‖

Tactic:
conv_lhs => rw [← mul_one p]

Result:
case intro
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
hu : ↑(addOrderOf u) ≠ 0
⊢ p * 1 ≤ addOrderOf u • ‖u‖

Proof state:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
⊢ ↑(addOrderOf u) ≠ 0

Tactic:
norm_cast

Result:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
⊢ ¬addOrderOf u = 0
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem containsThenInsert_eq_insertₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (b : β a) :
    (m.containsThenInsert a b).2 = m.insertₘ a b

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
b : β a
⊢ (match mkIdx m.1.buckets.size ⋯ (hash a) with
      | ⟨i, h⟩ =>
        let bkt := m.1.buckets[i];
        if AssocList.contains a bkt = true then
          let buckets' := m.1.buckets.uset i AssocList.nil h;
          (true, ⟨{ size := m.1.size, buckets := buckets'.uset i (AssocList.replace a b bkt) ⋯ }, ⋯⟩)
        else
          let size' := m.1.size + 1;
          let buckets' := m.1.buckets.uset i (AssocList.cons a b bkt) h;
          (false, expandIfNecessary ⟨{ size := size', buckets := buckets' }, ⋯⟩)).snd =
    if
        AssocList.contains a
            (match mkIdx m.val.buckets.size ⋯ (hash a) with
            | ⟨i, h⟩ => m.val.buckets[i]) =
          true then
      m.replaceₘ a b
    else (m.consₘ a b).expandIfNecessary

Tactic:
dsimp only [Array.ugetElem_eq_getElem, Array.uset]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
b : β a
⊢ (if AssocList.contains a m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat] = true then
        (true,
          ⟨{ size := m.1.size,
              buckets :=
                (m.1.buckets.set (mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat AssocList.nil ⋯).set
                  (mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat
                  (AssocList.replace a b m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat]) ⋯ },
            ⋯⟩)
      else
        (false,
          expandIfNecessary
            ⟨{ size := m.1.size + 1,
                buckets :=
                  m.1.buckets.set (mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat
                    (AssocList.cons a b m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat]) ⋯ },
              ⋯⟩)).snd =
    if AssocList.contains a m.val.buckets[(mkIdx m.val.buckets.size ⋯ (hash a)).val.toNat] = true then m.replaceₘ a b
    else (m.consₘ a b).expandIfNecessary

Proof state:
case isFalse
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
b : β a
h✝ : ¬AssocList.contains a m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat] = true
⊢ (false,
        expandIfNecessary
          ⟨{ size := m.1.size + 1,
              buckets :=
                m.1.buckets.set (mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat
                  (AssocList.cons a b m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat]) ⋯ },
            ⋯⟩).snd =
    (m.consₘ a b).expandIfNecessary

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma closure_insert_eq_of_mem_closure (he : e ∈ M.closure X) :
    M.closure (insert e X) = M.closure X

Proof state:
α : Type u_2
M : Matroid α
X : Set α
e : α
he : e ∈ M.closure X
⊢ M.closure (insert e X) = M.closure X

Tactic:
rw [← closure_insert_closure_eq_closure_insert, insert_eq_of_mem he, closure_closure]

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Finset.lean
lemma Multiset.iSup_mem_map_of_exists_sSup_empty_le {s : Multiset ι} (f : ι → α)
    (h : ∃ x ∈ s, sSup ∅ ≤ f x) :
    ⨆ x ∈ s, f x ∈ s.map f

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Multiset ι
f : ι → α
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ∃ x ∈ s.toFinset, sSup ∅ ≤ f x

Tactic:
simpa using h

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Multiset ι
f : ι → α
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ⨆ x ∈ s, f x ∈ map f s

Tactic:
classical
simpa using s.toFinset.ciSup_mem_image f (by simpa using h)

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Multiset ι
f : ι → α
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ⨆ x ∈ s, f x ∈ map f s

Tactic:
simpa using s.toFinset.ciSup_mem_image f (by simpa using h)

Result:
no goals
-- Mathlib/Topology/LocallyConstant/Basic.lean
@[simp]
lemma piecewise'_apply_left {C₀ C₁ C₂ : Set X} (h₀ : C₀ ⊆ C₁ ∪ C₂) (h₁ : IsClosed C₁)
    (h₂ : IsClosed C₂) (f₁ : LocallyConstant C₁ Z) (f₂ : LocallyConstant C₂ Z)
    [DecidablePred (· ∈ C₁)] (hf : ∀ x (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, hx.1⟩ = f₂ ⟨x, hx.2⟩)
    (x : C₀) (hx : x.val ∈ C₁) :
    piecewise' h₀ h₁ h₂ f₁ f₂ hf x = f₁ ⟨x.val, hx⟩

Proof state:
X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₀ C₁ C₂ : Set X
h₀ : C₀ ⊆ C₁ ∪ C₂
h₁ : IsClosed C₁
h₂ : IsClosed C₂
f₁ : LocallyConstant (↑C₁) Z
f₂ : LocallyConstant (↑C₂) Z
inst✝ : DecidablePred fun x => x ∈ C₁
hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩
x : ↑C₀
hx : ↑x ∈ C₁
this : (j : ↑C₀) → Decidable (j ∈ Subtype.val ⁻¹' C₁) := fun j => decidable_of_iff (↑j ∈ C₁) ⋯
⊢ (piecewise' h₀ h₁ h₂ f₁ f₂ hf) x = f₁ ⟨↑x, hx⟩

Tactic:
rw [piecewise', piecewise_apply_left (f := (f₁.comap
  ⟨(restrictPreimage C₁ ((↑) : C₀ → X)), continuous_subtype_val.restrictPreimage⟩))
  (hx := hx)]

Result:
X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₀ C₁ C₂ : Set X
h₀ : C₀ ⊆ C₁ ∪ C₂
h₁ : IsClosed C₁
h₂ : IsClosed C₂
f₁ : LocallyConstant (↑C₁) Z
f₂ : LocallyConstant (↑C₂) Z
inst✝ : DecidablePred fun x => x ∈ C₁
hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩
x : ↑C₀
hx : ↑x ∈ C₁
this : (j : ↑C₀) → Decidable (j ∈ Subtype.val ⁻¹' C₁) := fun j => decidable_of_iff (↑j ∈ C₁) ⋯
⊢ (comap { toFun := C₁.restrictPreimage Subtype.val, continuous_toFun := ⋯ } f₁) ⟨x, hx⟩ = f₁ ⟨↑x, hx⟩

Proof state:
X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₀ C₁ C₂ : Set X
h₀ : C₀ ⊆ C₁ ∪ C₂
h₁ : IsClosed C₁
h₂ : IsClosed C₂
f₁ : LocallyConstant (↑C₁) Z
f₂ : LocallyConstant (↑C₂) Z
inst✝ : DecidablePred fun x => x ∈ C₁
hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩
x : ↑C₀
hx : ↑x ∈ C₁
⊢ (piecewise' h₀ h₁ h₂ f₁ f₂ hf) x = f₁ ⟨↑x, hx⟩

Tactic:
letI : ∀ j : C₀, Decidable (j ∈ Subtype.val ⁻¹' C₁) := fun j ↦ decidable_of_iff (↑j ∈ C₁) Iff.rfl

Result:
X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₀ C₁ C₂ : Set X
h₀ : C₀ ⊆ C₁ ∪ C₂
h₁ : IsClosed C₁
h₂ : IsClosed C₂
f₁ : LocallyConstant (↑C₁) Z
f₂ : LocallyConstant (↑C₂) Z
inst✝ : DecidablePred fun x => x ∈ C₁
hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩
x : ↑C₀
hx : ↑x ∈ C₁
this : (j : ↑C₀) → Decidable (j ∈ Subtype.val ⁻¹' C₁) := fun j => decidable_of_iff (↑j ∈ C₁) ⋯
⊢ (piecewise' h₀ h₁ h₂ f₁ f₂ hf) x = f₁ ⟨↑x, hx⟩

Proof state:
X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₀ C₁ C₂ : Set X
h₀ : C₀ ⊆ C₁ ∪ C₂
h₁ : IsClosed C₁
h₂ : IsClosed C₂
f₁ : LocallyConstant (↑C₁) Z
f₂ : LocallyConstant (↑C₂) Z
inst✝ : DecidablePred fun x => x ∈ C₁
hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩
x : ↑C₀
hx : ↑x ∈ C₁
this : (j : ↑C₀) → Decidable (j ∈ Subtype.val ⁻¹' C₁) := fun j => decidable_of_iff (↑j ∈ C₁) ⋯
⊢ (comap { toFun := C₁.restrictPreimage Subtype.val, continuous_toFun := ⋯ } f₁) ⟨x, hx⟩ = f₁ ⟨↑x, hx⟩

Tactic:
rfl

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
theorem IsMatching.support_eq_verts (h : M.IsMatching) : M.support = M.verts

Proof state:
case intro.intro
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
hv : v ∈ M.verts
w : V
hvw : M.Adj v w
⊢ v ∈ M.support

Tactic:
exact ⟨_, hvw⟩

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
⊢ M.support = M.verts

Tactic:
refine M.support_subset_verts.antisymm fun v hv => ?_

Result:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
hv : v ∈ M.verts
⊢ v ∈ M.support

Proof state:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
hv : v ∈ M.verts
⊢ v ∈ M.support

Tactic:
obtain ⟨w, hvw, -⟩ := h hv

Result:
case intro.intro
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
hv : v ∈ M.verts
w : V
hvw : M.Adj v w
⊢ v ∈ M.support
-- Mathlib/Data/Set/Finite/Lattice.lean
theorem union_finset_finite_of_range_finite (f : α → Finset β) (h : (range f).Finite) :
    (⋃ a, (f a : Set β)).Finite

Proof state:
α : Type u
β : Type v
f : α → Finset β
h : (range f).Finite
⊢ (⋃ a, ↑(f a)).Finite

Tactic:
rw [← biUnion_range]

Result:
α : Type u
β : Type v
f : α → Finset β
h : (range f).Finite
⊢ (⋃ x ∈ range f, ↑x).Finite

Proof state:
α : Type u
β : Type v
f : α → Finset β
h : (range f).Finite
⊢ (⋃ x ∈ range f, ↑x).Finite

Tactic:
exact h.biUnion fun y _ => y.finite_toSet

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Images.lean
theorem image.ext [HasImage f] {W : C} {g h : image f ⟶ W} [HasLimit (parallelPair g h)]
    (w : factorThruImage f ≫ g = factorThruImage f ≫ h) : g = h

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := MonoFactorisation.mk (equalizer g h) (q ≫ ι f) e' ⋯
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
⊢ v ≫ q ≫ h = 𝟙 (image f) ≫ h

Tactic:
rw [← Category.assoc, t]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := MonoFactorisation.mk (equalizer g h) (q ≫ ι f) e' ⋯
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
⊢ g = 𝟙 (image f) ≫ g

Tactic:
rw [Category.id_comp]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
⊢ g = h

Tactic:
let q := equalizer.ι g h

Result:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
⊢ g = h

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := MonoFactorisation.mk (equalizer g h) (q ≫ ι f) e' ⋯
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
⊢ 𝟙 (image f) ≫ g = v ≫ q ≫ g

Tactic:
rw [← t, Category.assoc]

Result:
no goals
-- Mathlib/Logic/Relation.lean
theorem iff_comp {r : Prop → α → Prop} : (· ↔ ·) ∘r r = r

Proof state:
α : Type u_1
r : Prop → α → Prop
⊢ (fun x1 x2 => x1 ↔ x2) = fun x1 x2 => x1 = x2

Tactic:
funext a b

Result:
case h.h
α : Type u_1
r : Prop → α → Prop
a b : Prop
⊢ (a ↔ b) = (a = b)

Proof state:
case h.h
α : Type u_1
r : Prop → α → Prop
a b : Prop
⊢ (a ↔ b) = (a = b)

Tactic:
exact iff_eq_eq

Result:
no goals

Proof state:
α : Type u_1
r : Prop → α → Prop
this : (fun x1 x2 => x1 ↔ x2) = fun x1 x2 => x1 = x2
⊢ (fun x1 x2 => x1 ↔ x2) ∘r r = r

Tactic:
rw [this, eq_comp]

Result:
no goals
-- Mathlib/Data/Matroid/Rank/Finite.lean
@[simp]
lemma isRkFinite_closure_iff : M.IsRkFinite (M.closure X) ↔ M.IsRkFinite X

Proof state:
α : Type u_1
M : Matroid α
X : Set α
h : M.IsRkFinite (X ∩ M.E)
⊢ M.IsRkFinite (M.closure X)

Tactic:
simpa using h.closure

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.IsRkFinite (M.closure X) ↔ M.IsRkFinite X

Tactic:
rw [← isRkFinite_inter_ground_iff (X := X)]

Result:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.IsRkFinite (M.closure X) ↔ M.IsRkFinite (X ∩ M.E)

Proof state:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.IsRkFinite (M.closure X) ↔ M.IsRkFinite (X ∩ M.E)

Tactic:
exact ⟨fun h ↦ h.subset <| M.inter_ground_subset_closure X, fun h ↦ by simpa using h.closure⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem ofNat'_sub [NeZero n] (x : Nat) (y : Fin n) :
    Fin.ofNat' n x - y = Fin.ofNat' n ((n - y.val) + x)

Proof state:
case a
n : Nat
inst✝ : NeZero n
x : Nat
y : Fin n
⊢ ↑(Fin.ofNat' n x - y) = ↑(Fin.ofNat' n (n - ↑y + x))

Tactic:
simp [Fin.ofNat', Fin.sub_def]

Result:
no goals

Proof state:
n : Nat
inst✝ : NeZero n
x : Nat
y : Fin n
⊢ Fin.ofNat' n x - y = Fin.ofNat' n (n - ↑y + x)

Tactic:
apply Fin.eq_of_val_eq

Result:
case a
n : Nat
inst✝ : NeZero n
x : Nat
y : Fin n
⊢ ↑(Fin.ofNat' n x - y) = ↑(Fin.ofNat' n (n - ↑y + x))