harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem dTwo_comp_eq :
    dTwo A ∘ₗ twoCochainsLequiv A =
      threeCochainsLequiv A ∘ₗ ((inhomogeneousCochains A).d 2 3).hom

Proof state:
case h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (dTwo A ∘ₗ ↑(twoCochainsLequiv A)) x y =
    (↑(threeCochainsLequiv A) ∘ₗ ModuleCat.Hom.hom ((inhomogeneousCochains A).d 2 3)) x y

Tactic:
show A.ρ y.1 (x _) - x _ + x _ - x _ = _ + _

Result:
case h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (A.ρ y.1) (x ((piFinTwoEquiv fun x => G).symm (y.2.1, y.2.2))) -
          x ((piFinTwoEquiv fun x => G).symm (y.1 * y.2.1, y.2.2)) +
        x ((piFinTwoEquiv fun x => G).symm (y.1, y.2.1 * y.2.2)) -
      x ((piFinTwoEquiv fun x => G).symm (y.1, y.2.1)) =
    (A.ρ (((Fin.consEquiv fun a => G).symm.trans ((Equiv.refl G).prodCongr (piFinTwoEquiv fun x => G))).symm y 0))
        (x fun i =>
          ((Fin.consEquiv fun a => G).symm.trans ((Equiv.refl G).prodCongr (piFinTwoEquiv fun x => G))).symm y i.succ) +
      ∑ j : Fin (2 + 1),
        (-1) ^ (↑j + 1) •
          x
            (j.contractNth (fun x1 x2 => x1 * x2)
              (((Fin.consEquiv fun a => G).symm.trans ((Equiv.refl G).prodCongr (piFinTwoEquiv fun x => G))).symm y))
-- Mathlib/GroupTheory/Perm/Fin.lean
theorem cycleRange_of_eq {n : ℕ} [NeZero n] {i j : Fin n} (h : j = i) : cycleRange i j = 0

Proof state:
n : ℕ
inst✝ : NeZero n
i j : Fin n
h : j = i
⊢ i.cycleRange j = 0

Tactic:
rw [cycleRange_of_le h.le, if_pos h]

Result:
no goals
-- Mathlib/Logic/Equiv/Option.lean
theorem some_removeNone_iff {x : α} : some (removeNone e x) = e none ↔ e.symm none = some x

Proof state:
case some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
a : β
h : e (some x) = some a
h1 : some x = e.symm (some a)
⊢ e (some x) = e none ↔ e.symm none = some x

Tactic:
simp only [apply_eq_iff_eq, reduceCtorEq]

Result:
case some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
a : β
h : e (some x) = some a
h1 : some x = e.symm (some a)
⊢ False ↔ e.symm none = some x

Proof state:
case none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h : e (some x) = none
⊢ e none = e none ↔ e.symm none = some x

Tactic:
simpa using (congr_arg e.symm h).symm

Result:
no goals

Proof state:
case none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h : e (some x) = none
⊢ some (e.removeNone x) = e none ↔ e.symm none = some x

Tactic:
rw [removeNone_none _ h]

Result:
case none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h : e (some x) = none
⊢ e none = e none ↔ e.symm none = some x

Proof state:
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
⊢ some (e.removeNone x) = e none ↔ e.symm none = some x

Tactic:
rcases h : e (some x) with a | a

Result:
case none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h : e (some x) = none
⊢ some (e.removeNone x) = e none ↔ e.symm none = some x

case some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
a : β
h : e (some x) = some a
⊢ some (e.removeNone x) = e none ↔ e.symm none = some x

Proof state:
case some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
a : β
h : e (some x) = some a
⊢ e (some x) = e none ↔ e.symm none = some x

Tactic:
have h1 := congr_arg e.symm h

Result:
case some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
a : β
h : e (some x) = some a
h1 : e.symm (e (some x)) = e.symm (some a)
⊢ e (some x) = e none ↔ e.symm none = some x

Proof state:
case some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
a : β
h : e (some x) = some a
⊢ some (e.removeNone x) = e none ↔ e.symm none = some x

Tactic:
rw [removeNone_some _ ⟨a, h⟩]

Result:
case some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
a : β
h : e (some x) = some a
⊢ e (some x) = e none ↔ e.symm none = some x

Proof state:
case some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
a : β
h : e (some x) = some a
h1 : e.symm (e (some x)) = e.symm (some a)
⊢ e (some x) = e none ↔ e.symm none = some x

Tactic:
rw [symm_apply_apply] at h1

Result:
case some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
a : β
h : e (some x) = some a
h1 : some x = e.symm (some a)
⊢ e (some x) = e none ↔ e.symm none = some x

Proof state:
case some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
a : β
h : e (some x) = some a
h1 : some x = e.symm (some a)
⊢ False ↔ e.symm none = some x

Tactic:
simp [h1, apply_eq_iff_eq]

Result:
no goals
-- Mathlib/Topology/Constructible.lean
@[stacks 09YG]
lemma IsConstructible.image_of_isClosedEmbedding (hf : IsClosedEmbedding f)
    (hfcomp : IsRetrocompact (range f)ᶜ) (hs : IsConstructible s) : IsConstructible (f '' s)

Proof state:
case compl
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s✝ : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
s : Set X
hs : IsConstructible s
hs' : IsConstructible (f '' s)
⊢ IsConstructible (f '' sᶜ)

Tactic:
rw [← range_diff_image hf.injective]

Result:
case compl
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s✝ : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
s : Set X
hs : IsConstructible s
hs' : IsConstructible (f '' s)
⊢ IsConstructible (range f \ f '' s)
-- Mathlib/Data/DFinsupp/NeLocus.lean
theorem zipWith_neLocus_eq_right [∀ a, DecidableEq (M a)] [∀ a, DecidableEq (P a)]
    {F : ∀ a, M a → N a → P a} (F0 : ∀ a, F a 0 0 = 0) (f₁ f₂ : Π₀ a, M a) (g : Π₀ a, N a)
    (hF : ∀ a g, Function.Injective fun f ↦ F a f g) :
    (zipWith F F0 f₁ g).neLocus (zipWith F F0 f₂ g) = f₁.neLocus f₂

Proof state:
α : Type u_1
N : α → Type u_2
inst✝⁵ : DecidableEq α
M : α → Type u_3
P : α → Type u_4
inst✝⁴ : (a : α) → Zero (N a)
inst✝³ : (a : α) → Zero (M a)
inst✝² : (a : α) → Zero (P a)
inst✝¹ : (a : α) → DecidableEq (M a)
inst✝ : (a : α) → DecidableEq (P a)
F : (a : α) → M a → N a → P a
F0 : ∀ (a : α), F a 0 0 = 0
f₁ f₂ : Π₀ (a : α), M a
g : Π₀ (a : α), N a
hF : ∀ (a : α) (g : N a), Function.Injective fun f => F a f g
⊢ (zipWith F F0 f₁ g).neLocus (zipWith F F0 f₂ g) = f₁.neLocus f₂

Tactic:
ext a

Result:
case h
α : Type u_1
N : α → Type u_2
inst✝⁵ : DecidableEq α
M : α → Type u_3
P : α → Type u_4
inst✝⁴ : (a : α) → Zero (N a)
inst✝³ : (a : α) → Zero (M a)
inst✝² : (a : α) → Zero (P a)
inst✝¹ : (a : α) → DecidableEq (M a)
inst✝ : (a : α) → DecidableEq (P a)
F : (a : α) → M a → N a → P a
F0 : ∀ (a : α), F a 0 0 = 0
f₁ f₂ : Π₀ (a : α), M a
g : Π₀ (a : α), N a
hF : ∀ (a : α) (g : N a), Function.Injective fun f => F a f g
a : α
⊢ a ∈ (zipWith F F0 f₁ g).neLocus (zipWith F F0 f₂ g) ↔ a ∈ f₁.neLocus f₂

Proof state:
case h
α : Type u_1
N : α → Type u_2
inst✝⁵ : DecidableEq α
M : α → Type u_3
P : α → Type u_4
inst✝⁴ : (a : α) → Zero (N a)
inst✝³ : (a : α) → Zero (M a)
inst✝² : (a : α) → Zero (P a)
inst✝¹ : (a : α) → DecidableEq (M a)
inst✝ : (a : α) → DecidableEq (P a)
F : (a : α) → M a → N a → P a
F0 : ∀ (a : α), F a 0 0 = 0
f₁ f₂ : Π₀ (a : α), M a
g : Π₀ (a : α), N a
hF : ∀ (a : α) (g : N a), Function.Injective fun f => F a f g
a : α
⊢ a ∈ (zipWith F F0 f₁ g).neLocus (zipWith F F0 f₂ g) ↔ a ∈ f₁.neLocus f₂

Tactic:
simpa only [mem_neLocus] using (hF a _).ne_iff

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_setIfInBounds {as : Array α} {i j : Nat} {a : α}  :
    (as.setIfInBounds i a)[j]? = if i = j then if i < as.size then some a else none else as[j]?

Proof state:
α : Type u_1
as : Array α
i j : Nat
a : α
⊢ (as.setIfInBounds i a)[j]? = if i = j then if i < as.size then some a else none else as[j]?

Tactic:
cases as

Result:
case mk
α : Type u_1
i j : Nat
a : α
toList✝ : List α
⊢ ({ toList := toList✝ }.setIfInBounds i a)[j]? =
    if i = j then if i < { toList := toList✝ }.size then some a else none else { toList := toList✝ }[j]?

Proof state:
case mk
α : Type u_1
i j : Nat
a : α
toList✝ : List α
⊢ ({ toList := toList✝ }.setIfInBounds i a)[j]? =
    if i = j then if i < { toList := toList✝ }.size then some a else none else { toList := toList✝ }[j]?

Tactic:
simp [List.getElem?_set]

Result:
no goals
-- Mathlib/Algebra/Lie/TraceForm.lean
/-- This lemma justifies the terminology "invariant" for trace forms. -/
@[simp] lemma lie_traceForm_eq_zero (x : L) : ⁅x, traceForm R L M⁆ = 0

Proof state:
R : Type u_1
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
x : L
⊢ ⁅x, traceForm R L M⁆ = 0

Tactic:
ext y z

Result:
case H
R : Type u_1
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
x y z : L
⊢ (⁅x, traceForm R L M⁆ y) z = (0 y) z

Proof state:
case H
R : Type u_1
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
x y z : L
⊢ (⁅x, traceForm R L M⁆ y) z = (0 y) z

Tactic:
rw [LieHom.lie_apply, LinearMap.sub_apply, Module.Dual.lie_apply, LinearMap.zero_apply,
  LinearMap.zero_apply, traceForm_apply_lie_apply', sub_self]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem parallelogram_law_with_norm (x y : E) :
    ‖x + y‖ * ‖x + y‖ + ‖x - y‖ * ‖x - y‖ = 2 * (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ re ⟪x + y, x + y⟫_𝕜 + re ⟪x - y, x - y⟫_𝕜 = 2 * (re ⟪x, x⟫_𝕜 + re ⟪y, y⟫_𝕜)

Tactic:
rw [← re.map_add, parallelogram_law, two_mul, two_mul]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ re (⟪x, x⟫_𝕜 + ⟪y, y⟫_𝕜 + (⟪x, x⟫_𝕜 + ⟪y, y⟫_𝕜)) = re ⟪x, x⟫_𝕜 + re ⟪y, y⟫_𝕜 + (re ⟪x, x⟫_𝕜 + re ⟪y, y⟫_𝕜)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ re (⟪x, x⟫_𝕜 + ⟪y, y⟫_𝕜 + (⟪x, x⟫_𝕜 + ⟪y, y⟫_𝕜)) = re ⟪x, x⟫_𝕜 + re ⟪y, y⟫_𝕜 + (re ⟪x, x⟫_𝕜 + re ⟪y, y⟫_𝕜)

Tactic:
simp only [re.map_add]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ‖x + y‖ * ‖x + y‖ + ‖x - y‖ * ‖x - y‖ = 2 * (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)

Tactic:
simp only [← @inner_self_eq_norm_mul_norm 𝕜]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ re ⟪x + y, x + y⟫_𝕜 + re ⟪x - y, x - y⟫_𝕜 = 2 * (re ⟪x, x⟫_𝕜 + re ⟪y, y⟫_𝕜)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem gcd_eq_iff {xs : IntList} {g : Nat} :
    xs.gcd = g ↔
      (∀ {a : Int}, a ∈ xs → (g : Int) ∣ a) ∧
        (∀ (c : Nat), (∀ {a : Int}, a ∈ xs → (c : Int) ∣ a) → c ∣ g)

Proof state:
case mpr.intro
xs : IntList
g : Nat
hi : ∀ {a : Int}, a ∈ xs → ↑g ∣ a
hg : ∀ (c : Nat), (∀ {a : Int}, a ∈ xs → ↑c ∣ a) → c ∣ g
⊢ xs.gcd = g

Tactic:
apply Nat.dvd_antisymm

Result:
case mpr.intro.a
xs : IntList
g : Nat
hi : ∀ {a : Int}, a ∈ xs → ↑g ∣ a
hg : ∀ (c : Nat), (∀ {a : Int}, a ∈ xs → ↑c ∣ a) → c ∣ g
⊢ xs.gcd ∣ g

case mpr.intro.a
xs : IntList
g : Nat
hi : ∀ {a : Int}, a ∈ xs → ↑g ∣ a
hg : ∀ (c : Nat), (∀ {a : Int}, a ∈ xs → ↑c ∣ a) → c ∣ g
⊢ g ∣ xs.gcd

Proof state:
case mpr.intro.a.a
xs : IntList
g : Nat
hi : ∀ {a : Int}, a ∈ xs → ↑g ∣ a
hg : ∀ (c : Nat), (∀ {a : Int}, a ∈ xs → ↑c ∣ a) → c ∣ g
i : Int
m : i ∈ xs
⊢ ↑xs.gcd ∣ i

Tactic:
exact gcd_dvd xs m

Result:
no goals

Proof state:
case mpr.intro.a
xs : IntList
g : Nat
hi : ∀ {a : Int}, a ∈ xs → ↑g ∣ a
hg : ∀ (c : Nat), (∀ {a : Int}, a ∈ xs → ↑c ∣ a) → c ∣ g
⊢ g ∣ xs.gcd

Tactic:
exact dvd_gcd xs g hi

Result:
no goals

Proof state:
xs : IntList
g : Nat
⊢ xs.gcd = g ↔ (∀ {a : Int}, a ∈ xs → ↑g ∣ a) ∧ ∀ (c : Nat), (∀ {a : Int}, a ∈ xs → ↑c ∣ a) → c ∣ g

Tactic:
constructor

Result:
case mp
xs : IntList
g : Nat
⊢ xs.gcd = g → (∀ {a : Int}, a ∈ xs → ↑g ∣ a) ∧ ∀ (c : Nat), (∀ {a : Int}, a ∈ xs → ↑c ∣ a) → c ∣ g

case mpr
xs : IntList
g : Nat
⊢ ((∀ {a : Int}, a ∈ xs → ↑g ∣ a) ∧ ∀ (c : Nat), (∀ {a : Int}, a ∈ xs → ↑c ∣ a) → c ∣ g) → xs.gcd = g

Proof state:
case mpr.intro.a.a
xs : IntList
g : Nat
hi : ∀ {a : Int}, a ∈ xs → ↑g ∣ a
hg : ∀ (c : Nat), (∀ {a : Int}, a ∈ xs → ↑c ∣ a) → c ∣ g
⊢ ∀ {a : Int}, a ∈ xs → ↑xs.gcd ∣ a

Tactic:
intro i m

Result:
case mpr.intro.a.a
xs : IntList
g : Nat
hi : ∀ {a : Int}, a ∈ xs → ↑g ∣ a
hg : ∀ (c : Nat), (∀ {a : Int}, a ∈ xs → ↑c ∣ a) → c ∣ g
i : Int
m : i ∈ xs
⊢ ↑xs.gcd ∣ i

Proof state:
case mpr
xs : IntList
g : Nat
⊢ ((∀ {a : Int}, a ∈ xs → ↑g ∣ a) ∧ ∀ (c : Nat), (∀ {a : Int}, a ∈ xs → ↑c ∣ a) → c ∣ g) → xs.gcd = g

Tactic:
rintro ⟨hi, hg⟩

Result:
case mpr.intro
xs : IntList
g : Nat
hi : ∀ {a : Int}, a ∈ xs → ↑g ∣ a
hg : ∀ (c : Nat), (∀ {a : Int}, a ∈ xs → ↑c ∣ a) → c ∣ g
⊢ xs.gcd = g

Proof state:
case mp
xs : IntList
⊢ (∀ {a : Int}, a ∈ xs → ↑xs.gcd ∣ a) ∧ ∀ (c : Nat), (∀ {a : Int}, a ∈ xs → ↑c ∣ a) → c ∣ xs.gcd

Tactic:
exact ⟨gcd_dvd _, dvd_gcd _⟩

Result:
no goals

Proof state:
case mpr.intro.a
xs : IntList
g : Nat
hi : ∀ {a : Int}, a ∈ xs → ↑g ∣ a
hg : ∀ (c : Nat), (∀ {a : Int}, a ∈ xs → ↑c ∣ a) → c ∣ g
⊢ xs.gcd ∣ g

Tactic:
apply hg

Result:
case mpr.intro.a.a
xs : IntList
g : Nat
hi : ∀ {a : Int}, a ∈ xs → ↑g ∣ a
hg : ∀ (c : Nat), (∀ {a : Int}, a ∈ xs → ↑c ∣ a) → c ∣ g
⊢ ∀ {a : Int}, a ∈ xs → ↑xs.gcd ∣ a

Proof state:
case mp
xs : IntList
g : Nat
⊢ xs.gcd = g → (∀ {a : Int}, a ∈ xs → ↑g ∣ a) ∧ ∀ (c : Nat), (∀ {a : Int}, a ∈ xs → ↑c ∣ a) → c ∣ g

Tactic:
rintro rfl

Result:
case mp
xs : IntList
⊢ (∀ {a : Int}, a ∈ xs → ↑xs.gcd ∣ a) ∧ ∀ (c : Nat), (∀ {a : Int}, a ∈ xs → ↑c ∣ a) → c ∣ xs.gcd
-- Mathlib/Algebra/ModEq.lean
theorem ModEq.trans : a ≡ b [PMOD p] → b ≡ c [PMOD p] → a ≡ c [PMOD p] := fun ⟨m, hm⟩ ⟨n, hn⟩ =>
  ⟨m + n, by simp [add_smul, ← hm, ← hn]⟩

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
p a b c : α
x✝¹ : a ≡ b [PMOD p]
x✝ : b ≡ c [PMOD p]
m : ℤ
hm : b - a = m • p
n : ℤ
hn : c - b = n • p
⊢ c - a = (m + n) • p

Tactic:
simp [add_smul, ← hm, ← hn]

Result:
no goals
-- Mathlib/Tactic/NormNum/Prime.lean
theorem minFacHelper_0 (n : ℕ)
    (h1 : Nat.ble (nat_lit 2) n = true) (h2 : nat_lit 1 = n % (nat_lit 2)) :
    MinFacHelper n (nat_lit 3)

Proof state:
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
⊢ 3 % 2 = 1

Tactic:
norm_num

Result:
no goals

Proof state:
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
⊢ 3 ≤ n.minFac

Tactic:
refine (le_minFac'.mpr fun p hp hpn ↦ ?_).resolve_left (Nat.ne_of_gt (Nat.le_of_ble_eq_true h1))

Result:
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
p : ℕ
hp : 2 ≤ p
hpn : p ∣ n
⊢ 3 ≤ p

Proof state:
case inl
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
hp : 2 ≤ 2
hpn : 2 ∣ n
⊢ 3 ≤ 2

Tactic:
simp [(Nat.dvd_iff_mod_eq_zero ..).1 hpn] at h2

Result:
no goals

Proof state:
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
⊢ MinFacHelper n 3

Tactic:
refine ⟨by norm_num, by norm_num, ?_⟩

Result:
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
⊢ 3 ≤ n.minFac

Proof state:
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
p : ℕ
hp : 2 ≤ p
hpn : p ∣ n
⊢ 3 ≤ p

Tactic:
rcases hp.eq_or_lt with rfl|h

Result:
case inl
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
hp : 2 ≤ 2
hpn : 2 ∣ n
⊢ 3 ≤ 2

case inr
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
p : ℕ
hp : 2 ≤ p
hpn : p ∣ n
h : 2 < p
⊢ 3 ≤ p

Proof state:
case inr
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
p : ℕ
hp : 2 ≤ p
hpn : p ∣ n
h : 2 < p
⊢ 3 ≤ p

Tactic:
exact h

Result:
no goals

Proof state:
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
⊢ 2 < 3

Tactic:
norm_num

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem isPrefixOfAux_toArray_zero [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) :
    Array.isPrefixOfAux l₁.toArray l₂.toArray hle 0 =
      l₁.isPrefixOf l₂

Proof state:
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
⊢ l₁.toArray.isPrefixOfAux l₂.toArray hle 0 = l₁.isPrefixOf l₂

Tactic:
rw [Array.isPrefixOfAux]

Result:
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
⊢ (if h : 0 < l₁.toArray.size then
      let a := l₁.toArray[0];
      let_fun this := ⋯;
      let b := l₂.toArray[0];
      if (a == b) = true then l₁.toArray.isPrefixOfAux l₂.toArray hle (0 + 1) else false
    else true) =
    l₁.isPrefixOf l₂

Proof state:
α : Type u_1
inst✝ : BEq α
l₁ l₂ x✝ : List α
hle : [].length ≤ x✝.length
⊢ (if h : 0 < #[].size then
      let a := #[][0];
      let_fun this := ⋯;
      let b := x✝.toArray[0];
      if (a == b) = true then #[].isPrefixOfAux x✝.toArray hle (0 + 1) else false
    else true) =
    [].isPrefixOf x✝

Tactic:
rw [dif_neg] <;> simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
⊢ (if h : 0 < l₁.toArray.size then
      let a := l₁.toArray[0];
      let_fun this := ⋯;
      let b := l₂.toArray[0];
      if (a == b) = true then l₁.toArray.isPrefixOfAux l₂.toArray hle (0 + 1) else false
    else true) =
    l₁.isPrefixOf l₂

Tactic:
match l₁, l₂ with
| [], _ => rw [dif_neg] <;> simp
| _::_, [] => simp at hle
| a::l₁, b::l₂ =>
  simp [isPrefixOf_cons₂, isPrefixOfAux_toArray_succ', isPrefixOfAux_toArray_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
l₁✝ l₂✝ : List α
a : α
l₁ : List α
b : α
l₂ : List α
hle : (a :: l₁).length ≤ (b :: l₂).length
⊢ (if h : 0 < (a :: l₁).toArray.size then
      let a_1 := (a :: l₁).toArray[0];
      let_fun this := ⋯;
      let b_1 := (b :: l₂).toArray[0];
      if (a_1 == b_1) = true then (a :: l₁).toArray.isPrefixOfAux (b :: l₂).toArray hle (0 + 1) else false
    else true) =
    (a :: l₁).isPrefixOf (b :: l₂)

Tactic:
simp [isPrefixOf_cons₂, isPrefixOfAux_toArray_succ', isPrefixOfAux_toArray_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
head✝ : α
tail✝ : List α
hle : (head✝ :: tail✝).length ≤ [].length
⊢ (if h : 0 < (head✝ :: tail✝).toArray.size then
      let a := (head✝ :: tail✝).toArray[0];
      let_fun this := ⋯;
      let b := #[][0];
      if (a == b) = true then (head✝ :: tail✝).toArray.isPrefixOfAux #[] hle (0 + 1) else false
    else true) =
    (head✝ :: tail✝).isPrefixOf []

Tactic:
simp at hle

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem map_attachWith {l : Vector α n} {P : α → Prop} {H : ∀ (a : α), a ∈ l → P a}
    (f : { x // P x } → β) :
    (l.attachWith P H).map f =
      l.pmap (fun a (h : a ∈ l ∧ P a) => f ⟨a, H _ h.1⟩) (fun a h => ⟨h, H a h⟩)

Proof state:
case mk
α : Type u_1
n : Nat
β : Type u_2
P : α → Prop
f : { x // P x } → β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
H : ∀ (a : α), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → P a
⊢ map f ({ toArray := toArray✝, size_toArray := size_toArray✝ }.attachWith P H) =
    pmap (fun a h => f ⟨a, ⋯⟩) { toArray := toArray✝, size_toArray := size_toArray✝ } ⋯

Tactic:
ext <;> simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
P : α → Prop
H : ∀ (a : α), a ∈ l → P a
f : { x // P x } → β
⊢ map f (l.attachWith P H) = pmap (fun a h => f ⟨a, ⋯⟩) l ⋯

Tactic:
cases l

Result:
case mk
α : Type u_1
n : Nat
β : Type u_2
P : α → Prop
f : { x // P x } → β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
H : ∀ (a : α), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → P a
⊢ map f ({ toArray := toArray✝, size_toArray := size_toArray✝ }.attachWith P H) =
    pmap (fun a h => f ⟨a, ⋯⟩) { toArray := toArray✝, size_toArray := size_toArray✝ } ⋯
-- Mathlib/Data/ENNReal/Real.lean
theorem toReal_le_toReal (ha : a ≠ ∞) (hb : b ≠ ∞) : a.toReal ≤ b.toReal ↔ a ≤ b

Proof state:
case intro.intro
a b : ℝ≥0
⊢ (↑a).toReal ≤ (↑b).toReal ↔ ↑a ≤ ↑b

Tactic:
norm_cast

Result:
no goals

Proof state:
a b : ℝ≥0∞
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ a.toReal ≤ b.toReal ↔ a ≤ b

Tactic:
lift a to ℝ≥0 using ha

Result:
case intro
b : ℝ≥0∞
hb : b ≠ ⊤
a : ℝ≥0
⊢ (↑a).toReal ≤ b.toReal ↔ ↑a ≤ b

Proof state:
case intro
b : ℝ≥0∞
hb : b ≠ ⊤
a : ℝ≥0
⊢ (↑a).toReal ≤ b.toReal ↔ ↑a ≤ b

Tactic:
lift b to ℝ≥0 using hb

Result:
case intro.intro
a b : ℝ≥0
⊢ (↑a).toReal ≤ (↑b).toReal ↔ ↑a ≤ ↑b
-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem exists_simpleFunc_nonneg_ae_eq {f : Lp.simpleFunc G p μ} (hf : 0 ≤ f) :
    ∃ f' : α →ₛ G, 0 ≤ f' ∧ f =ᵐ[μ] f'

Proof state:
case mk.mk.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝ : NormedLatticeAddCommGroup G
g : α →ₛ G
hp : AEEqFun.mk ⇑g ⋯ ∈ Lp G p μ
hf : 0 ≤ᶠ[ae μ] ⇑g
⊢ ∃ f', 0 ≤ f' ∧ ↑↑↑⟨⟨AEEqFun.mk ⇑g ⋯, hp⟩, ⋯⟩ =ᶠ[ae μ] ⇑f'

Tactic:
refine ⟨g ⊔ 0, le_sup_right, (AEEqFun.coeFn_mk _ _).trans ?_⟩

Result:
case mk.mk.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝ : NormedLatticeAddCommGroup G
g : α →ₛ G
hp : AEEqFun.mk ⇑g ⋯ ∈ Lp G p μ
hf : 0 ≤ᶠ[ae μ] ⇑g
⊢ ⇑g =ᶠ[ae μ] ⇑(g ⊔ 0)

Proof state:
case mk.mk.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝ : NormedLatticeAddCommGroup G
g : α →ₛ G
hp : AEEqFun.mk ⇑g ⋯ ∈ Lp G p μ
hf : 0 ≤ ⟨⟨AEEqFun.mk ⇑g ⋯, hp⟩, ⋯⟩
⊢ ∃ f', 0 ≤ f' ∧ ↑↑↑⟨⟨AEEqFun.mk ⇑g ⋯, hp⟩, ⋯⟩ =ᶠ[ae μ] ⇑f'

Tactic:
change 0 ≤ᵐ[μ] g at hf

Result:
case mk.mk.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝ : NormedLatticeAddCommGroup G
g : α →ₛ G
hp : AEEqFun.mk ⇑g ⋯ ∈ Lp G p μ
hf : 0 ≤ᶠ[ae μ] ⇑g
⊢ ∃ f', 0 ≤ f' ∧ ↑↑↑⟨⟨AEEqFun.mk ⇑g ⋯, hp⟩, ⋯⟩ =ᶠ[ae μ] ⇑f'

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝ : NormedLatticeAddCommGroup G
f : ↥(simpleFunc G p μ)
hf : 0 ≤ f
⊢ ∃ f', 0 ≤ f' ∧ ↑↑↑f =ᶠ[ae μ] ⇑f'

Tactic:
rcases f with ⟨⟨f, hp⟩, g, (rfl : _ = f)⟩

Result:
case mk.mk.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝ : NormedLatticeAddCommGroup G
g : α →ₛ G
hp : AEEqFun.mk ⇑g ⋯ ∈ Lp G p μ
hf : 0 ≤ ⟨⟨AEEqFun.mk ⇑g ⋯, hp⟩, ⋯⟩
⊢ ∃ f', 0 ≤ f' ∧ ↑↑↑⟨⟨AEEqFun.mk ⇑g ⋯, hp⟩, ⋯⟩ =ᶠ[ae μ] ⇑f'

Proof state:
case mk.mk.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝ : NormedLatticeAddCommGroup G
g : α →ₛ G
hp : AEEqFun.mk ⇑g ⋯ ∈ Lp G p μ
hf : 0 ≤ᶠ[ae μ] ⇑g
⊢ ⇑g =ᶠ[ae μ] ⇑(g ⊔ 0)

Tactic:
exact hf.mono fun x hx ↦ (sup_of_le_left hx).symm

Result:
no goals
-- Mathlib/LinearAlgebra/LinearDisjoint.lean
theorem LinearDisjoint.symm_of_commute (H : M.LinearDisjoint N)
    (hc : ∀ (m : M) (n : N), Commute m.1 n.1) : N.LinearDisjoint M

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hc : ∀ (m : ↥M) (n : ↥N), Commute ↑m ↑n
⊢ N.LinearDisjoint M

Tactic:
rw [linearDisjoint_iff, mulMap_comm_of_commute M N hc]

Result:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hc : ∀ (m : ↥M) (n : ↥N), Commute ↑m ↑n
⊢ Function.Injective ⇑(M.mulMap N ∘ₗ ↑(TensorProduct.comm R ↥N ↥M))

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hc : ∀ (m : ↥M) (n : ↥N), Commute ↑m ↑n
⊢ Function.Injective ⇑(M.mulMap N ∘ₗ ↑(TensorProduct.comm R ↥N ↥M))

Tactic:
exact ((TensorProduct.comm R N M).toEquiv.injective_comp _).2 H.injective

Result:
no goals