harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean
private lemma reduce_aux {A : Δ m} (h : (A.1 1 0) ≠ 0) :
    |((reduceStep A).1 1 0)| < |(A.1 1 0)|

Proof state:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 ≠ 0
this : ↑(reduceStep A) 1 0 = ↑A 0 0 % ↑A 1 0
⊢ |↑(reduceStep A) 1 0| < |↑A 1 0|

Tactic:
rw [this, abs_eq_self.mpr (Int.emod_nonneg (A.1 0 0) h)]

Result:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 ≠ 0
this : ↑(reduceStep A) 1 0 = ↑A 0 0 % ↑A 1 0
⊢ ↑A 0 0 % ↑A 1 0 < |↑A 1 0|

Proof state:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 ≠ 0
⊢ ↑(reduceStep A) 1 0 = ↑A 0 0 % ↑A 1 0

Tactic:
simp_rw [Int.emod_def, sub_eq_add_neg, reduceStep, smul_coe, coe_T_zpow, S]

Result:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 ≠ 0
⊢ (!![0, -1; 1, 0] * (!![1, -(↑A 0 0 / ↑A 1 0); 0, 1] * ↑A)) 1 0 = ↑A 0 0 + -(↑A 1 0 * (↑A 0 0 / ↑A 1 0))

Proof state:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 ≠ 0
⊢ |↑(reduceStep A) 1 0| < |↑A 1 0|

Tactic:
suffices ((reduceStep A).1 1 0) = A.1 0 0 % A.1 1 0 by
  rw [this, abs_eq_self.mpr (Int.emod_nonneg (A.1 0 0) h)]
  exact Int.emod_lt (A.1 0 0) h

Result:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 ≠ 0
⊢ ↑(reduceStep A) 1 0 = ↑A 0 0 % ↑A 1 0

Proof state:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 ≠ 0
this : ↑(reduceStep A) 1 0 = ↑A 0 0 % ↑A 1 0
⊢ ↑A 0 0 % ↑A 1 0 < |↑A 1 0|

Tactic:
exact Int.emod_lt (A.1 0 0) h

Result:
no goals

Proof state:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 ≠ 0
⊢ (!![0, -1; 1, 0] * (!![1, -(↑A 0 0 / ↑A 1 0); 0, 1] * ↑A)) 1 0 = ↑A 0 0 + -(↑A 1 0 * (↑A 0 0 / ↑A 1 0))

Tactic:
norm_num [vecMul, vecHead, vecTail, mul_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Cylinders.lean
theorem cylinder_mem_measurableCylinders (s : Finset ι) (S : Set (∀ i : s, α i))
    (hS : MeasurableSet S) :
    cylinder s S ∈ measurableCylinders α

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
hS : MeasurableSet S
⊢ ∃ s_1 S_1, MeasurableSet S_1 ∧ cylinder s S = cylinder s_1 S_1

Tactic:
exact ⟨s, S, hS, rfl⟩

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
hS : MeasurableSet S
⊢ cylinder s S ∈ measurableCylinders α

Tactic:
rw [mem_measurableCylinders]

Result:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
hS : MeasurableSet S
⊢ ∃ s_1 S_1, MeasurableSet S_1 ∧ cylinder s S = cylinder s_1 S_1
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem wfImp_updateBucket_alter [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α]
    {m : Raw₀ α (fun _ => β)} (h : Raw.WFImp m.1) {a : α} {f : Option β → Option β} :
    Raw.WFImp (withComputedSize <| updateBucket m.1.buckets m.2 a (AssocList.Const.alter a f)) where
  buckets_hash_self := isHashSelf_updateBucket_alter h
  size_eq

Proof state:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : EquivBEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : Raw.WFImp m.val
a : α
f : Option β → Option β
⊢ (toListModel (updateBucket m.val.buckets ⋯ a (AssocList.Const.alter a f))).length =
    (toListModel (withComputedSize (updateBucket m.val.buckets ⋯ a (AssocList.Const.alter a f))).buckets).length

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : EquivBEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : Raw.WFImp m.val
a : α
f : Option β → Option β
⊢ (withComputedSize (updateBucket m.val.buckets ⋯ a (AssocList.Const.alter a f))).size =
    (toListModel (withComputedSize (updateBucket m.val.buckets ⋯ a (AssocList.Const.alter a f))).buckets).length

Tactic:
rw [size_withComputedSize, computeSize_eq]

Result:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : EquivBEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : Raw.WFImp m.val
a : α
f : Option β → Option β
⊢ (toListModel (updateBucket m.val.buckets ⋯ a (AssocList.Const.alter a f))).length =
    (toListModel (withComputedSize (updateBucket m.val.buckets ⋯ a (AssocList.Const.alter a f))).buckets).length
-- Mathlib/RingTheory/Ideal/Prime.lean
theorem IsPrime.mul_mem_iff_mem_or_mem {I : Ideal α} (hI : I.IsPrime) :
    ∀ {x y : α}, x * y ∈ I ↔ x ∈ I ∨ y ∈ I := @fun x y =>
  ⟨hI.mem_or_mem, by
    rintro (h | h)
    exacts [I.mul_mem_right y h, I.mul_mem_left x h]⟩

Proof state:
case inl
α : Type u
inst✝ : CommSemiring α
I : Ideal α
hI : I.IsPrime
x y : α
h : x ∈ I
⊢ x * y ∈ I

case inr
α : Type u
inst✝ : CommSemiring α
I : Ideal α
hI : I.IsPrime
x y : α
h : y ∈ I
⊢ x * y ∈ I

Tactic:
exacts [I.mul_mem_right y h, I.mul_mem_left x h]

Result:
no goals

Proof state:
α : Type u
inst✝ : CommSemiring α
I : Ideal α
hI : I.IsPrime
x y : α
⊢ x ∈ I ∨ y ∈ I → x * y ∈ I

Tactic:
rintro (h | h)

Result:
case inl
α : Type u
inst✝ : CommSemiring α
I : Ideal α
hI : I.IsPrime
x y : α
h : x ∈ I
⊢ x * y ∈ I

case inr
α : Type u
inst✝ : CommSemiring α
I : Ideal α
hI : I.IsPrime
x y : α
h : y ∈ I
⊢ x * y ∈ I
-- Mathlib/Algebra/Order/Field/Basic.lean
lemma le_mul_of_forall_lt₀ {a b c : α} (h : ∀ a' > a, ∀ b' > b, c ≤ a' * b') : c ≤ a * b

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
⊢ c ≤ a * b

Tactic:
refine le_of_forall_gt_imp_ge_of_dense fun d hd ↦ ?_

Result:
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : α
hd : a * b < d
⊢ c ≤ d

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : α
hd : a * b < d
⊢ c ≤ d

Tactic:
obtain ⟨a', ha', hd⟩ := exists_mul_left_lt₀ hd

Result:
case intro.intro
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : α
hd✝ : a * b < d
a' : α
ha' : a' > a
hd : a' * b < d
⊢ c ≤ d

Proof state:
case intro.intro.intro.intro
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : α
hd✝¹ : a * b < d
a' : α
ha' : a' > a
hd✝ : a' * b < d
b' : α
hb' : b' > b
hd : a' * b' < d
⊢ c ≤ d

Tactic:
exact (h a' ha' b' hb').trans hd.le

Result:
no goals

Proof state:
case intro.intro
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : α
hd✝ : a * b < d
a' : α
ha' : a' > a
hd : a' * b < d
⊢ c ≤ d

Tactic:
obtain ⟨b', hb', hd⟩ := exists_mul_right_lt₀ hd

Result:
case intro.intro.intro.intro
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : α
hd✝¹ : a * b < d
a' : α
ha' : a' > a
hd✝ : a' * b < d
b' : α
hb' : b' > b
hd : a' * b' < d
⊢ c ≤ d
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_updateCol_sum (A : Matrix n n R) (j : n) (c : n → R) :
    (A.updateCol j (fun k ↦ ∑ i, (c i) • A k i)).det = (c j) • A.det

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
j : n
c : n → R
⊢ (A.updateCol j fun k => ∑ i : n, c i • A k i).det = c j • A.det

Tactic:
rw [← det_transpose, ← updateRow_transpose, ← det_transpose A]

Result:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
j : n
c : n → R
⊢ (Aᵀ.updateRow j fun k => ∑ i : n, c i • A k i).det = c j • Aᵀ.det

Proof state:
case h.e'_2.h.e'_6.h.e'_7.h
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
j : n
c : n → R
x✝ : n
⊢ ∑ i : n, c i • A x✝ i = (∑ k : n, c k • Aᵀ k) x✝

Tactic:
simp only [smul_eq_mul, Finset.sum_apply, Pi.smul_apply, transpose_apply]

Result:
no goals

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
j : n
c : n → R
⊢ (Aᵀ.updateRow j fun k => ∑ i : n, c i • A k i).det = c j • Aᵀ.det

Tactic:
convert det_updateRow_sum A.transpose j c

Result:
case h.e'_2.h.e'_6.h.e'_7.h
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
j : n
c : n → R
x✝ : n
⊢ ∑ i : n, c i • A x✝ i = (∑ k : n, c k • Aᵀ k) x✝
-- Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean
/-- The standard additive character `ZMod N → ℂ` is primitive. -/
lemma isPrimitive_stdAddChar (N : ℕ) [NeZero N] :
    (stdAddChar (N := N)).IsPrimitive

Proof state:
N : ℕ
inst✝ : NeZero N
⊢ stdAddChar.IsPrimitive

Tactic:
refine AddChar.zmod_char_primitive_of_eq_one_only_at_zero _ _ (fun t ht ↦ ?_)

Result:
N : ℕ
inst✝ : NeZero N
t : ZMod N
ht : stdAddChar t = 1
⊢ t = 0

Proof state:
N : ℕ
inst✝ : NeZero N
t : ZMod N
ht : stdAddChar t = 1
⊢ t = 0

Tactic:
rwa [← (stdAddChar (N := N)).map_zero_eq_one, injective_stdAddChar.eq_iff] at ht

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Prod.lean
theorem integral_prod_smul {𝕜 : Type*} [RCLike 𝕜] [NormedSpace 𝕜 E] (f : α → 𝕜) (g : β → E) :
    ∫ z, f z.1 • g z.2 ∂μ.prod ν = (∫ x, f x ∂μ) • ∫ y, g y ∂ν

Proof state:
case pos
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : SFinite ν
inst✝³ : NormedSpace ℝ E
inst✝² : SFinite μ
𝕜 : Type u_5
inst✝¹ : RCLike 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hE : CompleteSpace E
⊢ ∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν = (∫ (x : α), f x ∂μ) • ∫ (y : β), g y ∂ν

case neg
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : SFinite ν
inst✝³ : NormedSpace ℝ E
inst✝² : SFinite μ
𝕜 : Type u_5
inst✝¹ : RCLike 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hE : ¬CompleteSpace E
⊢ ∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν = (∫ (x : α), f x ∂μ) • ∫ (y : β), g y ∂ν

Tactic:
swap

Result:
case neg
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : SFinite ν
inst✝³ : NormedSpace ℝ E
inst✝² : SFinite μ
𝕜 : Type u_5
inst✝¹ : RCLike 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hE : ¬CompleteSpace E
⊢ ∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν = (∫ (x : α), f x ∂μ) • ∫ (y : β), g y ∂ν

case pos
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : SFinite ν
inst✝³ : NormedSpace ℝ E
inst✝² : SFinite μ
𝕜 : Type u_5
inst✝¹ : RCLike 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hE : CompleteSpace E
⊢ ∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν = (∫ (x : α), f x ∂μ) • ∫ (y : β), g y ∂ν

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : SFinite ν
inst✝³ : NormedSpace ℝ E
inst✝² : SFinite μ
𝕜 : Type u_5
inst✝¹ : RCLike 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hE : CompleteSpace E
h : ¬Integrable (fun z => f z.1 • g z.2) (μ.prod ν)
⊢ ¬Integrable f μ ∨ ¬Integrable g ν

Tactic:
contrapose! h

Result:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : SFinite ν
inst✝³ : NormedSpace ℝ E
inst✝² : SFinite μ
𝕜 : Type u_5
inst✝¹ : RCLike 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hE : CompleteSpace E
h : Integrable f μ ∧ Integrable g ν
⊢ Integrable (fun z => f z.1 • g z.2) (μ.prod ν)
-- Mathlib/Order/JordanHolder.lean
theorem smash {s₁ s₂ t₁ t₂ : CompositionSeries X}
    (hs : s₁.last = s₂.head) (ht : t₁.last = t₂.head)
    (h₁ : Equivalent s₁ t₁) (h₂ : Equivalent s₂ t₂) :
    Equivalent (smash s₁ s₂ hs) (smash t₁ t₂ ht) :=
  let e : Fin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
    calc
      Fin (s₁.length + s₂.length) ≃ (Fin s₁.length) ⊕ (Fin s₂.length) := finSumFinEquiv.symm
      _ ≃ (Fin t₁.length) ⊕ (Fin t₂.length) := Equiv.sumCongr h₁.choose h₂.choose
      _ ≃ Fin (t₁.length + t₂.length) := finSumFinEquiv
  ⟨e, by
    intro i
    refine Fin.addCases ?_ ?_ i
    · intro i
      simpa [-smash_toFun, e, smash_castAdd, smash_succ_castAdd] using h₁.choose_spec i
    · intro i
      simpa [-smash_toFun, e, smash_natAdd, smash_succ_natAdd] using h₂.choose_spec i⟩

Proof state:
case refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ t₁ t₂ : CompositionSeries X
hs : last s₁ = head s₂
ht : last t₁ = head t₂
h₁ : s₁.Equivalent t₁
h₂ : s₂.Equivalent t₂
e : Fin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
  Trans.trans (Trans.trans finSumFinEquiv.symm ((Exists.choose h₁).sumCongr (Exists.choose h₂))) finSumFinEquiv
i✝ : Fin (smash s₁ s₂ hs).length
i : Fin s₁.length
⊢ Iso ((smash s₁ s₂ hs).toFun (Fin.castAdd s₂.length i).castSucc, (smash s₁ s₂ hs).toFun (Fin.castAdd s₂.length i).succ)
    ((smash t₁ t₂ ht).toFun (e (Fin.castAdd s₂.length i)).castSucc,
      (smash t₁ t₂ ht).toFun (e (Fin.castAdd s₂.length i)).succ)

Tactic:
simpa [-smash_toFun, e, smash_castAdd, smash_succ_castAdd] using h₁.choose_spec i

Result:
no goals
-- Mathlib/Data/Set/Function.lean
protected lemma SurjOn.extendDomain (h : SurjOn g s t) :
    SurjOn (g.extendDomain f) ((↑) ∘ f '' s) ((↑) ∘ f '' t)

Proof state:
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
s t : Set α
h : SurjOn (⇑g) s t
b : α
hb : b ∈ s
ha : g b ∈ t
⊢ (g.extendDomain f) ((Subtype.val ∘ ⇑f) b) = (Subtype.val ∘ ⇑f) (g b)

Tactic:
simp_rw [Function.comp_apply, extendDomain_apply_image]

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
s t : Set α
h : SurjOn (⇑g) s t
b : α
hb : b ∈ s
ha : g b ∈ t
⊢ (Subtype.val ∘ ⇑f) (g b) ∈ ⇑(g.extendDomain f) '' (Subtype.val ∘ ⇑f '' s)

Tactic:
exact ⟨_, ⟨_, hb, rfl⟩, by simp_rw [Function.comp_apply, extendDomain_apply_image]⟩

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
s t : Set α
h : SurjOn (⇑g) s t
a : α
ha : a ∈ t
⊢ (Subtype.val ∘ ⇑f) a ∈ ⇑(g.extendDomain f) '' (Subtype.val ∘ ⇑f '' s)

Tactic:
obtain ⟨b, hb, rfl⟩ := h ha

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
s t : Set α
h : SurjOn (⇑g) s t
b : α
hb : b ∈ s
ha : g b ∈ t
⊢ (Subtype.val ∘ ⇑f) (g b) ∈ ⇑(g.extendDomain f) '' (Subtype.val ∘ ⇑f '' s)

Proof state:
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
s t : Set α
h : SurjOn (⇑g) s t
⊢ SurjOn (⇑(g.extendDomain f)) (Subtype.val ∘ ⇑f '' s) (Subtype.val ∘ ⇑f '' t)

Tactic:
rintro _ ⟨a, ha, rfl⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
s t : Set α
h : SurjOn (⇑g) s t
a : α
ha : a ∈ t
⊢ (Subtype.val ∘ ⇑f) a ∈ ⇑(g.extendDomain f) '' (Subtype.val ∘ ⇑f '' s)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey?_insert [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a k : α} {v : β k} :
    (m.insert k v).getKey? a = if k == a then some k else m.getKey? a

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
a k : α
v : β k
⊢ (m.insert k v).getKey? a = if (k == a) = true then some k else m.getKey? a

Tactic:
simp_to_model [insert] using List.getKey?_insertEntry

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem coe_monomial (n : σ →₀ ℕ) (a : R) :
    (monomial n a : MvPowerSeries σ R) = MvPowerSeries.monomial R n a :=
  MvPowerSeries.ext fun m => by
    classical
    rw [coeff_coe, coeff_monomial, MvPowerSeries.coeff_monomial]
    split_ifs with h₁ h₂ <;> first |rfl|subst m; contradiction

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
⊢ (MvPowerSeries.coeff R m) ↑((monomial n) a) = (MvPowerSeries.coeff R m) ((MvPowerSeries.monomial R n) a)

Tactic:
classical
rw [coeff_coe, coeff_monomial, MvPowerSeries.coeff_monomial]
split_ifs with h₁ h₂ <;> first |rfl|subst m; contradiction

Result:
no goals

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
h₁ : ¬n = n
⊢ 0 = a

Tactic:
contradiction

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
⊢ (if n = m then a else 0) = if m = n then a else 0

Tactic:
split_ifs with h₁ h₂ <;> first |rfl|subst m; contradiction

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
⊢ (MvPowerSeries.coeff R m) ↑((monomial n) a) = (MvPowerSeries.coeff R m) ((MvPowerSeries.monomial R n) a)

Tactic:
rw [coeff_coe, coeff_monomial, MvPowerSeries.coeff_monomial]

Result:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
⊢ (if n = m then a else 0) = if m = n then a else 0

Proof state:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
h₁ : ¬n = m
h✝ : ¬m = n
⊢ 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
h₁ : ¬n = m
h✝ : m = n
⊢ 0 = a

Tactic:
subst m

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
h₁ : ¬n = n
⊢ 0 = a
-- Mathlib/AlgebraicTopology/DoldKan/GammaCompN.lean
theorem N₁Γ₀_app (K : ChainComplex C ℕ) :
    N₁Γ₀.app K = (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.symm ≪≫
      (toKaroubi _).mapIso (Γ₀NondegComplexIso K)

Proof state:
case w
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ Split.toKaroubiNondegComplexFunctorIsoN₁.inv.app (Split.mk' (Γ₀.splitting K)) ≫
      (toKaroubi (ChainComplex C ℕ)).map (Γ₀'CompNondegComplexFunctor.hom.app K) =
    (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv ≫ (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom

Tactic:
rfl

Result:
no goals

Proof state:
case w
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ (((𝟙 (N₁.obj (Γ₀.obj K)) ≫ Split.toKaroubiNondegComplexFunctorIsoN₁.inv.app (Split.mk' (Γ₀.splitting K))) ≫
          𝟙 ((toKaroubi (ChainComplex C ℕ)).obj (Γ₀.splitting K).nondegComplex)) ≫
        (toKaroubi (ChainComplex C ℕ)).map (Γ₀'CompNondegComplexFunctor.hom.app K)) ≫
      𝟙 ((toKaroubi (ChainComplex C ℕ)).obj K) =
    (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv ≫ (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom

Tactic:
erw [id_comp, comp_id, comp_id]

Result:
case w
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ Split.toKaroubiNondegComplexFunctorIsoN₁.inv.app (Split.mk' (Γ₀.splitting K)) ≫
      (toKaroubi (ChainComplex C ℕ)).map (Γ₀'CompNondegComplexFunctor.hom.app K) =
    (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv ≫ (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom

Proof state:
case w
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ (N₁Γ₀.app K).hom =
    ((Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.symm ≪≫
        (toKaroubi (ChainComplex C ℕ)).mapIso (Γ₀NondegComplexIso K)).hom

Tactic:
dsimp [N₁Γ₀]

Result:
case w
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ (((𝟙 (N₁.obj (Γ₀.obj K)) ≫ Split.toKaroubiNondegComplexFunctorIsoN₁.inv.app (Split.mk' (Γ₀.splitting K))) ≫
          𝟙 ((toKaroubi (ChainComplex C ℕ)).obj (Γ₀.splitting K).nondegComplex)) ≫
        (toKaroubi (ChainComplex C ℕ)).map (Γ₀'CompNondegComplexFunctor.hom.app K)) ≫
      𝟙 ((toKaroubi (ChainComplex C ℕ)).obj K) =
    (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv ≫ (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ N₁Γ₀.app K =
    (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.symm ≪≫ (toKaroubi (ChainComplex C ℕ)).mapIso (Γ₀NondegComplexIso K)

Tactic:
ext1

Result:
case w
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ (N₁Γ₀.app K).hom =
    ((Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.symm ≪≫
        (toKaroubi (ChainComplex C ℕ)).mapIso (Γ₀NondegComplexIso K)).hom
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Roots.lean
theorem _root_.isRoot_of_unity_iff (h : 0 < n) (R : Type*) [CommRing R] [IsDomain R] {ζ : R} :
    ζ ^ n = 1 ↔ ∃ i ∈ n.divisors, (cyclotomic i R).IsRoot ζ

Proof state:
n : ℕ
h : 0 < n
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
⊢ ζ ^ n = 1 ↔ ∃ i ∈ n.divisors, (cyclotomic i R).IsRoot ζ

Tactic:
rw [← mem_nthRoots h, nthRoots, mem_roots <| X_pow_sub_C_ne_zero h _, C_1, ←
    prod_cyclotomic_eq_X_pow_sub_one h, isRoot_prod]

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem orderOf_dvd_natCard {G : Type*} [Group G] (x : G) : orderOf x ∣ Nat.card G

Proof state:
G : Type u_6
inst✝ : Group G
x : G
⊢ orderOf x ∣ Nat.card G

Tactic:
obtain h | h := fintypeOrInfinite G

Result:
case inl
G : Type u_6
inst✝ : Group G
x : G
h : Fintype G
⊢ orderOf x ∣ Nat.card G

case inr
G : Type u_6
inst✝ : Group G
x : G
h : Infinite G
⊢ orderOf x ∣ Nat.card G

Proof state:
case inr
G : Type u_6
inst✝ : Group G
x : G
h : Infinite G
⊢ orderOf x ∣ Nat.card G

Tactic:
simp only [card_eq_zero_of_infinite, dvd_zero]

Result:
no goals

Proof state:
case inl
G : Type u_6
inst✝ : Group G
x : G
h : Fintype G
⊢ orderOf x ∣ Nat.card G

Tactic:
simp only [Nat.card_eq_fintype_card, orderOf_dvd_card]

Result:
no goals