harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Asymptotics/ExpGrowth.lean
lemma le_expGrowthInf_mul {u v : ℕ → ℝ≥0∞} :
    expGrowthInf u + expGrowthInf v ≤ expGrowthInf (u * v)

Proof state:
u v : ℕ → ℝ≥0∞
⊢ expGrowthInf u + expGrowthInf v ≤ expGrowthInf (u * v)

Tactic:
refine le_liminf_add.trans_eq (liminf_congr (Eventually.of_forall fun n ↦ ?_))

Result:
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ ((fun n => (u n).log / ↑n) + fun n => (v n).log / ↑n) n = ((u * v) n).log / ↑n

Proof state:
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ ((fun n => (u n).log / ↑n) + fun n => (v n).log / ↑n) n = ((u * v) n).log / ↑n

Tactic:
rw [Pi.add_apply, Pi.mul_apply, ← add_div_of_nonneg_right n.cast_nonneg', log_mul_add]

Result:
no goals
-- Mathlib/Data/PNat/Xgcd.lean
theorem finish_isSpecial (hs : u.IsSpecial) : u.finish.IsSpecial

Proof state:
u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.wp + (u.y * u.qp + u.zp) + u.wp * (u.y * u.qp + u.zp) = ((u.wp + 1) * u.qp + u.x) * u.y

Tactic:
rw [add_mul _ _ u.y, add_comm _ (u.x * u.y), ← hs]

Result:
u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.wp + (u.y * u.qp + u.zp) + u.wp * (u.y * u.qp + u.zp) = u.wp + u.zp + u.wp * u.zp + (u.wp + 1) * u.qp * u.y

Proof state:
u : XgcdType
hs : u.IsSpecial
⊢ u.finish.IsSpecial

Tactic:
dsimp [IsSpecial, finish] at hs ⊢

Result:
u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.wp + (u.y * u.qp + u.zp) + u.wp * (u.y * u.qp + u.zp) = ((u.wp + 1) * u.qp + u.x) * u.y

Proof state:
u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.wp + (u.y * u.qp + u.zp) + u.wp * (u.y * u.qp + u.zp) = u.wp + u.zp + u.wp * u.zp + (u.wp + 1) * u.qp * u.y

Tactic:
ring

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem map_filterMap_of_inv (f : α → Option β) (g : β → α) (H : ∀ x : α, (f x).map g = some x)
    (l : List α) : map g (filterMap f l) = l

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
g : β → α
H : ∀ (x : α), Option.map g (f x) = some x
l : List α
⊢ map g (filterMap f l) = l

Tactic:
simp only [map_filterMap, H, filterMap_some, id]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/CharacterSpace.lean
theorem isClosed [Nontrivial 𝕜] [T2Space 𝕜] [ContinuousMul 𝕜] :
    IsClosed (characterSpace 𝕜 A)

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing 𝕜
inst✝⁹ : NoZeroDivisors 𝕜
inst✝⁸ : TopologicalSpace 𝕜
inst✝⁷ : ContinuousAdd 𝕜
inst✝⁶ : ContinuousConstSMul 𝕜 𝕜
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Semiring A
inst✝³ : Algebra 𝕜 A
inst✝² : Nontrivial 𝕜
inst✝¹ : T2Space 𝕜
inst✝ : ContinuousMul 𝕜
⊢ IsClosed (characterSpace 𝕜 A)

Tactic:
rw [eq_set_map_one_map_mul, Set.setOf_and]

Result:
𝕜 : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing 𝕜
inst✝⁹ : NoZeroDivisors 𝕜
inst✝⁸ : TopologicalSpace 𝕜
inst✝⁷ : ContinuousAdd 𝕜
inst✝⁶ : ContinuousConstSMul 𝕜 𝕜
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Semiring A
inst✝³ : Algebra 𝕜 A
inst✝² : Nontrivial 𝕜
inst✝¹ : T2Space 𝕜
inst✝ : ContinuousMul 𝕜
⊢ IsClosed ({a | a 1 = 1} ∩ {a | ∀ (x y : A), a (x * y) = a x * a y})

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing 𝕜
inst✝⁹ : NoZeroDivisors 𝕜
inst✝⁸ : TopologicalSpace 𝕜
inst✝⁷ : ContinuousAdd 𝕜
inst✝⁶ : ContinuousConstSMul 𝕜 𝕜
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Semiring A
inst✝³ : Algebra 𝕜 A
inst✝² : Nontrivial 𝕜
inst✝¹ : T2Space 𝕜
inst✝ : ContinuousMul 𝕜
⊢ IsClosed {a | ∀ (x y : A), a (x * y) = a x * a y}

Tactic:
simpa only [(union_zero 𝕜 A).symm] using union_zero_isClosed _ _

Result:
no goals

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing 𝕜
inst✝⁹ : NoZeroDivisors 𝕜
inst✝⁸ : TopologicalSpace 𝕜
inst✝⁷ : ContinuousAdd 𝕜
inst✝⁶ : ContinuousConstSMul 𝕜 𝕜
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Semiring A
inst✝³ : Algebra 𝕜 A
inst✝² : Nontrivial 𝕜
inst✝¹ : T2Space 𝕜
inst✝ : ContinuousMul 𝕜
⊢ IsClosed ({a | a 1 = 1} ∩ {a | ∀ (x y : A), a (x * y) = a x * a y})

Tactic:
refine IsClosed.inter (isClosed_eq (eval_continuous _) continuous_const) ?_

Result:
𝕜 : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing 𝕜
inst✝⁹ : NoZeroDivisors 𝕜
inst✝⁸ : TopologicalSpace 𝕜
inst✝⁷ : ContinuousAdd 𝕜
inst✝⁶ : ContinuousConstSMul 𝕜 𝕜
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Semiring A
inst✝³ : Algebra 𝕜 A
inst✝² : Nontrivial 𝕜
inst✝¹ : T2Space 𝕜
inst✝ : ContinuousMul 𝕜
⊢ IsClosed {a | ∀ (x y : A), a (x * y) = a x * a y}
-- Mathlib/GroupTheory/Nilpotent.lean
theorem comap_center_subst {H₁ H₂ : Subgroup G} [Normal H₁] [Normal H₂] (h : H₁ = H₂) :
    comap (mk' H₁) (center (G ⧸ H₁)) = comap (mk' H₂) (center (G ⧸ H₂))

Proof state:
G : Type u_1
inst✝² : Group G
H₁ : Subgroup G
inst✝¹ inst✝ : H₁.Normal
⊢ comap (mk' H₁) (center (G ⧸ H₁)) = comap (mk' H₁) (center (G ⧸ H₁))

Tactic:
rfl

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
H₁ H₂ : Subgroup G
inst✝¹ : H₁.Normal
inst✝ : H₂.Normal
h : H₁ = H₂
⊢ comap (mk' H₁) (center (G ⧸ H₁)) = comap (mk' H₂) (center (G ⧸ H₂))

Tactic:
subst h

Result:
G : Type u_1
inst✝² : Group G
H₁ : Subgroup G
inst✝¹ inst✝ : H₁.Normal
⊢ comap (mk' H₁) (center (G ⧸ H₁)) = comap (mk' H₁) (center (G ⧸ H₁))
-- Mathlib/CategoryTheory/Monoidal/Grp_.lean
theorem isPullback (A : Grp_ C) :
    IsPullback (A.mul ▷ A.X) ((α_ A.X A.X A.X).hom ≫ (A.X ◁ A.mul)) A.mul A.mul where
  w

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : Grp_ C
s : PullbackCone A.mul A.mul
⊢ ((fun s =>
            lift (lift (s.snd ≫ fst A.X A.X) (lift (s.snd ≫ fst A.X A.X ≫ A.inv) (s.fst ≫ fst A.X A.X) ≫ A.mul))
              (s.fst ≫ snd A.X A.X))
          s ≫
        (α_ A.X A.X A.X).hom ≫ A.X ◁ A.mul) ≫
      snd A.X A.X =
    s.snd ≫ snd A.X A.X

Tactic:
simp only [lift_lift_associator_hom_assoc, lift_whiskerLeft, lift_snd]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : Grp_ C
s : PullbackCone A.mul A.mul
⊢ lift (lift (s.snd ≫ fst A.X A.X ≫ A.inv) (s.fst ≫ fst A.X A.X) ≫ A.mul) (s.fst ≫ snd A.X A.X) ≫ A.mul =
    s.snd ≫ snd A.X A.X

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : Grp_ C
s : PullbackCone A.mul A.mul
m : s.pt ⟶ (A.X ⊗ A.X) ⊗ A.X
hm₁ : m ≫ A.mul ▷ A.X = s.fst
hm₂ : m ≫ (α_ A.X A.X A.X).hom ≫ A.X ◁ A.mul = s.snd
⊢ m ≫ fst (A.X ⊗ A.X) A.X ≫ fst A.X A.X = s.snd ≫ fst A.X A.X

Tactic:
simpa using hm₂ =≫ fst _ _

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
@[simp]
lemma measure_smul (c : ℝ≥0) (f : StieltjesFunction) : (c • f).measure = c • f.measure

Proof state:
c : ℝ≥0
f : StieltjesFunction
a b : ℝ
x✝ : a < b
⊢ ofReal (↑(c • f) b - ↑(c • f) a) = c • ofReal (↑f b - ↑f a)

Tactic:
change ofReal (c * f b - c * f a) = c • ofReal (f b - f a)

Result:
c : ℝ≥0
f : StieltjesFunction
a b : ℝ
x✝ : a < b
⊢ ofReal (↑c * ↑f b - ↑c * ↑f a) = c • ofReal (↑f b - ↑f a)

Proof state:
c : ℝ≥0
f : StieltjesFunction
a b : ℝ
x✝ : a < b
⊢ (c • f).measure (Ioc a b) = (c • f.measure) (Ioc a b)

Tactic:
simp only [measure_Ioc, Measure.smul_apply]

Result:
c : ℝ≥0
f : StieltjesFunction
a b : ℝ
x✝ : a < b
⊢ ofReal (↑(c • f) b - ↑(c • f) a) = c • ofReal (↑f b - ↑f a)

Proof state:
c : ℝ≥0
f : StieltjesFunction
a b : ℝ
x✝ : a < b
⊢ ofReal (↑c * ↑f b - ↑c * ↑f a) = c • ofReal (↑f b - ↑f a)

Tactic:
rw [← _root_.mul_sub, ENNReal.ofReal_mul zero_le_coe, ofReal_coe_nnreal, ← smul_eq_mul]

Result:
c : ℝ≥0
f : StieltjesFunction
a b : ℝ
x✝ : a < b
⊢ ↑c • ofReal (↑f b - ↑f a) = c • ofReal (↑f b - ↑f a)

Proof state:
c : ℝ≥0
f : StieltjesFunction
⊢ (c • f).measure = c • f.measure

Tactic:
refine Measure.ext_of_Ioc _ _ (fun a b _ ↦ ?_)

Result:
c : ℝ≥0
f : StieltjesFunction
a b : ℝ
x✝ : a < b
⊢ (c • f).measure (Ioc a b) = (c • f.measure) (Ioc a b)

Proof state:
c : ℝ≥0
f : StieltjesFunction
a b : ℝ
x✝ : a < b
⊢ ↑c • ofReal (↑f b - ↑f a) = c • ofReal (↑f b - ↑f a)

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Extensive.lean
theorem finitaryExtensive_of_reflective
    [HasFiniteCoproducts D] [HasPullbacksOfInclusions D] [FinitaryExtensive C]
    {Gl : C ⥤ D} {Gr : D ⥤ C} (adj : Gl ⊣ Gr) [Gr.Full] [Gr.Faithful]
    [∀ X Y (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)]
    [∀ X Y (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl]
    [PreservesPullbacksOfInclusions Gl] :
    FinitaryExtensive D

Proof state:
case h_map
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
inst✝⁷ : HasFiniteCoproducts D
inst✝⁶ : HasPullbacksOfInclusions D
inst✝⁵ : FinitaryExtensive C
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝⁴ : Gr.Full
inst✝³ : Gr.Faithful
inst✝² : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst✝¹ : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst✝ : PreservesPullbacksOfInclusions Gl
this : PreservesColimitsOfSize.{?u.98831, ?u.98830, v, v'', u, u''} Gl
X Y : D
c : BinaryCofan X Y
hc : IsColimit c
⊢ ∀ (X_1 Y_1 : Discrete WalkingPair) (f : X_1 ⟶ Y_1), HEq ((pair X Y ⋙ Gr).map f) ((pair (Gr.obj X) (Gr.obj Y)).map f)

Tactic:
rintro ⟨⟨⟩⟩ ⟨j⟩ ⟨⟨rfl : _ = j⟩⟩ <;> simp

Result:
no goals

Proof state:
case van_kampen'
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
inst✝⁷ : HasFiniteCoproducts D
inst✝⁶ : HasPullbacksOfInclusions D
inst✝⁵ : FinitaryExtensive C
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝⁴ : Gr.Full
inst✝³ : Gr.Faithful
inst✝² : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst✝¹ : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst✝ : PreservesPullbacksOfInclusions Gl
this : PreservesColimitsOfSize.{?u.98831, ?u.98830, v, v'', u, u''} Gl
X Y : D
c : BinaryCofan X Y
hc : IsColimit c
⊢ IsVanKampenColimit c

Tactic:
apply (IsVanKampenColimit.precompose_isIso_iff
  (isoWhiskerLeft _ (asIso adj.counit) ≪≫ Functor.rightUnitor _).hom).mp

Result:
case van_kampen'
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
inst✝⁷ : HasFiniteCoproducts D
inst✝⁶ : HasPullbacksOfInclusions D
inst✝⁵ : FinitaryExtensive C
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝⁴ : Gr.Full
inst✝³ : Gr.Faithful
inst✝² : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst✝¹ : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst✝ : PreservesPullbacksOfInclusions Gl
this : PreservesColimitsOfSize.{?u.98831, ?u.98830, v, v'', u, u''} Gl
X Y : D
c : BinaryCofan X Y
hc : IsColimit c
⊢ IsVanKampenColimit
    ((Cocones.precompose (isoWhiskerLeft (pair X Y) (asIso adj.counit) ≪≫ (pair X Y).rightUnitor).hom).obj c)
-- Mathlib/Analysis/NormedSpace/Connected.lean
theorem Set.Countable.isPathConnected_compl_of_one_lt_rank
    (h : 1 < Module.rank ℝ E) {s : Set E} (hs : s.Countable) :
    IsPathConnected sᶜ

Proof state:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
t t' : ℝ
htt' : t ≠ t'
⊢ Function.onFun Disjoint (fun t => [c + x-[ℝ]c + t • y] ∩ s) t t'

Tactic:
apply disjoint_iff_inter_eq_empty.2

Result:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
t t' : ℝ
htt' : t ≠ t'
⊢ (fun t => [c + x-[ℝ]c + t • y] ∩ s) t ∩ (fun t => [c + x-[ℝ]c + t • y] ∩ s) t' = ∅

Proof state:
case intro.inr
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
⊢ JoinedIn sᶜ a b

Tactic:
let c := (2 : ℝ)⁻¹ • (a + b)

Result:
case intro.inr
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
⊢ JoinedIn sᶜ a b
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma ofHom_zero : ofHom (0 : F ⟶ G) = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
⊢ ofHom 0 = 0

Tactic:
simp only [ofHom, HomologicalComplex.zero_f_apply, ofHoms_zero]

Result:
no goals
-- Mathlib/Data/Fin/VecNotation.lean
theorem cons_vec_bit0_eq_alt0 (x : α) (u : Fin n → α) (i : Fin (n + 1)) :
    vecCons x u (i + i) = vecAlt0 rfl (vecAppend rfl (vecCons x u) (vecCons x u)) i

Proof state:
α : Type u
n : ℕ
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (i + i) = vecAlt0 ⋯ (vecAppend ⋯ (vecCons x u) (vecCons x u)) i

Tactic:
rw [vecAlt0_vecAppend]

Result:
α : Type u
n : ℕ
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (i + i) = (vecCons x u ∘ fun n_1 => n_1 + n_1) i

Proof state:
α : Type u
n : ℕ
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (i + i) = (vecCons x u ∘ fun n_1 => n_1 + n_1) i

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Asymptotics/ExpGrowth.lean
/-- See `expGrowthInf_mul_le'` for a version with swapped argument `u` and `v`. -/
lemma expGrowthInf_mul_le {u v : ℕ → ℝ≥0∞} (h : expGrowthSup u ≠ ⊥ ∨ expGrowthInf v ≠ ⊤)
    (h' : expGrowthSup u ≠ ⊤ ∨ expGrowthInf v ≠ ⊥) :
    expGrowthInf (u * v) ≤ expGrowthSup u + expGrowthInf v

Proof state:
u v : ℕ → ℝ≥0∞
h : expGrowthSup u ≠ ⊥ ∨ expGrowthInf v ≠ ⊤
h' : expGrowthSup u ≠ ⊤ ∨ expGrowthInf v ≠ ⊥
⊢ expGrowthInf (u * v) ≤ expGrowthSup u + expGrowthInf v

Tactic:
refine (liminf_add_le h h').trans_eq' (liminf_congr (Eventually.of_forall fun n ↦ ?_))

Result:
u v : ℕ → ℝ≥0∞
h : expGrowthSup u ≠ ⊥ ∨ expGrowthInf v ≠ ⊤
h' : expGrowthSup u ≠ ⊤ ∨ expGrowthInf v ≠ ⊥
n : ℕ
⊢ ((u * v) n).log / ↑n = ((fun n => (u n).log / ↑n) + fun n => (v n).log / ↑n) n

Proof state:
u v : ℕ → ℝ≥0∞
h : expGrowthSup u ≠ ⊥ ∨ expGrowthInf v ≠ ⊤
h' : expGrowthSup u ≠ ⊤ ∨ expGrowthInf v ≠ ⊥
n : ℕ
⊢ ((u * v) n).log / ↑n = ((fun n => (u n).log / ↑n) + fun n => (v n).log / ↑n) n

Tactic:
rw [Pi.add_apply, Pi.mul_apply, ← add_div_of_nonneg_right n.cast_nonneg', log_mul_add]

Result:
no goals
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem factorial_mul_descFactorial : ∀ {n k : ℕ}, k ≤ n → (n - k)! * n.descFactorial k = n !
  | n, 0 => fun _ => by rw [descFactorial_zero, Nat.mul_one, Nat.sub_zero]
  | 0, succ k => fun h => by
    exfalso
    exact not_succ_le_zero k h
  | succ n, succ k => fun h => by
    rw [succ_descFactorial_succ, succ_sub_succ, ← Nat.mul_assoc, Nat.mul_comm (n - k)!,
      Nat.mul_assoc, factorial_mul_descFactorial (Nat.succ_le_succ_iff.1 h), factorial_succ]

Proof state:
k : ℕ
h : k.succ ≤ 0
⊢ False

Tactic:
exact not_succ_le_zero k h

Result:
no goals

Proof state:
n : ℕ
x✝ : 0 ≤ n
⊢ (n - 0)! * n.descFactorial 0 = n !

Tactic:
rw [descFactorial_zero, Nat.mul_one, Nat.sub_zero]

Result:
no goals

Proof state:
n k : ℕ
h : k.succ ≤ n.succ
⊢ (n.succ - k.succ)! * n.succ.descFactorial k.succ = n.succ !

Tactic:
rw [succ_descFactorial_succ, succ_sub_succ, ← Nat.mul_assoc, Nat.mul_comm (n - k)!,
  Nat.mul_assoc, factorial_mul_descFactorial (Nat.succ_le_succ_iff.1 h), factorial_succ]

Result:
no goals

Proof state:
k : ℕ
h : k.succ ≤ 0
⊢ (0 - k.succ)! * descFactorial 0 k.succ = 0!

Tactic:
exfalso

Result:
k : ℕ
h : k.succ ≤ 0
⊢ False
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem isWide_iff_objs_eq_univ : S.IsWide ↔ S.objs = Set.univ

Proof state:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
h : S.IsWide
⊢ S.objs = univ

Tactic:
ext x

Result:
case mp.h
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
h : S.IsWide
x : C
⊢ x ∈ S.objs ↔ x ∈ univ

Proof state:
case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
h : S.objs = univ
c : C
⊢ 𝟙 c ∈ S.arrows c c

Tactic:
obtain ⟨γ, γS⟩ := (le_of_eq h.symm : ⊤ ⊆ S.objs) (Set.mem_univ c)

Result:
case mpr.intro
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
h : S.objs = univ
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
⊢ 𝟙 c ∈ S.arrows c c

Proof state:
case mp.h.mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
h : S.IsWide
x : C
⊢ x ∈ S.objs

Tactic:
apply mem_objs_of_src S (h.wide x)

Result:
no goals

Proof state:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ S.IsWide → S.objs = univ

Tactic:
rintro h

Result:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
h : S.IsWide
⊢ S.objs = univ

Proof state:
case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
h : S.objs = univ
⊢ S.IsWide

Tactic:
refine ⟨fun c => ?_⟩

Result:
case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
h : S.objs = univ
c : C
⊢ 𝟙 c ∈ S.arrows c c

Proof state:
case mpr.intro
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
h : S.objs = univ
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
⊢ 𝟙 c ∈ S.arrows c c

Tactic:
exact id_mem_of_src S γS

Result:
no goals

Proof state:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ S.IsWide ↔ S.objs = univ

Tactic:
constructor

Result:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ S.IsWide → S.objs = univ

case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ S.objs = univ → S.IsWide

Proof state:
case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ S.objs = univ → S.IsWide

Tactic:
rintro h

Result:
case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
h : S.objs = univ
⊢ S.IsWide

Proof state:
case mp.h
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
h : S.IsWide
x : C
⊢ x ∈ S.objs ↔ x ∈ univ

Tactic:
constructor <;> simp only [top_eq_univ, mem_univ, imp_true_iff, forall_true_left]

Result:
case mp.h.mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
h : S.IsWide
x : C
⊢ x ∈ S.objs
-- Mathlib/GroupTheory/ArchimedeanDensely.lean
@[to_additive existing]
lemma LinearOrderedCommGroup.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete
    {G : Type*} [LinearOrderedCommGroup G] [Nontrivial G] (g : G) :
    Set.WellFoundedOn {x : G | x ≤ g} (· > ·) ↔ Nonempty (G ≃*o Multiplicative ℤ)

Proof state:
case refine_4
G : Type u_2
inst✝¹ : LinearOrderedCommGroup G
inst✝ : Nontrivial G
g : G
h : {x | g⁻¹ ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
⊢ ∀ a ∈ {x | x ≤ g}, ∀ b ∈ {x | x ≤ g}, a > b → Function.onFun (fun x1 x2 => x1 < x2) (fun x => x⁻¹) a b

Tactic:
intro

Result:
case refine_4
G : Type u_2
inst✝¹ : LinearOrderedCommGroup G
inst✝ : Nontrivial G
g : G
h : {x | g⁻¹ ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
a✝ : G
⊢ a✝ ∈ {x | x ≤ g} → ∀ b ∈ {x | x ≤ g}, a✝ > b → Function.onFun (fun x1 x2 => x1 < x2) (fun x => x⁻¹) a✝ b

Proof state:
case refine_4
G : Type u_2
inst✝¹ : LinearOrderedCommGroup G
inst✝ : Nontrivial G
g : G
h : {x | g⁻¹ ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
a✝ : G
⊢ a✝ ∈ {x | x ≤ g} → ∀ b ∈ {x | x ≤ g}, a✝ > b → Function.onFun (fun x1 x2 => x1 < x2) (fun x => x⁻¹) a✝ b

Tactic:
simp [Function.onFun, inv_le']

Result:
no goals

Proof state:
G : Type u_2
inst✝¹ : LinearOrderedCommGroup G
inst✝ : Nontrivial G
g : G
⊢ ({x | x ≤ g}.WellFoundedOn fun x1 x2 => x1 > x2) ↔ Nonempty (G ≃*o Multiplicative ℤ)

Tactic:
rw [← wellFoundedOn_setOf_le_lt_iff_nonempty_discrete (g := g⁻¹)]

Result:
G : Type u_2
inst✝¹ : LinearOrderedCommGroup G
inst✝ : Nontrivial G
g : G
⊢ ({x | x ≤ g}.WellFoundedOn fun x1 x2 => x1 > x2) ↔ {x | g⁻¹ ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
-- Mathlib/RingTheory/Adjoin/Tower.lean
theorem adjoin_restrictScalars (C D E : Type*) [CommSemiring C] [CommSemiring D] [CommSemiring E]
    [Algebra C D] [Algebra C E] [Algebra D E] [IsScalarTower C D E] (S : Set E) :
    (Algebra.adjoin D S).restrictScalars C =
      (Algebra.adjoin ((⊤ : Subalgebra C D).map (IsScalarTower.toAlgHom C D E)) S).restrictScalars
        C

Proof state:
case h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : CommSemiring C
inst✝⁵ : CommSemiring D
inst✝⁴ : CommSemiring E
inst✝³ : Algebra C D
inst✝² : Algebra C E
inst✝¹ : Algebra D E
inst✝ : IsScalarTower C D E
S : Set E
x : E
⊢ x ∈ Set.range ⇑(algebraMap D E) ↔ x ∈ Set.range ⇑(algebraMap (↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤)) E)

Tactic:
constructor

Result:
case h.mp
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : CommSemiring C
inst✝⁵ : CommSemiring D
inst✝⁴ : CommSemiring E
inst✝³ : Algebra C D
inst✝² : Algebra C E
inst✝¹ : Algebra D E
inst✝ : IsScalarTower C D E
S : Set E
x : E
⊢ x ∈ Set.range ⇑(algebraMap D E) → x ∈ Set.range ⇑(algebraMap (↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤)) E)

case h.mpr
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : CommSemiring C
inst✝⁵ : CommSemiring D
inst✝⁴ : CommSemiring E
inst✝³ : Algebra C D
inst✝² : Algebra C E
inst✝¹ : Algebra D E
inst✝ : IsScalarTower C D E
S : Set E
x : E
⊢ x ∈ Set.range ⇑(algebraMap (↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤)) E) → x ∈ Set.range ⇑(algebraMap D E)
-- Mathlib/Order/InitialSeg.lean
theorem le_apply_iff [LinearOrder α] (f : α ≤i β) : b ≤ f a ↔ ∃ c ≤ a, f c = b

Proof state:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : b ≤ f a
⊢ ∃ c ≤ a, f c = b

Tactic:
obtain ⟨c, hc⟩ := f.mem_range_of_le h

Result:
case mp.intro
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : b ≤ f a
c : α
hc : f c = b
⊢ ∃ c ≤ a, f c = b

Proof state:
case mpr.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
inst✝ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
c : α
hc : c ≤ a
⊢ f c ≤ f a

Tactic:
exact f.monotone hc

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
⊢ b ≤ f a ↔ ∃ c ≤ a, f c = b

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
⊢ b ≤ f a → ∃ c ≤ a, f c = b

case mpr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
⊢ (∃ c ≤ a, f c = b) → b ≤ f a

Proof state:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
⊢ b ≤ f a → ∃ c ≤ a, f c = b

Tactic:
intro h

Result:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : b ≤ f a
⊢ ∃ c ≤ a, f c = b

Proof state:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
⊢ (∃ c ≤ a, f c = b) → b ≤ f a

Tactic:
rintro ⟨c, hc, rfl⟩

Result:
case mpr.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
inst✝ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
c : α
hc : c ≤ a
⊢ f c ≤ f a

Proof state:
case mp.intro
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : b ≤ f a
c : α
hc : f c = b
⊢ c ≤ a

Tactic:
rwa [← hc, f.le_iff_le] at h

Result:
no goals

Proof state:
case mp.intro
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : b ≤ f a
c : α
hc : f c = b
⊢ ∃ c ≤ a, f c = b

Tactic:
refine ⟨c, ?_, hc⟩

Result:
case mp.intro
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : LinearOrder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
h : b ≤ f a
c : α
hc : f c = b
⊢ c ≤ a