harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
theorem Basis.nonempty_fintype_index_of_rank_lt_aleph0 {ι : Type*} (b : Basis ι R M)
    (h : Module.rank R M < ℵ₀) : Nonempty (Fintype ι)

Proof state:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type u_1
b : Basis ι R M
h : Module.rank R M < ℵ₀
⊢ Nonempty (Fintype ι)

Tactic:
rwa [← Cardinal.lift_lt, ← b.mk_eq_rank, Cardinal.lift_aleph0, Cardinal.lift_lt_aleph0,
  Cardinal.lt_aleph0_iff_fintype] at h

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem IsCyclic.card_mulAut [Group G] [Finite G] [h : IsCyclic G] :
    Nat.card (MulAut G) = Nat.totient (Nat.card G)

Proof state:
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
h : IsCyclic G
this : NeZero (Nat.card G)
⊢ Nat.card (MulAut G) = (Nat.card G).totient

Tactic:
rw [← ZMod.card_units_eq_totient, ← Nat.card_eq_fintype_card]

Result:
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
h : IsCyclic G
this : NeZero (Nat.card G)
⊢ Nat.card (MulAut G) = Nat.card (ZMod (Nat.card G))ˣ

Proof state:
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
h : IsCyclic G
this : NeZero (Nat.card G)
⊢ Nat.card (MulAut G) = Nat.card (ZMod (Nat.card G))ˣ

Tactic:
exact Nat.card_congr (mulAutMulEquiv G)

Result:
no goals

Proof state:
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
h : IsCyclic G
⊢ Nat.card (MulAut G) = (Nat.card G).totient

Tactic:
have : NeZero (Nat.card G) := ⟨Nat.card_pos.ne'⟩

Result:
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
h : IsCyclic G
this : NeZero (Nat.card G)
⊢ Nat.card (MulAut G) = (Nat.card G).totient
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_add_const_Ioo : (fun x => x + a) ⁻¹' Ioo b c = Ioo (b - a) (c - a)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x + a) ⁻¹' Ioo b c = Ioo (b - a) (c - a)

Tactic:
simp [← Ioi_inter_Iio]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem contDiffAt_inv {x : 𝕜'} (hx : x ≠ 0) {n} : ContDiffAt 𝕜 n Inv.inv x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜'
hx : x ≠ 0
n : WithTop ℕ∞
⊢ ContDiffAt 𝕜 n Inv.inv x

Tactic:
simpa only [Ring.inverse_eq_inv'] using contDiffAt_ring_inverse 𝕜 (Units.mk0 x hx)

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean
theorem nnnorm_def (f : E →SL[σ₁₂] F) : ‖f‖₊ = sInf { c | ∀ x, ‖f x‖₊ ≤ c * ‖x‖₊ }

Proof state:
case a
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_6
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
⊢ sInf {c | 0 ≤ c ∧ ∀ (x : E), ‖f x‖ ≤ c * ‖x‖} = sInf {x | ∃ (h : 0 ≤ x), ⟨x, h⟩ ∈ {c | ∀ (x : E), ‖f x‖₊ ≤ c * ‖x‖₊}}

Tactic:
simp_rw [← NNReal.coe_le_coe, NNReal.coe_mul, coe_nnnorm, mem_setOf_eq, NNReal.coe_mk,
  exists_prop]

Result:
no goals

Proof state:
case a
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_6
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
⊢ ↑‖f‖₊ = ↑(sInf {c | ∀ (x : E), ‖f x‖₊ ≤ c * ‖x‖₊})

Tactic:
rw [NNReal.coe_sInf, coe_nnnorm, norm_def, NNReal.coe_image]

Result:
case a
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_6
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
⊢ sInf {c | 0 ≤ c ∧ ∀ (x : E), ‖f x‖ ≤ c * ‖x‖} = sInf {x | ∃ (h : 0 ≤ x), ⟨x, h⟩ ∈ {c | ∀ (x : E), ‖f x‖₊ ≤ c * ‖x‖₊}}

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_6
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
⊢ ‖f‖₊ = sInf {c | ∀ (x : E), ‖f x‖₊ ≤ c * ‖x‖₊}

Tactic:
ext

Result:
case a
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_6
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
⊢ ↑‖f‖₊ = ↑(sInf {c | ∀ (x : E), ‖f x‖₊ ≤ c * ‖x‖₊})
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem nonsing_inv_apply_not_isUnit (h : ¬IsUnit A.det) : A⁻¹ = 0

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : ¬IsUnit A.det
⊢ A⁻¹ = 0

Tactic:
rw [inv_def, Ring.inverse_non_unit _ h, zero_smul]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem iteratedFDerivWithin_succ_eq_comp_right {n : ℕ} (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
    iteratedFDerivWithin 𝕜 (n + 1) f s x =
      ((continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm ∘
          iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s)
        x

Proof state:
case H
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
m : Fin (n + 1) → E
⊢ ((iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s x) (init m)) (m (last n)) =
    ((⇑(continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm ∘
          iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s)
        x)
      m

Tactic:
rfl

Result:
no goals

Proof state:
case H
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
m : Fin (n + 1) → E
⊢ (iteratedFDerivWithin 𝕜 (n + 1) f s x) m =
    ((⇑(continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm ∘
          iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s)
        x)
      m

Tactic:
rw [iteratedFDerivWithin_succ_apply_right hs hx]

Result:
case H
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
m : Fin (n + 1) → E
⊢ ((iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s x) (init m)) (m (last n)) =
    ((⇑(continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm ∘
          iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s)
        x)
      m

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 (n + 1) f s x =
    (⇑(continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm ∘ iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s)
      x

Tactic:
ext m

Result:
case H
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
m : Fin (n + 1) → E
⊢ (iteratedFDerivWithin 𝕜 (n + 1) f s x) m =
    ((⇑(continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm ∘
          iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s)
        x)
      m
-- Mathlib/Order/Interval/Set/ProjIcc.lean
theorem range_IicExtend (f : Iic b → β) : range (IicExtend f) = range f

Proof state:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
b : α
f : ↑(Iic b) → β
⊢ range (IicExtend f) = range f

Tactic:
simp only [IicExtend, range_comp f, range_projIic, range_id', image_univ]

Result:
no goals
-- Mathlib/Topology/Compactness/Lindelof.lean
theorem Set.Countable.isLindelof_sUnion {S : Set (Set X)} (hf : S.Countable)
    (hc : ∀ s ∈ S, IsLindelof s) : IsLindelof (⋃₀ S)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hf : S.Countable
hc : ∀ s ∈ S, IsLindelof s
⊢ IsLindelof (⋃₀ S)

Tactic:
rw [sUnion_eq_biUnion]

Result:
X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hf : S.Countable
hc : ∀ s ∈ S, IsLindelof s
⊢ IsLindelof (⋃ i ∈ S, i)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hf : S.Countable
hc : ∀ s ∈ S, IsLindelof s
⊢ IsLindelof (⋃ i ∈ S, i)

Tactic:
exact hf.isLindelof_biUnion hc

Result:
no goals
-- Mathlib/Order/Irreducible.lean
theorem supIrred_iff_not_isMin : SupIrred a ↔ ¬IsMin a :=
  and_iff_left fun _ _ => by simpa only [max_eq_iff] using Or.imp And.left And.left

Proof state:
α : Type u_2
inst✝ : LinearOrder α
a x✝¹ x✝ : α
⊢ x✝¹ ⊔ x✝ = a → x✝¹ = a ∨ x✝ = a

Tactic:
simpa only [max_eq_iff] using Or.imp And.left And.left

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Linear.lean
@[simp]
lemma leftHomologyMap'_smul :
    leftHomologyMap' (a • φ) h₁ h₂ = a • leftHomologyMap' φ h₁ h₂

Proof state:
R : Type u_1
C : Type u_2
inst✝³ : Semiring R
inst✝² : Category.{u_3, u_2} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
a : R
γ : LeftHomologyMapData φ h₁ h₂
⊢ leftHomologyMap' (a • φ) h₁ h₂ = a • leftHomologyMap' φ h₁ h₂

Tactic:
simp only [(γ.smul a).leftHomologyMap'_eq, LeftHomologyMapData.smul_φH, γ.leftHomologyMap'_eq]

Result:
no goals

Proof state:
R : Type u_1
C : Type u_2
inst✝³ : Semiring R
inst✝² : Category.{u_3, u_2} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
a : R
⊢ leftHomologyMap' (a • φ) h₁ h₂ = a • leftHomologyMap' φ h₁ h₂

Tactic:
have γ : LeftHomologyMapData φ h₁ h₂ := default

Result:
R : Type u_1
C : Type u_2
inst✝³ : Semiring R
inst✝² : Category.{u_3, u_2} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
a : R
γ : LeftHomologyMapData φ h₁ h₂
⊢ leftHomologyMap' (a • φ) h₁ h₂ = a • leftHomologyMap' φ h₁ h₂
-- Mathlib/Data/Set/Lattice.lean
theorem prod_iUnion₂ {s : Set α} {t : ∀ i, κ i → Set β} :
    (s ×ˢ ⋃ (i) (j), t i j) = ⋃ (i) (j), s ×ˢ t i j

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
s : Set α
t : (i : ι) → κ i → Set β
⊢ s ×ˢ ⋃ i, ⋃ j, t i j = ⋃ i, ⋃ j, s ×ˢ t i j

Tactic:
simp_rw [prod_iUnion]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem colimit.ι_pre (k : K) : colimit.ι (E ⋙ F) k ≫ colimit.pre F E = colimit.ι F (E.obj k)

Proof state:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimit F
E : K ⥤ J
inst✝ : HasColimit (E ⋙ F)
k : K
⊢ ι (E ⋙ F) k ≫ pre F E = ι F (E.obj k)

Tactic:
erw [IsColimit.fac]

Result:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimit F
E : K ⥤ J
inst✝ : HasColimit (E ⋙ F)
k : K
⊢ (Cocone.whisker E (cocone F)).ι.app k = ι F (E.obj k)

Proof state:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimit F
E : K ⥤ J
inst✝ : HasColimit (E ⋙ F)
k : K
⊢ (Cocone.whisker E (cocone F)).ι.app k = ι F (E.obj k)

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Order/MonotoneConvergence.lean
theorem tendsto_atTop_isLUB (h_mono : Monotone f) (ha : IsLUB (Set.range f) a) :
    Tendsto f atTop (𝓝 a)

Proof state:
α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsLUB (range f) a
⊢ Tendsto f atTop (𝓝 a)

Tactic:
suffices Tendsto (rangeFactorization f) atTop atTop from
  (SupConvergenceClass.tendsto_coe_atTop_isLUB _ _ ha).comp this

Result:
α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsLUB (range f) a
⊢ Tendsto (rangeFactorization f) atTop atTop

Proof state:
α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsLUB (range f) a
⊢ Tendsto (rangeFactorization f) atTop atTop

Tactic:
exact h_mono.rangeFactorization.tendsto_atTop_atTop fun b => b.2.imp fun a ha => ha.ge

Result:
no goals
-- Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
theorem lift_ι_apply {A : Type*} [Semiring A] [Algebra R A] (f : M →ₗ[R] A) (x) :
    lift R f (ι R x) = f x

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
x : M
⊢ ((lift R) f) ((ι R) x) = f x

Tactic:
conv_rhs => rw [← ι_comp_lift f]

Result:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
x : M
⊢ ((lift R) f) ((ι R) x) = (((lift R) f).toLinearMap ∘ₗ ι R) x

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
x : M
⊢ ((lift R) f) ((ι R) x) = (((lift R) f).toLinearMap ∘ₗ ι R) x

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/ZMod/IntUnitsPower.lean
@[norm_cast] lemma uzpow_intCast (u : ℤˣ) (z : ℤ) : u ^ (z : R) = u ^ z

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Module R (Additive ℤˣ)
u : ℤˣ
z : ℤ
⊢ Additive.toMul (↑z • Additive.ofMul u) = u ^ z

Tactic:
rw [Int.cast_smul_eq_zsmul, toMul_zsmul, toMul_ofMul]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Module R (Additive ℤˣ)
u : ℤˣ
z : ℤ
⊢ u ^ ↑z = u ^ z

Tactic:
change ((z : R) • Additive.ofMul u).toMul = _

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Module R (Additive ℤˣ)
u : ℤˣ
z : ℤ
⊢ Additive.toMul (↑z • Additive.ofMul u) = u ^ z
-- Mathlib/Data/List/Basic.lean
theorem get_length_sub_one {l : List α} (h : l.length - 1 < l.length) :
    l.get ⟨l.length - 1, h⟩ = l.getLast (by rintro rfl; exact Nat.lt_irrefl 0 h) :=
  (getLast_eq_getElem l _).symm

Proof state:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l₁ l₂ l : List α
h : l.length - 1 < l.length
⊢ l ≠ []

Tactic:
rintro rfl

Result:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l₁ l₂ : List α
h : [].length - 1 < [].length
⊢ False

Proof state:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l₁ l₂ : List α
h : [].length - 1 < [].length
⊢ False

Tactic:
exact Nat.lt_irrefl 0 h

Result:
no goals
-- Mathlib/Algebra/Ring/BooleanRing.lean
theorem ofBoolAlg_symmDiff (a b : AsBoolAlg α) : ofBoolAlg (a ∆ b) = ofBoolAlg a + ofBoolAlg b

Proof state:
α : Type u_1
inst✝ : BooleanRing α
a b : AsBoolAlg α
⊢ ofBoolAlg ((a ⊔ b) \ (a ⊓ b)) = ofBoolAlg a + ofBoolAlg b

Tactic:
exact of_boolalg_symmDiff_aux _ _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BooleanRing α
a b : AsBoolAlg α
⊢ ofBoolAlg (a ∆ b) = ofBoolAlg a + ofBoolAlg b

Tactic:
rw [symmDiff_eq_sup_sdiff_inf]

Result:
α : Type u_1
inst✝ : BooleanRing α
a b : AsBoolAlg α
⊢ ofBoolAlg ((a ⊔ b) \ (a ⊓ b)) = ofBoolAlg a + ofBoolAlg b
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filterMap_eq_map (f : α → β) : filterMap (some ∘ f) = map f

Proof state:
α : Type u_1
β : Type u_2
f : α → β
⊢ (fun as => filterMap (some ∘ f) as) = map f

Tactic:
funext l

Result:
case h
α : Type u_1
β : Type u_2
f : α → β
l : Array α
⊢ filterMap (some ∘ f) l = map f l

Proof state:
case h.mk
α : Type u_1
β : Type u_2
f : α → β
toList✝ : List α
⊢ filterMap (some ∘ f) { toList := toList✝ } = map f { toList := toList✝ }

Tactic:
simp

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → β
l : Array α
⊢ filterMap (some ∘ f) l = map f l

Tactic:
cases l

Result:
case h.mk
α : Type u_1
β : Type u_2
f : α → β
toList✝ : List α
⊢ filterMap (some ∘ f) { toList := toList✝ } = map f { toList := toList✝ }
-- Mathlib/Algebra/Module/Submodule/Bilinear.lean
theorem map₂_span_singleton_eq_map_flip (f : M →ₗ[R] N →ₗ[R] P) (s : Submodule R M) (n : N) :
    map₂ f s (span R {n}) = map (f.flip n) s

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Submodule R M
n : N
⊢ map₂ f s (span R {n}) = map (f.flip n) s

Tactic:
rw [← map₂_span_singleton_eq_map, map₂_flip]

Result:
no goals
-- Mathlib/NumberTheory/MulChar/Basic.lean
theorem IsQuadratic.sq_eq_one {χ : MulChar R R'} (hχ : χ.IsQuadratic) : χ ^ 2 = 1

Proof state:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
⊢ χ ^ 2 = 1

Tactic:
rw [← inv_mul_cancel χ, pow_two, hχ.inv]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
theorem isUniformEmbedding_subtypeEmb (p : α → Prop) {e : α → β} (ue : IsUniformEmbedding e)
    (de : IsDenseEmbedding e) : IsUniformEmbedding (IsDenseEmbedding.subtypeEmb p e) :=
  { comap_uniformity

Proof state:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
p : α → Prop
e : α → β
ue : IsUniformEmbedding e
de : IsDenseEmbedding e
⊢ comap (fun x => (IsDenseEmbedding.subtypeEmb p e x.1, IsDenseEmbedding.subtypeEmb p e x.2))
      (𝓤 { x // x ∈ closure (e '' {x | p x}) }) =
    𝓤 { x // p x }

Tactic:
simp [comap_comap, Function.comp_def, IsDenseEmbedding.subtypeEmb, uniformity_subtype,
  ue.comap_uniformity.symm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem ite_then_decide_self (p : Prop) [h : Decidable p] {w : Decidable p} (q : Bool) :
    (@ite _ p h (decide p) q) = (decide p || q)

Proof state:
p : Prop
h w : Decidable p
q : Bool
⊢ (if p then decide p else q) = (decide p || q)

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Order/Interval/Set/WithBotTop.lean
theorem image_coe_Ioi : (some : α → WithBot α) '' Ioi a = Ioi (a : WithBot α)

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ some '' Ioi a = Ioi ↑a

Tactic:
rw [← preimage_coe_Ioi, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left (Ioi_subset_Ioi bot_le)]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Operations.lean
theorem eq_bot_iff_forall : S = ⊥ ↔ ∀ x ∈ S, x = (1 : M) :=
  SetLike.ext_iff.trans <| by simp +contextual [iff_def, S.one_mem]

Proof state:
M : Type u_1
inst✝ : MulOneClass M
S : Submonoid M
⊢ (∀ (x : M), x ∈ S ↔ x ∈ ⊥) ↔ ∀ x ∈ S, x = 1

Tactic:
simp +contextual [iff_def, S.one_mem]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Inversion/Calculus.lean
theorem DifferentiableAt.inversion (hc : DifferentiableAt ℝ c a)
    (hR : DifferentiableAt ℝ R a) (hx : DifferentiableAt ℝ x a) (hne : x a ≠ c a) :
    DifferentiableAt ℝ (fun a ↦ inversion (c a) (R a) (x a)) a

Proof state:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
c x : E → F
R : E → ℝ
a : E
hc : DifferentiableWithinAt ℝ c univ a
hR : DifferentiableWithinAt ℝ R univ a
hx : DifferentiableWithinAt ℝ x univ a
hne : x a ≠ c a
⊢ DifferentiableWithinAt ℝ (fun a => inversion (c a) (R a) (x a)) univ a

Tactic:
exact hc.inversion hR hx hne

Result:
no goals

Proof state:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
c x : E → F
R : E → ℝ
a : E
hc : DifferentiableAt ℝ c a
hR : DifferentiableAt ℝ R a
hx : DifferentiableAt ℝ x a
hne : x a ≠ c a
⊢ DifferentiableAt ℝ (fun a => inversion (c a) (R a) (x a)) a

Tactic:
rw [← differentiableWithinAt_univ] at *

Result:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
c x : E → F
R : E → ℝ
a : E
hc : DifferentiableWithinAt ℝ c univ a
hR : DifferentiableWithinAt ℝ R univ a
hx : DifferentiableWithinAt ℝ x univ a
hne : x a ≠ c a
⊢ DifferentiableWithinAt ℝ (fun a => inversion (c a) (R a) (x a)) univ a
-- Mathlib/Analysis/SpecialFunctions/Log/NegMulLog.lean
@[fun_prop] lemma continuous_negMulLog : Continuous negMulLog

Proof state:
⊢ Continuous negMulLog

Tactic:
simpa only [negMulLog_eq_neg] using continuous_mul_log.neg

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem div_le_one (hb : 0 < b) : a / b ≤ 1 ↔ a ≤ b

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a b : α
hb : 0 < b
⊢ a / b ≤ 1 ↔ a ≤ b

Tactic:
rw [div_le_iff₀ hb, one_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldr_congr {as bs : Vector α n} (h₀ : as = bs) {f g : α → β → β} (h₁ : f = g)
     {a b : β} (h₂ : a = b) :
    as.foldr f a = bs.foldr g b

Proof state:
α : Type u_1
n : Nat
β : Type u_2
as bs : Vector α n
h₀ : as = bs
f g : α → β → β
h₁ : f = g
a b : β
h₂ : a = b
⊢ foldr f a as = foldr g b bs

Tactic:
congr

Result:
no goals
-- Mathlib/Data/List/Duplicate.lean
theorem nodup_iff_forall_not_duplicate : Nodup l ↔ ∀ x : α, ¬x ∈+ l

Proof state:
α : Type u_1
l : List α
⊢ l.Nodup ↔ ∀ (x : α), ¬x ∈+ l

Tactic:
simp_rw [nodup_iff_sublist, duplicate_iff_sublist]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem characteristic_iff_le_map : H.Characteristic ↔ ∀ ϕ : G ≃* G, H ≤ H.map ϕ.toMonoidHom

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), H ≤ comap ϕ.symm.toMonoidHom H

Tactic:
exact characteristic_iff_le_comap.trans ⟨fun h ϕ => h ϕ.symm, fun h ϕ => h ϕ.symm⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), H ≤ map ϕ.toMonoidHom H

Tactic:
simp_rw [map_equiv_eq_comap_symm']

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), H ≤ comap ϕ.symm.toMonoidHom H
-- Mathlib/GroupTheory/Sylow.lean
theorem ne_bot_of_dvd_card [Finite G] {p : ℕ} [hp : Fact p.Prime] (P : Sylow p G)
    (hdvd : p ∣ Nat.card G) : (P : Subgroup G) ≠ ⊥

Proof state:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Nat.card G
h : ↑P = ⊥
⊢ p ∣ 1

Tactic:
have key : p ∣ Nat.card P := P.dvd_card_of_dvd_card hdvd

Result:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Nat.card G
h : ↑P = ⊥
key : p ∣ Nat.card ↥↑P
⊢ p ∣ 1

Proof state:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Nat.card G
h : ↑P = ⊥
key : p ∣ Nat.card ↥↑P
⊢ p ∣ 1

Tactic:
rwa [h, card_bot] at key

Result:
no goals

Proof state:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Nat.card G
⊢ ↑P ≠ ⊥

Tactic:
refine fun h => hp.out.not_dvd_one ?_

Result:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Nat.card G
h : ↑P = ⊥
⊢ p ∣ 1