harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem Products.max_eq_o_cons_tail' [Inhabited I] (l : Products I) (hl : l.val ≠ [])
    (hlh : l.val.head! = term I ho) (hlc : List.Chain' (· > ·) (term I ho :: l.Tail.val)) :
    l = ⟨term I ho :: l.Tail.val, hlc⟩

Proof state:
I : Type u
inst✝² : LinearOrder I
inst✝¹ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.Chain' (fun x1 x2 => x1 > x2) (term I ho :: ↑l.Tail)
⊢ l = ⟨↑l, ⋯⟩

Tactic:
rfl

Result:
no goals

Proof state:
I : Type u
inst✝² : LinearOrder I
inst✝¹ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.Chain' (fun x1 x2 => x1 > x2) (term I ho :: ↑l.Tail)
⊢ l = ⟨term I ho :: ↑l.Tail, hlc⟩

Tactic:
simp_rw [← max_eq_o_cons_tail ho l hl hlh]

Result:
I : Type u
inst✝² : LinearOrder I
inst✝¹ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.Chain' (fun x1 x2 => x1 > x2) (term I ho :: ↑l.Tail)
⊢ l = ⟨↑l, ⋯⟩
-- Mathlib/Order/Filter/ENNReal.lean
theorem limsup_mul_le [CountableInterFilter f] (u v : α → ℝ≥0∞) :
    f.limsup (u * v) ≤ f.limsup u * f.limsup v :=
  calc
    f.limsup (u * v) ≤ f.limsup fun x => f.limsup u * v x

Proof state:
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u v : α → ℝ≥0∞
⊢ u * v ≤ᶠ[f] fun x => limsup u f * v x

Tactic:
filter_upwards [@eventually_le_limsup _ f _ u] with x hx using mul_le_mul' hx le_rfl

Result:
no goals

Proof state:
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u v : α → ℝ≥0∞
⊢ limsup (u * v) f ≤ limsup (fun x => limsup u f * v x) f

Tactic:
refine limsup_le_limsup ?_

Result:
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u v : α → ℝ≥0∞
⊢ u * v ≤ᶠ[f] fun x => limsup u f * v x
-- Mathlib/Geometry/RingedSpace/OpenImmersion.lean
theorem inv_invApp (U : Opens X) :
    inv (H.invApp _ U) =
      f.c.app (op (opensFunctor f |>.obj U)) ≫ X.presheaf.map
        (eqToHom (by simp [Opens.map, Set.preimage_image_eq _ H.base_open.injective])) :=
  PresheafedSpace.IsOpenImmersion.inv_invApp f U

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : SheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑X.toPresheafedSpace
⊢ (Opens.map f.base).op.obj (op ((opensFunctor f).obj U)) = op U

Tactic:
simp [Opens.map, Set.preimage_image_eq _ H.base_open.injective]

Result:
no goals
-- Mathlib/Analysis/Calculus/VectorField.lean
lemma lieBracketWithin_smul_right {c : 𝕜} (hW : DifferentiableWithinAt 𝕜 W s x)
    (hs : UniqueDiffWithinAt 𝕜 s x) :
    lieBracketWithin 𝕜 V (c • W) s x =
      c • lieBracketWithin 𝕜 V W s x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
s : Set E
x : E
c : 𝕜
hW : DifferentiableWithinAt 𝕜 W s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ lieBracketWithin 𝕜 V (c • W) s x = c • lieBracketWithin 𝕜 V W s x

Tactic:
simp only [lieBracketWithin, Pi.add_apply, map_add, Pi.smul_apply, map_smul, smul_sub]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
s : Set E
x : E
c : 𝕜
hW : DifferentiableWithinAt 𝕜 W s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ (fderivWithin 𝕜 (c • W) s x) (V x) - c • (fderivWithin 𝕜 V s x) (W x) =
    c • (fderivWithin 𝕜 W s x) (V x) - c • (fderivWithin 𝕜 V s x) (W x)

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
s : Set E
x : E
c : 𝕜
hW : DifferentiableWithinAt 𝕜 W s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ (c • fderivWithin 𝕜 W s x) (V x) - c • (fderivWithin 𝕜 V s x) (W x) =
    c • (fderivWithin 𝕜 W s x) (V x) - c • (fderivWithin 𝕜 V s x) (W x)

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
s : Set E
x : E
c : 𝕜
hW : DifferentiableWithinAt 𝕜 W s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ (fderivWithin 𝕜 (c • W) s x) (V x) - c • (fderivWithin 𝕜 V s x) (W x) =
    c • (fderivWithin 𝕜 W s x) (V x) - c • (fderivWithin 𝕜 V s x) (W x)

Tactic:
rw [fderivWithin_const_smul' hs hW]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
s : Set E
x : E
c : 𝕜
hW : DifferentiableWithinAt 𝕜 W s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ (c • fderivWithin 𝕜 W s x) (V x) - c • (fderivWithin 𝕜 V s x) (W x) =
    c • (fderivWithin 𝕜 W s x) (V x) - c • (fderivWithin 𝕜 V s x) (W x)
-- Mathlib/RingTheory/FractionalIdeal/Norm.lean
theorem coeIdeal_absNorm (I₀ : Ideal R) :
    absNorm (I₀ : FractionalIdeal R⁰ K) = Ideal.absNorm I₀

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Module.Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I₀ : Ideal R
⊢ 1 • ↑↑I₀ = Submodule.map (Algebra.linearMap R K) I₀

Tactic:
rw [one_smul]

Result:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Module.Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I₀ : Ideal R
⊢ ↑↑I₀ = Submodule.map (Algebra.linearMap R K) I₀

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Module.Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I₀ : Ideal R
⊢ absNorm ↑I₀ = ↑(Ideal.absNorm I₀)

Tactic:
rw [absNorm_eq' 1 I₀ (by rw [one_smul]; rfl), OneMemClass.coe_one, _root_.map_one, abs_one,
  Int.cast_one, _root_.div_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Module.Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I₀ : Ideal R
⊢ ↑↑I₀ = Submodule.map (Algebra.linearMap R K) I₀

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
theorem ιPi_π (a) : ιPi I ≫ Pi.π I.left a = ι I a

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
inst✝² : HasMultiequalizer I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
a : J.L
⊢ equalizer.ι I.fstPiMap I.sndPiMap ≫ Pi.π I.left a =
    (limit.isoLimitCone
          { cone := I.multiforkEquivPiFork.inverse.obj (limit.cone (parallelPair I.fstPiMap I.sndPiMap)),
            isLimit :=
              IsLimit.ofPreservesConeTerminal I.multiforkEquivPiFork.inverse
                (limit.isLimit (parallelPair I.fstPiMap I.sndPiMap)) }).inv ≫
      ι I a

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
inst✝² : HasMultiequalizer I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
a : J.L
⊢ ιPi I ≫ Pi.π I.left a = ι I a

Tactic:
rw [ιPi, Category.assoc, ← Iso.eq_inv_comp, isoEqualizer]

Result:
C : Type u
inst✝³ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
inst✝² : HasMultiequalizer I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
a : J.L
⊢ equalizer.ι I.fstPiMap I.sndPiMap ≫ Pi.π I.left a =
    (limit.isoLimitCone
          { cone := I.multiforkEquivPiFork.inverse.obj (limit.cone (parallelPair I.fstPiMap I.sndPiMap)),
            isLimit :=
              IsLimit.ofPreservesConeTerminal I.multiforkEquivPiFork.inverse
                (limit.isLimit (parallelPair I.fstPiMap I.sndPiMap)) }).inv ≫
      ι I a
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem fderiv_eq_smul_deriv (y : 𝕜) : (fderiv 𝕜 f x : 𝕜 → F) y = y • deriv f x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x y : 𝕜
⊢ (fderiv 𝕜 f x) y = (fderiv 𝕜 f x) (y • 1)

Tactic:
simp only [smul_eq_mul, mul_one]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x y : 𝕜
⊢ (fderiv 𝕜 f x) y = y • deriv f x

Tactic:
rw [← fderiv_deriv, ← ContinuousLinearMap.map_smul]

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x y : 𝕜
⊢ (fderiv 𝕜 f x) y = (fderiv 𝕜 f x) (y • 1)
-- Mathlib/Order/Minimal.lean
theorem image_setOf_maximal (f : α ≃o β) (P : α → Prop) :
    f '' {x | Maximal P x} = {x | Maximal (fun x ↦ P (f.symm x)) x}

Proof state:
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α ≃o β
P : α → Prop
⊢ ∀ ⦃x y : α⦄, ?m.90682 x → ?m.90682 y → (f x ≤ f y ↔ x ≤ y)

Tactic:
simp [f.le_iff_le]

Result:
no goals

Proof state:
case h.e'_3.h.e'_2.h.h.e'_3.h.a
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α ≃o β
P : α → Prop
x✝¹ x✝ : β
⊢ P (f.symm x✝) ↔ ∃ x₀, P x₀ ∧ f x₀ = x✝

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α ≃o β
P : α → Prop
⊢ ⇑f '' {x | Maximal P x} = {x | Maximal (fun x => P (f.symm x)) x}

Tactic:
convert _root_.image_monotone_setOf_maximal (f := f) (by simp [f.le_iff_le])

Result:
case h.e'_3.h.e'_2.h.h.e'_3.h.a
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α ≃o β
P : α → Prop
x✝¹ x✝ : β
⊢ P (f.symm x✝) ↔ ∃ x₀, P x₀ ∧ f x₀ = x✝
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma j_eq_zero (h : W.c₄ = 0) : W.j = 0

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsElliptic
h : W.c₄ = 0
⊢ W.j = 0

Tactic:
rw [j_eq_zero_iff', h, zero_pow three_ne_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Basic.lean
lemma shiftFunctorAdd_assoc (a₁ a₂ a₃ : A) :
    shiftFunctorAdd C (a₁ + a₂) a₃ ≪≫
      isoWhiskerRight (shiftFunctorAdd C a₁ a₂) _ ≪≫ Functor.associator _ _ _ =
    shiftFunctorAdd' C a₁ (a₂ + a₃) _ (add_assoc a₁ a₂ a₃).symm ≪≫
      isoWhiskerLeft _ (shiftFunctorAdd C a₂ a₃)

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
⊢ shiftFunctorAdd C (a₁ + a₂) a₃ ≪≫
      isoWhiskerRight (shiftFunctorAdd C a₁ a₂) (shiftFunctor C a₃) ≪≫
        (shiftFunctor C a₁).associator (shiftFunctor C a₂) (shiftFunctor C a₃) =
    shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯ ≪≫ isoWhiskerLeft (shiftFunctor C a₁) (shiftFunctorAdd C a₂ a₃)

Tactic:
ext X

Result:
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ (shiftFunctorAdd C (a₁ + a₂) a₃ ≪≫
            isoWhiskerRight (shiftFunctorAdd C a₁ a₂) (shiftFunctor C a₃) ≪≫
              (shiftFunctor C a₁).associator (shiftFunctor C a₂) (shiftFunctor C a₃)).hom.app
      X =
    (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯ ≪≫
            isoWhiskerLeft (shiftFunctor C a₁) (shiftFunctorAdd C a₂ a₃)).hom.app
      X

Proof state:
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ (shiftFunctorAdd C (a₁ + a₂) a₃ ≪≫
            isoWhiskerRight (shiftFunctorAdd C a₁ a₂) (shiftFunctor C a₃) ≪≫
              (shiftFunctor C a₁).associator (shiftFunctor C a₂) (shiftFunctor C a₃)).hom.app
      X =
    (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯ ≪≫
            isoWhiskerLeft (shiftFunctor C a₁) (shiftFunctorAdd C a₂ a₃)).hom.app
      X

Tactic:
simpa [shiftFunctorAdd'_eq_shiftFunctorAdd]
  using NatTrans.congr_app (congr_arg Iso.hom
    (shiftFunctorAdd'_assoc C a₁ a₂ a₃ _ _ _ rfl rfl rfl)) X

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
theorem isWeightedHomogeneous_monomial (w : σ → M) (d : σ →₀ ℕ) (r : R) {m : M}
    (hm : weight w d = m) : IsWeightedHomogeneous w (monomial d r) m

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : (weight w) d = m
c : σ →₀ ℕ
hc : coeff c ((monomial d) r) ≠ 0
⊢ (weight w) c = m

Tactic:
rw [coeff_monomial] at hc

Result:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : (weight w) d = m
c : σ →₀ ℕ
hc : (if d = c then r else 0) ≠ 0
⊢ (weight w) c = m

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : (weight w) d = m
⊢ IsWeightedHomogeneous w ((monomial d) r) m

Tactic:
intro c hc

Result:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : (weight w) d = m
c : σ →₀ ℕ
hc : coeff c ((monomial d) r) ≠ 0
⊢ (weight w) c = m

Proof state:
case pos
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : (weight w) d = m
c : σ →₀ ℕ
h : d = c
hc : r ≠ 0
⊢ (weight w) c = m

Tactic:
subst c

Result:
case pos
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : (weight w) d = m
hc : r ≠ 0
⊢ (weight w) d = m

Proof state:
case neg
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : (weight w) d = m
c : σ →₀ ℕ
h : ¬d = c
hc : 0 ≠ 0
⊢ (weight w) c = m

Tactic:
contradiction

Result:
no goals

Proof state:
case pos
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : (weight w) d = m
hc : r ≠ 0
⊢ (weight w) d = m

Tactic:
exact hm

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : (weight w) d = m
c : σ →₀ ℕ
hc : (if d = c then r else 0) ≠ 0
⊢ (weight w) c = m

Tactic:
split_ifs at hc with h

Result:
case pos
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : (weight w) d = m
c : σ →₀ ℕ
h : d = c
hc : r ≠ 0
⊢ (weight w) c = m

case neg
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : (weight w) d = m
c : σ →₀ ℕ
h : ¬d = c
hc : 0 ≠ 0
⊢ (weight w) c = m
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Monadic.lean
theorem forIn'_map [Monad m] [LawfulMonad m]
    (o : Option α) (g : α → β) (f : (b : β) → b ∈ o.map g → γ → m (ForInStep γ)) :
    forIn' (o.map g) init f = forIn' o init fun a h y => f (g a) (mem_map_of_mem g h) y

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
init : γ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
o : Option α
g : α → β
f : (b : β) → b ∈ Option.map g o → γ → m (ForInStep γ)
⊢ forIn' (Option.map g o) init f = forIn' o init fun a h y => f (g a) ⋯ y

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem laverage_eq (f : α → ℝ≥0∞) : ⨍⁻ x, f x ∂μ = (∫⁻ x, f x ∂μ) / μ univ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ⨍⁻ (x : α), f x ∂μ = (∫⁻ (x : α), f x ∂μ) / μ univ

Tactic:
rw [laverage_eq', lintegral_smul_measure, ENNReal.div_eq_inv_mul]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Gcd.lean
theorem Coprime.pow_left (n : Nat) (H1 : Coprime m k) : Coprime (m ^ n) k

Proof state:
case zero
m k : Nat
H1 : m.Coprime k
⊢ (m ^ 0).Coprime k

Tactic:
exact coprime_one_left _

Result:
no goals

Proof state:
case succ
m k : Nat
H1 : m.Coprime k
n : Nat
ih : (m ^ n).Coprime k
⊢ (m ^ (n + 1)).Coprime k

Tactic:
have hm := H1.mul ih

Result:
case succ
m k : Nat
H1 : m.Coprime k
n : Nat
ih : (m ^ n).Coprime k
hm : (m * m ^ n).Coprime k
⊢ (m ^ (n + 1)).Coprime k

Proof state:
m k n : Nat
H1 : m.Coprime k
⊢ (m ^ n).Coprime k

Tactic:
induction n with
| zero => exact coprime_one_left _
| succ n ih => have hm := H1.mul ih; rwa [Nat.pow_succ, Nat.mul_comm]

Result:
no goals

Proof state:
case succ
m k : Nat
H1 : m.Coprime k
n : Nat
ih : (m ^ n).Coprime k
hm : (m * m ^ n).Coprime k
⊢ (m ^ (n + 1)).Coprime k

Tactic:
rwa [Nat.pow_succ, Nat.mul_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/DecidableEq.lean
theorem beq_eq_decide [BEq α] (a b : Vector α n) :
    (a == b) = decide (∀ (i : Nat) (h' : i < n), a[i] == b[i])

Proof state:
α : Type u_1
n : Nat
inst✝ : BEq α
a b : Vector α n
⊢ (a == b) = decide (∀ (i : Nat) (h' : i < n), (a[i] == b[i]) = true)

Tactic:
simp [BEq.beq, isEqv_eq_decide]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
/-- Two natural numbers are equal if and only if they have the same multiples. -/
lemma dvd_right_iff_eq : (∀ a : ℕ, m ∣ a ↔ n ∣ a) ↔ m = n :=
  ⟨fun h => Nat.dvd_antisymm ((h _).mpr (Nat.dvd_refl _)) ((h _).mp (Nat.dvd_refl _)),
    fun h n => by rw [h]⟩

Proof state:
m n✝ : ℕ
h : m = n✝
n : ℕ
⊢ m ∣ n ↔ n✝ ∣ n

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
lemma mem_iff (hnm : n + 1 = m) (z : Cochain F G n) :
    z ∈ cocycle F G n ↔ δ n m z = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z : Cochain F G n
⊢ z ∈ cocycle F G n ↔ δ n (n + 1) z = 0

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n m : ℤ
hnm : n + 1 = m
z : Cochain F G n
⊢ z ∈ cocycle F G n ↔ δ n m z = 0

Tactic:
subst hnm

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z : Cochain F G n
⊢ z ∈ cocycle F G n ↔ δ n (n + 1) z = 0
-- Mathlib/Algebra/Order/CauSeq/Completion.lean
theorem mul_inv_cancel {x : (Cauchy abv)} : x ≠ 0 → x * x⁻¹ = 1 :=
  Quotient.inductionOn x fun f hf => by
    simp only [mk_eq_mk, ne_eq, mk_eq_zero] at hf
    simp only [mk_eq_mk, hf, not_false_eq_true, inv_mk, mk_mul]
    exact Quotient.sound (CauSeq.mul_inv_cancel hf)

Proof state:
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f : CauSeq β abv
hf : ¬f.LimZero
⊢ ⟦f⟧ * (⟦f⟧)⁻¹ = 1

Tactic:
simp only [mk_eq_mk, hf, not_false_eq_true, inv_mk, mk_mul]

Result:
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f : CauSeq β abv
hf : ¬f.LimZero
⊢ mk (f * f.inv ⋯) = 1

Proof state:
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f : CauSeq β abv
hf : ⟦f⟧ ≠ 0
⊢ ⟦f⟧ * (⟦f⟧)⁻¹ = 1

Tactic:
simp only [mk_eq_mk, ne_eq, mk_eq_zero] at hf

Result:
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f : CauSeq β abv
hf : ¬f.LimZero
⊢ ⟦f⟧ * (⟦f⟧)⁻¹ = 1

Proof state:
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f : CauSeq β abv
hf : ¬f.LimZero
⊢ mk (f * f.inv ⋯) = 1

Tactic:
exact Quotient.sound (CauSeq.mul_inv_cancel hf)

Result:
no goals
-- Mathlib/Order/RelIso/Basic.lean
theorem symm_apply_rel (e : r ≃r s) {x y} : r (e.symm x) y ↔ s x (e y)

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
x : β
y : α
⊢ r (e.symm x) y ↔ s x (e y)

Tactic:
rw [← e.map_rel_iff, e.apply_symm_apply]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Box/Basic.lean
theorem mapsTo_insertNth_face {n} (I : Box (Fin (n + 1))) {i : Fin (n + 1)} {x : ℝ}
    (hx : x ∈ Ioc (I.lower i) (I.upper i)) :
    MapsTo (i.insertNth x) (I.face i : Set (_ → _)) (I : Set (_ → _))

Proof state:
n : ℕ
I : Box (Fin (n + 1))
i : Fin (n + 1)
x : ℝ
hx : x ∈ Ioc (I.lower i) (I.upper i)
⊢ MapsTo (i.insertNth x) ↑(I.face i) ↑I

Tactic:
intro y hy

Result:
n : ℕ
I : Box (Fin (n + 1))
i : Fin (n + 1)
x : ℝ
hx : x ∈ Ioc (I.lower i) (I.upper i)
y : Fin n → ℝ
hy : y ∈ ↑(I.face i)
⊢ i.insertNth x y ∈ ↑I

Proof state:
n : ℕ
I : Box (Fin (n + 1))
i : Fin (n + 1)
x : ℝ
hx : x ∈ Ioc (I.lower i) (I.upper i)
y : Fin n → ℝ
hy : y ∈ ↑(I.face i)
⊢ x ∈ Ioc (I.lower i) (I.upper i) ∧ ∀ (i_1 : Fin n), y i_1 ∈ Ioc (I.lower (i.succAbove i_1)) (I.upper (i.succAbove i_1))

Tactic:
exact ⟨hx, hy⟩

Result:
no goals

Proof state:
n : ℕ
I : Box (Fin (n + 1))
i : Fin (n + 1)
x : ℝ
hx : x ∈ Ioc (I.lower i) (I.upper i)
y : Fin n → ℝ
hy : y ∈ ↑(I.face i)
⊢ i.insertNth x y ∈ ↑I

Tactic:
simp_rw [mem_coe, mem_def, i.forall_iff_succAbove, Fin.insertNth_apply_same,
  Fin.insertNth_apply_succAbove]

Result:
n : ℕ
I : Box (Fin (n + 1))
i : Fin (n + 1)
x : ℝ
hx : x ∈ Ioc (I.lower i) (I.upper i)
y : Fin n → ℝ
hy : y ∈ ↑(I.face i)
⊢ x ∈ Ioc (I.lower i) (I.upper i) ∧ ∀ (i_1 : Fin n), y i_1 ∈ Ioc (I.lower (i.succAbove i_1)) (I.upper (i.succAbove i_1))
-- Mathlib/Algebra/Group/Commute/Units.lean
@[to_additive (attr := simp)]
lemma Units.pow_ofPowEqOne (ha : a ^ n = 1) (hn : n ≠ 0) :
    Units.ofPowEqOne _ n ha hn ^ n = 1 := Units.ext <| by simp [ha]

Proof state:
M : Type u_1
inst✝ : Monoid M
n : ℕ
a : M
ha : a ^ n = 1
hn : n ≠ 0
⊢ ↑(ofPowEqOne a n ha hn ^ n) = ↑1

Tactic:
simp [ha]

Result:
no goals
-- Mathlib/Data/List/Range.lean
/-- See `List.ranges_flatten` for the version about `List.sum`. -/
@[deprecated "Use `List.ranges_flatten`." (since := "2024-10-17")]
lemma ranges_flatten' : ∀ l : List ℕ, l.ranges.flatten = range (Nat.sum l)
  | [] => rfl
  | a :: l => by
    simp only [ranges, flatten_cons, ← map_flatten, ranges_flatten', Nat.sum_cons, range_add]

Proof state:
a : ℕ
l : List ℕ
⊢ (a :: l).ranges.flatten = range (Nat.sum (a :: l))

Tactic:
simp only [ranges, flatten_cons, ← map_flatten, ranges_flatten', Nat.sum_cons, range_add]

Result:
no goals
-- Mathlib/Combinatorics/Colex.lean
theorem twoPowSum_toFinset_bitIndices (n : ℕ) :
    ∑ i ∈ n.bitIndices.toFinset, 2 ^ i = n

Proof state:
n : ℕ
⊢ ∑ i ∈ n.bitIndices.toFinset, 2 ^ i = n

Tactic:
simp [List.sum_toFinset _ Nat.bitIndices_sorted.nodup]

Result:
no goals