harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem basis_toMatrix_basisFun_mul [Fintype ι]
    {𝕜} [SeminormedCommRing 𝕜] (b : Basis ι 𝕜 (PiLp p fun _ : ι => 𝕜))
    (A : Matrix ι ι 𝕜) :
    b.toMatrix (PiLp.basisFun _ _ _) * A =
      Matrix.of fun i j => b.repr ((WithLp.equiv _ _).symm (Aᵀ j)) i

Proof state:
p : ℝ≥0∞
ι : Type u_2
inst✝¹ : Fintype ι
𝕜 : Type u_5
inst✝ : SeminormedCommRing 𝕜
b : Basis ι 𝕜 (PiLp p fun x => 𝕜)
A : Matrix ι ι 𝕜
⊢ b.toMatrix ⇑(basisFun p 𝕜 ι) * A = of fun i j => (b.repr ((WithLp.equiv p ((i : ι) → (fun x => 𝕜) i)).symm (Aᵀ j))) i

Tactic:
have := basis_toMatrix_basisFun_mul (b.map (WithLp.linearEquiv _ 𝕜 _)) A

Result:
p : ℝ≥0∞
ι : Type u_2
inst✝¹ : Fintype ι
𝕜 : Type u_5
inst✝ : SeminormedCommRing 𝕜
b : Basis ι 𝕜 (PiLp p fun x => 𝕜)
A : Matrix ι ι 𝕜
this :
  (b.map (WithLp.linearEquiv p 𝕜 ((i : ι) → (fun x => 𝕜) i))).toMatrix ⇑(Pi.basisFun 𝕜 ι) * A =
    of fun i j => ((b.map (WithLp.linearEquiv p 𝕜 ((i : ι) → (fun x => 𝕜) i))).repr (Aᵀ j)) i
⊢ b.toMatrix ⇑(basisFun p 𝕜 ι) * A = of fun i j => (b.repr ((WithLp.equiv p ((i : ι) → (fun x => 𝕜) i)).symm (Aᵀ j))) i

Proof state:
p : ℝ≥0∞
ι : Type u_2
inst✝¹ : Fintype ι
𝕜 : Type u_5
inst✝ : SeminormedCommRing 𝕜
b : Basis ι 𝕜 (PiLp p fun x => 𝕜)
A : Matrix ι ι 𝕜
this :
  (b.map (WithLp.linearEquiv p 𝕜 ((i : ι) → (fun x => 𝕜) i))).toMatrix ⇑(Pi.basisFun 𝕜 ι) * A =
    of fun i j => ((b.map (WithLp.linearEquiv p 𝕜 ((i : ι) → (fun x => 𝕜) i))).repr (Aᵀ j)) i
⊢ b.toMatrix ⇑(basisFun p 𝕜 ι) * A = of fun i j => (b.repr ((WithLp.equiv p ((i : ι) → (fun x => 𝕜) i)).symm (Aᵀ j))) i

Tactic:
simp_rw [← PiLp.basisFun_map p, Basis.map_repr, LinearEquiv.trans_apply,
  WithLp.linearEquiv_symm_apply, Basis.toMatrix_map, Function.comp_def, Basis.map_apply,
  LinearEquiv.symm_apply_apply] at this

Result:
p : ℝ≥0∞
ι : Type u_2
inst✝¹ : Fintype ι
𝕜 : Type u_5
inst✝ : SeminormedCommRing 𝕜
b : Basis ι 𝕜 (PiLp p fun x => 𝕜)
A : Matrix ι ι 𝕜
this : (b.toMatrix fun x => (basisFun p 𝕜 ι) x) * A = of fun i j => (b.repr ((WithLp.equiv p (ι → 𝕜)).symm (Aᵀ j))) i
⊢ b.toMatrix ⇑(basisFun p 𝕜 ι) * A = of fun i j => (b.repr ((WithLp.equiv p ((i : ι) → (fun x => 𝕜) i)).symm (Aᵀ j))) i

Proof state:
p : ℝ≥0∞
ι : Type u_2
inst✝¹ : Fintype ι
𝕜 : Type u_5
inst✝ : SeminormedCommRing 𝕜
b : Basis ι 𝕜 (PiLp p fun x => 𝕜)
A : Matrix ι ι 𝕜
this : (b.toMatrix fun x => (basisFun p 𝕜 ι) x) * A = of fun i j => (b.repr ((WithLp.equiv p (ι → 𝕜)).symm (Aᵀ j))) i
⊢ b.toMatrix ⇑(basisFun p 𝕜 ι) * A = of fun i j => (b.repr ((WithLp.equiv p ((i : ι) → (fun x => 𝕜) i)).symm (Aᵀ j))) i

Tactic:
exact this

Result:
no goals
-- Mathlib/Order/SemiconjSup.lean
theorem comp_orderIso [Preorder α] [Preorder β] [Preorder γ] {f : α → β} {g : β → α}
    (h : IsOrderRightAdjoint f g) (e : γ ≃o α) : IsOrderRightAdjoint (f ∘ e) (e.symm ∘ g)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
e : γ ≃o α
⊢ IsOrderRightAdjoint (f ∘ ⇑e) (⇑e.symm ∘ g)

Tactic:
intro y

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
e : γ ≃o α
y : β
⊢ IsLUB {x | (f ∘ ⇑e) x ≤ y} ((⇑e.symm ∘ g) y)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
e : γ ≃o α
y : β
⊢ IsLUB {x | f x ≤ y} (g y)

Tactic:
exact h y

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
e : γ ≃o α
y : β
⊢ IsLUB {x | (f ∘ ⇑e) x ≤ y} ((⇑e.symm ∘ g) y)

Tactic:
change IsLUB (e ⁻¹' { x | f x ≤ y }) (e.symm (g y))

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
e : γ ≃o α
y : β
⊢ IsLUB (⇑e ⁻¹' {x | f x ≤ y}) (e.symm (g y))

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
e : γ ≃o α
y : β
⊢ IsLUB (⇑e ⁻¹' {x | f x ≤ y}) (e.symm (g y))

Tactic:
rw [e.isLUB_preimage, e.apply_symm_apply]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
e : γ ≃o α
y : β
⊢ IsLUB {x | f x ≤ y} (g y)
-- Mathlib/Data/Finsupp/Basic.lean
theorem support_subtypeDomain [D : DecidablePred p] {f : α →₀ M} :
    (subtypeDomain p f).support = f.support.subtype p

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
p : α → Prop
D : DecidablePred p
f : α →₀ M
⊢ (subtypeDomain p f).support = Finset.subtype p f.support

Tactic:
rw [Subsingleton.elim D] <;> rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
lemma mem_genEigenspace_zero {f : End R M} {μ : R} {x : M} :
    x ∈ f.genEigenspace μ 0 ↔ x = 0

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x : M
⊢ x ∈ (f.genEigenspace μ) 0 ↔ x = 0

Tactic:
rw [← Nat.cast_zero, mem_genEigenspace_nat, pow_zero, LinearMap.mem_ker, LinearMap.one_apply]

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem Perm.extendDomain_refl : Perm.extendDomain (Equiv.refl _) f = Equiv.refl _

Proof state:
α' : Type u_9
β' : Type u_10
p : β' → Prop
inst✝ : DecidablePred p
f : α' ≃ Subtype p
⊢ extendDomain (Equiv.refl α') f = Equiv.refl β'

Tactic:
simp [Perm.extendDomain]

Result:
no goals
-- Mathlib/Probability/Distributions/Gaussian.lean
@[simp]
lemma gaussianPDFReal_zero_var (m : ℝ) : gaussianPDFReal m 0 = 0

Proof state:
case h
m x : ℝ
⊢ gaussianPDFReal m 0 x = 0 x

Tactic:
simp [gaussianPDFReal]

Result:
no goals

Proof state:
m : ℝ
⊢ gaussianPDFReal m 0 = 0

Tactic:
ext1 x

Result:
case h
m x : ℝ
⊢ gaussianPDFReal m 0 x = 0 x
-- Mathlib/Data/Real/Irrational.lean
theorem of_one_div (h : Irrational (1 / x)) : Irrational x :=
  of_rat_div 1 <| by rwa [cast_one]

Proof state:
x : ℝ
h : Irrational (1 / x)
⊢ Irrational (↑1 / x)

Tactic:
rwa [cast_one]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Dirac.lean
theorem ae_eq_dirac [MeasurableSingletonClass α] {a : α} (f : α → δ) :
    f =ᵐ[dirac a] const α (f a)

Proof state:
α : Type u_1
δ : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
f : α → δ
⊢ f =ᶠ[ae (dirac a)] const α (f a)

Tactic:
simp [Filter.EventuallyEq]

Result:
no goals
-- Mathlib/Topology/Order.lean
theorem nhds_induced [T : TopologicalSpace α] (f : β → α) (a : β) :
    @nhds β (TopologicalSpace.induced f T) a = comap f (𝓝 (f a))

Proof state:
case h
α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
s : Set β
⊢ s ∈ 𝓝 a ↔ s ∈ comap f (𝓝 (f a))

Tactic:
rw [mem_nhds_induced, mem_comap]

Result:
no goals

Proof state:
α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
⊢ 𝓝 a = comap f (𝓝 (f a))

Tactic:
ext s

Result:
case h
α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
s : Set β
⊢ s ∈ 𝓝 a ↔ s ∈ comap f (𝓝 (f a))
-- Mathlib/Algebra/Lie/Normalizer.lean
theorem normalizer_inf : (N₁ ⊓ N₂).normalizer = N₁.normalizer ⊓ N₂.normalizer

Proof state:
case h
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N₁ N₂ : LieSubmodule R L M
m✝ : M
⊢ m✝ ∈ (N₁ ⊓ N₂).normalizer ↔ m✝ ∈ N₁.normalizer ⊓ N₂.normalizer

Tactic:
simp [← forall_and]

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N₁ N₂ : LieSubmodule R L M
⊢ (N₁ ⊓ N₂).normalizer = N₁.normalizer ⊓ N₂.normalizer

Tactic:
ext

Result:
case h
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N₁ N₂ : LieSubmodule R L M
m✝ : M
⊢ m✝ ∈ (N₁ ⊓ N₂).normalizer ↔ m✝ ∈ N₁.normalizer ⊓ N₂.normalizer
-- Mathlib/NumberTheory/FactorisationProperties.lean
theorem Prime.deficient (h : Prime n) : Deficient n

Proof state:
n : ℕ
h : Prime n
⊢ n.Deficient

Tactic:
rw [← pow_one n]

Result:
n : ℕ
h : Prime n
⊢ (n ^ 1).Deficient

Proof state:
n : ℕ
h : Prime n
⊢ (n ^ 1).Deficient

Tactic:
exact h.deficient_pow

Result:
no goals
-- Mathlib/Probability/Process/Stopping.lean
theorem stoppedProcess_eq'' [LinearOrder ι] [LocallyFiniteOrderBot ι] [AddCommMonoid E] (n : ι) :
    stoppedProcess u τ n = Set.indicator {a | n ≤ τ a} (u n) +
      ∑ i ∈ Finset.Iio n, Set.indicator {ω | τ ω = i} (u i)

Proof state:
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : AddCommMonoid E
n : ι
h_mem : ∀ (ω : Ω), τ ω < n → τ ω ∈ Finset.Iio n
⊢ {a | n ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.filter (fun x => x < n) (Finset.Iio n), {ω | τ ω = i}.indicator (u i) =
    {a | n ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.Iio n, {ω | τ ω = i}.indicator (u i)

Tactic:
congr with i

Result:
case e_a.e_s.h
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : AddCommMonoid E
n : ι
h_mem : ∀ (ω : Ω), τ ω < n → τ ω ∈ Finset.Iio n
i : ι
⊢ i ∈ Finset.filter (fun x => x < n) (Finset.Iio n) ↔ i ∈ Finset.Iio n

Proof state:
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : AddCommMonoid E
n : ι
h_mem : ∀ (ω : Ω), τ ω < n → τ ω ∈ Finset.Iio n
⊢ stoppedProcess u τ n = {a | n ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.Iio n, {ω | τ ω = i}.indicator (u i)

Tactic:
rw [stoppedProcess_eq_of_mem_finset n h_mem]

Result:
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : AddCommMonoid E
n : ι
h_mem : ∀ (ω : Ω), τ ω < n → τ ω ∈ Finset.Iio n
⊢ {a | n ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.filter (fun x => x < n) (Finset.Iio n), {ω | τ ω = i}.indicator (u i) =
    {a | n ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.Iio n, {ω | τ ω = i}.indicator (u i)

Proof state:
case e_a.e_s.h
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : AddCommMonoid E
n : ι
h_mem : ∀ (ω : Ω), τ ω < n → τ ω ∈ Finset.Iio n
i : ι
⊢ i ∈ Finset.filter (fun x => x < n) (Finset.Iio n) ↔ i ∈ Finset.Iio n

Tactic:
simp

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : AddCommMonoid E
n : ι
⊢ stoppedProcess u τ n = {a | n ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.Iio n, {ω | τ ω = i}.indicator (u i)

Tactic:
have h_mem : ∀ ω, τ ω < n → τ ω ∈ Finset.Iio n := fun ω h => Finset.mem_Iio.mpr h

Result:
Ω : Type u_1
ι : Type u_3
τ : Ω → ι
E : Type u_4
u : ι → Ω → E
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : AddCommMonoid E
n : ι
h_mem : ∀ (ω : Ω), τ ω < n → τ ω ∈ Finset.Iio n
⊢ stoppedProcess u τ n = {a | n ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.Iio n, {ω | τ ω = i}.indicator (u i)
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem div' {m : ℕ} (cpm : Coprime p m) {b : ℕ} (dvd : m ∣ b) :
    padicValNat p (b / m) = padicValNat p b

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
cpm : p.Coprime m
b : ℕ
dvd : m ∣ b
⊢ padicValNat p (b / m) = padicValNat p b

Tactic:
rw [padicValNat.div_of_dvd dvd, eq_zero_of_not_dvd (hp.out.coprime_iff_not_dvd.mp cpm),
  Nat.sub_zero]

Result:
no goals
-- Mathlib/Order/Minimal.lean
theorem minimal_apply_mem_iff (ht : t ⊆ Set.range f) :
    Minimal (· ∈ t) (f x) ↔ Minimal (fun x ↦ f x ∈ t) x

Proof state:
α : Type u_1
x : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α ↪o β
t : Set β
ht : t ⊆ range ⇑f
⊢ Minimal (fun x => x ∈ t) (f x) ↔ Minimal (fun x => f x ∈ t) x

Tactic:
rw [← f.minimal_apply_mem_inter_range_iff, inter_eq_self_of_subset_left ht]

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem IsRestriction.rankFinite {M : Matroid α} [RankFinite M] (h : N ≤r M) : N.RankFinite

Proof state:
α : Type u_1
N M : Matroid α
inst✝ : M.RankFinite
h : N ≤r M
⊢ N.RankFinite

Tactic:
obtain ⟨R, -, rfl⟩ := h

Result:
case intro.intro
α : Type u_1
M : Matroid α
inst✝ : M.RankFinite
R : Set α
⊢ (M ↾ R).RankFinite

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
inst✝ : M.RankFinite
R : Set α
⊢ (M ↾ R).RankFinite

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/Extend.lean
lemma isZero_X {i : Option ι} (hi : i = none) :
    IsZero (X K i)

Proof state:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
i : Option ι
hi : i = none
⊢ IsZero (X K i)

Tactic:
subst hi

Result:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
⊢ IsZero (X K none)

Proof state:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
⊢ IsZero (X K none)

Tactic:
exact Limits.isZero_zero _

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Pi.lean
lemma nndist_pi_lt_iff {f g : ∀ b, π b} {r : ℝ≥0} (hr : 0 < r) :
    nndist f g < r ↔ ∀ b, nndist (f b) (g b) < r

Proof state:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
r : ℝ≥0
hr : ⊥ < r
⊢ nndist f g < r ↔ ∀ (b : β), nndist (f b) (g b) < r

Tactic:
simp [nndist_pi_def, Finset.sup_lt_iff hr]

Result:
no goals

Proof state:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
r : ℝ≥0
hr : 0 < r
⊢ nndist f g < r ↔ ∀ (b : β), nndist (f b) (g b) < r

Tactic:
rw [← bot_eq_zero'] at hr

Result:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
r : ℝ≥0
hr : ⊥ < r
⊢ nndist f g < r ↔ ∀ (b : β), nndist (f b) (g b) < r
-- Mathlib/CategoryTheory/Limits/IsLimit.lean
theorem uniq_cone_morphism {s t : Cone F} (h : IsLimit t) {f f' : s ⟶ t} : f = f' :=
  have : ∀ {g : s ⟶ t}, g = h.liftConeMorphism s

Proof state:
case w
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
s t : Cone F
h : IsLimit t
f f' g : s ⟶ t
⊢ g.hom = (h.liftConeMorphism s).hom

Tactic:
exact h.uniq _ _ g.w

Result:
no goals

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
s t : Cone F
h : IsLimit t
f f' : s ⟶ t
⊢ ∀ {g : s ⟶ t}, g = h.liftConeMorphism s

Tactic:
intro g

Result:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
s t : Cone F
h : IsLimit t
f f' g : s ⟶ t
⊢ g = h.liftConeMorphism s

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
s t : Cone F
h : IsLimit t
f f' g : s ⟶ t
⊢ g = h.liftConeMorphism s

Tactic:
apply ConeMorphism.ext

Result:
case w
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
s t : Cone F
h : IsLimit t
f f' g : s ⟶ t
⊢ g.hom = (h.liftConeMorphism s).hom
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem cons_prefix_cons : a :: l₁ <+: b :: l₂ ↔ a = b ∧ l₁ <+: l₂

Proof state:
case mpr.intro
α✝ : Type u_1
a : α✝
l₁ l₂ : List α✝
h : l₁ <+: l₂
⊢ ∃ t, (a = a ∧ l₁ = t) ∧ t <+: l₂

Tactic:
exact ⟨l₁, ⟨rfl, rfl⟩, h⟩

Result:
no goals

Proof state:
case mpr
α✝ : Type u_1
a : α✝
l₁ : List α✝
b : α✝
l₂ : List α✝
⊢ a = b ∧ l₁ <+: l₂ → ∃ t, (a = b ∧ l₁ = t) ∧ t <+: l₂

Tactic:
rintro ⟨rfl, h⟩

Result:
case mpr.intro
α✝ : Type u_1
a : α✝
l₁ l₂ : List α✝
h : l₁ <+: l₂
⊢ ∃ t, (a = a ∧ l₁ = t) ∧ t <+: l₂

Proof state:
case mp
α✝ : Type u_1
a : α✝
l₁ : List α✝
b : α✝
l₂ : List α✝
⊢ (∃ t, (a = b ∧ l₁ = t) ∧ t <+: l₂) → a = b ∧ l₁ <+: l₂

Tactic:
rintro ⟨t, ⟨rfl, rfl⟩, h⟩

Result:
case mp.intro.intro.intro
α✝ : Type u_1
a : α✝
l₁ l₂ : List α✝
h : l₁ <+: l₂
⊢ a = a ∧ l₁ <+: l₂

Proof state:
case mp.intro.intro.intro
α✝ : Type u_1
a : α✝
l₁ l₂ : List α✝
h : l₁ <+: l₂
⊢ a = a ∧ l₁ <+: l₂

Tactic:
exact ⟨rfl, h⟩

Result:
no goals

Proof state:
α✝ : Type u_1
a : α✝
l₁ : List α✝
b : α✝
l₂ : List α✝
⊢ (∃ t, (a = b ∧ l₁ = t) ∧ t <+: l₂) ↔ a = b ∧ l₁ <+: l₂

Tactic:
constructor

Result:
case mp
α✝ : Type u_1
a : α✝
l₁ : List α✝
b : α✝
l₂ : List α✝
⊢ (∃ t, (a = b ∧ l₁ = t) ∧ t <+: l₂) → a = b ∧ l₁ <+: l₂

case mpr
α✝ : Type u_1
a : α✝
l₁ : List α✝
b : α✝
l₂ : List α✝
⊢ a = b ∧ l₁ <+: l₂ → ∃ t, (a = b ∧ l₁ = t) ∧ t <+: l₂

Proof state:
α✝ : Type u_1
a : α✝
l₁ : List α✝
b : α✝
l₂ : List α✝
⊢ a :: l₁ <+: b :: l₂ ↔ a = b ∧ l₁ <+: l₂

Tactic:
simp only [prefix_cons_iff, cons.injEq, false_or, List.cons_ne_nil]

Result:
α✝ : Type u_1
a : α✝
l₁ : List α✝
b : α✝
l₂ : List α✝
⊢ (∃ t, (a = b ∧ l₁ = t) ∧ t <+: l₂) ↔ a = b ∧ l₁ <+: l₂
-- Mathlib/Data/Real/EReal.lean
theorem add_top_of_ne_bot {x : EReal} (h : x ≠ ⊥) : x + ⊤ = ⊤

Proof state:
x : EReal
h : x ≠ ⊥
⊢ x + ⊤ = ⊤

Tactic:
rw [add_comm, top_add_of_ne_bot h]

Result:
no goals
-- Mathlib/Order/Category/BddDistLat.lean
lemma comp_apply {X Y Z : BddDistLat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
    (f ≫ g) x = g (f x)

Proof state:
X Y Z : BddDistLat
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X.toDistLat
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem lt_div_iff_mul_lt : a < c / b ↔ a * b < c

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b c : α
⊢ a < c / b ↔ a * b < c

Tactic:
rw [← mul_lt_mul_iff_right b, div_eq_mul_inv, inv_mul_cancel_right]

Result:
no goals
-- Mathlib/NumberTheory/FLT/Three.lean
private lemma cube_of_castHom_ne_zero {n : ZMod 9} :
    castHom (show 3 ∣ 9 by norm_num) (ZMod 3) n ≠ 0 → n ^ 3 = 1 ∨ n ^ 3 = 8

Proof state:
n : ZMod 9
⊢ (castHom ⋯ (ZMod 3)) n ≠ 0 → n ^ 3 = 1 ∨ n ^ 3 = 8

Tactic:
revert n

Result:
⊢ ∀ {n : ZMod 9}, (castHom ⋯ (ZMod 3)) n ≠ 0 → n ^ 3 = 1 ∨ n ^ 3 = 8

Proof state:
⊢ ∀ {n : ZMod 9}, (castHom ⋯ (ZMod 3)) n ≠ 0 → n ^ 3 = 1 ∨ n ^ 3 = 8

Tactic:
decide

Result:
no goals

Proof state:
n : ZMod 9
⊢ 3 ∣ 9

Tactic:
norm_num

Result:
no goals
-- Mathlib/RingTheory/RingHom/StandardSmooth.lean
lemma IsStandardSmoothOfRelativeDimension.isStandardSmooth (f : R →+* S)
    (hf : IsStandardSmoothOfRelativeDimension.{t, w} n f) :
    IsStandardSmooth.{t, w} f

Proof state:
n : ℕ
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : IsStandardSmoothOfRelativeDimension n f
⊢ f.IsStandardSmooth

Tactic:
algebraize [f]

Result:
n : ℕ
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : IsStandardSmoothOfRelativeDimension n f
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.IsStandardSmoothOfRelativeDimension n R S
⊢ f.IsStandardSmooth

Proof state:
n : ℕ
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : IsStandardSmoothOfRelativeDimension n f
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.IsStandardSmoothOfRelativeDimension n R S
⊢ f.IsStandardSmooth

Tactic:
exact Algebra.IsStandardSmoothOfRelativeDimension.isStandardSmooth n

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Coloring.lean
lemma chromaticNumber_eq_iff_forall_surjective (hG : G.Colorable n) :
    G.chromaticNumber = n ↔ ∀ C : G.Coloring (Fin n), Surjective C

Proof state:
V : Type u
G : SimpleGraph V
n : ℕ
hG : G.Colorable n
⊢ G.chromaticNumber = ↑n ↔ ∀ (C : G.Coloring (Fin n)), Surjective ⇑C

Tactic:
rw [← hG.chromaticNumber_le.ge_iff_eq, le_chromaticNumber_iff_forall_surjective]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Powerset.lean
/-- A product over `Finset.powersetCard` which only depends on the size of the sets is constant. -/
@[to_additive
"A sum over `Finset.powersetCard` which only depends on the size of the sets is constant."]
lemma prod_powersetCard (n : ℕ) (s : Finset α) (f : ℕ → β) :
    ∏ t ∈ powersetCard n s, f #t = f n ^ (#s).choose n

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
s : Finset α
f : ℕ → β
⊢ ∀ a ∈ powersetCard n s, f #a = f n

Tactic:
rintro a ha

Result:
α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
s : Finset α
f : ℕ → β
a : Finset α
ha : a ∈ powersetCard n s
⊢ f #a = f n

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
s : Finset α
f : ℕ → β
⊢ ∏ t ∈ powersetCard n s, f #t = f n ^ (#s).choose n

Tactic:
rw [prod_eq_pow_card, card_powersetCard]

Result:
α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
s : Finset α
f : ℕ → β
⊢ ∀ a ∈ powersetCard n s, f #a = f n

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
s : Finset α
f : ℕ → β
a : Finset α
ha : a ∈ powersetCard n s
⊢ f #a = f n

Tactic:
rw [(mem_powersetCard.1 ha).2]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Tilted.lean
lemma rnDeriv_tilted_left_self [SigmaFinite μ] (hf : AEMeasurable f μ) :
    (μ.tilted f).rnDeriv μ =ᵐ[μ] fun x ↦ ENNReal.ofReal (exp (f x) / ∫ x, exp (f x) ∂μ)

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : SigmaFinite μ
hf : AEMeasurable f μ
⊢ (μ.tilted f).rnDeriv μ =ᶠ[ae μ] fun x => ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)

Tactic:
refine (rnDeriv_tilted_left μ hf).trans ?_

Result:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : SigmaFinite μ
hf : AEMeasurable f μ
⊢ (fun x => ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv μ x) =ᶠ[ae μ] fun x =>
    ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : SigmaFinite μ
hf : AEMeasurable f μ
x : α
hx : μ.rnDeriv μ x = 1
⊢ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv μ x =
    ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)

Tactic:
rw [hx, mul_one]

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : SigmaFinite μ
hf : AEMeasurable f μ
⊢ (fun x => ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv μ x) =ᶠ[ae μ] fun x =>
    ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)

Tactic:
filter_upwards [Measure.rnDeriv_self μ] with x hx

Result:
case h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : SigmaFinite μ
hf : AEMeasurable f μ
x : α
hx : μ.rnDeriv μ x = 1
⊢ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv μ x =
    ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)