harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem drop_modify_of_ge (f : α → α) (n m) (l : List α) (h : n ≥ m) :
    (modify f n l).drop m = modify f (n - m) (drop m l)

Proof state:
case h
α : Type u_1
f : α → α
n m : Nat
l : List α
h : n ≥ m
m' : Nat
h₁ : m' < (drop m (modify f n l)).length
h₂ : m' < (modify f (n - m) (drop m l)).length
⊢ (drop m (modify f n l))[m'] = (modify f (n - m) (drop m l))[m']

Tactic:
simp [getElem_drop, getElem_modify, ite_eq_right_iff]

Result:
case h
α : Type u_1
f : α → α
n m : Nat
l : List α
h : n ≥ m
m' : Nat
h₁ : m' < (drop m (modify f n l)).length
h₂ : m' < (modify f (n - m) (drop m l)).length
⊢ (if n = m + m' then f l[m + m'] else l[m + m']) = if n - m = m' then f l[m + m'] else l[m + m']

Proof state:
case hl
α : Type u_1
f : α → α
n m : Nat
l : List α
h : n ≥ m
⊢ (drop m (modify f n l)).length = (modify f (n - m) (drop m l)).length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
f : α → α
n m : Nat
l : List α
h : n ≥ m
⊢ drop m (modify f n l) = modify f (n - m) (drop m l)

Tactic:
apply ext_getElem

Result:
case hl
α : Type u_1
f : α → α
n m : Nat
l : List α
h : n ≥ m
⊢ (drop m (modify f n l)).length = (modify f (n - m) (drop m l)).length

case h
α : Type u_1
f : α → α
n m : Nat
l : List α
h : n ≥ m
⊢ ∀ (i : Nat) (h₁ : i < (drop m (modify f n l)).length) (h₂ : i < (modify f (n - m) (drop m l)).length),
    (drop m (modify f n l))[i] = (modify f (n - m) (drop m l))[i]

Proof state:
case h.isFalse.isTrue
α : Type u_1
f : α → α
n m : Nat
l : List α
h : n ≥ m
m' : Nat
h₁ : m' < (drop m (modify f n l)).length
h₂ : m' < (modify f (n - m) (drop m l)).length
h✝¹ : ¬n = m + m'
h✝ : n - m = m'
⊢ l[m + m'] = f l[m + m']

Tactic:
omega

Result:
no goals

Proof state:
case h
α : Type u_1
f : α → α
n m : Nat
l : List α
h : n ≥ m
m' : Nat
h₁ : m' < (drop m (modify f n l)).length
h₂ : m' < (modify f (n - m) (drop m l)).length
⊢ (if n = m + m' then f l[m + m'] else l[m + m']) = if n - m = m' then f l[m + m'] else l[m + m']

Tactic:
split <;> split <;> first | rfl | omega

Result:
no goals

Proof state:
case h
α : Type u_1
f : α → α
n m : Nat
l : List α
h : n ≥ m
⊢ ∀ (i : Nat) (h₁ : i < (drop m (modify f n l)).length) (h₂ : i < (modify f (n - m) (drop m l)).length),
    (drop m (modify f n l))[i] = (modify f (n - m) (drop m l))[i]

Tactic:
intro m' h₁ h₂

Result:
case h
α : Type u_1
f : α → α
n m : Nat
l : List α
h : n ≥ m
m' : Nat
h₁ : m' < (drop m (modify f n l)).length
h₂ : m' < (modify f (n - m) (drop m l)).length
⊢ (drop m (modify f n l))[m'] = (modify f (n - m) (drop m l))[m']

Proof state:
case h.isFalse.isFalse
α : Type u_1
f : α → α
n m : Nat
l : List α
h : n ≥ m
m' : Nat
h₁ : m' < (drop m (modify f n l)).length
h₂ : m' < (modify f (n - m) (drop m l)).length
h✝¹ : ¬n = m + m'
h✝ : ¬n - m = m'
⊢ l[m + m'] = l[m + m']

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem mem_insert_self {t : RBNode α} (ht : Balanced t c n) : v ∈ t.insert cmp v

Proof state:
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
v : α
t : RBNode α
ht : t.Balanced c n
⊢ ∃ s t_1, (insert cmp t v).toList = s ++ v :: t_1

Tactic:
exact match e : zoom (cmp v) t with
| (nil, p) => let ⟨_, _, _, h⟩ := exists_insert_toList_zoom_nil ht e; ⟨_, _, h⟩
| (node .., p) => let ⟨_, _, _, h⟩ := exists_insert_toList_zoom_node ht e; ⟨_, _, h⟩

Result:
no goals

Proof state:
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
v : α
t : RBNode α
ht : t.Balanced c n
⊢ v ∈ insert cmp t v

Tactic:
rw [← mem_toList, List.mem_iff_append]

Result:
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
v : α
t : RBNode α
ht : t.Balanced c n
⊢ ∃ s t_1, (insert cmp t v).toList = s ++ v :: t_1
-- Mathlib/Topology/Algebra/ConstMulAction.lean
theorem smul_mem_nhds_self [TopologicalSpace G] [ContinuousConstSMul G G] {g : G} {s : Set G} :
    g • s ∈ 𝓝 g ↔ s ∈ 𝓝 1

Proof state:
G : Type u_4
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousConstSMul G G
g : G
s : Set G
⊢ g⁻¹ • g • s ∈ 𝓝 (g⁻¹ • g) ↔ s ∈ 𝓝 1

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_4
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousConstSMul G G
g : G
s : Set G
⊢ g • s ∈ 𝓝 g ↔ s ∈ 𝓝 1

Tactic:
rw [← smul_mem_nhds_smul_iff g⁻¹]

Result:
G : Type u_4
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousConstSMul G G
g : G
s : Set G
⊢ g⁻¹ • g • s ∈ 𝓝 (g⁻¹ • g) ↔ s ∈ 𝓝 1
-- Mathlib/GroupTheory/Perm/ClosureSwap.lean
theorem swap_mem_closure_isSwap {S : Set (Perm α)} (hS : ∀ f ∈ S, f.IsSwap) {x y : α} :
    swap x y ∈ closure S ↔ x ∈ orbit (closure S) y

Proof state:
case refine_3
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : swap x y ∉ closure S
⊢ y ∈ {x | swap x y ∈ closure S}

Tactic:
rw [mem_setOf, swap_self]

Result:
case refine_3
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : swap x y ∉ closure S
⊢ Equiv.refl α ∈ closure S
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem not_eq_of_eq_true {a : Prop} (h : a = True) : (Not a) = False

Proof state:
a : Prop
h : a = True
⊢ (¬a) = False

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem exists_subset_range_and_iff {f : α → β} {p : Set β → Prop} :
    (∃ s, s ⊆ range f ∧ p s) ↔ ∃ s, p (f '' s)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
p : Set β → Prop
⊢ (∃ s ⊆ range f, p s) ↔ ∃ s, p (f '' s)

Tactic:
rw [← exists_range_iff, range_image]

Result:
α : Type u_1
β : Type u_2
f : α → β
p : Set β → Prop
⊢ (∃ s ⊆ range f, p s) ↔ ∃ a ∈ 𝒫 range f, p a

Proof state:
α : Type u_1
β : Type u_2
f : α → β
p : Set β → Prop
⊢ (∃ s ⊆ range f, p s) ↔ ∃ a ∈ 𝒫 range f, p a

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Bimod.lean
theorem middle_assoc' :
    (actLeft P Q ▷ T.X) ≫ actRight P Q =
      (α_ R.X _ T.X).hom ≫ (R.X ◁ actRight P Q) ≫ actLeft P Q

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S T : Mon_ C
P : Bimod R S
Q : Bimod S T
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ actLeft P Q ▷ T.X ≫ actRight P Q = (α_ R.X (X P Q) T.X).hom ≫ R.X ◁ actRight P Q ≫ actLeft P Q

Tactic:
refine (cancel_epi ((tensorLeft _ ⋙ tensorRight _).map (coequalizer.π _ _))).1 ?_

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S T : Mon_ C
P : Bimod R S
Q : Bimod S T
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ (tensorLeft R.X ⋙ tensorRight T.X).map (coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) ≫
      actLeft P Q ▷ T.X ≫ actRight P Q =
    (tensorLeft R.X ⋙ tensorRight T.X).map (coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) ≫
      (α_ R.X (X P Q) T.X).hom ≫ R.X ◁ actRight P Q ≫ actLeft P Q
-- Mathlib/Algebra/Order/Floor.lean
theorem preimage_Ici : ((↑) : ℤ → α) ⁻¹' Set.Ici a = Set.Ici ⌈a⌉

Proof state:
case h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
x✝ : ℤ
⊢ x✝ ∈ Int.cast ⁻¹' Ici a ↔ x✝ ∈ Ici ⌈a⌉

Tactic:
simp [ceil_le]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ Int.cast ⁻¹' Ici a = Ici ⌈a⌉

Tactic:
ext

Result:
case h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
x✝ : ℤ
⊢ x✝ ∈ Int.cast ⁻¹' Ici a ↔ x✝ ∈ Ici ⌈a⌉
-- Mathlib/Data/Finset/NAry.lean
@[simp (default + 1)] -- otherwise `simp` doesn't use `forall_mem_image₂`
lemma sup_image₂_le {g : γ → δ} {a : δ} :
    sup (image₂ f s t) g ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝¹ : SemilatticeSup δ
inst✝ : OrderBot δ
g : γ → δ
a : δ
⊢ (image₂ f s t).sup g ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a

Tactic:
rw [Finset.sup_le_iff, forall_mem_image₂]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Split.lean
theorem eqId_iff_len_le : A.EqId ↔ Δ.unop.len ≤ A.1.unop.len

Proof state:
case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (unop A.fst).len = (unop Δ).len → (unop Δ).len ≤ (unop A.fst).len

Tactic:
intro h

Result:
case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : (unop A.fst).len = (unop Δ).len
⊢ (unop Δ).len ≤ (unop A.fst).len

Proof state:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.EqId ↔ (unop Δ).len ≤ (unop A.fst).len

Tactic:
rw [eqId_iff_len_eq]

Result:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (unop A.fst).len = (unop Δ).len ↔ (unop Δ).len ≤ (unop A.fst).len

Proof state:
case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : (unop A.fst).len = (unop Δ).len
⊢ (unop Δ).len ≤ (unop A.fst).len

Tactic:
rw [h]

Result:
no goals

Proof state:
case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (unop Δ).len ≤ (unop A.fst).len → (unop A.fst).len = (unop Δ).len

Tactic:
exact le_antisymm (len_le_of_epi (inferInstance : Epi A.e))

Result:
no goals

Proof state:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (unop A.fst).len = (unop Δ).len ↔ (unop Δ).len ≤ (unop A.fst).len

Tactic:
constructor

Result:
case mp
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (unop A.fst).len = (unop Δ).len → (unop Δ).len ≤ (unop A.fst).len

case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (unop Δ).len ≤ (unop A.fst).len → (unop A.fst).len = (unop Δ).len
-- Mathlib/Data/Complex/Trigonometric.lean
theorem two_mul_sin_mul_sin (x y : ℝ) : 2 * sin x * sin y = cos (x - y) - cos (x + y)

Proof state:
x y : ℝ
⊢ 2 * sin x * sin y = sin x * sin y + sin x * sin y

Tactic:
ring

Result:
no goals

Proof state:
x y : ℝ
⊢ 2 * sin x * sin y = cos (x - y) - cos (x + y)

Tactic:
simp [cos_add, cos_sub]

Result:
x y : ℝ
⊢ 2 * sin x * sin y = sin x * sin y + sin x * sin y
-- Mathlib/Data/Set/Finite/Lattice.lean
theorem Finite.biUnion' {ι} {s : Set ι} (hs : s.Finite) {t : ∀ i ∈ s, Set α}
    (ht : ∀ i (hi : i ∈ s), (t i hi).Finite) : (⋃ i ∈ s, t i ‹_›).Finite

Proof state:
α : Type u
ι : Type u_1
s : Set ι
hs : s.Finite
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), (t i hi).Finite
⊢ (⋃ i, ⋃ (h : i ∈ s), t i h).Finite

Tactic:
have := hs.to_subtype

Result:
α : Type u
ι : Type u_1
s : Set ι
hs : s.Finite
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), (t i hi).Finite
this : Finite ↑s
⊢ (⋃ i, ⋃ (h : i ∈ s), t i h).Finite

Proof state:
α : Type u
ι : Type u_1
s : Set ι
hs : s.Finite
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), (t i hi).Finite
this : Finite ↑s
⊢ (⋃ x, t ↑x ⋯).Finite

Tactic:
apply finite_iUnion fun i : s => ht i.1 i.2

Result:
no goals

Proof state:
α : Type u
ι : Type u_1
s : Set ι
hs : s.Finite
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), (t i hi).Finite
this : Finite ↑s
⊢ (⋃ i, ⋃ (h : i ∈ s), t i h).Finite

Tactic:
rw [biUnion_eq_iUnion]

Result:
α : Type u
ι : Type u_1
s : Set ι
hs : s.Finite
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), (t i hi).Finite
this : Finite ↑s
⊢ (⋃ x, t ↑x ⋯).Finite
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem unzip_fst : (unzip l).fst = l.map Prod.fst

Proof state:
α✝ : Type u_1
β✝ : Type u_2
l : Array (α✝ × β✝)
⊢ l.unzip.fst = map Prod.fst l

Tactic:
induction l <;> simp_all

Result:
no goals
-- Mathlib/Data/Nat/Prime/Defs.lean
theorem coprime_of_dvd {m n : ℕ} (H : ∀ k, Prime k → k ∣ m → ¬k ∣ n) : Coprime m n

Proof state:
case intro.intro.a
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬m.gcd n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ m.gcd n
⊢ m.gcd n ∣ n

Tactic:
exact gcd_dvd_right _ _

Result:
no goals

Proof state:
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
⊢ m.Coprime n

Tactic:
rw [coprime_iff_gcd_eq_one]

Result:
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
⊢ m.gcd n = 1

Proof state:
case intro.intro.a
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬m.gcd n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ m.gcd n
⊢ m.gcd n ∣ m

Tactic:
exact gcd_dvd_left _ _

Result:
no goals

Proof state:
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
⊢ m.gcd n = 1

Tactic:
by_contra g2

Result:
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬m.gcd n = 1
⊢ False

Proof state:
case intro.intro
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬m.gcd n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ m.gcd n
⊢ False

Tactic:
apply H p hp <;> apply dvd_trans hpdvd

Result:
case intro.intro.a
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬m.gcd n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ m.gcd n
⊢ m.gcd n ∣ m

case intro.intro.a
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬m.gcd n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ m.gcd n
⊢ m.gcd n ∣ n

Proof state:
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬m.gcd n = 1
⊢ False

Tactic:
obtain ⟨p, hp, hpdvd⟩ := exists_prime_and_dvd g2

Result:
case intro.intro
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬m.gcd n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ m.gcd n
⊢ False
-- Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean
theorem Fix.rec_unique {β : Type u} (g : F (append1 α β) → β) (h : Fix F α → β)
    (hyp : ∀ x, h (Fix.mk x) = g (appendFun id h <$$> x)) : Fix.rec g = h

Proof state:
case h.h
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)
x✝ : Fix F α
x : F (α ::: Fix F α)
hyp' : (TypeVec.id ::: rec g) <$$> x = (TypeVec.id ::: h) <$$> x
⊢ rec g (mk x) = h (mk x)

Tactic:
rw [hyp, ← hyp', Fix.rec_eq]

Result:
no goals

Proof state:
case h
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)
x : Fix F α
⊢ rec g x = h x

Tactic:
apply Fix.ind_rec

Result:
case h.h
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)
x : Fix F α
⊢ ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: rec g) <$$> x = (TypeVec.id ::: h) <$$> x → rec g (mk x) = h (mk x)

Proof state:
case h.h
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)
x : Fix F α
⊢ ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: rec g) <$$> x = (TypeVec.id ::: h) <$$> x → rec g (mk x) = h (mk x)

Tactic:
intro x hyp'

Result:
case h.h
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)
x✝ : Fix F α
x : F (α ::: Fix F α)
hyp' : (TypeVec.id ::: rec g) <$$> x = (TypeVec.id ::: h) <$$> x
⊢ rec g (mk x) = h (mk x)

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)
⊢ rec g = h

Tactic:
ext x

Result:
case h
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)
x : Fix F α
⊢ rec g x = h x
-- Mathlib/NumberTheory/Multiplicity.lean
theorem Int.emultiplicity_pow_sub_pow {x y : ℤ} (hxy : ↑p ∣ x - y) (hx : ¬↑p ∣ x) (n : ℕ) :
    emultiplicity (↑p) (x ^ n - y ^ n) = emultiplicity (↑p) (x - y) + emultiplicity p n

Proof state:
case succ
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p n.succ
⊢ emultiplicity (↑p) (x ^ (n + 1) - y ^ (n + 1)) = emultiplicity (↑p) (x - y) + emultiplicity p (n + 1)

Tactic:
simp only [Nat.succ_eq_add_one] at h

Result:
case succ
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
⊢ emultiplicity (↑p) (x ^ (n + 1) - y ^ (n + 1)) = emultiplicity (↑p) (x - y) + emultiplicity p (n + 1)

Proof state:
case succ.intro.intro
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ emultiplicity (↑p) ((x ^ p ^ multiplicity p (n + 1)) ^ k - (y ^ p ^ multiplicity p (n + 1)) ^ k) =
    emultiplicity (↑p) (x - y) + emultiplicity p (n + 1)

Tactic:
rw [Nat.prime_iff_prime_int] at hp

Result:
case succ.intro.intro
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ emultiplicity (↑p) ((x ^ p ^ multiplicity p (n + 1)) ^ k - (y ^ p ^ multiplicity p (n + 1)) ^ k) =
    emultiplicity (↑p) (x - y) + emultiplicity p (n + 1)

Proof state:
case succ.intro.intro.hxy
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ ↑p ∣ (∑ i ∈ range (p ^ multiplicity p (n + 1)), x ^ i * y ^ (p ^ multiplicity p (n + 1) - 1 - i)) * (x - y)

Tactic:
exact dvd_mul_of_dvd_right hxy _

Result:
no goals
-- Mathlib/LinearAlgebra/Trace.lean
lemma trace_comp_cycle' (f : M →ₗ[R] N) (g : N →ₗ[R] P) (h : P →ₗ[R] M) :
    trace R P ((g ∘ₗ f) ∘ₗ h) = trace R M ((h ∘ₗ g) ∘ₗ f)

Proof state:
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
N : Type u_3
P : Type u_4
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : P →ₗ[R] M
⊢ (trace R P) ((g ∘ₗ f) ∘ₗ h) = (trace R M) ((h ∘ₗ g) ∘ₗ f)

Tactic:
rw [trace_comp_comm', ← comp_assoc]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/AbelianImages.lean
theorem PreservesImage.iso_inv_ι :
    (PreservesImage.iso F f).inv ≫ F.map (Abelian.image.ι f) = Abelian.image.ι (F.map f)

Proof state:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
inst✝⁸ : HasKernels C
inst✝⁷ : HasCokernels C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
inst✝⁴ : HasKernels D
inst✝³ : HasCokernels D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : PreservesLimitsOfShape WalkingParallelPair F
inst✝ : PreservesColimitsOfShape WalkingParallelPair F
X Y : C
f : X ⟶ Y
⊢ (iso F f).inv ≫ F.map (image.ι f) = image.ι (F.map f)

Tactic:
simp [iso]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean
theorem contractLeft_ι (x : M) : d⌋ι Q x = algebraMap R _ (d x)

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
x : M
⊢ (contractLeft d) ((ι Q) x) = (algebraMap R (CliffordAlgebra Q)) (d x)

Tactic:
refine (foldr'_ι _ _ ?_ _ _).trans <| by
  simp_rw [contractLeftAux_apply_apply, mul_zero, sub_zero,
    Algebra.algebraMap_eq_smul_one]

Result:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
x : M
⊢ ∀ (m : M) (x fx : CliffordAlgebra Q),
    ((contractLeftAux Q d) m) ((ι Q) m * x, ((contractLeftAux Q d) m) (x, fx)) = Q m • fx

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
x : M
⊢ ∀ (m : M) (x fx : CliffordAlgebra Q),
    ((contractLeftAux Q d) m) ((ι Q) m * x, ((contractLeftAux Q d) m) (x, fx)) = Q m • fx

Tactic:
exact fun m x fx ↦ contractLeftAux_contractLeftAux Q d m x fx

Result:
no goals

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
x : M
⊢ ((contractLeftAux Q d) x) (1, 0) = (algebraMap R (CliffordAlgebra Q)) (d x)

Tactic:
simp_rw [contractLeftAux_apply_apply, mul_zero, sub_zero,
  Algebra.algebraMap_eq_smul_one]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem ae_map_iff {p : β → Prop} {μ : Measure α} : (∀ᵐ x ∂μ.map f, p x) ↔ ∀ᵐ x ∂μ, p (f x)

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
p : β → Prop
μ : Measure α
⊢ (∀ᵐ (x : β) ∂Measure.map f μ, p x) ↔ ∀ᵐ (x : α) ∂μ, p (f x)

Tactic:
simp only [ae_iff, hf.map_apply, preimage_setOf_eq]

Result:
no goals
-- Mathlib/FieldTheory/Separable.lean
theorem _root_.Irreducible.separable [CharZero F] {f : F[X]} (hf : Irreducible f) :
    f.Separable

Proof state:
case hp
F : Type u
inst✝¹ : Field F
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
⊢ 0 < f.natDegree

Tactic:
rw [pos_iff_ne_zero, Ne, natDegree_eq_zero_iff_degree_le_zero, degree_le_zero_iff]

Result:
case hp
F : Type u
inst✝¹ : Field F
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
⊢ ¬f = C (f.coeff 0)

Proof state:
case hp
F : Type u
inst✝¹ : Field F
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
hf1 : f = 0
hf2 : f.coeff 0 = 0
⊢ False

Tactic:
exact absurd hf1 hf.ne_zero

Result:
no goals

Proof state:
case hp
F : Type u
inst✝¹ : Field F
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
hf1 : f = C (f.coeff 0)
⊢ f.coeff 0 ≠ 0

Tactic:
intro hf2

Result:
case hp
F : Type u
inst✝¹ : Field F
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
hf1 : f = C (f.coeff 0)
hf2 : f.coeff 0 = 0
⊢ False

Proof state:
case hp
F : Type u
inst✝¹ : Field F
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
hf1 : f = C (f.coeff 0)
⊢ IsUnit f

Tactic:
rw [hf1, isUnit_C, isUnit_iff_ne_zero]

Result:
case hp
F : Type u
inst✝¹ : Field F
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
hf1 : f = C (f.coeff 0)
⊢ f.coeff 0 ≠ 0

Proof state:
F : Type u
inst✝¹ : Field F
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
⊢ ¬↑(f.natDegree - 1) = ⊥

Tactic:
rintro ⟨⟩

Result:
no goals

Proof state:
case hp
F : Type u
inst✝¹ : Field F
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
hf1 : f = C (f.coeff 0)
hf2 : f.coeff 0 = 0
⊢ False

Tactic:
rw [hf2, C_0] at hf1

Result:
case hp
F : Type u
inst✝¹ : Field F
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
hf1 : f = 0
hf2 : f.coeff 0 = 0
⊢ False

Proof state:
F : Type u
inst✝¹ : Field F
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
⊢ f.Separable

Tactic:
rw [separable_iff_derivative_ne_zero hf, Ne, ← degree_eq_bot, degree_derivative_eq]

Result:
F : Type u
inst✝¹ : Field F
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
⊢ ¬↑(f.natDegree - 1) = ⊥

case hp
F : Type u
inst✝¹ : Field F
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
⊢ 0 < f.natDegree

Proof state:
case hp
F : Type u
inst✝¹ : Field F
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
⊢ ¬f = C (f.coeff 0)

Tactic:
refine fun hf1 => hf.not_unit ?_

Result:
case hp
F : Type u
inst✝¹ : Field F
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
hf1 : f = C (f.coeff 0)
⊢ IsUnit f
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem ediv_eq_ediv_of_mul_eq_mul {a b c d : Int}
    (H2 : d ∣ c) (H3 : b ≠ 0) (H4 : d ≠ 0) (H5 : a * d = b * c) : a / b = c / d :=
  Int.ediv_eq_of_eq_mul_right H3 <| by
    rw [← Int.mul_ediv_assoc _ H2]; exact (Int.ediv_eq_of_eq_mul_left H4 H5.symm).symm

Proof state:
a b c d : Int
H2 : d ∣ c
H3 : b ≠ 0
H4 : d ≠ 0
H5 : a * d = b * c
⊢ a = b * (c / d)

Tactic:
rw [← Int.mul_ediv_assoc _ H2]

Result:
a b c d : Int
H2 : d ∣ c
H3 : b ≠ 0
H4 : d ≠ 0
H5 : a * d = b * c
⊢ a = b * c / d

Proof state:
a b c d : Int
H2 : d ∣ c
H3 : b ≠ 0
H4 : d ≠ 0
H5 : a * d = b * c
⊢ a = b * c / d

Tactic:
exact (Int.ediv_eq_of_eq_mul_left H4 H5.symm).symm

Result:
no goals