harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Quotient/Basic.lean
theorem range_eq_top_of_cancel {f : M →ₛₗ[τ₁₂] M₂}
    (h : ∀ u v : M₂ →ₗ[R₂] M₂ ⧸ (range f), u.comp f = v.comp f → u = v) : range f = ⊤

Proof state:
R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : M₂ →ₗ[R₂] M₂ ⧸ range f), u.comp f = v.comp f → u = v
⊢ range f = ⊤

Tactic:
have h₁ : (0 : M₂ →ₗ[R₂] M₂ ⧸ (range f)).comp f = 0 := zero_comp _

Result:
R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : M₂ →ₗ[R₂] M₂ ⧸ range f), u.comp f = v.comp f → u = v
h₁ : comp 0 f = 0
⊢ range f = ⊤

Proof state:
R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : M₂ →ₗ[R₂] M₂ ⧸ range f), u.comp f = v.comp f → u = v
h₁ : comp 0 f = 0
⊢ range f = ⊤

Tactic:
rw [← Submodule.ker_mkQ (range f), ← h 0 f.range.mkQ (Eq.trans h₁ (range_mkQ_comp _).symm)]

Result:
R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : M₂ →ₗ[R₂] M₂ ⧸ range f), u.comp f = v.comp f → u = v
h₁ : comp 0 f = 0
⊢ ker 0 = ⊤

Proof state:
R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : M₂ →ₗ[R₂] M₂ ⧸ range f), u.comp f = v.comp f → u = v
h₁ : comp 0 f = 0
⊢ ker 0 = ⊤

Tactic:
exact ker_zero

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Mates.lean
theorem mateEquiv_hcomp (α : TwoSquare G L₁ L₂ H) (β : TwoSquare H L₃ L₄ K) :
    (mateEquiv (adj₁.comp adj₃) (adj₂.comp adj₄)) (α ≫ᵥ β) =
      (mateEquiv adj₃ adj₄ β) ≫ₕ (mateEquiv adj₁ adj₂ α)

Proof state:
case h
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
inst✝² : Category.{v₄, u₄} D
inst✝¹ : Category.{v₅, u₅} E
inst✝ : Category.{v₆, u₆} F
G : A ⥤ D
H : B ⥤ E
K : C ⥤ F
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : D ⥤ E
R₂ : E ⥤ D
L₃ : B ⥤ C
R₃ : C ⥤ B
L₄ : E ⥤ F
R₄ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
adj₄ : L₄ ⊣ R₄
α : TwoSquare G L₁ L₂ H
β : TwoSquare H L₃ L₄ K
c : C
⊢ adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
      R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫
        R₂.map (R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c))))) ≫
          R₂.map (R₄.map (β.natTrans.app (L₁.obj (R₁.obj (R₃.obj c))))) ≫
            R₂.map (R₄.map (K.map (L₃.map (adj₁.counit.app (R₃.obj c))))) ≫
              R₂.map (R₄.map (K.map (adj₃.counit.app c))) =
    adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
      R₂.map (α.natTrans.app (R₁.obj (R₃.obj c))) ≫
        R₂.map (H.map (adj₁.counit.app (R₃.obj c))) ≫
          R₂.map (adj₄.unit.app (H.obj (R₃.obj c))) ≫
            R₂.map (R₄.map (β.natTrans.app (R₃.obj c))) ≫ R₂.map (R₄.map (K.map (adj₃.counit.app c)))

Tactic:
slice_rhs 2 4 =>
  rw [← R₂.map_comp, ← R₂.map_comp, ← assoc, ← unit_naturality (adj₄)]

Result:
case h
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
inst✝² : Category.{v₄, u₄} D
inst✝¹ : Category.{v₅, u₅} E
inst✝ : Category.{v₆, u₆} F
G : A ⥤ D
H : B ⥤ E
K : C ⥤ F
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : D ⥤ E
R₂ : E ⥤ D
L₃ : B ⥤ C
R₃ : C ⥤ B
L₄ : E ⥤ F
R₄ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
adj₄ : L₄ ⊣ R₄
α : TwoSquare G L₁ L₂ H
β : TwoSquare H L₃ L₄ K
c : C
⊢ adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
      R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫
        R₂.map (R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c))))) ≫
          R₂.map (R₄.map (β.natTrans.app (L₁.obj (R₁.obj (R₃.obj c))))) ≫
            R₂.map (R₄.map (K.map (L₃.map (adj₁.counit.app (R₃.obj c))))) ≫
              R₂.map (R₄.map (K.map (adj₃.counit.app c))) =
    adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
      (R₂.map
            (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c)))) ≫
              R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c)) ≫ H.map (adj₁.counit.app (R₃.obj c))))) ≫
          R₂.map (R₄.map (β.natTrans.app (R₃.obj c)))) ≫
        R₂.map (R₄.map (K.map (adj₃.counit.app c)))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldlM_empty [Monad m] (f : β → α → m β) (init : β) :
    foldlM f init #v[] = return init

Proof state:
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
init : β
⊢ foldlM f init { toArray := #[], size_toArray := ⋯ } = pure init

Tactic:
simp [foldlM]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem cond_true_right  : ∀(c t : Bool), cond c t true  = (!c || t)

Proof state:
⊢ ∀ (c t : Bool), (bif c then t else true) = (!c || t)

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/Group/Action/Defs.lean
lemma SMulCommClass.of_commMonoid
    (A B G : Type*) [CommMonoid G] [SMul A G] [SMul B G]
    [IsScalarTower A G G] [IsScalarTower B G G] :
    SMulCommClass A B G where
  smul_comm r s x

Proof state:
A : Type u_9
B : Type u_10
G : Type u_11
inst✝⁴ : CommMonoid G
inst✝³ : SMul A G
inst✝² : SMul B G
inst✝¹ : IsScalarTower A G G
inst✝ : IsScalarTower B G G
r : A
s : B
x : G
⊢ r • s • x = s • r • x

Tactic:
rw [← one_smul G (s • x), ← smul_assoc, ← one_smul G x, ← smul_assoc s 1 x,
  smul_comm, smul_assoc, one_smul, smul_assoc, one_smul]

Result:
no goals
-- Mathlib/Order/Cofinal.lean
theorem BddAbove.of_not_isCofinal {s : Set α} (h : ¬ IsCofinal s) : BddAbove s

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
h : ¬IsCofinal s
⊢ BddAbove s

Tactic:
rw [not_isCofinal_iff] at h

Result:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
h : ∃ x, ∀ y ∈ s, y < x
⊢ BddAbove s

Proof state:
case intro
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : α
h : ∀ y ∈ s, y < x
⊢ BddAbove s

Tactic:
exact ⟨x, fun y hy ↦ (h y hy).le⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
h : ∃ x, ∀ y ∈ s, y < x
⊢ BddAbove s

Tactic:
obtain ⟨x, h⟩ := h

Result:
case intro
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : α
h : ∀ y ∈ s, y < x
⊢ BddAbove s
-- Mathlib/Algebra/Lie/Weights/Basic.lean
theorem coe_genWeightSpace_of_top (χ : L → R) :
    (genWeightSpace M (χ ∘ (⊤ : LieSubalgebra R L).incl) : Submodule R M) = genWeightSpace M χ

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝ : LieRing.IsNilpotent L
χ : L → R
⊢ ↑(genWeightSpace M (χ ∘ ⇑⊤.incl)) = ↑(genWeightSpace M χ)

Tactic:
ext m

Result:
case h
R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝ : LieRing.IsNilpotent L
χ : L → R
m : M
⊢ m ∈ ↑(genWeightSpace M (χ ∘ ⇑⊤.incl)) ↔ m ∈ ↑(genWeightSpace M χ)

Proof state:
case h.h
R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝ : LieRing.IsNilpotent L
χ : L → R
m : M
⊢ ∀ (a : L),
    (∀ (b : a ∈ ⊤), ∃ k, (((toEnd R (↥⊤) M) ⟨a, b⟩ - (χ ∘ ⇑⊤.incl) ⟨a, b⟩ • 1) ^ k) m = 0) ↔
      ∃ k, (((toEnd R L M) a - χ a • 1) ^ k) m = 0

Tactic:
simp

Result:
no goals

Proof state:
case h
R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝ : LieRing.IsNilpotent L
χ : L → R
m : M
⊢ (∀ (a : L) (b : a ∈ ⊤), ∃ k, (((toEnd R (↥⊤) M) ⟨a, b⟩ - (χ ∘ ⇑⊤.incl) ⟨a, b⟩ • 1) ^ k) m = 0) ↔
    ∀ (x : L), ∃ k, (((toEnd R L M) x - χ x • 1) ^ k) m = 0

Tactic:
apply forall_congr'

Result:
case h.h
R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝ : LieRing.IsNilpotent L
χ : L → R
m : M
⊢ ∀ (a : L),
    (∀ (b : a ∈ ⊤), ∃ k, (((toEnd R (↥⊤) M) ⟨a, b⟩ - (χ ∘ ⇑⊤.incl) ⟨a, b⟩ • 1) ^ k) m = 0) ↔
      ∃ k, (((toEnd R L M) a - χ a • 1) ^ k) m = 0

Proof state:
case h
R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝ : LieRing.IsNilpotent L
χ : L → R
m : M
⊢ m ∈ ↑(genWeightSpace M (χ ∘ ⇑⊤.incl)) ↔ m ∈ ↑(genWeightSpace M χ)

Tactic:
simp only [mem_genWeightSpace, LieSubmodule.mem_toSubmodule, Subtype.forall]

Result:
case h
R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝ : LieRing.IsNilpotent L
χ : L → R
m : M
⊢ (∀ (a : L) (b : a ∈ ⊤), ∃ k, (((toEnd R (↥⊤) M) ⟨a, b⟩ - (χ ∘ ⇑⊤.incl) ⟨a, b⟩ • 1) ^ k) m = 0) ↔
    ∀ (x : L), ∃ k, (((toEnd R L M) x - χ x • 1) ^ k) m = 0
-- Mathlib/Topology/Compactness/Lindelof.lean
theorem LindelofSpace.of_continuous_surjective {f : X → Y} [LindelofSpace X] (hf : Continuous f)
    (hsur : Function.Surjective f) : LindelofSpace Y where
  isLindelof_univ

Proof state:
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : LindelofSpace X
hf : Continuous f
hsur : Function.Surjective f
⊢ IsLindelof (f '' univ)

Tactic:
exact IsLindelof.image (isLindelof_univ_iff.mpr ‹_›) hf

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : LindelofSpace X
hf : Continuous f
hsur : Function.Surjective f
⊢ IsLindelof univ

Tactic:
rw [← Set.image_univ_of_surjective hsur]

Result:
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : LindelofSpace X
hf : Continuous f
hsur : Function.Surjective f
⊢ IsLindelof (f '' univ)
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
theorem Module.finrank_zero_of_subsingleton [Subsingleton M] :
    finrank R M = 0

Proof state:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : Subsingleton M
⊢ finrank R M = 0

Tactic:
rw [finrank, rank_subsingleton', _root_.map_zero]

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
@[simp]
lemma natCast_lt_toNNReal {r : ℝ} {n : ℕ} : n < r.toNNReal ↔ n < r

Proof state:
r : ℝ
n : ℕ
⊢ ↑n < r.toNNReal ↔ ↑n < r

Tactic:
simpa only [not_le] using toNNReal_le_natCast.not

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem coeFn_abs {β} [TopologicalSpace β] [Lattice β] [TopologicalLattice β] [AddGroup β]
    [IsTopologicalAddGroup β] (f : α →ₘ[μ] β) : ⇑|f| =ᵐ[μ] fun x => |f x|

Proof state:
case h
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝⁴ : TopologicalSpace β
inst✝³ : Lattice β
inst✝² : TopologicalLattice β
inst✝¹ : AddGroup β
inst✝ : IsTopologicalAddGroup β
f : α →ₘ[μ] β
x : α
hx_sup : ↑(f ⊔ -f) x = ↑f x ⊔ ↑(-f) x
hx_neg : ↑(-f) x = (-↑f) x
⊢ ↑(f ⊔ -f) x = ↑f x ⊔ -↑f x

Tactic:
rw [hx_sup, hx_neg, Pi.neg_apply]

Result:
no goals

Proof state:
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝⁴ : TopologicalSpace β
inst✝³ : Lattice β
inst✝² : TopologicalLattice β
inst✝¹ : AddGroup β
inst✝ : IsTopologicalAddGroup β
f : α →ₘ[μ] β
⊢ ↑(f ⊔ -f) =ᶠ[ae μ] fun x => ↑f x ⊔ -↑f x

Tactic:
filter_upwards [AEEqFun.coeFn_sup f (-f), AEEqFun.coeFn_neg f] with x hx_sup hx_neg

Result:
case h
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝⁴ : TopologicalSpace β
inst✝³ : Lattice β
inst✝² : TopologicalLattice β
inst✝¹ : AddGroup β
inst✝ : IsTopologicalAddGroup β
f : α →ₘ[μ] β
x : α
hx_sup : ↑(f ⊔ -f) x = ↑f x ⊔ ↑(-f) x
hx_neg : ↑(-f) x = (-↑f) x
⊢ ↑(f ⊔ -f) x = ↑f x ⊔ -↑f x

Proof state:
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝⁴ : TopologicalSpace β
inst✝³ : Lattice β
inst✝² : TopologicalLattice β
inst✝¹ : AddGroup β
inst✝ : IsTopologicalAddGroup β
f : α →ₘ[μ] β
⊢ ↑|f| =ᶠ[ae μ] fun x => |↑f x|

Tactic:
simp_rw [abs]

Result:
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝⁴ : TopologicalSpace β
inst✝³ : Lattice β
inst✝² : TopologicalLattice β
inst✝¹ : AddGroup β
inst✝ : IsTopologicalAddGroup β
f : α →ₘ[μ] β
⊢ ↑(f ⊔ -f) =ᶠ[ae μ] fun x => ↑f x ⊔ -↑f x
-- Mathlib/NumberTheory/Rayleigh.lean
theorem hit_or_miss (h : r > 0) :
    j ∈ {beattySeq r k | k} ∨ ∃ k : ℤ, k < j / r ∧ (j + 1) / r ≤ k + 1

Proof state:
case inl
r : ℝ
j : ℤ
h : r > 0
h✝ : (↑⌈(↑j + 1) / r⌉ - 1) * r < ↑j
⊢ ↑(⌈(↑j + 1) / r⌉ - 1) < ↑j / r ∧ (↑j + 1) / r ≤ ↑(⌈(↑j + 1) / r⌉ - 1) + 1

Tactic:
rw [Int.cast_sub, Int.cast_one, lt_div_iff₀ h, sub_add_cancel]

Result:
case inl
r : ℝ
j : ℤ
h : r > 0
h✝ : (↑⌈(↑j + 1) / r⌉ - 1) * r < ↑j
⊢ (↑⌈(↑j + 1) / r⌉ - 1) * r < ↑j ∧ (↑j + 1) / r ≤ ↑⌈(↑j + 1) / r⌉

Proof state:
r : ℝ
j : ℤ
h : r > 0
⊢ j ∈ {x | ∃ k, beattySeq r k = x} ∨ ∃ k, ↑k < ↑j / r ∧ (↑j + 1) / r ≤ ↑k + 1

Tactic:
cases lt_or_ge ((⌈(j + 1) / r⌉ - 1) * r) j

Result:
case inl
r : ℝ
j : ℤ
h : r > 0
h✝ : (↑⌈(↑j + 1) / r⌉ - 1) * r < ↑j
⊢ j ∈ {x | ∃ k, beattySeq r k = x} ∨ ∃ k, ↑k < ↑j / r ∧ (↑j + 1) / r ≤ ↑k + 1

case inr
r : ℝ
j : ℤ
h : r > 0
h✝ : (↑⌈(↑j + 1) / r⌉ - 1) * r ≥ ↑j
⊢ j ∈ {x | ∃ k, beattySeq r k = x} ∨ ∃ k, ↑k < ↑j / r ∧ (↑j + 1) / r ≤ ↑k + 1

Proof state:
case inl
r : ℝ
j : ℤ
h : r > 0
h✝ : (↑⌈(↑j + 1) / r⌉ - 1) * r < ↑j
⊢ j ∈ {x | ∃ k, beattySeq r k = x} ∨ ∃ k, ↑k < ↑j / r ∧ (↑j + 1) / r ≤ ↑k + 1

Tactic:
refine Or.inr ⟨⌈(j + 1) / r⌉ - 1, ?_⟩

Result:
case inl
r : ℝ
j : ℤ
h : r > 0
h✝ : (↑⌈(↑j + 1) / r⌉ - 1) * r < ↑j
⊢ ↑(⌈(↑j + 1) / r⌉ - 1) < ↑j / r ∧ (↑j + 1) / r ≤ ↑(⌈(↑j + 1) / r⌉ - 1) + 1

Proof state:
case inr
r : ℝ
j : ℤ
h : r > 0
h✝ : (↑⌈(↑j + 1) / r⌉ - 1) * r ≥ ↑j
⊢ beattySeq r (⌈(↑j + 1) / r⌉ - 1) = j

Tactic:
rw [beattySeq, Int.floor_eq_iff, Int.cast_sub, Int.cast_one, ← lt_div_iff₀ h, sub_lt_iff_lt_add]

Result:
case inr
r : ℝ
j : ℤ
h : r > 0
h✝ : (↑⌈(↑j + 1) / r⌉ - 1) * r ≥ ↑j
⊢ ↑j ≤ (↑⌈(↑j + 1) / r⌉ - 1) * r ∧ ↑⌈(↑j + 1) / r⌉ < (↑j + 1) / r + 1

Proof state:
case inr
r : ℝ
j : ℤ
h : r > 0
h✝ : (↑⌈(↑j + 1) / r⌉ - 1) * r ≥ ↑j
⊢ ↑j ≤ (↑⌈(↑j + 1) / r⌉ - 1) * r ∧ ↑⌈(↑j + 1) / r⌉ < (↑j + 1) / r + 1

Tactic:
exact ⟨‹_›, Int.ceil_lt_add_one _⟩

Result:
no goals

Proof state:
case inr
r : ℝ
j : ℤ
h : r > 0
h✝ : (↑⌈(↑j + 1) / r⌉ - 1) * r ≥ ↑j
⊢ j ∈ {x | ∃ k, beattySeq r k = x} ∨ ∃ k, ↑k < ↑j / r ∧ (↑j + 1) / r ≤ ↑k + 1

Tactic:
refine Or.inl ⟨⌈(j + 1) / r⌉ - 1, ?_⟩

Result:
case inr
r : ℝ
j : ℤ
h : r > 0
h✝ : (↑⌈(↑j + 1) / r⌉ - 1) * r ≥ ↑j
⊢ beattySeq r (⌈(↑j + 1) / r⌉ - 1) = j

Proof state:
case inl
r : ℝ
j : ℤ
h : r > 0
h✝ : (↑⌈(↑j + 1) / r⌉ - 1) * r < ↑j
⊢ (↑⌈(↑j + 1) / r⌉ - 1) * r < ↑j ∧ (↑j + 1) / r ≤ ↑⌈(↑j + 1) / r⌉

Tactic:
exact ⟨‹_›, Int.le_ceil _⟩

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem T_eval_one (n : ℤ) : (T R n).eval 1 = 1

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ eval 1 (T R n) = 1

Tactic:
induction n using Polynomial.Chebyshev.induct with
| zero => simp
| one => simp
| add_two n ih1 ih2 => simp [T_add_two, ih1, ih2]; norm_num
| neg_add_one n ih1 ih2 => simp [T_sub_one, -T_neg, ih1, ih2]; norm_num

Result:
no goals

Proof state:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 1 (T R (↑n + 1)) = 1
ih2 : eval 1 (T R ↑n) = 1
⊢ eval 1 (T R (↑n + 2)) = 1

Tactic:
simp [T_add_two, ih1, ih2]

Result:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 1 (T R (↑n + 1)) = 1
ih2 : eval 1 (T R ↑n) = 1
⊢ 2 - 1 = 1

Proof state:
case one
R : Type u_1
inst✝ : CommRing R
⊢ eval 1 (T R 1) = 1

Tactic:
simp

Result:
no goals

Proof state:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 1 (T R (↑n + 1)) = 1
ih2 : eval 1 (T R ↑n) = 1
⊢ 2 - 1 = 1

Tactic:
norm_num

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝ : CommRing R
⊢ eval 1 (T R 0) = 1

Tactic:
simp

Result:
no goals

Proof state:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 1 (T R (-↑n)) = 1
ih2 : eval 1 (T R (-↑n + 1)) = 1
⊢ eval 1 (T R (-↑n - 1)) = 1

Tactic:
simp [T_sub_one, -T_neg, ih1, ih2]

Result:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 1 (T R (-↑n)) = 1
ih2 : eval 1 (T R (-↑n + 1)) = 1
⊢ 2 - 1 = 1

Proof state:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 1 (T R (-↑n)) = 1
ih2 : eval 1 (T R (-↑n + 1)) = 1
⊢ 2 - 1 = 1

Tactic:
norm_num

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
theorem exp_bound' {x : ℂ} {n : ℕ} (hx : ‖x‖ / n.succ ≤ 1 / 2) :
    ‖exp x - ∑ m ∈ range n, x ^ m / m.factorial‖ ≤ ‖x‖ ^ n / n.factorial * 2

Proof state:
case calc_3.h
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ∑ i ∈ range k, ‖x‖ ^ i / ↑n.succ ^ i ≤ 2

Tactic:
simp_rw [← div_pow]

Result:
case calc_3.h
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ∑ x_1 ∈ range k, (‖x‖ / ↑n.succ) ^ x_1 ≤ 2

Proof state:
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ∑ i ∈ range k, ‖x ^ (n + i) / ↑(n + i).factorial‖ ≤ ∑ i ∈ range k, ‖x‖ ^ (n + i) / ↑(n + i).factorial

Tactic:
simp [norm_natCast, Complex.norm_pow]

Result:
no goals

Proof state:
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj : j ≥ n
k : ℕ := j - n
⊢ ‖∑ m ∈ range j, x ^ m / ↑m.factorial - ∑ m ∈ range n, x ^ m / ↑m.factorial‖ ≤ ‖x‖ ^ n / ↑n.factorial * 2

Tactic:
have hj : j = n + k := (add_tsub_cancel_of_le hj).symm

Result:
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ‖∑ m ∈ range j, x ^ m / ↑m.factorial - ∑ m ∈ range n, x ^ m / ↑m.factorial‖ ≤ ‖x‖ ^ n / ↑n.factorial * 2

Proof state:
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ 2 * (‖x‖ / ↑n.succ - 1) ≤ -1

Tactic:
linarith

Result:
no goals

Proof state:
case calc_3.h
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ 2 * (‖x‖ / ↑n.succ - 1) ≤ (‖x‖ / ↑n.succ) ^ k - 1

Tactic:
trans (-1 : ℝ)

Result:
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ 2 * (‖x‖ / ↑n.succ - 1) ≤ -1

x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ -1 ≤ (‖x‖ / ↑n.succ) ^ k - 1
-- Mathlib/Data/List/GetD.lean
theorem getI_eq_iget_getElem? (n : ℕ) : l.getI n = l[n]?.iget

Proof state:
α : Type u
l : List α
inst✝ : Inhabited α
n : ℕ
⊢ l.getI n = l[n]?.iget

Tactic:
rw [← getD_default_eq_getI, getD_eq_getD_getElem?, Option.getD_default_eq_iget]

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem _root_.map_finset_inf' [SemilatticeInf β] [FunLike F α β] [InfHomClass F α β]
    (f : F) {s : Finset ι} (hs) (g : ι → α) :
    f (s.inf' hs g) = s.inf' hs (f ∘ g)

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝³ : SemilatticeInf α
inst✝² : SemilatticeInf β
inst✝¹ : FunLike F α β
inst✝ : InfHomClass F α β
f : F
s : Finset ι
hs : s.Nonempty
g : ι → α
⊢ f (s.inf' hs g) = s.inf' hs (⇑f ∘ g)

Tactic:
refine hs.cons_induction ?_ ?_ <;> intros <;> simp [*]

Result:
no goals
-- Mathlib/Data/Fintype/Defs.lean
theorem coe_eq_univ : (s : Set α) = Set.univ ↔ s = univ

Proof state:
α : Type u_1
inst✝ : Fintype α
s : Finset α
⊢ ↑s = Set.univ ↔ s = univ

Tactic:
rw [← coe_univ, coe_inj]

Result:
no goals
-- Mathlib/Data/PNat/Factors.lean
theorem coeNat_prime (v : PrimeMultiset) (p : ℕ) (h : p ∈ (v : Multiset ℕ)) : p.Prime

Proof state:
case intro.mk.intro
v : PrimeMultiset
p : ℕ
h : p ∈ v.toNatMultiset
val✝ : ℕ
hp' : Nat.Prime val✝
left✝ : ⟨val✝, hp'⟩ ∈ v
h_eq : Coe.coe ⟨val✝, hp'⟩ = p
⊢ Nat.Prime p

Tactic:
exact h_eq ▸ hp'

Result:
no goals

Proof state:
v : PrimeMultiset
p : ℕ
h : p ∈ v.toNatMultiset
⊢ Nat.Prime p

Tactic:
rcases Multiset.mem_map.mp h with ⟨⟨_, hp'⟩, ⟨_, h_eq⟩⟩

Result:
case intro.mk.intro
v : PrimeMultiset
p : ℕ
h : p ∈ v.toNatMultiset
val✝ : ℕ
hp' : Nat.Prime val✝
left✝ : ⟨val✝, hp'⟩ ∈ v
h_eq : Coe.coe ⟨val✝, hp'⟩ = p
⊢ Nat.Prime p
-- Mathlib/Data/List/InsertIdx.lean
theorem eraseIdx_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (hl : ∀ a ∈ l, p a) (n : ℕ) :
    (pmap f l hl).eraseIdx n = (l.eraseIdx n).pmap f fun a ha ↦ hl a (eraseIdx_subset _ _ ha) :=
  match l, hl, n with
  | [], _, _ => rfl
  | a :: _, _, 0 => rfl
  | a :: as, h, n + 1 => by rw [forall_mem_cons] at h; simp [eraseIdx_pmap f h.2 n]

Proof state:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
l : List α
hl : ∀ (a : α), a ∈ l → p a
n✝ : ℕ
a : α
as : List α
h : ∀ (a_1 : α), a_1 ∈ a :: as → p a_1
n : ℕ
⊢ (pmap f (a :: as) h).eraseIdx (n + 1) = pmap f ((a :: as).eraseIdx (n + 1)) ⋯

Tactic:
rw [forall_mem_cons] at h

Result:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
l : List α
hl : ∀ (a : α), a ∈ l → p a
n✝ : ℕ
a : α
as : List α
h✝ : ∀ (a_1 : α), a_1 ∈ a :: as → p a_1
h : p a ∧ ∀ (x : α), x ∈ as → p x
n : ℕ
⊢ (pmap f (a :: as) h✝).eraseIdx (n + 1) = pmap f ((a :: as).eraseIdx (n + 1)) ⋯

Proof state:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
l : List α
hl : ∀ (a : α), a ∈ l → p a
n✝ : ℕ
a : α
as : List α
h✝ : ∀ (a_1 : α), a_1 ∈ a :: as → p a_1
h : p a ∧ ∀ (x : α), x ∈ as → p x
n : ℕ
⊢ (pmap f (a :: as) h✝).eraseIdx (n + 1) = pmap f ((a :: as).eraseIdx (n + 1)) ⋯

Tactic:
simp [eraseIdx_pmap f h.2 n]

Result:
no goals
-- Mathlib/Logic/Relation.lean
theorem trans (hab : ReflTransGen r a b) (hbc : ReflTransGen r b c) : ReflTransGen r a c

Proof state:
case refl
α : Type u_1
r : α → α → Prop
a b c : α
hab : ReflTransGen r a b
⊢ ReflTransGen r a b

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
a b c : α
hab : ReflTransGen r a b
hbc : ReflTransGen r b c
⊢ ReflTransGen r a c

Tactic:
induction hbc with
| refl => assumption
| tail _ hcd hac => exact hac.tail hcd

Result:
no goals

Proof state:
case tail
α : Type u_1
r : α → α → Prop
a b c : α
hab : ReflTransGen r a b
b✝ c✝ : α
a✝ : ReflTransGen r b b✝
hcd : r b✝ c✝
hac : ReflTransGen r a b✝
⊢ ReflTransGen r a c✝

Tactic:
exact hac.tail hcd

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem preimage_eq_empty_iff {s : Set β} : f ⁻¹' s = ∅ ↔ Disjoint s (range f) :=
  ⟨fun h => by
    simp only [eq_empty_iff_forall_not_mem, disjoint_iff_inter_eq_empty, not_exists, mem_inter_iff,
      not_and, mem_range, mem_preimage] at h ⊢
    intro y hy x hx
    rw [← hx] at hy
    exact h x hy,
  preimage_eq_empty⟩

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
h : f ⁻¹' s = ∅
⊢ Disjoint s (range f)

Tactic:
simp only [eq_empty_iff_forall_not_mem, disjoint_iff_inter_eq_empty, not_exists, mem_inter_iff,
  not_and, mem_range, mem_preimage] at h ⊢

Result:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
h : ∀ (x : α), f x ∉ s
⊢ ∀ x ∈ s, ∀ (x_1 : α), ¬f x_1 = x

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
h : ∀ (x : α), f x ∉ s
y : β
hy : y ∈ s
x : α
hx : f x = y
⊢ False

Tactic:
rw [← hx] at hy

Result:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
h : ∀ (x : α), f x ∉ s
y : β
x : α
hy : f x ∈ s
hx : f x = y
⊢ False

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
h : ∀ (x : α), f x ∉ s
y : β
x : α
hy : f x ∈ s
hx : f x = y
⊢ False

Tactic:
exact h x hy

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
h : ∀ (x : α), f x ∉ s
⊢ ∀ x ∈ s, ∀ (x_1 : α), ¬f x_1 = x

Tactic:
intro y hy x hx

Result:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
h : ∀ (x : α), f x ∉ s
y : β
hy : y ∈ s
x : α
hx : f x = y
⊢ False