harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc]
lemma LeftHomologyData.leftHomologyIso_inv_naturality
    (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) :
    h₁.homologyIso.inv ≫ homologyMap φ =
      leftHomologyMap' φ h₁ h₂ ≫ h₂.homologyIso.inv

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ h₁.homologyIso.inv ≫ homologyMap φ = leftHomologyMap' φ h₁ h₂ ≫ h₂.homologyIso.inv

Tactic:
dsimp [homologyIso, ShortComplex.leftHomologyIso, homologyMap, homologyMap', leftHomologyIso]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ (leftHomologyMap' (𝟙 S₁) h₁ S₁.leftHomologyData ≫ leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData S₁.homologyData.left) ≫
      leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left =
    leftHomologyMap' φ h₁ h₂ ≫
      leftHomologyMap' (𝟙 S₂) h₂ S₂.leftHomologyData ≫ leftHomologyMap' (𝟙 S₂) S₂.leftHomologyData S₂.homologyData.left

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ (leftHomologyMap' (𝟙 S₁) h₁ S₁.leftHomologyData ≫ leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData S₁.homologyData.left) ≫
      leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left =
    leftHomologyMap' φ h₁ h₂ ≫
      leftHomologyMap' (𝟙 S₂) h₂ S₂.leftHomologyData ≫ leftHomologyMap' (𝟙 S₂) S₂.leftHomologyData S₂.homologyData.left

Tactic:
simp only [← leftHomologyMap'_comp, id_comp, comp_id]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Finite.lean
theorem support_pow_coprime {σ : Perm α} {n : ℕ} (h : Nat.Coprime n (orderOf σ)) :
    (σ ^ n).support = σ.support

Proof state:
case intro
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
n : ℕ
h : n.Coprime (orderOf σ)
m : ℕ
hm : (σ ^ n) ^ m = σ
⊢ (σ ^ n).support = σ.support

Tactic:
exact
  le_antisymm (support_pow_le σ n)
    (le_trans (ge_of_eq (congr_arg support hm)) (support_pow_le (σ ^ n) m))

Result:
no goals

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
n : ℕ
h : n.Coprime (orderOf σ)
⊢ (σ ^ n).support = σ.support

Tactic:
obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime h

Result:
case intro
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
n : ℕ
h : n.Coprime (orderOf σ)
m : ℕ
hm : (σ ^ n) ^ m = σ
⊢ (σ ^ n).support = σ.support
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Lp.lean
theorem MemLp.finStronglyMeasurable_of_stronglyMeasurable (hf : MemLp f p μ)
    (hf_meas : StronglyMeasurable f) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞) :
    FinStronglyMeasurable f μ

Proof state:
case refine_2.hx
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : MemLp f p μ
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(Set.range f ∪ {0})
fs : ℕ → α →ₛ G := SimpleFunc.approxOn f ⋯ (Set.range f ∪ {0}) 0 ⋯
x : α
⊢ f x ∈ closure (Set.range f ∪ {0})

Tactic:
apply subset_closure

Result:
case refine_2.hx.a
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : MemLp f p μ
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(Set.range f ∪ {0})
fs : ℕ → α →ₛ G := SimpleFunc.approxOn f ⋯ (Set.range f ∪ {0}) 0 ⋯
x : α
⊢ f x ∈ Set.range f ∪ {0}

Proof state:
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : MemLp f p μ
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
⊢ FinStronglyMeasurable f μ

Tactic:
borelize G

Result:
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : MemLp f p μ
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
⊢ FinStronglyMeasurable f μ
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
/-- See `Finset.card_pow_mono` for a version that works for the empty set. -/
@[to_additive "See `Finset.card_nsmul_mono` for a version that works for the empty set."]
protected lemma Nonempty.card_pow_mono (hs : s.Nonempty) : Monotone fun n : ℕ ↦ (s ^ n).card :=
  monotone_nat_of_le_succ fun n ↦ by rw [pow_succ]; exact card_le_card_mul_right hs

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelMonoid α
s : Finset α
hs : s.Nonempty
n : ℕ
⊢ #(s ^ n) ≤ #(s ^ (n + 1))

Tactic:
rw [pow_succ]

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelMonoid α
s : Finset α
hs : s.Nonempty
n : ℕ
⊢ #(s ^ n) ≤ #(s ^ n * s)

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelMonoid α
s : Finset α
hs : s.Nonempty
n : ℕ
⊢ #(s ^ n) ≤ #(s ^ n * s)

Tactic:
exact card_le_card_mul_right hs

Result:
no goals
-- Mathlib/Topology/PartitionOfUnity.lean
theorem finsupport_subset_fintsupport : ρ.finsupport x₀ ⊆ ρ.fintsupport x₀ := fun i hi ↦ by
  rw [ρ.mem_fintsupport_iff]
  apply subset_closure
  exact (ρ.mem_finsupport x₀).mp hi

Proof state:
case a
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
i : ι
hi : i ∈ ρ.finsupport x₀
⊢ x₀ ∈ support ⇑(ρ i)

Tactic:
exact (ρ.mem_finsupport x₀).mp hi

Result:
no goals

Proof state:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
i : ι
hi : i ∈ ρ.finsupport x₀
⊢ x₀ ∈ tsupport ⇑(ρ i)

Tactic:
apply subset_closure

Result:
case a
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
i : ι
hi : i ∈ ρ.finsupport x₀
⊢ x₀ ∈ support ⇑(ρ i)

Proof state:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
i : ι
hi : i ∈ ρ.finsupport x₀
⊢ i ∈ ρ.fintsupport x₀

Tactic:
rw [ρ.mem_fintsupport_iff]

Result:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
i : ι
hi : i ∈ ρ.finsupport x₀
⊢ x₀ ∈ tsupport ⇑(ρ i)
-- Mathlib/Data/Set/Lattice.lean
theorem iUnion_setOf (P : ι → α → Prop) : ⋃ i, { x : α | P i x } = { x : α | ∃ i, P i x }

Proof state:
α : Type u_1
ι : Sort u_5
P : ι → α → Prop
⊢ ⋃ i, {x | P i x} = {x | ∃ i, P i x}

Tactic:
ext

Result:
case h
α : Type u_1
ι : Sort u_5
P : ι → α → Prop
x✝ : α
⊢ x✝ ∈ ⋃ i, {x | P i x} ↔ x✝ ∈ {x | ∃ i, P i x}

Proof state:
case h
α : Type u_1
ι : Sort u_5
P : ι → α → Prop
x✝ : α
⊢ x✝ ∈ ⋃ i, {x | P i x} ↔ x✝ ∈ {x | ∃ i, P i x}

Tactic:
exact mem_iUnion

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem Basis.parallelepiped_eq_map  {ι E : Type*} [Fintype ι] [NormedAddCommGroup E]
    [NormedSpace ℝ E] (b : Basis ι ℝ E) :
    b.parallelepiped = (PositiveCompacts.piIcc01 ι).map b.equivFun.symm
      b.equivFunL.symm.continuous b.equivFunL.symm.isOpenMap

Proof state:
ι : Type u_1
E : Type u_2
inst✝² : Fintype ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : Basis ι ℝ E
⊢ b.parallelepiped = PositiveCompacts.map ⇑b.equivFun.symm ⋯ ⋯ (PositiveCompacts.piIcc01 ι)

Tactic:
classical
rw [← Basis.parallelepiped_basisFun, ← Basis.parallelepiped_map]
congr with x
simp [Pi.single_apply]

Result:
no goals

Proof state:
ι : Type u_1
E : Type u_2
inst✝² : Fintype ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : Basis ι ℝ E
⊢ b.parallelepiped = PositiveCompacts.map ⇑b.equivFun.symm ⋯ ⋯ (PositiveCompacts.piIcc01 ι)

Tactic:
rw [← Basis.parallelepiped_basisFun, ← Basis.parallelepiped_map]

Result:
ι : Type u_1
E : Type u_2
inst✝² : Fintype ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : Basis ι ℝ E
⊢ b.parallelepiped = ((Pi.basisFun ℝ ι).map b.equivFun.symm).parallelepiped

Proof state:
ι : Type u_1
E : Type u_2
inst✝² : Fintype ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : Basis ι ℝ E
⊢ b.parallelepiped = ((Pi.basisFun ℝ ι).map b.equivFun.symm).parallelepiped

Tactic:
congr with x

Result:
case e_b.a
ι : Type u_1
E : Type u_2
inst✝² : Fintype ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : Basis ι ℝ E
x : ι
⊢ b x = ((Pi.basisFun ℝ ι).map b.equivFun.symm) x

Proof state:
case e_b.a
ι : Type u_1
E : Type u_2
inst✝² : Fintype ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : Basis ι ℝ E
x : ι
⊢ b x = ((Pi.basisFun ℝ ι).map b.equivFun.symm) x

Tactic:
simp [Pi.single_apply]

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem mk_of_lt (ζ : M) (hk : 0 < k) (h1 : ζ ^ k = 1) (h : ∀ l : ℕ, 0 < l → l < k → ζ ^ l ≠ 1) :
    IsPrimitiveRoot ζ k

Proof state:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
⊢ IsPrimitiveRoot ζ k

Tactic:
refine ⟨h1, fun l hl ↦ ?_⟩

Result:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
⊢ k ∣ l

Proof state:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
⊢ ¬k.gcd l < k

Tactic:
intro h'

Result:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
h' : k.gcd l < k
⊢ False

Proof state:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
⊢ k ∣ l

Tactic:
suffices k.gcd l = k by exact this ▸ k.gcd_dvd_right l

Result:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
⊢ k.gcd l = k

Proof state:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
h' : k.gcd l < k
⊢ ζ ^ k.gcd l = 1

Tactic:
exact pow_gcd_eq_one _ h1 hl

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
⊢ k.gcd l ≤ k ∧ ¬k.gcd l < k

Tactic:
refine ⟨Nat.le_of_dvd hk (k.gcd_dvd_left l), ?_⟩

Result:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
⊢ ¬k.gcd l < k

Proof state:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
h' : k.gcd l < k
⊢ False

Tactic:
apply h _ (Nat.gcd_pos_of_pos_left _ hk) h'

Result:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
h' : k.gcd l < k
⊢ ζ ^ k.gcd l = 1

Proof state:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
this : k.gcd l = k
⊢ k ∣ l

Tactic:
exact this ▸ k.gcd_dvd_right l

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
⊢ k.gcd l = k

Tactic:
rw [eq_iff_le_not_lt]

Result:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h1 : ζ ^ k = 1
h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
l : ℕ
hl : ζ ^ l = 1
⊢ k.gcd l ≤ k ∧ ¬k.gcd l < k
-- Mathlib/RingTheory/Binomial.lean
theorem multichoose_zero_right [MulOneClass R] [NatPowAssoc R]
    (r : R) : multichoose r 0 = 1

Proof state:
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : Pow R ℕ
inst✝² : BinomialRing R
inst✝¹ : MulOneClass R
inst✝ : NatPowAssoc R
r : R
⊢ multichoose r 0 = 1

Tactic:
rw [multichoose_zero_right', npow_zero]

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem IsBoundedUnder.bddAbove_range [Preorder β] [IsDirected β (· ≤ ·)] {f : ℕ → β}
    (hf : IsBoundedUnder (· ≤ ·) atTop f) : BddAbove (range f)

Proof state:
β : Type u_2
inst✝¹ : Preorder β
inst✝ : IsDirected β fun x1 x2 => x1 ≤ x2
f : ℕ → β
hf : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) cofinite f
⊢ BddAbove (range f)

Tactic:
exact hf.bddAbove_range_of_cofinite

Result:
no goals

Proof state:
β : Type u_2
inst✝¹ : Preorder β
inst✝ : IsDirected β fun x1 x2 => x1 ≤ x2
f : ℕ → β
hf : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) atTop f
⊢ BddAbove (range f)

Tactic:
rw [← Nat.cofinite_eq_atTop] at hf

Result:
β : Type u_2
inst✝¹ : Preorder β
inst✝ : IsDirected β fun x1 x2 => x1 ≤ x2
f : ℕ → β
hf : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) cofinite f
⊢ BddAbove (range f)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Basic.lean
theorem map_congr [Functor m] {x : m α} {f g : α → β} (h : ∀ a, f a = g a) : (f <$> x : m β) = g <$> x

Proof state:
m : Type u_1 → Type u_2
α β : Type u_1
inst✝ : Functor m
x : m α
f g : α → β
h : ∀ (a : α), f a = g a
⊢ f <$> x = g <$> x

Tactic:
simp [funext h]

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem intCast_dvd_intCast (a b : ℤ) : (a : ℤ√d) ∣ b ↔ a ∣ b

Proof state:
case mp
d a b : ℤ
⊢ a ∣ (↑b).re ∧ a ∣ (↑b).im → a ∣ b

Tactic:
rintro ⟨hre, -⟩

Result:
case mp.intro
d a b : ℤ
hre : a ∣ (↑b).re
⊢ a ∣ b

Proof state:
case mpr
d a b : ℤ
⊢ a ∣ b → a ∣ b ∧ a ∣ 0

Tactic:
exact fun hc => ⟨hc, dvd_zero a⟩

Result:
no goals

Proof state:
case mp.intro
d a b : ℤ
hre : a ∣ (↑b).re
⊢ a ∣ b

Tactic:
rwa [intCast_re] at hre

Result:
no goals

Proof state:
d a b : ℤ
⊢ a ∣ (↑b).re ∧ a ∣ (↑b).im ↔ a ∣ b

Tactic:
constructor

Result:
case mp
d a b : ℤ
⊢ a ∣ (↑b).re ∧ a ∣ (↑b).im → a ∣ b

case mpr
d a b : ℤ
⊢ a ∣ b → a ∣ (↑b).re ∧ a ∣ (↑b).im

Proof state:
case mpr
d a b : ℤ
⊢ a ∣ b → a ∣ (↑b).re ∧ a ∣ (↑b).im

Tactic:
rw [intCast_re, intCast_im]

Result:
case mpr
d a b : ℤ
⊢ a ∣ b → a ∣ b ∧ a ∣ 0

Proof state:
d a b : ℤ
⊢ ↑a ∣ ↑b ↔ a ∣ b

Tactic:
rw [intCast_dvd]

Result:
d a b : ℤ
⊢ a ∣ (↑b).re ∧ a ∣ (↑b).im ↔ a ∣ b
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma cfcₙ_smul {S : Type*} [SMulZeroClass S R] [ContinuousConstSMul S R]
    [SMulZeroClass S A] [IsScalarTower S R A] [IsScalarTower S R (R → R)]
    (s : S) (f : R → R) (a : A) (hf : ContinuousOn f (σₙ R a)

Proof state:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : Nontrivial R
inst✝¹⁴ : StarRing R
inst✝¹³ : MetricSpace R
inst✝¹² : IsTopologicalSemiring R
inst✝¹¹ : ContinuousStar R
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : TopologicalSpace A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
S : Type u_3
inst✝⁴ : SMulZeroClass S R
inst✝³ : ContinuousConstSMul S R
inst✝² : SMulZeroClass S A
inst✝¹ : IsScalarTower S R A
inst✝ : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
h0 : autoParam (f 0 = 0) _auto✝
ha : p a
⊢ (cfcₙHom ha) { toFun := (σₙ R a).restrict ((s • 1) • f), continuous_toFun := ⋯, map_zero' := ⋯ } =
    (s • 1) • (cfcₙHom ha) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ }

Tactic:
rw [← map_smul]

Result:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : Nontrivial R
inst✝¹⁴ : StarRing R
inst✝¹³ : MetricSpace R
inst✝¹² : IsTopologicalSemiring R
inst✝¹¹ : ContinuousStar R
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : TopologicalSpace A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
S : Type u_3
inst✝⁴ : SMulZeroClass S R
inst✝³ : ContinuousConstSMul S R
inst✝² : SMulZeroClass S A
inst✝¹ : IsScalarTower S R A
inst✝ : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
h0 : autoParam (f 0 = 0) _auto✝
ha : p a
⊢ (cfcₙHom ha) { toFun := (σₙ R a).restrict ((s • 1) • f), continuous_toFun := ⋯, map_zero' := ⋯ } =
    (cfcₙHom ha) ((s • 1) • { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ })
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/Relabel.lean
theorem relabel_id' : relabel (id : α → α) = id

Proof state:
case h
α : Type u_1
x✝ : Clause α
⊢ relabel id x✝ = id x✝

Tactic:
simp [relabel]

Result:
no goals

Proof state:
α : Type u_1
⊢ relabel id = id

Tactic:
funext

Result:
case h
α : Type u_1
x✝ : Clause α
⊢ relabel id x✝ = id x✝
-- Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean
theorem existsUnique_gluing' (V : Opens X) (iUV : ∀ i : ι, U i ⟶ V) (hcover : V ≤ iSup U)
    (sf : ∀ i : ι, ToType (F.1.obj (op (U i)))) (h : IsCompatible F.1 U sf) :
    ∃! s : ToType (F.1.obj (op V)), ∀ i : ι, F.1.map (iUV i).op s = sf i

Proof state:
case intro.intro.refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
sf : (i : ι) → ToType (F.val.obj (op (U i)))
h : IsCompatible F.val U sf
V_eq_supr_U : V = iSup U
gl : ToType (F.val.obj (op (iSup U)))
gl_spec : IsGluing F.val U sf gl
gl_uniq : ∀ (y : ToType (F.val.obj (op (iSup U)))), (fun s => IsGluing F.val U sf s) y → y = gl
⊢ (fun s => ∀ (i : ι), (ConcreteCategory.hom (F.val.map (iUV i).op)) s = sf i)
    ((ConcreteCategory.hom (F.val.map (eqToHom V_eq_supr_U).op)) gl)

Tactic:
intro i

Result:
case intro.intro.refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
sf : (i : ι) → ToType (F.val.obj (op (U i)))
h : IsCompatible F.val U sf
V_eq_supr_U : V = iSup U
gl : ToType (F.val.obj (op (iSup U)))
gl_spec : IsGluing F.val U sf gl
gl_uniq : ∀ (y : ToType (F.val.obj (op (iSup U)))), (fun s => IsGluing F.val U sf s) y → y = gl
i : ι
⊢ (ConcreteCategory.hom (F.val.map (iUV i).op)) ((ConcreteCategory.hom (F.val.map (eqToHom V_eq_supr_U).op)) gl) = sf i
-- Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean
theorem IsEquivalent.neg (huv : u ~[l] v) : (fun x ↦ -u x) ~[l] fun x ↦ -v x

Proof state:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
huv : u ~[l] v
⊢ (fun x => -u x) ~[l] fun x => -v x

Tactic:
rw [IsEquivalent]

Result:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
huv : u ~[l] v
⊢ ((fun x => -u x) - fun x => -v x) =o[l] fun x => -v x

Proof state:
case h.e'_7.h
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
huv : u ~[l] v
x✝ : α
⊢ ((fun x => -u x) - fun x => -v x) x✝ = -(u - v) x✝

Tactic:
simp [neg_add_eq_sub]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
huv : u ~[l] v
⊢ ((fun x => -u x) - fun x => -v x) =o[l] fun x => -v x

Tactic:
convert huv.isLittleO.neg_left.neg_right

Result:
case h.e'_7.h
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
huv : u ~[l] v
x✝ : α
⊢ ((fun x => -u x) - fun x => -v x) x✝ = -(u - v) x✝
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem setLIntegral_lt_top_of_le_nnreal {s : Set α} (hs : μ s ≠ ∞) {f : α → ℝ≥0∞}
    (hbdd : ∃ y : ℝ≥0, ∀ x ∈ s, f x ≤ y) : ∫⁻ x in s, f x ∂μ < ∞

Proof state:
case intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : μ s ≠ ⊤
f : α → ℝ≥0∞
M : ℝ≥0
hM : ∀ x ∈ s, f x ≤ ↑M
⊢ ∫⁻ (x : α) in s, f x ∂μ < ⊤

Tactic:
refine lt_of_le_of_lt (setLIntegral_mono measurable_const hM) ?_

Result:
case intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : μ s ≠ ⊤
f : α → ℝ≥0∞
M : ℝ≥0
hM : ∀ x ∈ s, f x ≤ ↑M
⊢ ∫⁻ (x : α) in s, ↑M ∂μ < ⊤

Proof state:
case intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : μ s ≠ ⊤
f : α → ℝ≥0∞
M : ℝ≥0
hM : ∀ x ∈ s, f x ≤ ↑M
⊢ ∫⁻ (x : α) in s, ↑M ∂μ < ⊤

Tactic:
simp [ENNReal.mul_lt_top, hs.lt_top]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : μ s ≠ ⊤
f : α → ℝ≥0∞
hbdd : ∃ y, ∀ x ∈ s, f x ≤ ↑y
⊢ ∫⁻ (x : α) in s, f x ∂μ < ⊤

Tactic:
obtain ⟨M, hM⟩ := hbdd

Result:
case intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : μ s ≠ ⊤
f : α → ℝ≥0∞
M : ℝ≥0
hM : ∀ x ∈ s, f x ≤ ↑M
⊢ ∫⁻ (x : α) in s, f x ∂μ < ⊤
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem nfpBFamily_lt_ord_lift {o : Ordinal} {f : ∀ a < o, Ordinal → Ordinal} {c} (hc : ℵ₀ < cof c)
    (hc' : Cardinal.lift.{v, u} o.card < cof c) (hf : ∀ (i hi), ∀ b < c, f i hi b < c) {a} :
    a < c → nfpBFamily.{u, v} o f a < c :=
  nfpFamily_lt_ord_lift hc (by rwa [mk_toType]) fun _ => hf _ _

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} → Ordinal.{max u v}
c : Ordinal.{max u v}
hc : ℵ₀ < c.cof
hc' : Cardinal.lift.{v, u} o.card < c.cof
hf : ∀ (i : Ordinal.{u}) (hi : i < o), ∀ b < c, f i hi b < c
a : Ordinal.{max u v}
⊢ Cardinal.lift.{?u.34065, u} #o.toType < c.cof

Tactic:
rwa [mk_toType]

Result:
no goals
-- Mathlib/Logic/Function/FiberPartition.lean
lemma image_eq_image_mk (f : Y → Z) (g : X → Y) (a : Fiber (f ∘ g)) :
    a.image = (Fiber.mk f (g (a.preimage _))).image

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : Y → Z
g : X → Y
a : Fiber (f ∘ g)
⊢ image (f ∘ g) a = image f (mk f (g (preimage (f ∘ g) a)))

Tactic:
rw [← map_preimage_eq_image_map _ _ a, mk_image]

Result:
no goals