harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/NormedSpace/PiTensorProduct/ProjectiveSeminorm.lean
theorem projectiveSeminorm_tprod_le (m : Π i, E i) :
    projectiveSeminorm (⨂ₜ[𝕜] i, m i) ≤ ∏ i, ‖m i‖

Proof state:
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
m : (i : ι) → E i
⊢ ⨅ p, projectiveSeminormAux ↑p ≤ ∏ i : ι, ‖m i‖

Tactic:
convert ciInf_le (bddBelow_projectiveSemiNormAux _) ⟨[((1 : 𝕜), m)] ,?_⟩

Result:
case h.e'_4
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
m : (i : ι) → E i
⊢ ∏ i : ι, ‖m i‖ = projectiveSeminormAux ↑⟨[(1, m)], ?convert_2⟩

case convert_2
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
m : (i : ι) → E i
⊢ [(1, m)] ∈ (⨂ₜ[𝕜] (i : ι), m i).lifts

Proof state:
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
m : (i : ι) → E i
⊢ projectiveSeminorm (⨂ₜ[𝕜] (i : ι), m i) ≤ ∏ i : ι, ‖m i‖

Tactic:
rw [projectiveSeminorm_apply]

Result:
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
m : (i : ι) → E i
⊢ ⨅ p, projectiveSeminormAux ↑p ≤ ∏ i : ι, ‖m i‖

Proof state:
case convert_2
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
m : (i : ι) → E i
⊢ [(1, m)] ∈ (⨂ₜ[𝕜] (i : ι), m i).lifts

Tactic:
rw [mem_lifts_iff, List.map_singleton, List.sum_singleton, one_smul]

Result:
no goals

Proof state:
case h.e'_4
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
m : (i : ι) → E i
⊢ ∏ i : ι, ‖m i‖ = projectiveSeminormAux ↑⟨[(1, m)], ?convert_2⟩

Tactic:
simp only [projectiveSeminormAux, Function.comp_apply, List.map_cons, norm_one, one_mul,
List.map_nil, List.sum_cons, List.sum_nil, add_zero]

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem gcd_add_self_left (m n : ℕ) : gcd (m + n) n = gcd m n

Proof state:
m n : ℕ
⊢ (m + n).gcd n = m.gcd n

Tactic:
rw [gcd_comm, gcd_add_self_right, gcd_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem subsingleton_dual_iff :
    Subsingleton (Dual K V) ↔ Subsingleton V

Proof state:
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Projective K V
h : Subsingleton (Dual K V)
v w : V
⊢ ∀ (φ : Dual K V), φ (v - w) = 0

Tactic:
intros f

Result:
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Projective K V
h : Subsingleton (Dual K V)
v w : V
f : Dual K V
⊢ f (v - w) = 0

Proof state:
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Projective K V
h : Subsingleton (Dual K V)
v w : V
f : Dual K V
⊢ f (v - w) = 0

Tactic:
simp [Subsingleton.elim f 0]

Result:
no goals

Proof state:
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Projective K V
⊢ Subsingleton (Dual K V) ↔ Subsingleton V

Tactic:
refine ⟨fun h ↦ ⟨fun v w ↦ ?_⟩, fun _ ↦ inferInstance⟩

Result:
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Projective K V
h : Subsingleton (Dual K V)
v w : V
⊢ v = w

Proof state:
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Projective K V
h : Subsingleton (Dual K V)
v w : V
⊢ v = w

Tactic:
rw [← sub_eq_zero, ← forall_dual_apply_eq_zero_iff K (v - w)]

Result:
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Projective K V
h : Subsingleton (Dual K V)
v w : V
⊢ ∀ (φ : Dual K V), φ (v - w) = 0
-- Mathlib/Data/Real/Hyperreal.lean
theorem IsSt.map₂ {x y : ℝ*} {r s : ℝ} (hxr : IsSt x r) (hys : IsSt y s) {f : ℝ → ℝ → ℝ}
    (hf : ContinuousAt (Function.uncurry f) (r, s)) : IsSt (x.map₂ f y) (f r s)

Proof state:
case intro.intro
r s : ℝ
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : (ofSeq x).IsSt r
y : ℕ → ℝ
hys : (ofSeq y).IsSt s
⊢ IsSt (Germ.map₂ f (ofSeq x) (ofSeq y)) (f r s)

Tactic:
rw [isSt_ofSeq_iff_tendsto] at hxr hys

Result:
case intro.intro
r s : ℝ
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : Tendsto x (↑(hyperfilter ℕ)) (𝓝 r)
y : ℕ → ℝ
hys : Tendsto y (↑(hyperfilter ℕ)) (𝓝 s)
⊢ IsSt (Germ.map₂ f (ofSeq x) (ofSeq y)) (f r s)

Proof state:
case intro
y : ℝ*
r s : ℝ
hys : y.IsSt s
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : (ofSeq x).IsSt r
⊢ IsSt (Germ.map₂ f (ofSeq x) y) (f r s)

Tactic:
rcases ofSeq_surjective y with ⟨y, rfl⟩

Result:
case intro.intro
r s : ℝ
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : (ofSeq x).IsSt r
y : ℕ → ℝ
hys : (ofSeq y).IsSt s
⊢ IsSt (Germ.map₂ f (ofSeq x) (ofSeq y)) (f r s)

Proof state:
x y : ℝ*
r s : ℝ
hxr : x.IsSt r
hys : y.IsSt s
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
⊢ IsSt (Germ.map₂ f x y) (f r s)

Tactic:
rcases ofSeq_surjective x with ⟨x, rfl⟩

Result:
case intro
y : ℝ*
r s : ℝ
hys : y.IsSt s
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : (ofSeq x).IsSt r
⊢ IsSt (Germ.map₂ f (ofSeq x) y) (f r s)

Proof state:
case intro.intro
r s : ℝ
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : Tendsto x (↑(hyperfilter ℕ)) (𝓝 r)
y : ℕ → ℝ
hys : Tendsto y (↑(hyperfilter ℕ)) (𝓝 s)
⊢ IsSt (Germ.map₂ f (ofSeq x) (ofSeq y)) (f r s)

Tactic:
exact isSt_ofSeq_iff_tendsto.2 <| hf.tendsto.comp (hxr.prod_mk_nhds hys)

Result:
no goals
-- Mathlib/Analysis/Calculus/LHopital.lean
theorem lhopital_zero_right_on_Ioo (hab : a < b) (hdf : DifferentiableOn ℝ f (Ioo a b))
    (hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0) (hfa : Tendsto f (𝓝[>] a) (𝓝 0))
    (hga : Tendsto g (𝓝[>] a) (𝓝 0))
    (hdiv : Tendsto (fun x => (deriv f) x / (deriv g) x) (𝓝[>] a) l) :
    Tendsto (fun x => f x / g x) (𝓝[>] a) l

Proof state:
a b : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hab : a < b
hdf : DifferentiableOn ℝ f (Ioo a b)
hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[>] a) l
⊢ Tendsto (fun x => f x / g x) (𝓝[>] a) l

Tactic:
have hdf : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x := fun x hx =>
  (hdf x hx).differentiableAt (Ioo_mem_nhds hx.1 hx.2)

Result:
a b : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hab : a < b
hdf✝ : DifferentiableOn ℝ f (Ioo a b)
hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[>] a) l
hdf : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x
⊢ Tendsto (fun x => f x / g x) (𝓝[>] a) l

Proof state:
a b : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hab : a < b
hdf✝ : DifferentiableOn ℝ f (Ioo a b)
hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[>] a) l
hdf : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x
⊢ Tendsto (fun x => f x / g x) (𝓝[>] a) l

Tactic:
have hdg : ∀ x ∈ Ioo a b, DifferentiableAt ℝ g x := fun x hx =>
  by_contradiction fun h => hg' x hx (deriv_zero_of_not_differentiableAt h)

Result:
a b : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hab : a < b
hdf✝ : DifferentiableOn ℝ f (Ioo a b)
hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[>] a) l
hdf : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x
hdg : ∀ x ∈ Ioo a b, DifferentiableAt ℝ g x
⊢ Tendsto (fun x => f x / g x) (𝓝[>] a) l

Proof state:
a b : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hab : a < b
hdf✝ : DifferentiableOn ℝ f (Ioo a b)
hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[>] a) l
hdf : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x
hdg : ∀ x ∈ Ioo a b, DifferentiableAt ℝ g x
⊢ Tendsto (fun x => f x / g x) (𝓝[>] a) l

Tactic:
exact HasDerivAt.lhopital_zero_right_on_Ioo hab (fun x hx => (hdf x hx).hasDerivAt)
  (fun x hx => (hdg x hx).hasDerivAt) hg' hfa hga hdiv

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem norm_eq_norm_app_of_nonzero {f : PadicSeq p} (hf : ¬f ≈ 0) :
    ∃ k, f.norm = padicNorm p k ∧ k ≠ 0 :=
  have heq : f.norm = padicNorm p (f <| stationaryPoint hf)

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
heq : f.norm = padicNorm p (↑f (stationaryPoint hf))
h : ↑f (stationaryPoint hf) = 0
⊢ f.norm = 0

Tactic:
simpa [h] using heq

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
⊢ f.norm = padicNorm p (↑f (stationaryPoint hf))

Tactic:
simp [norm, hf]

Result:
no goals
-- Mathlib/Algebra/Lie/Engel.lean
theorem Function.Surjective.isEngelian {f : L →ₗ⁅R⁆ L₂} (hf : Function.Surjective f)
    (h : LieAlgebra.IsEngelian.{u₁, u₂, u₄} R L) : LieAlgebra.IsEngelian.{u₁, u₃, u₄} R L₂

Proof state:
R : Type u₁
L : Type u₂
L₂ : Type u₃
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
hf : Surjective ⇑f
h : LieAlgebra.IsEngelian R L
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L₂ M
_i4 : LieModule R L₂ M
h' : ∀ (x : L₂), IsNilpotent ((toEnd R L₂ M) x)
⊢ LieModule.IsNilpotent L₂ M

Tactic:
letI : LieRingModule L M := LieRingModule.compLieHom M f

Result:
R : Type u₁
L : Type u₂
L₂ : Type u₃
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
hf : Surjective ⇑f
h : LieAlgebra.IsEngelian R L
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L₂ M
_i4 : LieModule R L₂ M
h' : ∀ (x : L₂), IsNilpotent ((toEnd R L₂ M) x)
this : LieRingModule L M := LieRingModule.compLieHom M f
⊢ LieModule.IsNilpotent L₂ M
-- Mathlib/Topology/Algebra/Ring/Basic.lean
theorem IsTopologicalRing.of_addGroup_of_nhds_zero [IsTopologicalAddGroup R]
    (hmul : Tendsto (uncurry ((· * ·) : R → R → R)) (𝓝 0 ×ˢ 𝓝 0) <| 𝓝 0)
    (hmul_left : ∀ x₀ : R, Tendsto (fun x : R => x₀ * x) (𝓝 0) <| 𝓝 0)
    (hmul_right : ∀ x₀ : R, Tendsto (fun x : R => x * x₀) (𝓝 0) <| 𝓝 0) : IsTopologicalRing R where
  continuous_mul

Proof state:
R : Type u_2
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
hmul : Tendsto (uncurry fun x1 x2 => x1 * x2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
hmul_left : ∀ (x₀ : R), Tendsto (fun x => x₀ * x) (𝓝 0) (𝓝 0)
hmul_right : ∀ (x₀ : R), Tendsto (fun x => x * x₀) (𝓝 0) (𝓝 0)
⊢ Continuous fun p => p.1 * p.2

Tactic:
refine continuous_of_continuousAt_zero₂ (AddMonoidHom.mul (R := R)) ?_ ?_ ?_ <;>
  simpa only [ContinuousAt, mul_zero, zero_mul, nhds_prod_eq, AddMonoidHom.mul_apply]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Perm.lean
theorem Perm.inter_left (l : List α) {t₁ t₂ : List α} (p : t₁ ~ t₂) : l ∩ t₁ = l ∩ t₂ :=
  filter_congr fun a _ => by simpa using p.mem_iff (a := a)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l t₁ t₂ : List α
p : t₁ ~ t₂
a : α
x✝ : a ∈ l
⊢ elem a t₁ = elem a t₂

Tactic:
simpa using p.mem_iff (a := a)

Result:
no goals
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem eq_symm_apply {x : α} {y : β} (hx : x ∈ e.source) (hy : y ∈ e.target) :
    x = e.symm y ↔ e x = y :=
  ⟨fun h => by rw [← e.right_inv hy, h], fun h => by rw [← e.left_inv hx, h]⟩

Proof state:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
x : α
y : β
hx : x ∈ e.source
hy : y ∈ e.target
h : ↑e x = y
⊢ x = ↑e.symm y

Tactic:
rw [← e.left_inv hx, h]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
x : α
y : β
hx : x ∈ e.source
hy : y ∈ e.target
h : x = ↑e.symm y
⊢ ↑e x = y

Tactic:
rw [← e.right_inv hy, h]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Pointwise.lean
lemma set_smul_le_iff (p : Submodule R M) :
    s • N ≤ p ↔
    ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p

Proof state:
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
N p : Submodule R M
⊢ s • N ≤ p ↔ ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p

Tactic:
fconstructor

Result:
case mp
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
N p : Submodule R M
⊢ s • N ≤ p → ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p

case mpr
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
N p : Submodule R M
⊢ (∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p) → s • N ≤ p

Proof state:
case mp
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
N p : Submodule R M
h : s • N ≤ p
r : S
n : M
hr : r ∈ s
hn : n ∈ N
⊢ r • n ∈ p

Tactic:
exact h <| mem_set_smul_of_mem_mem hr hn

Result:
no goals

Proof state:
case mpr
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
N p : Submodule R M
⊢ (∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p) → s • N ≤ p

Tactic:
apply set_smul_le

Result:
no goals

Proof state:
case mp
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
N p : Submodule R M
⊢ s • N ≤ p → ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p

Tactic:
intro h r n hr hn

Result:
case mp
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
N p : Submodule R M
h : s • N ≤ p
r : S
n : M
hr : r ∈ s
hn : n ∈ N
⊢ r • n ∈ p
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem add_factorial_lt_factorial_add {i n : ℕ} (hi : 2 ≤ i) (hn : 1 ≤ n) :
    i + n ! < (i + n)!

Proof state:
i n : ℕ
hi : 2 ≤ i
hn : 1 ≤ n
⊢ i + n ! < (i + n)!

Tactic:
cases hn

Result:
case refl
i : ℕ
hi : 2 ≤ i
⊢ i + 1! < (i + 1)!

case step
i : ℕ
hi : 2 ≤ i
m✝ : ℕ
a✝ : Nat.le 1 m✝
⊢ i + m✝.succ ! < (i + m✝.succ)!

Proof state:
case refl
i : ℕ
hi : 2 ≤ i
⊢ i + 1 < (i + 1)!

Tactic:
exact lt_factorial_self (succ_le_succ hi)

Result:
no goals

Proof state:
case step
i : ℕ
hi : 2 ≤ i
m✝ : ℕ
a✝ : Nat.le 1 m✝
⊢ i + m✝.succ ! < (i + m✝.succ)!

Tactic:
exact add_factorial_succ_lt_factorial_add_succ _ hi

Result:
no goals

Proof state:
case refl
i : ℕ
hi : 2 ≤ i
⊢ i + 1! < (i + 1)!

Tactic:
rw [factorial_one]

Result:
case refl
i : ℕ
hi : 2 ≤ i
⊢ i + 1 < (i + 1)!
-- Mathlib/LinearAlgebra/Trace.lean
theorem trace_transpose' (f : M →ₗ[R] M) :
    trace R _ (Module.Dual.transpose (R := R) f) = trace R M f

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
⊢ (trace R (Dual R M)) (Dual.transpose f) = (trace R M) f

Tactic:
rw [← comp_apply, trace_transpose]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
/-- A variant of `WeierstrassCurve.j_eq_zero_iff` without assuming a reduced ring. -/
lemma j_eq_zero_iff' : W.j = 0 ↔ W.c₄ ^ 3 = 0

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsElliptic
⊢ W.j = 0 ↔ W.c₄ ^ 3 = 0

Tactic:
rw [j, Units.mul_right_eq_zero]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem add_lt_add_left_coe {x y : EReal} (h : x < y) (z : ℝ) : (z : EReal) + x < z + y

Proof state:
x y : EReal
h : x < y
z : ℝ
⊢ ↑z + x < ↑z + y

Tactic:
simpa [add_comm] using add_lt_add_right_coe h z

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem image_union_image_compl_eq_range (f : α → β) : f '' s ∪ f '' sᶜ = range f

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ f '' s ∪ f '' sᶜ = range f

Tactic:
rw [← image_union, ← image_univ, ← union_compl_self]

Result:
no goals
-- Mathlib/Data/Nat/Cast/Order/Ring.lean
@[simp, norm_cast] lemma cast_eq_neg_cast : (m : R) = -n ↔ m = 0 ∧ n = 0

Proof state:
R : Type u_1
inst✝ : LinearOrderedRing R
m n : ℕ
⊢ ↑m = -↑n ↔ m = 0 ∧ n = 0

Tactic:
simp [eq_neg_iff_add_eq_zero, ← cast_add]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ioo_subset_Ioo (ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) : Ioo a₁ b₁ ⊆ Ioo a₂ b₂

Proof state:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
ha : a₂ ≤ a₁
hb : b₁ ≤ b₂
⊢ Ioo a₁ b₁ ⊆ Ioo a₂ b₂

Tactic:
simpa [← coe_subset] using Set.Ioo_subset_Ioo ha hb

Result:
no goals
-- Mathlib/Data/Multiset/Sym.lean
theorem sym2_mono {m m' : Multiset α} (h : m ≤ m') : m.sym2 ≤ m'.sym2

Proof state:
α : Type u_1
m m' : Multiset α
h : m ≤ m'
⊢ m.sym2 ≤ m'.sym2

Tactic:
refine Quotient.inductionOn₂ m m' (fun xs ys h => ?_) h

Result:
α : Type u_1
m m' : Multiset α
h✝ : m ≤ m'
xs ys : List α
h : ⟦xs⟧ ≤ ⟦ys⟧
⊢ Multiset.sym2 ⟦xs⟧ ≤ Multiset.sym2 ⟦ys⟧

Proof state:
α : Type u_1
m m' : Multiset α
h✝ : m ≤ m'
xs ys : List α
h : ⟦xs⟧ ≤ ⟦ys⟧
⊢ xs <+~ ys

Tactic:
simpa only [quot_mk_to_coe, coe_le, sym2_coe] using h

Result:
no goals

Proof state:
α : Type u_1
m m' : Multiset α
h✝ : m ≤ m'
xs ys : List α
h : ⟦xs⟧ ≤ ⟦ys⟧
⊢ Multiset.sym2 ⟦xs⟧ ≤ Multiset.sym2 ⟦ys⟧

Tactic:
suffices xs <+~ ys from this.sym2

Result:
α : Type u_1
m m' : Multiset α
h✝ : m ≤ m'
xs ys : List α
h : ⟦xs⟧ ≤ ⟦ys⟧
⊢ xs <+~ ys
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem Nontrivial.infsep_of_fintype [DecidableEq α] [Fintype s] (hs : s.Nontrivial) :
    s.infsep = s.offDiag.toFinset.inf' (by simpa) (uncurry dist)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
hs : s.Nontrivial
⊢ s.offDiag.toFinset.Nonempty

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
inst✝² : PseudoMetricSpace α
s : Set α
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
hs : s.Nontrivial
⊢ s.infsep = s.offDiag.toFinset.inf' ⋯ (uncurry dist)

Tactic:
rw [Set.infsep_of_fintype, dif_pos hs]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : PseudoMetricSpace α
s : Set α
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
hs : s.Nontrivial
⊢ s.infsep = s.offDiag.toFinset.inf' ⋯ (uncurry dist)

Tactic:
classical rw [Set.infsep_of_fintype, dif_pos hs]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem UniformSpace.ball_mem_nhdsWithin {x : α} {S : Set α} ⦃V : Set (α × α)⦄ (x_in : x ∈ S)
    (V_in : V ∈ 𝓤 α ⊓ 𝓟 (S ×ˢ S)) : ball x V ∈ 𝓝[S] x

Proof state:
α : Type ua
inst✝ : UniformSpace α
x : α
S : Set α
V : Set (α × α)
x_in : x ∈ S
V_in : V ∈ 𝓤 α ⊓ 𝓟 (S ×ˢ S)
⊢ ∃ t ∈ 𝓤 α ⊓ 𝓟 (S ×ˢ S), Prod.mk x ⁻¹' t ⊆ ball x V

Tactic:
exact ⟨V, V_in, Subset.rfl⟩

Result:
no goals

Proof state:
α : Type ua
inst✝ : UniformSpace α
x : α
S : Set α
V : Set (α × α)
x_in : x ∈ S
V_in : V ∈ 𝓤 α ⊓ 𝓟 (S ×ˢ S)
⊢ ball x V ∈ 𝓝[S] x

Tactic:
rw [nhdsWithin_eq_comap_uniformity_of_mem x_in, mem_comap]

Result:
α : Type ua
inst✝ : UniformSpace α
x : α
S : Set α
V : Set (α × α)
x_in : x ∈ S
V_in : V ∈ 𝓤 α ⊓ 𝓟 (S ×ˢ S)
⊢ ∃ t ∈ 𝓤 α ⊓ 𝓟 (S ×ˢ S), Prod.mk x ⁻¹' t ⊆ ball x V
-- Mathlib/Algebra/Ring/Defs.lean
theorem one_sub_mul (a b : α) : (1 - a) * b = b - a * b

Proof state:
α : Type u
inst✝ : NonAssocRing α
a b : α
⊢ (1 - a) * b = b - a * b

Tactic:
rw [sub_mul, one_mul]

Result:
no goals
-- Mathlib/Combinatorics/Digraph/Orientation.lean
@[mono]
lemma toSimpleGraphInclusive_mono : Monotone (toSimpleGraphInclusive : _ → SimpleGraph V)

Proof state:
case inl
V : Type u_1
a✝ b✝ : Digraph V
h₁ : a✝ ≤ b✝
v✝ w✝ : V
h₂ : a✝.toSimpleGraphInclusive.Adj v✝ w✝
h✝ : a✝.Adj v✝ w✝
⊢ b✝.Adj v✝ w✝ ∨ b✝.Adj w✝ v✝

Tactic:
exact Or.inl <| h₁ ‹_›

Result:
no goals

Proof state:
V : Type u_1
⊢ Monotone toSimpleGraphInclusive

Tactic:
intro _ _ h₁ _ _ h₂

Result:
V : Type u_1
a✝ b✝ : Digraph V
h₁ : a✝ ≤ b✝
v✝ w✝ : V
h₂ : a✝.toSimpleGraphInclusive.Adj v✝ w✝
⊢ b✝.toSimpleGraphInclusive.Adj v✝ w✝

Proof state:
case inr
V : Type u_1
a✝ b✝ : Digraph V
h₁ : a✝ ≤ b✝
v✝ w✝ : V
h₂ : a✝.toSimpleGraphInclusive.Adj v✝ w✝
h✝ : a✝.Adj w✝ v✝
⊢ b✝.Adj v✝ w✝ ∨ b✝.Adj w✝ v✝

Tactic:
exact Or.inr <| h₁ ‹_›

Result:
no goals

Proof state:
V : Type u_1
a✝ b✝ : Digraph V
h₁ : a✝ ≤ b✝
v✝ w✝ : V
h₂ : a✝.toSimpleGraphInclusive.Adj v✝ w✝
⊢ b✝.Adj v✝ w✝ ∨ b✝.Adj w✝ v✝

Tactic:
cases h₂.2

Result:
case inl
V : Type u_1
a✝ b✝ : Digraph V
h₁ : a✝ ≤ b✝
v✝ w✝ : V
h₂ : a✝.toSimpleGraphInclusive.Adj v✝ w✝
h✝ : a✝.Adj v✝ w✝
⊢ b✝.Adj v✝ w✝ ∨ b✝.Adj w✝ v✝

case inr
V : Type u_1
a✝ b✝ : Digraph V
h₁ : a✝ ≤ b✝
v✝ w✝ : V
h₂ : a✝.toSimpleGraphInclusive.Adj v✝ w✝
h✝ : a✝.Adj w✝ v✝
⊢ b✝.Adj v✝ w✝ ∨ b✝.Adj w✝ v✝

Proof state:
V : Type u_1
a✝ b✝ : Digraph V
h₁ : a✝ ≤ b✝
v✝ w✝ : V
h₂ : a✝.toSimpleGraphInclusive.Adj v✝ w✝
⊢ b✝.toSimpleGraphInclusive.Adj v✝ w✝

Tactic:
apply And.intro h₂.1

Result:
V : Type u_1
a✝ b✝ : Digraph V
h₁ : a✝ ≤ b✝
v✝ w✝ : V
h₂ : a✝.toSimpleGraphInclusive.Adj v✝ w✝
⊢ b✝.Adj v✝ w✝ ∨ b✝.Adj w✝ v✝
-- Mathlib/Algebra/Module/Submodule/Lattice.lean
theorem sub_mem_sup {R' M' : Type*} [Ring R'] [AddCommGroup M'] [Module R' M']
    {S T : Submodule R' M'} {s t : M'} (hs : s ∈ S) (ht : t ∈ T) : s - t ∈ S ⊔ T

Proof state:
R' : Type u_4
M' : Type u_5
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
S T : Submodule R' M'
s t : M'
hs : s ∈ S
ht : t ∈ T
⊢ s - t ∈ S ⊔ T

Tactic:
rw [sub_eq_add_neg]

Result:
R' : Type u_4
M' : Type u_5
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
S T : Submodule R' M'
s t : M'
hs : s ∈ S
ht : t ∈ T
⊢ s + -t ∈ S ⊔ T

Proof state:
R' : Type u_4
M' : Type u_5
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
S T : Submodule R' M'
s t : M'
hs : s ∈ S
ht : t ∈ T
⊢ s + -t ∈ S ⊔ T

Tactic:
exact add_mem_sup hs (neg_mem ht)

Result:
no goals
-- Mathlib/MeasureTheory/PiSystem.lean
theorem generate_inter {s : Set (Set α)} (hs : IsPiSystem s) {t₁ t₂ : Set α}
    (ht₁ : (generate s).Has t₁) (ht₂ : (generate s).Has t₂) : (generate s).Has (t₁ ∩ t₂) :=
  have : generate s ≤ (generate s).restrictOn ht₂ :=
    generate_le _ fun s₁ hs₁ =>
      have : (generate s).Has s₁ := GenerateHas.basic s₁ hs₁
      have : generate s ≤ (generate s).restrictOn this :=
        generate_le _ fun s₂ hs₂ =>
          show (generate s).Has (s₂ ∩ s₁) from
            (s₂ ∩ s₁).eq_empty_or_nonempty.elim (fun h => h.symm ▸ GenerateHas.empty) fun h =>
              GenerateHas.basic _ <| hs _ hs₂ _ hs₁ h
      have : (generate s).Has (t₂ ∩ s₁) := this _ ht₂
      show (generate s).Has (s₁ ∩ t₂) by rwa [inter_comm]
  this _ ht₁

Proof state:
α : Type u_3
s : Set (Set α)
hs : IsPiSystem s
t₁ t₂ : Set α
ht₁ : (generate s).Has t₁
ht₂ : (generate s).Has t₂
s₁ : Set α
hs₁ : s₁ ∈ s
this✝¹ : (generate s).Has s₁
this✝ : generate s ≤ (generate s).restrictOn this✝¹
this : (generate s).Has (t₂ ∩ s₁)
⊢ (generate s).Has (s₁ ∩ t₂)

Tactic:
rwa [inter_comm]

Result:
no goals