harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/DedekindDomain/Factorization.lean
theorem count_zpow (n : ℤ) (I : FractionalIdeal R⁰ K) :
    count K v (I ^ n) = n * count K v I

Proof state:
case ofNat
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
n : ℕ
⊢ count K v (I ^ n) = ↑n * count K v I

Tactic:
exact count_pow K v n I

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
n : ℤ
I : FractionalIdeal R⁰ K
⊢ count K v (I ^ n) = n * count K v I

Tactic:
obtain n | n := n

Result:
case ofNat
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
n : ℕ
⊢ count K v (I ^ ofNat n) = ofNat n * count K v I

case negSucc
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
n : ℕ
⊢ count K v (I ^ -[n+1]) = -[n+1] * count K v I

Proof state:
case negSucc
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
n : ℕ
⊢ count K v (I ^ -[n+1]) = -[n+1] * count K v I

Tactic:
rw [negSucc_coe, count_neg_zpow, zpow_natCast, count_pow]

Result:
case negSucc
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
n : ℕ
⊢ -(↑(n + 1) * count K v I) = -↑(n + 1) * count K v I

Proof state:
case ofNat
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
n : ℕ
⊢ count K v (I ^ ofNat n) = ofNat n * count K v I

Tactic:
rw [ofNat_eq_coe, zpow_natCast]

Result:
case ofNat
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
n : ℕ
⊢ count K v (I ^ n) = ↑n * count K v I

Proof state:
case negSucc
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
n : ℕ
⊢ -(↑(n + 1) * count K v I) = -↑(n + 1) * count K v I

Tactic:
ring

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem iInf_sup_eq_top {s : Finset ι} {J : ι → Ideal R} (h : ∀ i, i ∈ s → J i ⊔ I = ⊤) :
    (⨅ i ∈ s, J i) ⊔ I = ⊤

Proof state:
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
s : Finset ι
J : ι → Ideal R
h : ∀ i ∈ s, J i ⊔ I = ⊤
i : ι
hi : i ∈ s
⊢ I ⊔ J i = ⊤

Tactic:
rw [sup_comm, h i hi]

Result:
no goals

Proof state:
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
s : Finset ι
J : ι → Ideal R
h : ∀ i ∈ s, J i ⊔ I = ⊤
⊢ ∀ i ∈ s, I ⊔ J i = ⊤

Tactic:
intro i hi

Result:
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
s : Finset ι
J : ι → Ideal R
h : ∀ i ∈ s, J i ⊔ I = ⊤
i : ι
hi : i ∈ s
⊢ I ⊔ J i = ⊤

Proof state:
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
s : Finset ι
J : ι → Ideal R
h : ∀ i ∈ s, J i ⊔ I = ⊤
⊢ (⨅ i ∈ s, J i) ⊔ I = ⊤

Tactic:
rw [sup_comm, sup_iInf_eq_top]

Result:
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
s : Finset ι
J : ι → Ideal R
h : ∀ i ∈ s, J i ⊔ I = ⊤
⊢ ∀ i ∈ s, I ⊔ J i = ⊤
-- Mathlib/CategoryTheory/Monoidal/Bimod.lean
theorem hom_inv_id : hom P ≫ inv P = 𝟙 _

Proof state:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
⊢ (ρ_ (P.X ⊗ S.X)).inv ≫
      ((P.X ⊗ S.X) ◁ S.one ≫ P.actRight ▷ S.X) ≫ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) =
    coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul))

Tactic:
slice_lhs 3 4 => rw [coequalizer.condition]

Result:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
⊢ (ρ_ (P.X ⊗ S.X)).inv ≫
      (P.X ⊗ S.X) ◁ S.one ≫
        ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ≫ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) =
    coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul))

Proof state:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
⊢ (ρ_ (P.X ⊗ S.X)).inv ≫
      (P.X ⊗ S.X) ◁ S.one ≫
        ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ≫ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) =
    coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul))

Tactic:
slice_lhs 2 3 => rw [associator_naturality_right]

Result:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
⊢ (ρ_ (P.X ⊗ S.X)).inv ≫
      (((α_ P.X S.X (𝟙_ C)).hom ≫ P.X ◁ S.X ◁ S.one) ≫ P.X ◁ S.mul) ≫
        coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) =
    coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul))

Proof state:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
⊢ (ρ_ (P.X ⊗ S.X)).inv ≫
      (α_ P.X S.X (𝟙_ C)).hom ≫
        P.X ◁ (ρ_ S.X).hom ≫ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) =
    coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul)

Tactic:
monoidal

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem support_monomial' (n) (a : R) : (monomial n a).support ⊆ singleton n

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ ((monomial n) a).support ⊆ {n}

Tactic:
rw [← ofFinsupp_single, support]

Result:
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ (Finsupp.single n a).support ⊆ {n}

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ (Finsupp.single n a).support ⊆ {n}

Tactic:
exact Finsupp.support_single_subset

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem getLast?_range (n : Nat) : (range n).getLast? = if n = 0 then none else some (n - 1)

Proof state:
case succ
n : Nat
ih : (range n).getLast? = if n = 0 then none else some (n - 1)
⊢ (range (n + 1)).getLast? = if n + 1 = 0 then none else some (n + 1 - 1)

Tactic:
simp only [range_succ, getLast?_append, ih]

Result:
case succ
n : Nat
ih : (range n).getLast? = if n = 0 then none else some (n - 1)
⊢ [n].getLast?.or (if n = 0 then none else some (n - 1)) = if n + 1 = 0 then none else some (n + 1 - 1)

Proof state:
case zero

⊢ (range 0).getLast? = if 0 = 0 then none else some (0 - 1)

Tactic:
simp

Result:
no goals

Proof state:
case succ
n : Nat
ih : (range n).getLast? = if n = 0 then none else some (n - 1)
⊢ [n].getLast?.or (if n = 0 then none else some (n - 1)) = if n + 1 = 0 then none else some (n + 1 - 1)

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
n : Nat
⊢ (range n).getLast? = if n = 0 then none else some (n - 1)

Tactic:
induction n with
| zero => simp
| succ n ih =>
  simp only [range_succ, getLast?_append, ih]
  split <;> simp_all

Result:
no goals
-- Mathlib/GroupTheory/Perm/Fin.lean
theorem cycleRange_succAbove {n : ℕ} (i : Fin (n + 1)) (j : Fin n) :
    i.cycleRange (i.succAbove j) = j.succ

Proof state:
n : ℕ
i : Fin (n + 1)
j : Fin n
⊢ i.cycleRange (i.succAbove j) = j.succ

Tactic:
rcases lt_or_ge (castSucc j) i with h | h

Result:
case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ i.cycleRange (i.succAbove j) = j.succ

case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc ≥ i
⊢ i.cycleRange (i.succAbove j) = j.succ

Proof state:
case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc ≥ i
⊢ i.cycleRange (i.succAbove j) = j.succ

Tactic:
rw [Fin.succAbove_of_le_castSucc _ _ h, Fin.cycleRange_of_gt (Fin.le_castSucc_iff.mp h)]

Result:
no goals

Proof state:
case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ i.cycleRange (i.succAbove j) = j.succ

Tactic:
rw [Fin.succAbove_of_castSucc_lt _ _ h, Fin.cycleRange_of_lt h, Fin.coeSucc_eq_succ]

Result:
no goals
-- Mathlib/Data/Matrix/RowCol.lean
theorem updateRow_subsingleton [Subsingleton m] (A : Matrix m n R) (i : m) (b : n → R) :
    A.updateRow i b = (row (Fin 1) b).submatrix (Function.const m 0) id

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝ : Subsingleton m
A : Matrix m n R
i : m
b : n → R
⊢ A.updateRow i b = (row (Fin 1) b).submatrix (Function.const m 0) id

Tactic:
ext x y

Result:
case a
m : Type u_2
n : Type u_3
R : Type u_5
inst✝ : Subsingleton m
A : Matrix m n R
i : m
b : n → R
x : m
y : n
⊢ A.updateRow i b x y = (row (Fin 1) b).submatrix (Function.const m 0) id x y

Proof state:
case a
m : Type u_2
n : Type u_3
R : Type u_5
inst✝ : Subsingleton m
A : Matrix m n R
i : m
b : n → R
x : m
y : n
⊢ A.updateRow i b x y = (row (Fin 1) b).submatrix (Function.const m 0) id x y

Tactic:
simp [updateCol_apply, Subsingleton.elim i x]

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem map_sigma_mk_comap {π : α → Type*} {π' : β → Type*} {f : α → β}
    (hf : Function.Injective f) (g : ∀ a, π a → π' (f a)) (a : α) (l : Filter (π' (f a))) :
    map (Sigma.mk a) (comap (g a) l) = comap (Sigma.map f g) (map (Sigma.mk (f a)) l)

Proof state:
α : Type u_1
β : Type u_2
π : α → Type u_6
π' : β → Type u_7
f : α → β
hf : Function.Injective f
g : (a : α) → π a → π' (f a)
a : α
l : Filter (π' (f a))
⊢ map (Sigma.mk a) (comap (g a) l) = comap (Sigma.map f g) (map (Sigma.mk (f a)) l)

Tactic:
refine (((basis_sets _).comap _).map _).eq_of_same_basis ?_

Result:
α : Type u_1
β : Type u_2
π : α → Type u_6
π' : β → Type u_7
f : α → β
hf : Function.Injective f
g : (a : α) → π a → π' (f a)
a : α
l : Filter (π' (f a))
⊢ (comap (Sigma.map f g) (map (Sigma.mk (f a)) l)).HasBasis (fun s => s ∈ l) fun i => Sigma.mk a '' (g a ⁻¹' id i)

Proof state:
case h.e'_5.h
α : Type u_1
β : Type u_2
π : α → Type u_6
π' : β → Type u_7
f : α → β
hf : Function.Injective f
g : (a : α) → π a → π' (f a)
a : α
l : Filter (π' (f a))
x✝ : Set (π' (f a))
⊢ Sigma.mk a '' (g a ⁻¹' id x✝) = Sigma.map f g ⁻¹' (Sigma.mk (f a) '' id x✝)

Tactic:
apply image_sigmaMk_preimage_sigmaMap hf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
π : α → Type u_6
π' : β → Type u_7
f : α → β
hf : Function.Injective f
g : (a : α) → π a → π' (f a)
a : α
l : Filter (π' (f a))
⊢ (comap (Sigma.map f g) (map (Sigma.mk (f a)) l)).HasBasis (fun s => s ∈ l) fun i => Sigma.mk a '' (g a ⁻¹' id i)

Tactic:
convert ((basis_sets l).map (Sigma.mk (f a))).comap (Sigma.map f g)

Result:
case h.e'_5.h
α : Type u_1
β : Type u_2
π : α → Type u_6
π' : β → Type u_7
f : α → β
hf : Function.Injective f
g : (a : α) → π a → π' (f a)
a : α
l : Filter (π' (f a))
x✝ : Set (π' (f a))
⊢ Sigma.mk a '' (g a ⁻¹' id x✝) = Sigma.map f g ⁻¹' (Sigma.mk (f a) '' id x✝)
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem coe_npowRec (f : α →ᵇ R) : ∀ n, ⇑(npowRec n f) = (⇑f) ^ n
  | 0 => by rw [npowRec, pow_zero, coe_one]
  | n + 1 => by rw [npowRec, pow_succ, coe_mul, coe_npowRec f n]

Proof state:
α : Type u
inst✝¹ : TopologicalSpace α
R : Type u_2
inst✝ : SeminormedRing R
f : α →ᵇ R
n : ℕ
⊢ ⇑(npowRec (n + 1) f) = ⇑f ^ (n + 1)

Tactic:
rw [npowRec, pow_succ, coe_mul, coe_npowRec f n]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : TopologicalSpace α
R : Type u_2
inst✝ : SeminormedRing R
f : α →ᵇ R
⊢ ⇑(npowRec 0 f) = ⇑f ^ 0

Tactic:
rw [npowRec, pow_zero, coe_one]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/IsLimit.lean
theorem hom_ext (h : IsColimit t) {W : C} {f f' : t.pt ⟶ W}
    (w : ∀ j, t.ι.app j ≫ f = t.ι.app j ≫ f') : f = f'

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cocone F
h : IsColimit t
W : C
f f' : t.pt ⟶ W
w : ∀ (j : J), t.ι.app j ≫ f = t.ι.app j ≫ f'
⊢ f = f'

Tactic:
rw [h.hom_desc f, h.hom_desc f']

Result:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cocone F
h : IsColimit t
W : C
f f' : t.pt ⟶ W
w : ∀ (j : J), t.ι.app j ≫ f = t.ι.app j ≫ f'
⊢ h.desc { pt := W, ι := { app := fun b => t.ι.app b ≫ f, naturality := ⋯ } } =
    h.desc { pt := W, ι := { app := fun b => t.ι.app b ≫ f', naturality := ⋯ } }

Proof state:
case h.e_8.h.e_ι.e_app
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cocone F
h : IsColimit t
W : C
f f' : t.pt ⟶ W
w : ∀ (j : J), t.ι.app j ≫ f = t.ι.app j ≫ f'
⊢ (fun b => t.ι.app b ≫ f) = fun b => t.ι.app b ≫ f'

Tactic:
exact funext w

Result:
no goals

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cocone F
h : IsColimit t
W : C
f f' : t.pt ⟶ W
w : ∀ (j : J), t.ι.app j ≫ f = t.ι.app j ≫ f'
⊢ h.desc { pt := W, ι := { app := fun b => t.ι.app b ≫ f, naturality := ⋯ } } =
    h.desc { pt := W, ι := { app := fun b => t.ι.app b ≫ f', naturality := ⋯ } }

Tactic:
congr

Result:
case h.e_8.h.e_ι.e_app
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cocone F
h : IsColimit t
W : C
f f' : t.pt ⟶ W
w : ∀ (j : J), t.ι.app j ≫ f = t.ι.app j ≫ f'
⊢ (fun b => t.ι.app b ≫ f) = fun b => t.ι.app b ≫ f'
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Basic.lean
theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l

Proof state:
α : Type u
a : α
l : List α
⊢ a ∈ l.toArray ↔ a ∈ l

Tactic:
simp [mem_def]

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem exists_quadraticMap_ne_zero {Q : QuadraticMap R M N}
    -- Porting note: added implicit argument
    (hB₁ : associated' (R := R) (N := N) Q ≠ 0) :
    ∃ x, Q x ≠ 0

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
hB₁ : associated' Q ≠ 0
⊢ ¬∀ (x : M), Q x = 0

Tactic:
intro h

Result:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
hB₁ : associated' Q ≠ 0
h : ∀ (x : M), Q x = 0
⊢ False

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
hB₁ : associated' Q ≠ 0
h : ∀ (x : M), Q x = 0
⊢ False

Tactic:
apply hB₁

Result:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
hB₁ : associated' Q ≠ 0
h : ∀ (x : M), Q x = 0
⊢ associated' Q = 0

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
hB₁ : associated' Q ≠ 0
⊢ ∃ x, Q x ≠ 0

Tactic:
rw [← not_forall]

Result:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
hB₁ : associated' Q ≠ 0
⊢ ¬∀ (x : M), Q x = 0

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
hB₁ : associated' Q ≠ 0
h : ∀ (x : M), Q x = 0
⊢ associated' Q = 0

Tactic:
rw [(QuadraticMap.ext h : Q = 0), LinearMap.map_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem sum_smul (i : Int) (xs : IntList) : (i * xs).sum = i * (xs.sum)

Proof state:
i : Int
xs : IntList
⊢ (i * xs).sum = i * xs.sum

Tactic:
induction xs with
| nil => simp
| cons x xs ih => simp_all [Int.mul_add]

Result:
no goals

Proof state:
case cons
i x : Int
xs : List Int
ih : (i * xs).sum = i * sum xs
⊢ (i * (x :: xs)).sum = i * sum (x :: xs)

Tactic:
simp_all [Int.mul_add]

Result:
no goals

Proof state:
case nil
i : Int
⊢ (i * []).sum = i * sum []

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Closed/Ideal.lean
theorem prodComparison_iso (A B : C) : IsIso
    (prodComparison (reflector i) A B) :=
  ⟨⟨bijection i _ _ _ (𝟙 _), by
      rw [← (bijection i _ _ _).injective.eq_iff, bijection_natural, ← bijection_symm_apply_id,
        Equiv.apply_symm_apply, id_comp],
      by rw [← bijection_natural, id_comp, ← bijection_symm_apply_id, Equiv.apply_symm_apply]⟩⟩

Proof state:
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : ChosenFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
⊢ prodComparison (reflector i) A B ≫ (bijection i A B ((reflector i).obj (A ⊗ B))) (𝟙 ((reflector i).obj (A ⊗ B))) =
    𝟙 ((reflector i).obj (A ⊗ B))

Tactic:
rw [← (bijection i _ _ _).injective.eq_iff, bijection_natural, ← bijection_symm_apply_id,
  Equiv.apply_symm_apply, id_comp]

Result:
no goals

Proof state:
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : ChosenFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
⊢ (bijection i A B ((reflector i).obj (A ⊗ B))) (𝟙 ((reflector i).obj (A ⊗ B))) ≫ prodComparison (reflector i) A B =
    𝟙 ((reflector i).obj A ⊗ (reflector i).obj B)

Tactic:
rw [← bijection_natural, id_comp, ← bijection_symm_apply_id, Equiv.apply_symm_apply]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
@[simp] lemma zpow_le_one_iff_right_of_lt_one₀ (ha₀ : 0 < a) (ha₁ : a < 1) : a ^ n ≤ 1 ↔ 0 ≤ n

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulStrictMono G₀
n : ℤ
ha₀ : 0 < a
ha₁ : a < 1
⊢ a ^ n ≤ 1 ↔ 0 ≤ n

Tactic:
simp [← zpow_le_zpow_iff_right_of_lt_one₀ ha₀ ha₁]

Result:
no goals
-- Mathlib/FieldTheory/IsAlgClosed/Classification.lean
theorem cardinal_le_max_transcendence_basis' (hv : IsTranscendenceBasis R v') :
    #K' ≤ max (max #R #ι') ℵ₀

Proof state:
R : Type u
inst✝³ : CommRing R
K' : Type u
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsAlgClosed K'
ι' : Type u
v' : ι' → K'
hv : IsTranscendenceBasis R v'
⊢ #K' ≤ #R ⊔ #ι' ⊔ ℵ₀

Tactic:
simpa using cardinal_le_max_transcendence_basis v' hv

Result:
no goals
-- Mathlib/Data/List/FinRange.lean
theorem mem_finRange {n : ℕ} (a : Fin n) : a ∈ finRange n

Proof state:
case mk
n val✝ : ℕ
isLt✝ : val✝ < n
⊢ ⟨↑⟨val✝, isLt✝⟩, ⋯⟩ = ⟨val✝, isLt✝⟩

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
a : Fin n
⊢ a ∈ pmap Fin.mk (range n) ⋯

Tactic:
exact mem_pmap.2
  ⟨a.1, mem_range.2 a.2, by
    cases a
    rfl⟩

Result:
no goals

Proof state:
n : ℕ
a : Fin n
⊢ a ∈ finRange n

Tactic:
rw [finRange_eq_pmap_range]

Result:
n : ℕ
a : Fin n
⊢ a ∈ pmap Fin.mk (range n) ⋯

Proof state:
n : ℕ
a : Fin n
⊢ ⟨↑a, ⋯⟩ = a

Tactic:
cases a

Result:
case mk
n val✝ : ℕ
isLt✝ : val✝ < n
⊢ ⟨↑⟨val✝, isLt✝⟩, ⋯⟩ = ⟨val✝, isLt✝⟩
-- Mathlib/Topology/Order/IsLocallyClosed.lean
theorem isLocallyClosed_Ioc [LinearOrder X] [ClosedIicTopology X] :
    IsLocallyClosed (Set.Ioc a b)

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
a b : X
inst✝¹ : LinearOrder X
inst✝ : ClosedIicTopology X
⊢ IsLocallyClosed (Set.Iic b ∩ Set.Ioi a)

Tactic:
exact isLocallyClosed_Iic.inter isLocallyClosed_Ioi

Result:
no goals

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
a b : X
inst✝¹ : LinearOrder X
inst✝ : ClosedIicTopology X
⊢ IsLocallyClosed (Set.Ioc a b)

Tactic:
rw [← Set.Iic_inter_Ioi]

Result:
X : Type u_1
inst✝² : TopologicalSpace X
a b : X
inst✝¹ : LinearOrder X
inst✝ : ClosedIicTopology X
⊢ IsLocallyClosed (Set.Iic b ∩ Set.Ioi a)
-- Mathlib/Data/Seq/Seq.lean
theorem destruct_eq_nil {s : Seq α} : destruct s = none → s = nil

Proof state:
case none
α : Type u
s : Seq α
f0 : s.get? 0 = none
h : Option.map (fun a' => (a', s.tail)) none = none
⊢ s = nil

Tactic:
apply Subtype.eq

Result:
case none.a
α : Type u
s : Seq α
f0 : s.get? 0 = none
h : Option.map (fun a' => (a', s.tail)) none = none
⊢ ↑s = ↑nil

Proof state:
case none.a
α : Type u
s : Seq α
f0 : s.get? 0 = none
h : Option.map (fun a' => (a', s.tail)) none = none
⊢ ↑s = ↑nil

Tactic:
funext n

Result:
case none.a.h
α : Type u
s : Seq α
f0 : s.get? 0 = none
h : Option.map (fun a' => (a', s.tail)) none = none
n : ℕ
⊢ ↑s n = ↑nil n

Proof state:
α : Type u
s : Seq α
⊢ Option.map (fun a' => (a', s.tail)) (s.get? 0) = none → s = nil

Tactic:
induction' f0 : get? s 0 <;> intro h

Result:
case none
α : Type u
s : Seq α
f0 : s.get? 0 = none
h : Option.map (fun a' => (a', s.tail)) none = none
⊢ s = nil

case some
α : Type u
s : Seq α
val✝ : α
f0 : s.get? 0 = some val✝
h : Option.map (fun a' => (a', s.tail)) (some val✝) = none
⊢ s = nil

Proof state:
case none.a.h
α : Type u
s : Seq α
f0 : s.get? 0 = none
h : Option.map (fun a' => (a', s.tail)) none = none
n : ℕ
⊢ ↑s n = ↑nil n

Tactic:
induction' n with n IH

Result:
case none.a.h.zero
α : Type u
s : Seq α
f0 : s.get? 0 = none
h : Option.map (fun a' => (a', s.tail)) none = none
⊢ ↑s 0 = ↑nil 0

case none.a.h.succ
α : Type u
s : Seq α
f0 : s.get? 0 = none
h : Option.map (fun a' => (a', s.tail)) none = none
n : ℕ
IH : ↑s n = ↑nil n
⊢ ↑s (n + 1) = ↑nil (n + 1)

Proof state:
case some
α : Type u
s : Seq α
val✝ : α
f0 : s.get? 0 = some val✝
h : Option.map (fun a' => (a', s.tail)) (some val✝) = none
⊢ s = nil

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type u
s : Seq α
⊢ s.destruct = none → s = nil

Tactic:
dsimp [destruct]

Result:
α : Type u
s : Seq α
⊢ Option.map (fun a' => (a', s.tail)) (s.get? 0) = none → s = nil

Proof state:
case none.a.h.zero
α : Type u
s : Seq α
f0 : s.get? 0 = none
h : Option.map (fun a' => (a', s.tail)) none = none
⊢ ↑s 0 = ↑nil 0

case none.a.h.succ
α : Type u
s : Seq α
f0 : s.get? 0 = none
h : Option.map (fun a' => (a', s.tail)) none = none
n : ℕ
IH : ↑s n = ↑nil n
⊢ ↑s (n + 1) = ↑nil (n + 1)

Tactic:
exacts [f0, s.2 IH]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/AddCircle.lean
theorem norm_neg_period (x : ℝ) : ‖(x : AddCircle (-p))‖ = ‖(x : AddCircle p)‖

Proof state:
p x : ℝ
⊢ ‖↑(-1 * x)‖ = ‖↑x‖

Tactic:
simp only [norm_coe_mul, abs_neg, abs_one, one_mul]

Result:
no goals

Proof state:
p x : ℝ
⊢ ‖↑x‖ = ‖↑x‖

Tactic:
suffices ‖(↑(-1 * x) : AddCircle (-1 * p))‖ = ‖(x : AddCircle p)‖ by
  rw [← this, neg_one_mul]
  simp

Result:
p x : ℝ
⊢ ‖↑(-1 * x)‖ = ‖↑x‖

Proof state:
p x : ℝ
this : ‖↑(-1 * x)‖ = ‖↑x‖
⊢ ‖↑x‖ = ‖↑(-1 * x)‖

Tactic:
simp

Result:
no goals

Proof state:
p x : ℝ
this : ‖↑(-1 * x)‖ = ‖↑x‖
⊢ ‖↑x‖ = ‖↑x‖

Tactic:
rw [← this, neg_one_mul]

Result:
p x : ℝ
this : ‖↑(-1 * x)‖ = ‖↑x‖
⊢ ‖↑x‖ = ‖↑(-1 * x)‖
-- Mathlib/Analysis/CStarAlgebra/Multiplier.lean
theorem norm_fst_eq_snd (a : 𝓜(𝕜, A)) : ‖a.fst‖ = ‖a.snd‖

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CStarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h : ∀ (b : A), ‖f b‖₊ ^ 2 ≤ C * ‖f b‖₊ * ‖b‖₊
h1 : ∀ (b : A), C * ‖f b‖₊ * ‖b‖₊ ≤ C * ‖f‖₊ * ‖b‖₊ ^ 2
⊢ ∀ (x : A), ‖f x‖₊ ≤ ?m.428509 * ?m.428510 * ‖x‖₊

Tactic:
simpa only [sqrt_sq, sqrt_mul] using fun b ↦ sqrt_le_sqrt.2 <| (h b).trans (h1 b)

Result:
no goals