harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/ENNReal/Inv.lean
/-- See `ENNReal.mul_inv_cancel_left` for a simpler version assuming `a ≠ 0`, `a ≠ ∞`. -/
protected lemma mul_inv_cancel_left' (ha₀ : a = 0 → b = 0) (ha : a = ∞ → b = 0) :
    a * (a⁻¹ * b) = b

Proof state:
case inr.inr
a b : ℝ≥0∞
ha₀✝ : a = 0 → b = 0
ha✝ : a = ⊤ → b = 0
ha₀ : a ≠ 0
ha : a ≠ ⊤
⊢ a * (a⁻¹ * b) = b

Tactic:
simp [← mul_assoc, ENNReal.mul_inv_cancel, *]

Result:
no goals

Proof state:
case inr
a b : ℝ≥0∞
ha₀✝ : a = 0 → b = 0
ha : a = ⊤ → b = 0
ha₀ : a ≠ 0
⊢ a * (a⁻¹ * b) = b

Tactic:
obtain rfl | ha := eq_or_ne a ⊤

Result:
case inr.inl
b : ℝ≥0∞
ha₀✝ : ⊤ = 0 → b = 0
ha : ⊤ = ⊤ → b = 0
ha₀ : ⊤ ≠ 0
⊢ ⊤ * (⊤⁻¹ * b) = b

case inr.inr
a b : ℝ≥0∞
ha₀✝ : a = 0 → b = 0
ha✝ : a = ⊤ → b = 0
ha₀ : a ≠ 0
ha : a ≠ ⊤
⊢ a * (a⁻¹ * b) = b

Proof state:
case inr.inl
b : ℝ≥0∞
ha₀✝ : ⊤ = 0 → b = 0
ha : ⊤ = ⊤ → b = 0
ha₀ : ⊤ ≠ 0
⊢ ⊤ * (⊤⁻¹ * b) = b

Tactic:
simp_all

Result:
no goals

Proof state:
a b : ℝ≥0∞
ha₀ : a = 0 → b = 0
ha : a = ⊤ → b = 0
⊢ a * (a⁻¹ * b) = b

Tactic:
obtain rfl | ha₀ := eq_or_ne a 0

Result:
case inl
b : ℝ≥0∞
ha₀ : 0 = 0 → b = 0
ha : 0 = ⊤ → b = 0
⊢ 0 * (0⁻¹ * b) = b

case inr
a b : ℝ≥0∞
ha₀✝ : a = 0 → b = 0
ha : a = ⊤ → b = 0
ha₀ : a ≠ 0
⊢ a * (a⁻¹ * b) = b

Proof state:
case inl
b : ℝ≥0∞
ha₀ : 0 = 0 → b = 0
ha : 0 = ⊤ → b = 0
⊢ 0 * (0⁻¹ * b) = b

Tactic:
simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_set (a : Array α) (i : Nat) (h : i < a.size) (v : α) (j : Nat) :
    (a.set i v)[j]? = if i = j then some v else a[j]?

Proof state:
α : Type u_1
a : Array α
i : Nat
h : i < a.size
v : α
j : Nat
⊢ (a.set i v h)[j]? = if i = j then some v else a[j]?

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean
theorem wEquiv.symm {α : TypeVec n} (x y : q.P.W α) : WEquiv x y → WEquiv y x

Proof state:
case trans
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ y✝ x y z : (P F).W α
_e₁ : WEquiv x y
_e₂ : WEquiv y z
ih₁ : WEquiv y x
ih₂ : WEquiv z y
⊢ WEquiv z x

Tactic:
exact MvQPF.WEquiv.trans _ _ _ ih₂ ih₁

Result:
no goals

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : (P F).W α
⊢ WEquiv x y → WEquiv y x

Tactic:
intro h

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : (P F).W α
h : WEquiv x y
⊢ WEquiv y x

Proof state:
case abs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : (P F).W α
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁ : (P F).last.B a₁ → (P F).W α
h : abs ⟨a₀, (P F).appendContents f'₀ f₀⟩ = abs ⟨a₁, (P F).appendContents f'₁ f₁⟩
⊢ WEquiv ((P F).wMk a₁ f'₁ f₁) ((P F).wMk a₀ f'₀ f₀)

Tactic:
exact WEquiv.abs _ _ _ _ _ _ h.symm

Result:
no goals

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : (P F).W α
h : WEquiv x y
⊢ WEquiv y x

Tactic:
induction h with
| ind a f' f₀ f₁ _h ih => exact WEquiv.ind _ _ _ _ ih
| abs a₀ f'₀ f₀ a₁ f'₁ f₁ h => exact WEquiv.abs _ _ _ _ _ _ h.symm
| trans x y z _e₁ _e₂ ih₁ ih₂ => exact MvQPF.WEquiv.trans _ _ _ ih₂ ih₁

Result:
no goals

Proof state:
case ind
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : (P F).W α
a : (P F).A
f' : (P F).drop.B a ⟹ α
f₀ f₁ : (P F).last.B a → (P F).W α
_h : ∀ (x : (P F).last.B a), WEquiv (f₀ x) (f₁ x)
ih : ∀ (x : (P F).last.B a), WEquiv (f₁ x) (f₀ x)
⊢ WEquiv ((P F).wMk a f' f₁) ((P F).wMk a f' f₀)

Tactic:
exact WEquiv.ind _ _ _ _ ih

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem edist_self (f : PiLp p β) : edist f f = 0

Proof state:
case inl
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f : PiLp 0 β
⊢ edist f f = 0

Tactic:
simp [edist_eq_card]

Result:
no goals

Proof state:
case inr.inl
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f : PiLp ⊤ β
⊢ edist f f = 0

Tactic:
simp [edist_eq_iSup]

Result:
no goals

Proof state:
case inr.inr
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f : PiLp p β
h : 0 < p.toReal
⊢ edist f f = 0

Tactic:
simp [edist_eq_sum h, ENNReal.zero_rpow_of_pos h, ENNReal.zero_rpow_of_pos (inv_pos.2 <| h)]

Result:
no goals

Proof state:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f : PiLp p β
⊢ edist f f = 0

Tactic:
rcases p.trichotomy with (rfl | rfl | h)

Result:
case inl
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f : PiLp 0 β
⊢ edist f f = 0

case inr.inl
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f : PiLp ⊤ β
⊢ edist f f = 0

case inr.inr
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f : PiLp p β
h : 0 < p.toReal
⊢ edist f f = 0
-- Mathlib/Data/Multiset/Pi.lean
theorem cons_injective {a : α} {b : δ a} {s : Multiset α} (hs : a ∉ s) :
    Function.Injective (Pi.cons s a b) := fun f₁ f₂ eq =>
  funext fun a' =>
    funext fun h' =>
      have ne : a ≠ a' := fun h => hs <| h.symm ▸ h'
      have : a' ∈ a ::ₘ s := mem_cons_of_mem h'
      calc
        f₁ a' h' = Pi.cons s a b f₁ a' this

Proof state:
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a : α
b : δ a
s : Multiset α
hs : a ∉ s
f₁ f₂ : (a : α) → a ∈ s → δ a
eq : cons s a b f₁ = cons s a b f₂
a' : α
h' : a' ∈ s
ne : a ≠ a'
this : a' ∈ a ::ₘ s
⊢ f₁ a' h' = cons s a b f₁ a' this

Tactic:
rw [Pi.cons_ne this ne.symm]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a : α
b : δ a
s : Multiset α
hs : a ∉ s
f₁ f₂ : (a : α) → a ∈ s → δ a
eq : cons s a b f₁ = cons s a b f₂
a' : α
h' : a' ∈ s
ne : a ≠ a'
this : a' ∈ a ::ₘ s
⊢ cons s a b f₂ a' this = f₂ a' h'

Tactic:
rw [Pi.cons_ne this ne.symm]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a : α
b : δ a
s : Multiset α
hs : a ∉ s
f₁ f₂ : (a : α) → a ∈ s → δ a
eq : cons s a b f₁ = cons s a b f₂
a' : α
h' : a' ∈ s
ne : a ≠ a'
this : a' ∈ a ::ₘ s
⊢ cons s a b f₁ a' this = cons s a b f₂ a' this

Tactic:
rw [eq]

Result:
no goals
-- Mathlib/Order/JordanHolder.lean
theorem total {s : CompositionSeries X} {x y : X} (hx : x ∈ s) (hy : y ∈ s) : x ≤ y ∨ y ≤ x

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x y : X
hx : x ∈ s
hy : y ∈ s
⊢ x ≤ y ∨ y ≤ x

Tactic:
rcases Set.mem_range.1 hx with ⟨i, rfl⟩

Result:
case intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
y : X
hy : y ∈ s
i : Fin (s.length + 1)
hx : s.toFun i ∈ s
⊢ s.toFun i ≤ y ∨ y ≤ s.toFun i

Proof state:
case intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
y : X
hy : y ∈ s
i : Fin (s.length + 1)
hx : s.toFun i ∈ s
⊢ s.toFun i ≤ y ∨ y ≤ s.toFun i

Tactic:
rcases Set.mem_range.1 hy with ⟨j, rfl⟩

Result:
case intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : s.toFun i ∈ s
j : Fin (s.length + 1)
hy : s.toFun j ∈ s
⊢ s.toFun i ≤ s.toFun j ∨ s.toFun j ≤ s.toFun i

Proof state:
case intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : s.toFun i ∈ s
j : Fin (s.length + 1)
hy : s.toFun j ∈ s
⊢ s.toFun i ≤ s.toFun j ∨ s.toFun j ≤ s.toFun i

Tactic:
rw [s.strictMono.le_iff_le, s.strictMono.le_iff_le]

Result:
case intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : s.toFun i ∈ s
j : Fin (s.length + 1)
hy : s.toFun j ∈ s
⊢ i ≤ j ∨ j ≤ i

Proof state:
case intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : s.toFun i ∈ s
j : Fin (s.length + 1)
hy : s.toFun j ∈ s
⊢ i ≤ j ∨ j ≤ i

Tactic:
exact le_total i j

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
lemma isoSpec_inv_image_zeroLocus [IsAffine X] (s : Set Γ(X, ⊤)) :
    X.isoSpec.inv.base '' PrimeSpectrum.zeroLocus s = X.zeroLocus s

Proof state:
X : Scheme
inst✝ : IsAffine X
s : Set ↑Γ(X, ⊤)
⊢ ⇑(hom X.isoSpec.inv.base) '' PrimeSpectrum.zeroLocus s = X.zeroLocus s

Tactic:
rw [← isoSpec_inv_preimage_zeroLocus, Set.image_preimage_eq]

Result:
case h
X : Scheme
inst✝ : IsAffine X
s : Set ↑Γ(X, ⊤)
⊢ Function.Surjective ⇑(hom X.isoSpec.inv.base)

Proof state:
case h
X : Scheme
inst✝ : IsAffine X
s : Set ↑Γ(X, ⊤)
⊢ Function.Surjective ⇑(hom X.isoSpec.inv.base)

Tactic:
exact (bijective_of_isIso X.isoSpec.inv.base).surjective

Result:
no goals
-- Mathlib/FieldTheory/Finite/Basic.lean
theorem pow_card_sub_one_eq_one {p : ℕ} [Fact p.Prime] {a : ZMod p} (ha : a ≠ 0) :
    a ^ (p - 1) = 1

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ a ^ (p - 1) = 1

Tactic:
have h := FiniteField.pow_card_sub_one_eq_one a ha

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
h : a ^ (Fintype.card (ZMod p) - 1) = 1
⊢ a ^ (p - 1) = 1

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
h : a ^ (Fintype.card (ZMod p) - 1) = 1
⊢ a ^ (p - 1) = 1

Tactic:
rwa [ZMod.card p] at h

Result:
no goals
-- Mathlib/CategoryTheory/Limits/IsLimit.lean
theorem cocone_fac (s : Cocone F) : (colimitCocone h).extend (homOfCocone h s) = s

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones
s : Cocone F
⊢ (colimitCocone h).extend (homOfCocone h s) = s

Tactic:
rw [← coconeOfHom_homOfCocone h s]

Result:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones
s : Cocone F
⊢ (colimitCocone h).extend (homOfCocone h (coconeOfHom h (homOfCocone h s))) = coconeOfHom h (homOfCocone h s)

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones
s : Cocone F
⊢ (colimitCocone h).extend (homOfCocone h (coconeOfHom h (homOfCocone h s))) = coconeOfHom h (homOfCocone h s)

Tactic:
conv_lhs => simp only [homOfCocone_cooneOfHom]

Result:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones
s : Cocone F
⊢ (colimitCocone h).extend (homOfCocone h s) = coconeOfHom h (homOfCocone h s)

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones
s : Cocone F
⊢ (colimitCocone h).extend (homOfCocone h s) = coconeOfHom h (homOfCocone h s)

Tactic:
apply (coconeOfHom_fac _ _).symm

Result:
no goals
-- Mathlib/Data/Finite/Card.lean
theorem Nat.card_eq (α : Type*) :
    Nat.card α = if _ : Finite α then @Fintype.card α (Fintype.ofFinite α) else 0

Proof state:
case inl
α : Type u_4
h✝ : Finite α
⊢ Nat.card α = if x : Finite α then Fintype.card α else 0

Tactic:
letI := Fintype.ofFinite α

Result:
case inl
α : Type u_4
h✝ : Finite α
this : Fintype α := Fintype.ofFinite α
⊢ Nat.card α = if x : Finite α then Fintype.card α else 0

Proof state:
case inl
α : Type u_4
h✝ : Finite α
this : Fintype α := Fintype.ofFinite α
⊢ Nat.card α = if x : Finite α then Fintype.card α else 0

Tactic:
simp only [this, *, Nat.card_eq_fintype_card, dif_pos]

Result:
no goals

Proof state:
case inr
α : Type u_4
h✝ : Infinite α
⊢ Nat.card α = if x : Finite α then Fintype.card α else 0

Tactic:
simp only [*, card_eq_zero_of_infinite, not_finite_iff_infinite.mpr, dite_false]

Result:
no goals

Proof state:
α : Type u_4
⊢ Nat.card α = if x : Finite α then Fintype.card α else 0

Tactic:
cases finite_or_infinite α

Result:
case inl
α : Type u_4
h✝ : Finite α
⊢ Nat.card α = if x : Finite α then Fintype.card α else 0

case inr
α : Type u_4
h✝ : Infinite α
⊢ Nat.card α = if x : Finite α then Fintype.card α else 0
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_pos_of_nonneg {p : ℝ} {x : ℝ≥0∞} (hx_pos : 0 < x) (hp_nonneg : 0 ≤ p) : 0 < x ^ p

Proof state:
case neg
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p ≠ 0
⊢ 0 < x ^ p

Tactic:
have hp_pos := lt_of_le_of_ne hp_nonneg hp_zero.symm

Result:
case neg
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p ≠ 0
hp_pos : 0 < p
⊢ 0 < x ^ p

Proof state:
case neg
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : ¬p = 0
⊢ 0 < x ^ p

Tactic:
rw [← Ne] at hp_zero

Result:
case neg
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p ≠ 0
⊢ 0 < x ^ p

Proof state:
case pos
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p = 0
⊢ 0 < x ^ p

Tactic:
simp [hp_zero, zero_lt_one]

Result:
no goals

Proof state:
case neg
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p ≠ 0
hp_pos : 0 < p
⊢ 0 ^ p < x ^ p

Tactic:
exact rpow_lt_rpow hx_pos hp_pos

Result:
no goals

Proof state:
case neg
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p ≠ 0
hp_pos : 0 < p
⊢ 0 < x ^ p

Tactic:
rw [← zero_rpow_of_pos hp_pos]

Result:
case neg
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p ≠ 0
hp_pos : 0 < p
⊢ 0 ^ p < x ^ p

Proof state:
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
⊢ 0 < x ^ p

Tactic:
by_cases hp_zero : p = 0

Result:
case pos
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p = 0
⊢ 0 < x ^ p

case neg
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : ¬p = 0
⊢ 0 < x ^ p
-- Mathlib/Data/Matroid/Circuit.lean
lemma fundCircuit_diff_eq_inter (M : Matroid α) (heI : e ∉ I) :
    (M.fundCircuit e I) \ {e} = (M.fundCircuit e I) ∩ I :=
  (subset_inter diff_subset (by simp [fundCircuit_subset_insert])).antisymm
    (subset_diff_singleton inter_subset_left (by simp [heI]))

Proof state:
α : Type u_1
I : Set α
e : α
M : Matroid α
heI : e ∉ I
⊢ M.fundCircuit e I \ {e} ⊆ I

Tactic:
simp [fundCircuit_subset_insert]

Result:
no goals

Proof state:
α : Type u_1
I : Set α
e : α
M : Matroid α
heI : e ∉ I
⊢ e ∉ M.fundCircuit e I ∩ I

Tactic:
simp [heI]

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem nndist_eq_of_L1 (x y : PiLp 1 β) : nndist x y = ∑ i, nndist (x i) (y i) :=
  NNReal.eq <| by push_cast; exact dist_eq_of_L1 _ _

Proof state:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 1 β
⊢ ↑(nndist x y) = ↑(∑ i : ι, nndist (x i) (y i))

Tactic:
push_cast

Result:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 1 β
⊢ dist x y = ∑ x_1 : ι, dist (x x_1) (y x_1)

Proof state:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 1 β
⊢ dist x y = ∑ x_1 : ι, dist (x x_1) (y x_1)

Tactic:
exact dist_eq_of_L1 _ _

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem image {q : ℚ_[p]} : q ≠ 0 → ∃ n : ℤ, ‖q‖ = ↑((p : ℚ) ^ (-n)) :=
  Quotient.inductionOn q fun f hf ↦
    have : ¬f ≈ 0 := (PadicSeq.ne_zero_iff_nequiv_zero f).1 hf
    let ⟨n, hn⟩ := PadicSeq.norm_values_discrete f this
    ⟨n, by rw [← hn]; rfl⟩

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ_[p]
f : CauSeq ℚ (padicNorm p)
hf : ⟦f⟧ ≠ 0
this : ¬f ≈ 0
n : ℤ
hn : PadicSeq.norm f = ↑p ^ (-n)
⊢ ‖⟦f⟧‖ = ↑(↑p ^ (-n))

Tactic:
rw [← hn]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ_[p]
f : CauSeq ℚ (padicNorm p)
hf : ⟦f⟧ ≠ 0
this : ¬f ≈ 0
n : ℤ
hn : PadicSeq.norm f = ↑p ^ (-n)
⊢ ‖⟦f⟧‖ = ↑(PadicSeq.norm f)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ_[p]
f : CauSeq ℚ (padicNorm p)
hf : ⟦f⟧ ≠ 0
this : ¬f ≈ 0
n : ℤ
hn : PadicSeq.norm f = ↑p ^ (-n)
⊢ ‖⟦f⟧‖ = ↑(PadicSeq.norm f)

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfcUnits_pow (hf' : ∀ x ∈ spectrum R a, f x ≠ 0) (n : ℕ)
    (hf : ContinuousOn f (spectrum R a)

Proof state:
case a.succ
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁰ : Semifield 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
inst✝¹ : ContinuousFunctionalCalculus R p
inst✝ : HasContinuousInv₀ R
f : R → R
a : A
hf' : ∀ x ∈ spectrum R a, f x ≠ 0
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
n : ℕ
⊢ ↑(cfcUnits f a hf' hf ha ^ (n + 1)) = ↑(cfcUnits (fun x => f x ^ (n + 1)) a ⋯ ⋯ ha)

Tactic:
simp [cfc_pow f _ a]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁰ : Semifield 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
inst✝¹ : ContinuousFunctionalCalculus R p
inst✝ : HasContinuousInv₀ R
f : R → R
a : A
hf' : ∀ x ∈ spectrum R a, f x ≠ 0
n : ℕ
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ cfcUnits f a hf' hf ha ^ n = cfcUnits (fun x => f x ^ n) a ⋯ ⋯ ha

Tactic:
ext

Result:
case a
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁰ : Semifield 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
inst✝¹ : ContinuousFunctionalCalculus R p
inst✝ : HasContinuousInv₀ R
f : R → R
a : A
hf' : ∀ x ∈ spectrum R a, f x ≠ 0
n : ℕ
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ ↑(cfcUnits f a hf' hf ha ^ n) = ↑(cfcUnits (fun x => f x ^ n) a ⋯ ⋯ ha)

Proof state:
case a.zero
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁰ : Semifield 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
inst✝¹ : ContinuousFunctionalCalculus R p
inst✝ : HasContinuousInv₀ R
f : R → R
a : A
hf' : ∀ x ∈ spectrum R a, f x ≠ 0
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ ↑(cfcUnits f a hf' hf ha ^ 0) = ↑(cfcUnits (fun x => f x ^ 0) a ⋯ ⋯ ha)

Tactic:
simp [cfc_const_one R a]

Result:
no goals

Proof state:
case a
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁰ : Semifield 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
inst✝¹ : ContinuousFunctionalCalculus R p
inst✝ : HasContinuousInv₀ R
f : R → R
a : A
hf' : ∀ x ∈ spectrum R a, f x ≠ 0
n : ℕ
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ ↑(cfcUnits f a hf' hf ha ^ n) = ↑(cfcUnits (fun x => f x ^ n) a ⋯ ⋯ ha)

Tactic:
cases n with
| zero => simp [cfc_const_one R a]
| succ n => simp [cfc_pow f _ a]

Result:
no goals
-- Mathlib/CategoryTheory/EqToHom.lean
theorem eqToHom_app {F G : C ⥤ D} (h : F = G) (X : C) :
    (eqToHom h : F ⟶ G).app X = eqToHom (Functor.congr_obj h X)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
⊢ (eqToHom ⋯).app X = eqToHom ⋯

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
h : F = G
X : C
⊢ (eqToHom h).app X = eqToHom ⋯

Tactic:
subst h

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
⊢ (eqToHom ⋯).app X = eqToHom ⋯
-- Mathlib/Data/Matroid/Rank/Finite.lean
lemma IsRkFinite.union (hX : M.IsRkFinite X) (hY : M.IsRkFinite Y) : M.IsRkFinite (X ∪ Y)

Proof state:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hY : M.IsRkFinite Y
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
J : Set α
hJ : M.IsBasis' J Y
hJfin : J.Finite
⊢ (X ∪ Y) ∩ M.E ⊆ M.closure (I ∪ J)

Tactic:
rw [closure_union_congr_left hI.closure_eq_closure,
  closure_union_congr_right hJ.closure_eq_closure]

Result:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hY : M.IsRkFinite Y
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
J : Set α
hJ : M.IsBasis' J Y
hJfin : J.Finite
⊢ (X ∪ Y) ∩ M.E ⊆ M.closure (X ∪ Y)

Proof state:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hY : M.IsRkFinite Y
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
J : Set α
hJ : M.IsBasis' J Y
hJfin : J.Finite
⊢ M.IsRkFinite ((X ∪ Y) ∩ M.E)

Tactic:
refine (M.isRkFinite_of_finite (hIfin.union hJfin)).closure.subset ?_

Result:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hY : M.IsRkFinite Y
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
J : Set α
hJ : M.IsBasis' J Y
hJfin : J.Finite
⊢ (X ∪ Y) ∩ M.E ⊆ M.closure (I ∪ J)

Proof state:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hY : M.IsRkFinite Y
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
J : Set α
hJ : M.IsBasis' J Y
hJfin : J.Finite
⊢ (X ∪ Y) ∩ M.E ⊆ M.closure (X ∪ Y)

Tactic:
exact inter_ground_subset_closure M (X ∪ Y)

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hY : M.IsRkFinite Y
⊢ M.IsRkFinite (X ∪ Y)

Tactic:
obtain ⟨I, hI, hIfin⟩ := hX.exists_finite_isBasis'

Result:
case intro.intro
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hY : M.IsRkFinite Y
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
⊢ M.IsRkFinite (X ∪ Y)

Proof state:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hY : M.IsRkFinite Y
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
J : Set α
hJ : M.IsBasis' J Y
hJfin : J.Finite
⊢ M.IsRkFinite (X ∪ Y)

Tactic:
rw [← isRkFinite_inter_ground_iff]

Result:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hY : M.IsRkFinite Y
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
J : Set α
hJ : M.IsBasis' J Y
hJfin : J.Finite
⊢ M.IsRkFinite ((X ∪ Y) ∩ M.E)

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hY : M.IsRkFinite Y
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
⊢ M.IsRkFinite (X ∪ Y)

Tactic:
obtain ⟨J, hJ, hJfin⟩ := hY.exists_finite_isBasis'

Result:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hY : M.IsRkFinite Y
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
J : Set α
hJ : M.IsBasis' J Y
hJfin : J.Finite
⊢ M.IsRkFinite (X ∪ Y)