harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem get?_set_of_lt' (a : α) {m n} (l : List α) (h : m < length l) :
    (set l m a).get? n = if m = n then some a else l.get? n

Proof state:
α : Type u_1
a : α
m n : Nat
l : List α
h : m < l.length
⊢ (if m = n then if m < l.length then some a else none else l[n]?) = if m = n then some a else l[n]?

Tactic:
split <;> subst_vars <;> simp [*, getElem?_eq_getElem h]

Result:
no goals

Proof state:
α : Type u_1
a : α
m n : Nat
l : List α
h : m < l.length
⊢ (l.set m a).get? n = if m = n then some a else l.get? n

Tactic:
simp [getElem?_set]

Result:
α : Type u_1
a : α
m n : Nat
l : List α
h : m < l.length
⊢ (if m = n then if m < l.length then some a else none else l[n]?) = if m = n then some a else l[n]?
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem eq_replicate_or_eq_replicate_append_cons {α : Type _} (l : List α) :
    (l = []) ∨ (∃ n a, l = replicate n a ∧ 0 < n) ∨
      (∃ n a b l', l = replicate n a ++ b :: l' ∧ 0 < n ∧ a ≠ b)

Proof state:
case cons.h.inr.inl.intro.intro.intro
α : Type u_1
x : α
n : Nat
a : α
h : 0 < n
⊢ (∃ n_1 a_1, x :: replicate n a = replicate n_1 a_1 ∧ 0 < n_1) ∨
    ∃ n_1 a_1 b l', x :: replicate n a = replicate n_1 a_1 ++ b :: l' ∧ 0 < n_1 ∧ a_1 ≠ b

Tactic:
by_cases h' : x = a

Result:
case pos
α : Type u_1
x : α
n : Nat
a : α
h : 0 < n
h' : x = a
⊢ (∃ n_1 a_1, x :: replicate n a = replicate n_1 a_1 ∧ 0 < n_1) ∨
    ∃ n_1 a_1 b l', x :: replicate n a = replicate n_1 a_1 ++ b :: l' ∧ 0 < n_1 ∧ a_1 ≠ b

case neg
α : Type u_1
x : α
n : Nat
a : α
h : 0 < n
h' : ¬x = a
⊢ (∃ n_1 a_1, x :: replicate n a = replicate n_1 a_1 ∧ 0 < n_1) ∨
    ∃ n_1 a_1 b l', x :: replicate n a = replicate n_1 a_1 ++ b :: l' ∧ 0 < n_1 ∧ a_1 ≠ b

Proof state:
case pos
α : Type u_1
x : α
n : Nat
a : α
h : 0 < n
h' : x = a
⊢ (∃ n_1 a_1, x :: replicate n a = replicate n_1 a_1 ∧ 0 < n_1) ∨
    ∃ n_1 a_1 b l', x :: replicate n a = replicate n_1 a_1 ++ b :: l' ∧ 0 < n_1 ∧ a_1 ≠ b

Tactic:
subst h'

Result:
case pos
α : Type u_1
x : α
n : Nat
h : 0 < n
⊢ (∃ n_1 a, x :: replicate n x = replicate n_1 a ∧ 0 < n_1) ∨
    ∃ n_1 a b l', x :: replicate n x = replicate n_1 a ++ b :: l' ∧ 0 < n_1 ∧ a ≠ b

Proof state:
case pos
α : Type u_1
x : α
n : Nat
b : α
l' : List α
h : 0 < n ∧ x ≠ b
⊢ ∃ n_1 a b_1 l'_1, x :: (replicate n x ++ b :: l') = replicate n_1 a ++ b_1 :: l'_1 ∧ 0 < n_1 ∧ a ≠ b_1

Tactic:
refine ⟨n + 1, x, b, l', by simp [replicate_succ], by simp, h.2⟩

Result:
no goals

Proof state:
case nil
α : Type u_1
⊢ [] = [] ∨ (∃ n a, [] = replicate n a ∧ 0 < n) ∨ ∃ n a b l', [] = replicate n a ++ b :: l' ∧ 0 < n ∧ a ≠ b

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
@[to_additive]
lemma prod_erase_of_comm [DecidableEq M] (ha : a ∈ l) (comm : ∀ x ∈ l, ∀ y ∈ l, x * y = y * x) :
    a * (l.erase a).prod = l.prod

Proof state:
case cons.inl
M : Type u_4
inst✝¹ : Monoid M
l✝ : List M
a : M
inst✝ : DecidableEq M
l : List M
ih : a ∈ l → (∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x) → a * (l.erase a).prod = l.prod
ha : a ∈ a :: l
comm : ∀ (x : M), x ∈ a :: l → ∀ (y : M), y ∈ a :: l → x * y = y * x
⊢ a * ((a :: l).erase a).prod = (a :: l).prod

Tactic:
simp only [erase_cons_head, prod_cons]

Result:
no goals

Proof state:
case cons
M : Type u_4
inst✝¹ : Monoid M
l✝ : List M
a : M
inst✝ : DecidableEq M
b : M
l : List M
ih : a ∈ l → (∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x) → a * (l.erase a).prod = l.prod
ha : a ∈ b :: l
comm : ∀ (x : M), x ∈ b :: l → ∀ (y : M), y ∈ b :: l → x * y = y * x
⊢ a * ((b :: l).erase a).prod = (b :: l).prod

Tactic:
obtain rfl | ⟨ne, h⟩ := List.eq_or_ne_mem_of_mem ha

Result:
case cons.inl
M : Type u_4
inst✝¹ : Monoid M
l✝ : List M
a : M
inst✝ : DecidableEq M
l : List M
ih : a ∈ l → (∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x) → a * (l.erase a).prod = l.prod
ha : a ∈ a :: l
comm : ∀ (x : M), x ∈ a :: l → ∀ (y : M), y ∈ a :: l → x * y = y * x
⊢ a * ((a :: l).erase a).prod = (a :: l).prod

case cons.inr.intro
M : Type u_4
inst✝¹ : Monoid M
l✝ : List M
a : M
inst✝ : DecidableEq M
b : M
l : List M
ih : a ∈ l → (∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x) → a * (l.erase a).prod = l.prod
ha : a ∈ b :: l
comm : ∀ (x : M), x ∈ b :: l → ∀ (y : M), y ∈ b :: l → x * y = y * x
ne : a ≠ b
h : a ∈ l
⊢ a * ((b :: l).erase a).prod = (b :: l).prod

Proof state:
case nil
M : Type u_4
inst✝¹ : Monoid M
l : List M
a : M
inst✝ : DecidableEq M
ha : a ∈ []
comm : ∀ (x : M), x ∈ [] → ∀ (y : M), y ∈ [] → x * y = y * x
⊢ a * ([].erase a).prod = [].prod

Tactic:
simp only [not_mem_nil] at ha

Result:
no goals

Proof state:
case cons.inr.intro
M : Type u_4
inst✝¹ : Monoid M
l✝ : List M
a : M
inst✝ : DecidableEq M
b : M
l : List M
ih : a ∈ l → (∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x) → a * (l.erase a).prod = l.prod
ha : a ∈ b :: l
comm : ∀ (x : M), x ∈ b :: l → ∀ (y : M), y ∈ b :: l → x * y = y * x
ne : a ≠ b
h : a ∈ l
⊢ a * ((b :: l).erase a).prod = (b :: l).prod

Tactic:
rw [List.erase, beq_false_of_ne ne.symm, List.prod_cons, List.prod_cons, ← mul_assoc,
  comm a ha b (l.mem_cons_self b), mul_assoc,
  ih h fun x hx y hy ↦ comm _ (List.mem_cons_of_mem b hx) _ (List.mem_cons_of_mem b hy)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem take_eq_take :
    ∀ {l : List α} {m n : Nat}, l.take m = l.take n ↔ min m l.length = min n l.length
  | [], m, n => by simp [Nat.min_zero]
  | _ :: xs, 0, 0 => by simp
  | x :: xs, m + 1, 0 => by simp [Nat.zero_min, succ_min_succ]
  | x :: xs, 0, n + 1 => by simp [Nat.zero_min, succ_min_succ]
  | x :: xs, m + 1, n + 1 => by simp [succ_min_succ, take_eq_take]

Proof state:
α : Type u_1
m n : Nat
⊢ take m [] = take n [] ↔ min m [].length = min n [].length

Tactic:
simp [Nat.min_zero]

Result:
no goals

Proof state:
α : Type u_1
x : α
xs : List α
m n : Nat
⊢ take (m + 1) (x :: xs) = take (n + 1) (x :: xs) ↔ min (m + 1) (x :: xs).length = min (n + 1) (x :: xs).length

Tactic:
simp [succ_min_succ, take_eq_take]

Result:
no goals

Proof state:
α : Type u_1
head✝ : α
xs : List α
⊢ take 0 (head✝ :: xs) = take 0 (head✝ :: xs) ↔ min 0 (head✝ :: xs).length = min 0 (head✝ :: xs).length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
x : α
xs : List α
m : Nat
⊢ take (m + 1) (x :: xs) = take 0 (x :: xs) ↔ min (m + 1) (x :: xs).length = min 0 (x :: xs).length

Tactic:
simp [Nat.zero_min, succ_min_succ]

Result:
no goals

Proof state:
α : Type u_1
x : α
xs : List α
n : Nat
⊢ take 0 (x :: xs) = take (n + 1) (x :: xs) ↔ min 0 (x :: xs).length = min (n + 1) (x :: xs).length

Tactic:
simp [Nat.zero_min, succ_min_succ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx_subtype {p : α → Prop} {l : List { x // p x }}
    {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
    l.findIdx f = l.unattach.findIdx g

Proof state:
case nil
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ findIdx f [] = findIdx g (map (fun x => x.val) [])

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
p : α → Prop
l : List { x // p x }
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ findIdx f l = findIdx g l.unattach

Tactic:
unfold unattach

Result:
α : Type u_1
p : α → Prop
l : List { x // p x }
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ findIdx f l = findIdx g (map (fun x => x.val) l)

Proof state:
case cons
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
a : { x // p x }
l : List { x // p x }
ih : findIdx f l = findIdx g (map (fun x => x.val) l)
⊢ findIdx f (a :: l) = findIdx g (map (fun x => x.val) (a :: l))

Tactic:
simp [ih, hf, findIdx_cons]

Result:
no goals

Proof state:
α : Type u_1
p : α → Prop
l : List { x // p x }
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ findIdx f l = findIdx g (map (fun x => x.val) l)

Tactic:
induction l with
| nil => simp
| cons a l ih =>
  simp [ih, hf, findIdx_cons]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_nat_mul_two_pi_add_pi (n : ℕ) : cos (n * (2 * π) + π) = -1

Proof state:
n : ℕ
⊢ cos (↑n * (2 * π) + π) = -1

Tactic:
simpa only [cos_zero] using (cos_periodic.nat_mul n).add_antiperiod_eq cos_antiperiodic

Result:
no goals
-- Mathlib/Data/List/Intervals.lean
theorem trichotomy (n a b : ℕ) : n < a ∨ b ≤ n ∨ n ∈ Ico a b

Proof state:
case neg.h
n a b : ℕ
h₁ : a ≤ n
h₂ : a ≤ n → b ≤ n
⊢ b ≤ n

Tactic:
exact h₂ h₁

Result:
no goals

Proof state:
case neg.h
n a b : ℕ
h₁ : ¬n < a
h₂ : ¬n ∈ Ico a b
⊢ b ≤ n

Tactic:
simp only [Ico.mem, not_and, not_lt] at *

Result:
case neg.h
n a b : ℕ
h₁ : a ≤ n
h₂ : a ≤ n → b ≤ n
⊢ b ≤ n

Proof state:
case neg
n a b : ℕ
h₁ : ¬n < a
h₂ : ¬n ∈ Ico a b
⊢ b ≤ n ∨ n ∈ Ico a b

Tactic:
left

Result:
case neg.h
n a b : ℕ
h₁ : ¬n < a
h₂ : ¬n ∈ Ico a b
⊢ b ≤ n

Proof state:
n a b : ℕ
⊢ n < a ∨ b ≤ n ∨ n ∈ Ico a b

Tactic:
by_cases h₁ : n < a

Result:
case pos
n a b : ℕ
h₁ : n < a
⊢ n < a ∨ b ≤ n ∨ n ∈ Ico a b

case neg
n a b : ℕ
h₁ : ¬n < a
⊢ n < a ∨ b ≤ n ∨ n ∈ Ico a b

Proof state:
case pos.h
n a b : ℕ
h₁ : n < a
⊢ n < a

Tactic:
exact h₁

Result:
no goals

Proof state:
case neg.h
n a b : ℕ
h₁ : ¬n < a
⊢ b ≤ n ∨ n ∈ Ico a b

Tactic:
by_cases h₂ : n ∈ Ico a b

Result:
case pos
n a b : ℕ
h₁ : ¬n < a
h₂ : n ∈ Ico a b
⊢ b ≤ n ∨ n ∈ Ico a b

case neg
n a b : ℕ
h₁ : ¬n < a
h₂ : ¬n ∈ Ico a b
⊢ b ≤ n ∨ n ∈ Ico a b

Proof state:
case pos.h
n a b : ℕ
h₁ : ¬n < a
h₂ : n ∈ Ico a b
⊢ n ∈ Ico a b

Tactic:
exact h₂

Result:
no goals

Proof state:
case pos
n a b : ℕ
h₁ : n < a
⊢ n < a ∨ b ≤ n ∨ n ∈ Ico a b

Tactic:
left

Result:
case pos.h
n a b : ℕ
h₁ : n < a
⊢ n < a

Proof state:
case neg
n a b : ℕ
h₁ : ¬n < a
⊢ n < a ∨ b ≤ n ∨ n ∈ Ico a b

Tactic:
right

Result:
case neg.h
n a b : ℕ
h₁ : ¬n < a
⊢ b ≤ n ∨ n ∈ Ico a b

Proof state:
case pos
n a b : ℕ
h₁ : ¬n < a
h₂ : n ∈ Ico a b
⊢ b ≤ n ∨ n ∈ Ico a b

Tactic:
right

Result:
case pos.h
n a b : ℕ
h₁ : ¬n < a
h₂ : n ∈ Ico a b
⊢ n ∈ Ico a b
-- Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean
theorem mem_parallelepiped_iff (v : ι → E) (x : E) :
    x ∈ parallelepiped v ↔ ∃ t ∈ Icc (0 : ι → ℝ) 1, x = ∑ i, t i • v i

Proof state:
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
x : E
⊢ x ∈ parallelepiped v ↔ ∃ t ∈ Icc 0 1, x = ∑ i : ι, t i • v i

Tactic:
simp [parallelepiped, eq_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem nonsing_inv_nonsing_inv (h : IsUnit A.det) : A⁻¹⁻¹ = A :=
  calc
    A⁻¹⁻¹ = 1 * A⁻¹⁻¹

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

Tactic:
rw [Matrix.mul_assoc, A⁻¹.mul_nonsing_inv (A.isUnit_nonsing_inv_det h), Matrix.mul_one]

Result:
no goals

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

Tactic:
rw [Matrix.one_mul]

Result:
no goals

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

Tactic:
rw [A.mul_nonsing_inv h]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Cardinality.lean
/-- In a topological vector space over a nontrivially normed field, any neighborhood of zero has
the same cardinality as the whole space.

See also `cardinal_eq_of_mem_nhds`. -/
lemma cardinal_eq_of_mem_nhds_zero
    {E : Type*} (𝕜 : Type*) [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E]
    [TopologicalSpace E] [ContinuousSMul 𝕜 E] {s : Set E} (hs : s ∈ 𝓝 (0 : E)) : #s = #E

Proof state:
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
x : E
⊢ Tendsto (fun n => c⁻¹ ^ n) atTop (𝓝 0)

Tactic:
apply tendsto_pow_atTop_nhds_zero_of_norm_lt_one

Result:
case h
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
x : E
⊢ ‖c⁻¹‖ < 1

Proof state:
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
x : E
this : Tendsto (fun n => (c ^ n)⁻¹) atTop (𝓝 0)
⊢ Tendsto (fun n => (c ^ n)⁻¹ • x) atTop (𝓝 (0 • x))

Tactic:
exact Tendsto.smul_const this x

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Basic.lean
theorem linearIndependent_sum {v : ι ⊕ ι' → M} :
    LinearIndependent R v ↔
      LinearIndependent R (v ∘ Sum.inl) ∧
        LinearIndependent R (v ∘ Sum.inr) ∧
          Disjoint (Submodule.span R (range (v ∘ Sum.inl)))
            (Submodule.span R (range (v ∘ Sum.inr)))

Proof state:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • (v ∘ Sum.inl) i = 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), ∑ i ∈ s, g i • (v ∘ Sum.inr) i = 0 → ∀ i ∈ s, g i = 0
hlr : Disjoint (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : ∑ i ∈ s, g i • v i = 0
i : ι ⊕ ι'
hi : i ∈ s
⊢ ∑ i ∈ s.preimage Sum.inl ⋯, (fun x => g x • v x) (Sum.inl i) +
      ∑ i ∈ s.preimage Sum.inr ⋯, (fun x => g x • v x) (Sum.inr i) =
    0

Tactic:
rw [Finset.sum_preimage' (g := fun x => g x • v x),
  Finset.sum_preimage' (g := fun x => g x • v x), ← Finset.sum_union, ← Finset.filter_or]

Result:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • (v ∘ Sum.inl) i = 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), ∑ i ∈ s, g i • (v ∘ Sum.inr) i = 0 → ∀ i ∈ s, g i = 0
hlr : Disjoint (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : ∑ i ∈ s, g i • v i = 0
i : ι ⊕ ι'
hi : i ∈ s
⊢ ∑ x ∈ Finset.filter (fun a => a ∈ range Sum.inl ∨ a ∈ range Sum.inr) s, g x • v x = 0

ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • (v ∘ Sum.inl) i = 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), ∑ i ∈ s, g i • (v ∘ Sum.inr) i = 0 → ∀ i ∈ s, g i = 0
hlr : Disjoint (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : ∑ i ∈ s, g i • v i = 0
i : ι ⊕ ι'
hi : i ∈ s
⊢ Disjoint (Finset.filter (fun x => x ∈ range Sum.inl) s) (Finset.filter (fun x => x ∈ range Sum.inr) s)
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem b₈_of_isCharThreeJNeZeroNF : W.b₈ = 4 * W.a₂ * W.a₆

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharThreeJNeZeroNF
⊢ W.b₈ = 4 * W.a₂ * W.a₆

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Factorization/PrimePow.lean
lemma IsPrimePow.factorization_minFac_ne_zero {n : ℕ} (hn : IsPrimePow n) :
    n.factorization n.minFac ≠ 0

Proof state:
n : ℕ
hn : IsPrimePow n
⊢ ¬(¬Nat.Prime n.minFac ∨ ¬n.minFac ∣ n ∨ n = 0)

Tactic:
push_neg

Result:
n : ℕ
hn : IsPrimePow n
⊢ Nat.Prime n.minFac ∧ n.minFac ∣ n ∧ n ≠ 0

Proof state:
n : ℕ
hn : IsPrimePow n
⊢ n.factorization n.minFac ≠ 0

Tactic:
refine mt (Nat.factorization_eq_zero_iff _ _).mp ?_

Result:
n : ℕ
hn : IsPrimePow n
⊢ ¬(¬Nat.Prime n.minFac ∨ ¬n.minFac ∣ n ∨ n = 0)

Proof state:
n : ℕ
hn : IsPrimePow n
⊢ Nat.Prime n.minFac ∧ n.minFac ∣ n ∧ n ≠ 0

Tactic:
exact ⟨n.minFac_prime hn.ne_one, n.minFac_dvd, hn.ne_zero⟩

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Shatter.lean
@[simp] lemma shatters_univ [Fintype α] : 𝒜.Shatters univ ↔ 𝒜 = univ

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Fintype α
⊢ 𝒜.Shatters univ ↔ 𝒜 = univ

Tactic:
rw [shatters_iff, powerset_univ]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Fintype α
⊢ image (fun t => univ ∩ t) 𝒜 = univ ↔ 𝒜 = univ

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Fintype α
⊢ image (fun t => univ ∩ t) 𝒜 = univ ↔ 𝒜 = univ

Tactic:
simp_rw [univ_inter, image_id']

Result:
no goals
-- Mathlib/FieldTheory/Perfect.lean
theorem roots_expand_pow_map_iterateFrobenius :
    (expand R (p ^ n) f).roots.map (iterateFrobenius R p n) = p ^ n • f.roots

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : PerfectRing R p
⊢ Multiset.map (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots = p ^ n • f.roots

Tactic:
simp_rw [← coe_iterateFrobeniusEquiv, roots_expand_pow, Multiset.map_nsmul,
  Multiset.map_map, comp_apply, RingEquiv.apply_symm_apply, map_id']

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem frequently_lt_of_lt_limsSup {f : Filter α} [ConditionallyCompleteLinearOrder α] {a : α}
    (hf : f.IsCobounded (· ≤ ·)

Proof state:
α : Type u_1
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder α
a : α
hf : autoParam (IsCobounded (fun x1 x2 => x1 ≤ x2) f) _auto✝
h : ∀ᶠ (x : α) in f, x ≤ a
⊢ f.limsSup ≤ a

Tactic:
exact limsSup_le_of_le hf h

Result:
no goals

Proof state:
α : Type u_1
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder α
a : α
hf : autoParam (IsCobounded (fun x1 x2 => x1 ≤ x2) f) _auto✝
h : a < f.limsSup
⊢ ∃ᶠ (n : α) in f, a < n

Tactic:
contrapose! h

Result:
α : Type u_1
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder α
a : α
hf : autoParam (IsCobounded (fun x1 x2 => x1 ≤ x2) f) _auto✝
h : ¬∃ᶠ (n : α) in f, a < n
⊢ f.limsSup ≤ a

Proof state:
α : Type u_1
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder α
a : α
hf : autoParam (IsCobounded (fun x1 x2 => x1 ≤ x2) f) _auto✝
h : ¬∃ᶠ (n : α) in f, a < n
⊢ f.limsSup ≤ a

Tactic:
simp only [not_frequently, not_lt] at h

Result:
α : Type u_1
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder α
a : α
hf : autoParam (IsCobounded (fun x1 x2 => x1 ≤ x2) f) _auto✝
h : ∀ᶠ (x : α) in f, x ≤ a
⊢ f.limsSup ≤ a
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem continuous_mass : Continuous fun μ : FiniteMeasure Ω ↦ μ.mass

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
⊢ Continuous fun μ => μ.mass

Tactic:
simp_rw [← testAgainstNN_one]

Result:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
⊢ Continuous fun μ => μ.testAgainstNN 1

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
⊢ Continuous fun μ => μ.testAgainstNN 1

Tactic:
exact continuous_testAgainstNN_eval 1

Result:
no goals
-- Mathlib/Algebra/Homology/TotalComplexShift.lean
@[reassoc]
lemma D₁_totalShift₂XIso_hom (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + y = n₀') (h₁ : n₁ + y = n₁') :
    ((shiftFunctor₂ C y).obj K).D₁ (up ℤ) n₀ n₁ ≫ (K.totalShift₂XIso y n₁ n₁' h₁).hom =
      y.negOnePow • ((K.totalShift₂XIso y n₀ n₀' h₀).hom ≫ K.D₁ (up ℤ) n₀' n₁')

Proof state:
case neg.h₁₂
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
y : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : ¬(up ℤ).Rel n₀ n₁
h' : n₀' + 1 = n₁'
⊢ n₀ + 1 = n₁

Tactic:
omega

Result:
no goals
-- Mathlib/CategoryTheory/Sites/LocallySurjective.lean
lemma isLocallySurjective_iff_epi {F G : Sheaf J (Type w)} (φ : F ⟶ G)
    [HasSheafify J (Type w)] :
    IsLocallySurjective φ ↔ Epi φ

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
φ : F ⟶ G
inst✝ : HasSheafify J (Type w)
⊢ IsLocallySurjective φ ↔ Epi φ

Tactic:
constructor

Result:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
φ : F ⟶ G
inst✝ : HasSheafify J (Type w)
⊢ IsLocallySurjective φ → Epi φ

case mpr
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
φ : F ⟶ G
inst✝ : HasSheafify J (Type w)
⊢ Epi φ → IsLocallySurjective φ

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
φ : F ⟶ G
inst✝ : HasSheafify J (Type w)
⊢ Epi φ → IsLocallySurjective φ

Tactic:
intro

Result:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
φ : F ⟶ G
inst✝ : HasSheafify J (Type w)
a✝ : Epi φ
⊢ IsLocallySurjective φ

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
φ : F ⟶ G
inst✝ : HasSheafify J (Type w)
a✝ : Epi φ
this : Epi (imageι φ)
⊢ IsIso (imageι φ)

Tactic:
apply isIso_of_mono_of_epi

Result:
no goals

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
φ : F ⟶ G
inst✝ : HasSheafify J (Type w)
a✝ : Epi φ
this : Epi (imageι φ)
⊢ IsLocallySurjective φ

Tactic:
rw [isLocallySurjective_iff_isIso φ]

Result:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
φ : F ⟶ G
inst✝ : HasSheafify J (Type w)
a✝ : Epi φ
this : Epi (imageι φ)
⊢ IsIso (imageι φ)

Proof state:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
φ : F ⟶ G
inst✝ : HasSheafify J (Type w)
a✝ : IsLocallySurjective φ
⊢ Epi φ

Tactic:
infer_instance

Result:
no goals

Proof state:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
φ : F ⟶ G
inst✝ : HasSheafify J (Type w)
⊢ IsLocallySurjective φ → Epi φ

Tactic:
intro

Result:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
φ : F ⟶ G
inst✝ : HasSheafify J (Type w)
a✝ : IsLocallySurjective φ
⊢ Epi φ

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
φ : F ⟶ G
inst✝ : HasSheafify J (Type w)
a✝ : Epi φ
⊢ IsLocallySurjective φ

Tactic:
have := epi_of_epi_fac (Sheaf.toImage_ι φ)

Result:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
φ : F ⟶ G
inst✝ : HasSheafify J (Type w)
a✝ : Epi φ
this : Epi (imageι φ)
⊢ IsLocallySurjective φ