harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Module/SnakeLemma.lean
/--
Suppose we have an exact commutative diagram
```
                K₃
                |
                ι₃
                ↓
M₁ -f₁→ M₂ -f₂→ M₃
|       |       |
i₁      i₂      i₃
↓       ↓       ↓
N₁ -g₁→ N₂ -g₂→ N₃
|       |
π₁      π₂
↓       ↓
C₁ -G-→ C₂

```
such that `f₂` is surjective with a (set-theoretic) section `σ`, `g₁` is injective with a
(set-theoretic) retraction `ρ`, and `π₁` is surjective, then `K₂ -δ→ C₁ -G→ C₂` is exact.
-/
lemma SnakeLemma.exact_δ_left (G : C₁ →ₗ[R] C₂) (hF : G.comp π₁ = π₂.comp g₁) (h : Surjective π₁) :
    Exact (δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) G

Proof state:
R : Type u_1
inst✝¹⁸ : CommRing R
M₁ : Type u_7
M₂ : Type u_8
M₃ : Type u_9
N₁ : Type u_4
N₂ : Type u_5
N₃ : Type u_10
inst✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : Module R M₁
inst✝¹⁵ : AddCommGroup M₂
inst✝¹⁴ : Module R M₂
inst✝¹³ : AddCommGroup M₃
inst✝¹² : Module R M₃
inst✝¹¹ : AddCommGroup N₁
inst✝¹⁰ : Module R N₁
inst✝⁹ : AddCommGroup N₂
inst✝⁸ : Module R N₂
inst✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_6
C₁ : Type u_2
C₂ : Type u_3
inst✝⁵ : AddCommGroup K₃
inst✝⁴ : Module R K₃
inst✝³ : AddCommGroup C₁
inst✝² : Module R C₁
inst✝¹ : AddCommGroup C₂
inst✝ : Module R C₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact ⇑i₂ ⇑π₂
G : C₁ →ₗ[R] C₂
hF : G ∘ₗ π₁ = π₂ ∘ₗ g₁
h : Surjective ⇑π₁
⊢ Exact ⇑(δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) ⇑G

Tactic:
haveI H₁ : ∀ x, f₂ (σ x) = x := congr_fun hσ

Result:
R : Type u_1
inst✝¹⁸ : CommRing R
M₁ : Type u_7
M₂ : Type u_8
M₃ : Type u_9
N₁ : Type u_4
N₂ : Type u_5
N₃ : Type u_10
inst✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : Module R M₁
inst✝¹⁵ : AddCommGroup M₂
inst✝¹⁴ : Module R M₂
inst✝¹³ : AddCommGroup M₃
inst✝¹² : Module R M₃
inst✝¹¹ : AddCommGroup N₁
inst✝¹⁰ : Module R N₁
inst✝⁹ : AddCommGroup N₂
inst✝⁸ : Module R N₂
inst✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_6
C₁ : Type u_2
C₂ : Type u_3
inst✝⁵ : AddCommGroup K₃
inst✝⁴ : Module R K₃
inst✝³ : AddCommGroup C₁
inst✝² : Module R C₁
inst✝¹ : AddCommGroup C₂
inst✝ : Module R C₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact ⇑i₂ ⇑π₂
G : C₁ →ₗ[R] C₂
hF : G ∘ₗ π₁ = π₂ ∘ₗ g₁
h : Surjective ⇑π₁
H₁ : ∀ (x : M₃), f₂ (σ x) = x
⊢ Exact ⇑(δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) ⇑G
-- Mathlib/MeasureTheory/Covering/Besicovitch.lean
theorem ae_tendsto_measure_inter_div_of_measurableSet (μ : Measure β) [IsLocallyFiniteMeasure μ]
    {s : Set β} (hs : MeasurableSet s) :
    ∀ᵐ x ∂μ,
      Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0)
        (𝓝 (s.indicator 1 x))

Proof state:
case h
β : Type u
inst✝⁵ : MetricSpace β
inst✝⁴ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : HasBesicovitchCovering β
μ : Measure β
inst✝ : IsLocallyFiniteMeasure μ
s : Set β
hs : MeasurableSet s
⊢ ∀ (a : β),
    Tendsto (fun a => μ (s ∩ a) / μ a) ((Besicovitch.vitaliFamily μ).filterAt a) (𝓝 (s.indicator 1 a)) →
      Tendsto (fun r => μ (s ∩ closedBall a r) / μ (closedBall a r)) (𝓝[>] 0) (𝓝 (s.indicator 1 a))

Tactic:
intro x hx

Result:
case h
β : Type u
inst✝⁵ : MetricSpace β
inst✝⁴ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : HasBesicovitchCovering β
μ : Measure β
inst✝ : IsLocallyFiniteMeasure μ
s : Set β
hs : MeasurableSet s
x : β
hx : Tendsto (fun a => μ (s ∩ a) / μ a) ((Besicovitch.vitaliFamily μ).filterAt x) (𝓝 (s.indicator 1 x))
⊢ Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 (s.indicator 1 x))

Proof state:
case h
β : Type u
inst✝⁵ : MetricSpace β
inst✝⁴ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : HasBesicovitchCovering β
μ : Measure β
inst✝ : IsLocallyFiniteMeasure μ
s : Set β
hs : MeasurableSet s
x : β
hx : Tendsto (fun a => μ (s ∩ a) / μ a) ((Besicovitch.vitaliFamily μ).filterAt x) (𝓝 (s.indicator 1 x))
⊢ Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 (s.indicator 1 x))

Tactic:
exact hx.comp (tendsto_filterAt μ x)

Result:
no goals

Proof state:
β : Type u
inst✝⁵ : MetricSpace β
inst✝⁴ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : HasBesicovitchCovering β
μ : Measure β
inst✝ : IsLocallyFiniteMeasure μ
s : Set β
hs : MeasurableSet s
⊢ ∀ᵐ (x : β) ∂μ, Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 (s.indicator 1 x))

Tactic:
filter_upwards [VitaliFamily.ae_tendsto_measure_inter_div_of_measurableSet
    (Besicovitch.vitaliFamily μ) hs]

Result:
case h
β : Type u
inst✝⁵ : MetricSpace β
inst✝⁴ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : HasBesicovitchCovering β
μ : Measure β
inst✝ : IsLocallyFiniteMeasure μ
s : Set β
hs : MeasurableSet s
⊢ ∀ (a : β),
    Tendsto (fun a => μ (s ∩ a) / μ a) ((Besicovitch.vitaliFamily μ).filterAt a) (𝓝 (s.indicator 1 a)) →
      Tendsto (fun r => μ (s ∩ closedBall a r) / μ (closedBall a r)) (𝓝[>] 0) (𝓝 (s.indicator 1 a))
-- Mathlib/Order/Filter/NAry.lean
theorem map₂_sup_right : map₂ m f (g₁ ⊔ g₂) = map₂ m f g₁ ⊔ map₂ m f g₂

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g₁ g₂ : Filter β
⊢ map₂ m f (g₁ ⊔ g₂) = map₂ m f g₁ ⊔ map₂ m f g₂

Tactic:
simp_rw [← map_prod_eq_map₂, prod_sup, map_sup]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignment)
    (assignments0_size : assignments0.size = n) (units : Array (Literal (PosFin n)))
    (assignments : Array Assignment) (assignments_size : assignments.size = n)
    (foundContradiction : Bool) (l : Literal (PosFin n)) :
    InsertUnitInvariant assignments0 assignments0_size units assignments assignments_size →
    let update_res := insertUnit (units, assignments, foundContradiction) l
    have update_res_size : update_res.snd.fst.size = n

Proof state:
case right.right.left
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
i : Fin n
i_in_bounds : ↑i < assignments.size
l_in_bounds : l.fst.val < assignments.size
j : Fin units.size
b : Bool
i_gt_zero : ↑i > 0
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_eq_l : ↑i = l.fst.val
units_size_lt_updatedUnits_size : units.size < (insertUnit (units, assignments, foundContradiction) l).fst.size
mostRecentUnitIdx : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size :=
  ⟨units.size, units_size_lt_updatedUnits_size⟩
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
h1 : units[↑j] = (⟨↑i, ⋯⟩, false)
h2 : assignments[↑i] = addAssignment false assignments0[↑i]
h3 : hasAssignment false assignments0[↑i] = false
hb : b = false
hl : l.snd = true
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[l.fst.val] = both

Tactic:
rw [Array.getElem_modify_self]

Result:
case right.right.left
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
i : Fin n
i_in_bounds : ↑i < assignments.size
l_in_bounds : l.fst.val < assignments.size
j : Fin units.size
b : Bool
i_gt_zero : ↑i > 0
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_eq_l : ↑i = l.fst.val
units_size_lt_updatedUnits_size : units.size < (insertUnit (units, assignments, foundContradiction) l).fst.size
mostRecentUnitIdx : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size :=
  ⟨units.size, units_size_lt_updatedUnits_size⟩
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
h1 : units[↑j] = (⟨↑i, ⋯⟩, false)
h2 : assignments[↑i] = addAssignment false assignments0[↑i]
h3 : hasAssignment false assignments0[↑i] = false
hb : b = false
hl : l.snd = true
⊢ addAssignment l.snd assignments[l.fst.val] = both
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignment)
    (assignments0_size : assignments0.size = n) (units : Array (Literal (PosFin n)))
    (assignments : Array Assignment) (assignments_size : assignments.size = n)
    (foundContradiction : Bool) (l : Literal (PosFin n)) :
    InsertUnitInvariant assignments0 assignments0_size units assignments assignments_size →
    let update_res := insertUnit (units, assignments, foundContradiction) l
    have update_res_size : update_res.snd.fst.size = n

Proof state:
case right.right.left
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
i : Fin n
i_in_bounds : ↑i < assignments.size
l_in_bounds : l.fst.val < assignments.size
j : Fin units.size
b : Bool
i_gt_zero : ↑i > 0
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_eq_l : ↑i = l.fst.val
units_size_lt_updatedUnits_size : units.size < (insertUnit (units, assignments, foundContradiction) l).fst.size
mostRecentUnitIdx : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size :=
  ⟨units.size, units_size_lt_updatedUnits_size⟩
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
h1 : units[↑j] = (⟨↑i, ⋯⟩, false)
h2 : assignments[↑i] = addAssignment false assignments0[↑i]
h3 : hasAssignment false assignments0[↑i] = false
hb : b = false
hl : l.snd = true
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[↑i] = both

Tactic:
simp only [i_eq_l]

Result:
case right.right.left
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
i : Fin n
i_in_bounds : ↑i < assignments.size
l_in_bounds : l.fst.val < assignments.size
j : Fin units.size
b : Bool
i_gt_zero : ↑i > 0
h4 : ∀ (k : Fin units.size), ¬k = j → ¬units[↑k].fst.val = ↑i
h5 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_eq_l : ↑i = l.fst.val
units_size_lt_updatedUnits_size : units.size < (insertUnit (units, assignments, foundContradiction) l).fst.size
mostRecentUnitIdx : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size :=
  ⟨units.size, units_size_lt_updatedUnits_size⟩
j_lt_updatedUnits_size : ↑j < (insertUnit (units, assignments, foundContradiction) l).fst.size
h1 : units[↑j] = (⟨↑i, ⋯⟩, false)
h2 : assignments[↑i] = addAssignment false assignments0[↑i]
h3 : hasAssignment false assignments0[↑i] = false
hb : b = false
hl : l.snd = true
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[l.fst.val] = both
-- Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean
theorem map (hf : f.IsWeaklyEisensteinAt 𝓟) {A : Type v} [CommRing A] (φ : R →+* A) :
    (f.map φ).IsWeaklyEisensteinAt (𝓟.map φ)

Proof state:
R : Type u
inst✝¹ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
A : Type v
inst✝ : CommRing A
φ : R →+* A
n✝ : ℕ
hn : n✝ < (Polynomial.map φ f).natDegree
⊢ (Polynomial.map φ f).coeff n✝ ∈ Ideal.map φ 𝓟

Tactic:
rw [coeff_map]

Result:
R : Type u
inst✝¹ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
A : Type v
inst✝ : CommRing A
φ : R →+* A
n✝ : ℕ
hn : n✝ < (Polynomial.map φ f).natDegree
⊢ φ (f.coeff n✝) ∈ Ideal.map φ 𝓟

Proof state:
R : Type u
inst✝¹ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ (Polynomial.map φ f).IsWeaklyEisensteinAt (Ideal.map φ 𝓟)

Tactic:
refine (isWeaklyEisensteinAt_iff _ _).2 fun hn => ?_

Result:
R : Type u
inst✝¹ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
A : Type v
inst✝ : CommRing A
φ : R →+* A
n✝ : ℕ
hn : n✝ < (Polynomial.map φ f).natDegree
⊢ (Polynomial.map φ f).coeff n✝ ∈ Ideal.map φ 𝓟

Proof state:
R : Type u
inst✝¹ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
A : Type v
inst✝ : CommRing A
φ : R →+* A
n✝ : ℕ
hn : n✝ < (Polynomial.map φ f).natDegree
⊢ φ (f.coeff n✝) ∈ Ideal.map φ 𝓟

Tactic:
exact mem_map_of_mem _ (hf.mem (lt_of_lt_of_le hn natDegree_map_le))

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[simp]
lemma inl_snd :
    (inl φ).comp (snd φ) (add_zero (-1)) = 0

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
p q : ℤ
hpq : p + -1 = q
⊢ q + 0 = q

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
⊢ (inl φ).comp (snd φ) ⋯ = 0

Tactic:
ext p q hpq

Result:
case h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
p q : ℤ
hpq : p + -1 = q
⊢ ((inl φ).comp (snd φ) ⋯).v p q hpq = Cochain.v 0 p q hpq

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
p q : ℤ
hpq : p + -1 = q
⊢ p + -1 = q

Tactic:
omega

Result:
no goals

Proof state:
case h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
p q : ℤ
hpq : p + -1 = q
⊢ ((inl φ).comp (snd φ) ⋯).v p q hpq = Cochain.v 0 p q hpq

Tactic:
simp [Cochain.comp_v _ _ (add_zero (-1)) p q q (by omega) (by omega)]

Result:
no goals
-- Mathlib/Data/ZMod/Units.lean
lemma unitsMap_comp {d : ℕ} (hm : n ∣ m) (hd : m ∣ d) :
    (unitsMap hm).comp (unitsMap hd) = unitsMap (dvd_trans hm hd)

Proof state:
n m d : ℕ
hm : n ∣ m
hd : m ∣ d
⊢ (Units.map ↑(castHom hm (ZMod n))).comp (Units.map ↑(castHom hd (ZMod m))) = Units.map ↑(castHom ⋯ (ZMod n))

Tactic:
rw [← Units.map_comp]

Result:
n m d : ℕ
hm : n ∣ m
hd : m ∣ d
⊢ Units.map ((↑(castHom hm (ZMod n))).comp ↑(castHom hd (ZMod m))) = Units.map ↑(castHom ⋯ (ZMod n))

Proof state:
n m d : ℕ
hm : n ∣ m
hd : m ∣ d
⊢ (unitsMap hm).comp (unitsMap hd) = unitsMap ⋯

Tactic:
simp only [unitsMap_def]

Result:
n m d : ℕ
hm : n ∣ m
hd : m ∣ d
⊢ (Units.map ↑(castHom hm (ZMod n))).comp (Units.map ↑(castHom hd (ZMod m))) = Units.map ↑(castHom ⋯ (ZMod n))

Proof state:
n m d : ℕ
hm : n ∣ m
hd : m ∣ d
⊢ Units.map ((↑(castHom hm (ZMod n))).comp ↑(castHom hd (ZMod m))) = Units.map ↑(castHom ⋯ (ZMod n))

Tactic:
exact congr_arg Units.map <| congr_arg RingHom.toMonoidHom <| castHom_comp hm hd

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
lemma isoSpec_inv_appTop :
    hU.isoSpec.inv.appTop = U.topIso.hom ≫ (Scheme.ΓSpecIso Γ(X, U)).inv

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Scheme.Hom.app (Spec.map (X.presheaf.map (eqToHom ⋯).op)) (inv (↑U).toSpecΓ ⁻¹ᵁ ⊤) =
    Scheme.Hom.appTop (↑U).toSpecΓ ≫
      (Scheme.ΓSpecIso Γ(X, U.ι ''ᵁ ⊤)).inv ≫ Scheme.Hom.appTop (Spec.map (X.presheaf.map (eqToHom ⋯).op))

Tactic:
rw [Scheme.toSpecΓ_appTop]

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Scheme.Hom.app (Spec.map (X.presheaf.map (eqToHom ⋯).op)) (inv (↑U).toSpecΓ ⁻¹ᵁ ⊤) =
    (Scheme.ΓSpecIso Γ(↑U, ⊤)).hom ≫
      (Scheme.ΓSpecIso Γ(X, U.ι ''ᵁ ⊤)).inv ≫ Scheme.Hom.appTop (Spec.map (X.presheaf.map (eqToHom ⋯).op))

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Scheme.Hom.app (Spec.map (X.presheaf.map (eqToHom ⋯).op)) (inv (↑U).toSpecΓ ⁻¹ᵁ ⊤) =
    (Scheme.ΓSpecIso Γ(↑U, ⊤)).hom ≫
      (Scheme.ΓSpecIso Γ(X, U.ι ''ᵁ ⊤)).inv ≫ Scheme.Hom.appTop (Spec.map (X.presheaf.map (eqToHom ⋯).op))

Tactic:
erw [Iso.hom_inv_id_assoc]

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Scheme.Hom.app (Spec.map (X.presheaf.map (eqToHom ⋯).op)) (inv (↑U).toSpecΓ ⁻¹ᵁ ⊤) =
    Scheme.Hom.appTop (Spec.map (X.presheaf.map (eqToHom ⋯).op))

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Scheme.Hom.appTop hU.isoSpec.inv = U.topIso.hom ≫ (Scheme.ΓSpecIso Γ(X, U)).inv

Tactic:
simp_rw [Scheme.Opens.toScheme_presheaf_obj, isoSpec_inv, Scheme.isoSpec, asIso_inv,
  Scheme.comp_app, Scheme.Opens.topIso_hom, Scheme.ΓSpecIso_inv_naturality,
  Scheme.inv_appTop, IsIso.inv_comp_eq]

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Scheme.Hom.app (Spec.map (X.presheaf.map (eqToHom ⋯).op)) (inv (↑U).toSpecΓ ⁻¹ᵁ ⊤) =
    Scheme.Hom.appTop (↑U).toSpecΓ ≫
      (Scheme.ΓSpecIso Γ(X, U.ι ''ᵁ ⊤)).inv ≫ Scheme.Hom.appTop (Spec.map (X.presheaf.map (eqToHom ⋯).op))

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Scheme.Hom.app (Spec.map (X.presheaf.map (eqToHom ⋯).op)) (inv (↑U).toSpecΓ ⁻¹ᵁ ⊤) =
    Scheme.Hom.appTop (Spec.map (X.presheaf.map (eqToHom ⋯).op))

Tactic:
simp only [Opens.map_top]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Operations.lean
theorem card_edgeFinset_eq [Fintype G.edgeSet] [Fintype G'.edgeSet] :
    #G.edgeFinset = #G'.edgeFinset

Proof state:
case i
V : Type u_1
G : SimpleGraph V
W : Type u_2
G' : SimpleGraph W
f : G ≃g G'
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype ↑G'.edgeSet
⊢ { x // x ∈ G.edgeFinset } ≃ { x // x ∈ G'.edgeFinset }

Tactic:
simp only [Set.mem_toFinset]

Result:
case i
V : Type u_1
G : SimpleGraph V
W : Type u_2
G' : SimpleGraph W
f : G ≃g G'
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype ↑G'.edgeSet
⊢ { x // x ∈ G.edgeSet } ≃ { x // x ∈ G'.edgeSet }

Proof state:
case i
V : Type u_1
G : SimpleGraph V
W : Type u_2
G' : SimpleGraph W
f : G ≃g G'
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype ↑G'.edgeSet
⊢ { x // x ∈ G.edgeSet } ≃ { x // x ∈ G'.edgeSet }

Tactic:
exact f.mapEdgeSet

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
W : Type u_2
G' : SimpleGraph W
f : G ≃g G'
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype ↑G'.edgeSet
⊢ #G.edgeFinset = #G'.edgeFinset

Tactic:
apply Finset.card_eq_of_equiv

Result:
case i
V : Type u_1
G : SimpleGraph V
W : Type u_2
G' : SimpleGraph W
f : G ≃g G'
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype ↑G'.edgeSet
⊢ { x // x ∈ G.edgeFinset } ≃ { x // x ∈ G'.edgeFinset }
-- Mathlib/Algebra/Order/Monoid/Unbundled/Defs.lean
theorem covariant_le_of_covariant_lt [PartialOrder N] :
    Covariant M N μ (· < ·) → Covariant M N μ (· ≤ ·)

Proof state:
case inl
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Covariant M N μ fun x1 x2 => x1 < x2
a : M
b : N
bc : b ≤ b
⊢ μ a b ≤ μ a b

Tactic:
exact le_rfl

Result:
no goals

Proof state:
case inr
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Covariant M N μ fun x1 x2 => x1 < x2
a : M
b c : N
bc✝ : b ≤ c
bc : b < c
⊢ μ a b ≤ μ a c

Tactic:
exact (h _ bc).le

Result:
no goals

Proof state:
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Covariant M N μ fun x1 x2 => x1 < x2
a : M
b c : N
bc : b ≤ c
⊢ μ a b ≤ μ a c

Tactic:
rcases bc.eq_or_lt with (rfl | bc)

Result:
case inl
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Covariant M N μ fun x1 x2 => x1 < x2
a : M
b : N
bc : b ≤ b
⊢ μ a b ≤ μ a b

case inr
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Covariant M N μ fun x1 x2 => x1 < x2
a : M
b c : N
bc✝ : b ≤ c
bc : b < c
⊢ μ a b ≤ μ a c

Proof state:
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
⊢ (Covariant M N μ fun x1 x2 => x1 < x2) → Covariant M N μ fun x1 x2 => x1 ≤ x2

Tactic:
intro h a b c bc

Result:
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Covariant M N μ fun x1 x2 => x1 < x2
a : M
b c : N
bc : b ≤ c
⊢ μ a b ≤ μ a c
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_comp (g f : R → R) (a : A) (ha : p a

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : UniqueHom R A
g f : R → R
a : A
ha : autoParam (p a) _auto✝
hg : autoParam (ContinuousOn g (f '' spectrum R a)) _auto✝
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
⊢ cfc (g ∘ f) a = cfc g (cfc f a)

Tactic:
have := hg.comp hf <| (spectrum R a).mapsTo_image f

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : UniqueHom R A
g f : R → R
a : A
ha : autoParam (p a) _auto✝
hg : autoParam (ContinuousOn g (f '' spectrum R a)) _auto✝
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
this : ContinuousOn (g ∘ f) (spectrum R a)
⊢ cfc (g ∘ f) a = cfc g (cfc f a)