harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean
theorem gradedMul_assoc (x y z : DirectSum _ 𝒜 ⊗[R] DirectSum _ ℬ) :
    gradedMul R 𝒜 ℬ (gradedMul R 𝒜 ℬ x y) z = gradedMul R 𝒜 ℬ x (gradedMul R 𝒜 ℬ y z)

Proof state:
case a.H.h.H.h.a.H.h.H.h.a.H.h.H.h
R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x y z : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
mA : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ :=
  gradedMul R 𝒜 ℬ
ixa : ι
xa : 𝒜 ixa
ixb : ι
xb : ℬ ixb
iya : ι
ya : 𝒜 iya
iyb : ι
yb : ℬ iyb
iza : ι
za : 𝒜 iza
izb : ι
zb : ℬ izb
⊢ ((gradedMul R 𝒜 ℬ)
        (((gradedMul R 𝒜 ℬ) ((lof R ι 𝒜 ixa) xa ⊗ₜ[R] (lof R ι ℬ ixb) xb))
          ((lof R ι 𝒜 iya) ya ⊗ₜ[R] (lof R ι ℬ iyb) yb)))
      ((lof R ι 𝒜 iza) za ⊗ₜ[R] (lof R ι ℬ izb) zb) =
    ((gradedMul R 𝒜 ℬ) ((lof R ι 𝒜 ixa) xa ⊗ₜ[R] (lof R ι ℬ ixb) xb))
      (((gradedMul R 𝒜 ℬ) ((lof R ι 𝒜 iya) ya ⊗ₜ[R] (lof R ι ℬ iyb) yb)) ((lof R ι 𝒜 iza) za ⊗ₜ[R] (lof R ι ℬ izb) zb))

Tactic:
simp_rw [tmul_of_gradedMul_of_tmul, Units.smul_def, ← Int.cast_smul_eq_zsmul R,
  LinearMap.map_smul₂, LinearMap.map_smul, DirectSum.lof_eq_of, DirectSum.of_mul_of,
  ← DirectSum.lof_eq_of R, tmul_of_gradedMul_of_tmul, DirectSum.lof_eq_of, ← DirectSum.of_mul_of,
  ← DirectSum.lof_eq_of R, mul_assoc]

Result:
case a.H.h.H.h.a.H.h.H.h.a.H.h.H.h
R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x y z : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
mA : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ :=
  gradedMul R 𝒜 ℬ
ixa : ι
xa : 𝒜 ixa
ixb : ι
xb : ℬ ixb
iya : ι
ya : 𝒜 iya
iyb : ι
yb : ℬ iyb
iza : ι
za : 𝒜 iza
izb : ι
zb : ℬ izb
⊢ ↑↑((-1) ^ (ixb * iya)) •
      (-1) ^ ((ixb + iyb) * iza) •
        ((lof R ι 𝒜 ixa) xa * ((lof R ι 𝒜 iya) ya * (lof R ι 𝒜 iza) za)) ⊗ₜ[R]
          ((lof R ι ℬ ixb) xb * ((lof R ι ℬ iyb) yb * (lof R ι ℬ izb) zb)) =
    ↑↑((-1) ^ (iyb * iza)) •
      (-1) ^ (ixb * (iya + iza)) •
        ((lof R ι 𝒜 ixa) xa * ((lof R ι 𝒜 iya) ya * (lof R ι 𝒜 iza) za)) ⊗ₜ[R]
          ((lof R ι ℬ ixb) xb * ((lof R ι ℬ iyb) yb * (lof R ι ℬ izb) zb))
-- Mathlib/RingTheory/MvPowerSeries/NoZeroDivisors.lean
theorem mem_nonZeroDivisors_of_constantCoeff {φ : MvPowerSeries σ R}
    (hφ : constantCoeff σ R φ ∈ nonZeroDivisors R) :
    φ ∈ nonZeroDivisors (MvPowerSeries σ R)

Proof state:
case h.e'_2.h₁
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : (constantCoeff σ R) φ ∈ nonZeroDivisors R
x : MvPowerSeries σ R
hx : x * φ = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff R y) x = (coeff R y) 0
⊢ (e, 0) ∉ antidiagonal e → (coeff R (e, 0).1) x * (coeff R (e, 0).2) φ = 0

Tactic:
simp only [mem_antidiagonal, add_zero, not_true_eq_false, coeff_zero_eq_constantCoeff,
  false_implies]

Result:
no goals

Proof state:
case h.e'_2.h₀.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : (constantCoeff σ R) φ ∈ nonZeroDivisors R
x : MvPowerSeries σ R
hx : x * φ = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff R y) x = (coeff R y) 0
u snd✝ : σ →₀ ℕ
huv : (u, snd✝) ∈ antidiagonal e
a✝ : (u, snd✝) ≠ (e, 0)
⊢ (coeff R (u, snd✝).1) x * (coeff R (u, snd✝).2) φ = 0

Tactic:
suffices u < e by simp only [he u this, zero_mul, map_zero]

Result:
case h.e'_2.h₀.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : (constantCoeff σ R) φ ∈ nonZeroDivisors R
x : MvPowerSeries σ R
hx : x * φ = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff R y) x = (coeff R y) 0
u snd✝ : σ →₀ ℕ
huv : (u, snd✝) ∈ antidiagonal e
a✝ : (u, snd✝) ≠ (e, 0)
⊢ u < e
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem filter_gt_eq_Iio [DecidablePred (· < a)] : ({x | x < a} : Finset _) = Iio a

Proof state:
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x => x < a
⊢ filter (fun x => x < a) univ = Iio a

Tactic:
ext

Result:
case h
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x => x < a
a✝ : α
⊢ a✝ ∈ filter (fun x => x < a) univ ↔ a✝ ∈ Iio a

Proof state:
case h
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x => x < a
a✝ : α
⊢ a✝ ∈ filter (fun x => x < a) univ ↔ a✝ ∈ Iio a

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean
lemma eventuallyEq_coe_comp_ofComplex {z : ℂ} (hz : 0 < z.im) :
    UpperHalfPlane.coe ∘ ofComplex =ᶠ[𝓝 z] id

Proof state:
case h
z : ℂ
hz : 0 < z.im
x : ℂ
hx : x ∈ Complex.im ⁻¹' Ioi 0
⊢ (UpperHalfPlane.coe ∘ ↑ofComplex) x = id x

Tactic:
simp only [Function.comp_apply, ofComplex_apply_of_im_pos hx, id_eq, coe_mk_subtype]

Result:
no goals

Proof state:
z : ℂ
hz : 0 < z.im
⊢ UpperHalfPlane.coe ∘ ↑ofComplex =ᶠ[𝓝 z] id

Tactic:
filter_upwards [(Complex.continuous_im.isOpen_preimage _ isOpen_Ioi).mem_nhds hz] with x hx

Result:
case h
z : ℂ
hz : 0 < z.im
x : ℂ
hx : x ∈ Complex.im ⁻¹' Ioi 0
⊢ (UpperHalfPlane.coe ∘ ↑ofComplex) x = id x
-- Mathlib/Data/List/Lattice.lean
theorem bagInter_sublist_left : ∀ l₁ l₂ : List α, l₁.bagInter l₂ <+ l₁
  | [], l₂ => by simp
  | b :: l₁, l₂ => by
    by_cases h : b ∈ l₂ <;> simp only [h, cons_bagInter_of_pos, cons_bagInter_of_neg, not_false_iff]
    · exact (bagInter_sublist_left _ _).cons_cons _
    · apply sublist_cons_of_sublist
      apply bagInter_sublist_left

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
b : α
l₁ l₂ : List α
h : b ∈ l₂
⊢ b :: l₁.bagInter (l₂.erase b) <+ b :: l₁

Tactic:
exact (bagInter_sublist_left _ _).cons_cons _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
⊢ [].bagInter l₂ <+ []

Tactic:
simp

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
b : α
l₁ l₂ : List α
h : ¬b ∈ l₂
⊢ l₁.bagInter l₂ <+ b :: l₁

Tactic:
apply sublist_cons_of_sublist

Result:
case neg.h
α : Type u_1
inst✝ : DecidableEq α
b : α
l₁ l₂ : List α
h : ¬b ∈ l₂
⊢ l₁.bagInter l₂ <+ l₁

Proof state:
case neg.h
α : Type u_1
inst✝ : DecidableEq α
b : α
l₁ l₂ : List α
h : ¬b ∈ l₂
⊢ l₁.bagInter l₂ <+ l₁

Tactic:
apply bagInter_sublist_left

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
b : α
l₁ l₂ : List α
⊢ (b :: l₁).bagInter l₂ <+ b :: l₁

Tactic:
by_cases h : b ∈ l₂ <;> simp only [h, cons_bagInter_of_pos, cons_bagInter_of_neg, not_false_iff]

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
b : α
l₁ l₂ : List α
h : b ∈ l₂
⊢ b :: l₁.bagInter (l₂.erase b) <+ b :: l₁

case neg
α : Type u_1
inst✝ : DecidableEq α
b : α
l₁ l₂ : List α
h : ¬b ∈ l₂
⊢ l₁.bagInter l₂ <+ b :: l₁
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem contains_eq_true_of_mem [BEq α] [LawfulBEq α] {a : α} {as : Vector α n} (h : a ∈ as) :
    as.contains a = true

Proof state:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as : Array α
h : a ∈ { toArray := as, size_toArray := ⋯ }
⊢ { toArray := as, size_toArray := ⋯ }.contains a = true

Tactic:
simp only [mem_mk] at h

Result:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as : Array α
h : a ∈ as
⊢ { toArray := as, size_toArray := ⋯ }.contains a = true

Proof state:
α : Type u_1
n : Nat
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as : Vector α n
h : a ∈ as
⊢ as.contains a = true

Tactic:
rcases as with ⟨as, rfl⟩

Result:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as : Array α
h : a ∈ { toArray := as, size_toArray := ⋯ }
⊢ { toArray := as, size_toArray := ⋯ }.contains a = true

Proof state:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as : Array α
h : a ∈ as
⊢ { toArray := as, size_toArray := ⋯ }.contains a = true

Tactic:
simp [Array.contains_eq_true_of_mem, h]

Result:
no goals
-- Mathlib/Algebra/Homology/QuasiIso.lean
lemma quasiIsoAt_of_comp_right (φ : K ⟶ L) (φ' : L ⟶ M) (i : ι) [K.HasHomology i]
    [L.HasHomology i] [M.HasHomology i]
    [hφ' : QuasiIsoAt φ' i] [hφφ' : QuasiIsoAt (φ ≫ φ') i] :
    QuasiIsoAt φ i

Proof state:
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ' : QuasiIsoAt φ' i
hφφ' : QuasiIsoAt (φ ≫ φ') i
⊢ QuasiIsoAt φ i

Tactic:
rw [quasiIsoAt_iff_isIso_homologyMap] at hφ' hφφ' ⊢

Result:
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ' : IsIso (homologyMap φ' i)
hφφ' : IsIso (homologyMap (φ ≫ φ') i)
⊢ IsIso (homologyMap φ i)

Proof state:
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ' : IsIso (homologyMap φ' i)
hφφ' : IsIso (homologyMap φ i ≫ homologyMap φ' i)
⊢ IsIso (homologyMap φ i)

Tactic:
exact IsIso.of_isIso_comp_right (homologyMap φ i) (homologyMap φ' i)

Result:
no goals

Proof state:
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ' : IsIso (homologyMap φ' i)
hφφ' : IsIso (homologyMap (φ ≫ φ') i)
⊢ IsIso (homologyMap φ i)

Tactic:
rw [homologyMap_comp] at hφφ'

Result:
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ' : IsIso (homologyMap φ' i)
hφφ' : IsIso (homologyMap φ i ≫ homologyMap φ' i)
⊢ IsIso (homologyMap φ i)
-- Mathlib/FieldTheory/PerfectClosure.lean
theorem R.sound (m n : ℕ) (x y : K) (H : (frobenius K p)^[m] x = y) :
    mk K p (n, x) = mk K p (m + n, y)

Proof state:
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
m : ℕ
ih : mk K p (n, x) = mk K p (m + n, (⇑(frobenius K p))^[m] x)
⊢ mk K p (n, x) = mk K p (m + 1 + n, (⇑(frobenius K p))^[m + 1] x)

Tactic:
rw [ih, Nat.succ_add, iterate_succ']

Result:
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
m : ℕ
ih : mk K p (n, x) = mk K p (m + n, (⇑(frobenius K p))^[m] x)
⊢ mk K p (m + n, (⇑(frobenius K p))^[m] x) = mk K p ((m + n).succ, (⇑(frobenius K p) ∘ (⇑(frobenius K p))^[m]) x)

Proof state:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
m n : ℕ
x y : K
H : (⇑(frobenius K p))^[m] x = y
⊢ mk K p (n, x) = mk K p (m + n, y)

Tactic:
subst H

Result:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
m n : ℕ
x : K
⊢ mk K p (n, x) = mk K p (m + n, (⇑(frobenius K p))^[m] x)

Proof state:
case succ.a
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
m : ℕ
ih : mk K p (n, x) = mk K p (m + n, (⇑(frobenius K p))^[m] x)
⊢ R K p (m + n, (⇑(frobenius K p))^[m] x) ((m + n).succ, (⇑(frobenius K p) ∘ (⇑(frobenius K p))^[m]) x)

Tactic:
apply R.intro

Result:
no goals

Proof state:
case zero
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
⊢ mk K p (n, x) = mk K p (0 + n, (⇑(frobenius K p))^[0] x)

Tactic:
simp only [zero_add, iterate_zero_apply]

Result:
no goals

Proof state:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
m n : ℕ
x : K
⊢ mk K p (n, x) = mk K p (m + n, (⇑(frobenius K p))^[m] x)

Tactic:
induction' m with m ih

Result:
case zero
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
⊢ mk K p (n, x) = mk K p (0 + n, (⇑(frobenius K p))^[0] x)

case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
m : ℕ
ih : mk K p (n, x) = mk K p (m + n, (⇑(frobenius K p))^[m] x)
⊢ mk K p (n, x) = mk K p (m + 1 + n, (⇑(frobenius K p))^[m + 1] x)

Proof state:
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
m : ℕ
ih : mk K p (n, x) = mk K p (m + n, (⇑(frobenius K p))^[m] x)
⊢ mk K p (m + n, (⇑(frobenius K p))^[m] x) = mk K p ((m + n).succ, (⇑(frobenius K p) ∘ (⇑(frobenius K p))^[m]) x)

Tactic:
apply Quot.sound

Result:
case succ.a
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
m : ℕ
ih : mk K p (n, x) = mk K p (m + n, (⇑(frobenius K p))^[m] x)
⊢ R K p (m + n, (⇑(frobenius K p))^[m] x) ((m + n).succ, (⇑(frobenius K p) ∘ (⇑(frobenius K p))^[m]) x)
-- Mathlib/GroupTheory/Exponent.lean
theorem Monoid.exponent_pi {ι : Type*} [Fintype ι] {M : ι → Type*} [∀ i, Monoid (M i)] :
    exponent ((i : ι) → M i) = lcm univ (exponent <| M ·)

Proof state:
case refine_1.h
ι : Type u_1
inst✝¹ : Fintype ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
m : (i : ι) → M i
i : ι
⊢ (m ^ univ.lcm fun x => exponent (M x)) i = 1 i

Tactic:
rw [Pi.pow_apply, Pi.one_apply, ← orderOf_dvd_iff_pow_eq_one]

Result:
case refine_1.h
ι : Type u_1
inst✝¹ : Fintype ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
m : (i : ι) → M i
i : ι
⊢ orderOf (m i) ∣ univ.lcm fun x => exponent (M x)

Proof state:
case refine_1
ι : Type u_1
inst✝¹ : Fintype ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
m : (i : ι) → M i
⊢ (m ^ univ.lcm fun x => exponent (M x)) = 1

Tactic:
ext i

Result:
case refine_1.h
ι : Type u_1
inst✝¹ : Fintype ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
m : (i : ι) → M i
i : ι
⊢ (m ^ univ.lcm fun x => exponent (M x)) i = 1 i

Proof state:
case refine_1.h
ι : Type u_1
inst✝¹ : Fintype ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
m : (i : ι) → M i
i : ι
⊢ orderOf (m i) ∣ univ.lcm fun x => exponent (M x)

Tactic:
apply dvd_trans (Monoid.order_dvd_exponent (m i))

Result:
case refine_1.h
ι : Type u_1
inst✝¹ : Fintype ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
m : (i : ι) → M i
i : ι
⊢ exponent (M i) ∣ univ.lcm fun x => exponent (M x)

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
⊢ exponent ((i : ι) → M i) = univ.lcm fun x => exponent (M x)

Tactic:
refine dvd_antisymm ?_ ?_

Result:
case refine_1
ι : Type u_1
inst✝¹ : Fintype ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
⊢ exponent ((i : ι) → M i) ∣ univ.lcm fun x => exponent (M x)

case refine_2
ι : Type u_1
inst✝¹ : Fintype ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
⊢ (univ.lcm fun x => exponent (M x)) ∣ exponent ((i : ι) → M i)

Proof state:
case refine_1.h
ι : Type u_1
inst✝¹ : Fintype ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
m : (i : ι) → M i
i : ι
⊢ exponent (M i) ∣ univ.lcm fun x => exponent (M x)

Tactic:
exact Finset.dvd_lcm (mem_univ i)

Result:
no goals

Proof state:
case refine_1
ι : Type u_1
inst✝¹ : Fintype ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
⊢ exponent ((i : ι) → M i) ∣ univ.lcm fun x => exponent (M x)

Tactic:
refine exponent_dvd_of_forall_pow_eq_one fun m ↦ ?_

Result:
case refine_1
ι : Type u_1
inst✝¹ : Fintype ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
m : (i : ι) → M i
⊢ (m ^ univ.lcm fun x => exponent (M x)) = 1

Proof state:
case refine_2
ι : Type u_1
inst✝¹ : Fintype ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
⊢ (univ.lcm fun x => exponent (M x)) ∣ exponent ((i : ι) → M i)

Tactic:
apply Finset.lcm_dvd fun i _ ↦ ?_

Result:
ι : Type u_1
inst✝¹ : Fintype ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i : ι
x✝ : i ∈ univ
⊢ exponent (M i) ∣ exponent ((i : ι) → M i)
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem degree_X_pow_le (n : ℕ) : degree (X ^ n : R[X]) ≤ n

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ (X ^ n).degree ≤ ↑n

Tactic:
simpa only [C_1, one_mul] using degree_C_mul_X_pow_le n (1 : R)

Result:
no goals
-- Mathlib/RingTheory/Norm/Basic.lean
theorem PowerBasis.norm_gen_eq_prod_roots [Algebra R F] (pb : PowerBasis R S)
    (hf : (minpoly R pb.gen).Splits (algebraMap R F)) :
    algebraMap R F (norm R pb.gen) = ((minpoly R pb.gen).aroots F).prod

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hf : Splits (algebraMap R F) (minpoly R pb.gen)
⊢ (algebraMap R F) ((norm R) pb.gen) = ((minpoly R pb.gen).aroots F).prod

Tactic:
haveI := Module.nontrivial R F

Result:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hf : Splits (algebraMap R F) (minpoly R pb.gen)
this : Nontrivial R
⊢ (algebraMap R F) ((norm R) pb.gen) = ((minpoly R pb.gen).aroots F).prod

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hf : Splits (algebraMap R F) (minpoly R pb.gen)
this✝ : Nontrivial R
this : (minpoly R pb.gen).Monic
⊢ (algebraMap R F) ((norm R) pb.gen) = ((minpoly R pb.gen).aroots F).prod

Tactic:
rw [PowerBasis.norm_gen_eq_coeff_zero_minpoly, ← pb.natDegree_minpoly, RingHom.map_mul,
  ← coeff_map,
  prod_roots_eq_coeff_zero_of_monic_of_splits (this.map _) ((splits_id_iff_splits _).2 hf),
  this.natDegree_map, map_pow, ← mul_assoc, ← mul_pow]

Result:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hf : Splits (algebraMap R F) (minpoly R pb.gen)
this✝ : Nontrivial R
this : (minpoly R pb.gen).Monic
⊢ ((algebraMap R F) (-1) * -1) ^ (minpoly R pb.gen).natDegree *
      (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).roots.prod =
    ((minpoly R pb.gen).aroots F).prod

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hf : Splits (algebraMap R F) (minpoly R pb.gen)
this✝ : Nontrivial R
this : (minpoly R pb.gen).Monic
⊢ ((algebraMap R F) (-1) * -1) ^ (minpoly R pb.gen).natDegree *
      (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).roots.prod =
    ((minpoly R pb.gen).aroots F).prod

Tactic:
simp only [map_neg, _root_.map_one, neg_mul, neg_neg, one_pow, one_mul]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hf : Splits (algebraMap R F) (minpoly R pb.gen)
this : Nontrivial R
⊢ (algebraMap R F) ((norm R) pb.gen) = ((minpoly R pb.gen).aroots F).prod

Tactic:
have := minpoly.monic pb.isIntegral_gen

Result:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hf : Splits (algebraMap R F) (minpoly R pb.gen)
this✝ : Nontrivial R
this : (minpoly R pb.gen).Monic
⊢ (algebraMap R F) ((norm R) pb.gen) = ((minpoly R pb.gen).aroots F).prod
-- Mathlib/Order/Interval/Finset/Nat.lean
theorem Ico_succ_left_eq_erase_Ico : Ico a.succ b = erase (Ico a b) a

Proof state:
a b : ℕ
⊢ Ico a.succ b = (Ico a b).erase a

Tactic:
ext x

Result:
case h
a b x : ℕ
⊢ x ∈ Ico a.succ b ↔ x ∈ (Ico a b).erase a

Proof state:
case h
a b x : ℕ
⊢ x ∈ Ico a.succ b ↔ x ∈ (Ico a b).erase a

Tactic:
rw [Ico_succ_left, mem_erase, mem_Ico, mem_Ioo, ← and_assoc, ne_comm,
  and_comm (a := a ≠ x), lt_iff_le_and_ne]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem leadingCoeff_mul_of_mul_leadingCoeff_ne_zero {f g : MvPolynomial σ R}
    (hfg : m.leadingCoeff f * m.leadingCoeff g ≠ 0) :
    m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hfg : m.leadingCoeff f * m.leadingCoeff g ≠ 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
rw [leadingCoeff, ← coeff_mul_of_degree_add, degree_mul_of_mul_leadingCoeff_ne_zero hfg]

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem of_affine_open_cover {X : Scheme} {P : X.affineOpens → Prop}
    {ι} (U : ι → X.affineOpens) (iSup_U : (⨆ i, U i : X.Opens) = ⊤)
    (V : X.affineOpens)
    (basicOpen : ∀ (U : X.affineOpens) (f : Γ(X, U)), P U → P (X.affineBasicOpen f))
    (openCover :
      ∀ (U : X.affineOpens) (s : Finset (Γ(X, U)))
        (_ : Ideal.span (s : Set (Γ(X, U))) = ⊤),
        (∀ f : s, P (X.affineBasicOpen f.1)) → P U)
    (hU : ∀ i, P (U i)) : P V

Proof state:
case intro
X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)),
    Ideal.span ↑s = ⊤ → (∀ (f : { x // x ∈ s }), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
x : ↥↑V
i : ι
hi : ↑x ∈ ↑(U i)
⊢ ∃ f, ↑x ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)

Tactic:
obtain ⟨f, g, e, hf⟩ := exists_basicOpen_le_affine_inter V.prop (U i).prop x ⟨x.prop, hi⟩

Result:
case intro.intro.intro.intro
X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)),
    Ideal.span ↑s = ⊤ → (∀ (f : { x // x ∈ s }), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
x : ↥↑V
i : ι
hi : ↑x ∈ ↑(U i)
f : ↑Γ(X, ↑V)
g : ↑Γ(X, ↑(U i))
e : X.basicOpen f = X.basicOpen g
hf : ↑x ∈ X.basicOpen f
⊢ ∃ f, ↑x ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)
-- Mathlib/NumberTheory/Padics/RingHoms.lean
theorem denseRange_intCast : DenseRange (Int.cast : ℤ → ℤ_[p])

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
⊢ DenseRange Int.cast

Tactic:
intro x

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ x ∈ closure (Set.range Int.cast)

Proof state:
case refine_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ∀ (a : ℕ), ↑a ∈ closure (Set.range Int.cast)

Tactic:
intro a

Result:
case refine_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
a : ℕ
⊢ ↑a ∈ closure (Set.range Int.cast)

Proof state:
case refine_1
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ IsClosed {b | b ∈ closure (Set.range Int.cast)}

Tactic:
exact isClosed_closure

Result:
no goals

Proof state:
case refine_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
a : ℕ
⊢ ↑a ∈ closure (Set.range Int.cast)

Tactic:
apply subset_closure

Result:
case refine_2.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
a : ℕ
⊢ ↑a ∈ Set.range Int.cast

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ x ∈ closure (Set.range Int.cast)

Tactic:
refine DenseRange.induction_on denseRange_natCast x ?_ ?_

Result:
case refine_1
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ IsClosed {b | b ∈ closure (Set.range Int.cast)}

case refine_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ∀ (a : ℕ), ↑a ∈ closure (Set.range Int.cast)

Proof state:
case refine_2.a
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
a : ℕ
⊢ ↑a ∈ Set.range Int.cast

Tactic:
exact Set.mem_range_self _

Result:
no goals