harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Tactic/NormNum/GCD.lean
theorem isInt_ratNum : ∀ {q : ℚ} {n : ℤ} {n' : ℕ} {d : ℕ},
    IsRat q n d → n.natAbs = n' → n'.gcd d = 1 → IsInt q.num n
  | _, n, _, d, ⟨hi, rfl⟩, rfl, h => by
    constructor
    have : 0 < d := Nat.pos_iff_ne_zero.mpr <| by simpa using hi.ne_zero
    simp_rw [Rat.mul_num, Rat.intCast_den, invOf_eq_inv,
      Rat.inv_natCast_den_of_pos this, Rat.inv_natCast_num_of_pos this,
      Rat.intCast_num, one_mul, mul_one, h, Nat.cast_one, Int.ediv_one, Int.cast_id]

Proof state:
case out
n : ℤ
d : ℕ
hi : Invertible ↑d
h : n.natAbs.gcd d = 1
this : 0 < d
⊢ (↑n * ⅟↑d).num = ↑n

Tactic:
simp_rw [Rat.mul_num, Rat.intCast_den, invOf_eq_inv,
  Rat.inv_natCast_den_of_pos this, Rat.inv_natCast_num_of_pos this,
  Rat.intCast_num, one_mul, mul_one, h, Nat.cast_one, Int.ediv_one, Int.cast_id]

Result:
no goals

Proof state:
n : ℤ
d : ℕ
hi : Invertible ↑d
h : n.natAbs.gcd d = 1
⊢ d ≠ 0

Tactic:
simpa using hi.ne_zero

Result:
no goals

Proof state:
n : ℤ
d : ℕ
hi : Invertible ↑d
h : n.natAbs.gcd d = 1
⊢ IsInt (↑n * ⅟↑d).num n

Tactic:
constructor

Result:
case out
n : ℤ
d : ℕ
hi : Invertible ↑d
h : n.natAbs.gcd d = 1
⊢ (↑n * ⅟↑d).num = ↑n

Proof state:
case out
n : ℤ
d : ℕ
hi : Invertible ↑d
h : n.natAbs.gcd d = 1
⊢ (↑n * ⅟↑d).num = ↑n

Tactic:
have : 0 < d := Nat.pos_iff_ne_zero.mpr <| by simpa using hi.ne_zero

Result:
case out
n : ℤ
d : ℕ
hi : Invertible ↑d
h : n.natAbs.gcd d = 1
this : 0 < d
⊢ (↑n * ⅟↑d).num = ↑n
-- Mathlib/Data/List/Perm/Basic.lean
theorem set_perm_cons_eraseIdx {n : ℕ} (h : n < l.length) (a : α) :
    l.set n a ~ a :: l.eraseIdx n

Proof state:
α : Type u_1
l : List α
n : ℕ
h : n < l.length
a : α
⊢ insertIdx n a (l.eraseIdx n) ~ a :: l.eraseIdx n

Tactic:
apply perm_insertIdx

Result:
case h
α : Type u_1
l : List α
n : ℕ
h : n < l.length
a : α
⊢ n ≤ (l.eraseIdx n).length

Proof state:
case h
α : Type u_1
l : List α
n : ℕ
h : n < l.length
a : α
⊢ n ≤ l.length - 1

Tactic:
exact Nat.le_sub_one_of_lt h

Result:
no goals

Proof state:
case h
α : Type u_1
l : List α
n : ℕ
h : n < l.length
a : α
⊢ n ≤ (l.eraseIdx n).length

Tactic:
rw [length_eraseIdx_of_lt h]

Result:
case h
α : Type u_1
l : List α
n : ℕ
h : n < l.length
a : α
⊢ n ≤ l.length - 1

Proof state:
α : Type u_1
l : List α
n : ℕ
h : n < l.length
a : α
⊢ l.set n a ~ a :: l.eraseIdx n

Tactic:
rw [← insertIdx_eraseIdx h.ne]

Result:
α : Type u_1
l : List α
n : ℕ
h : n < l.length
a : α
⊢ insertIdx n a (l.eraseIdx n) ~ a :: l.eraseIdx n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem mem_range' {n} : m ∈ range' s n step ↔ ∃ i < n, m = s + step * i

Proof state:
case mp.intro.mk.refl
s step n i : Nat
w : i < n
⊢ ∃ i_1, i_1 < n ∧ s + step * ↑⟨i, w⟩ = s + step * i_1

Tactic:
exact ⟨i, w, by simp_all⟩

Result:
no goals

Proof state:
s step m n : Nat
⊢ m ∈ range' s n step ↔ ∃ i, i < n ∧ m = s + step * i

Tactic:
simp [range']

Result:
s step m n : Nat
⊢ (∃ i, s + step * ↑i = m) ↔ ∃ i, i < n ∧ m = s + step * i

Proof state:
s step n i : Nat
w : i < n
⊢ s + step * ↑⟨i, w⟩ = s + step * i

Tactic:
simp_all

Result:
no goals

Proof state:
s step m n i : Nat
w : i < n
h' : m = s + step * i
⊢ s + step * ↑⟨i, w⟩ = m

Tactic:
simp_all

Result:
no goals

Proof state:
s step m n : Nat
⊢ (∃ i, s + step * ↑i = m) ↔ ∃ i, i < n ∧ m = s + step * i

Tactic:
constructor

Result:
case mp
s step m n : Nat
⊢ (∃ i, s + step * ↑i = m) → ∃ i, i < n ∧ m = s + step * i

case mpr
s step m n : Nat
⊢ (∃ i, i < n ∧ m = s + step * i) → ∃ i, s + step * ↑i = m

Proof state:
case mpr.intro.intro
s step m n i : Nat
w : i < n
h' : m = s + step * i
⊢ ∃ i, s + step * ↑i = m

Tactic:
exact ⟨⟨i, w⟩, by simp_all⟩

Result:
no goals

Proof state:
case mp
s step m n : Nat
⊢ (∃ i, s + step * ↑i = m) → ∃ i, i < n ∧ m = s + step * i

Tactic:
rintro ⟨⟨i, w⟩, h, h'⟩

Result:
case mp.intro.mk.refl
s step n i : Nat
w : i < n
⊢ ∃ i_1, i_1 < n ∧ s + step * ↑⟨i, w⟩ = s + step * i_1

Proof state:
case mpr
s step m n : Nat
⊢ (∃ i, i < n ∧ m = s + step * i) → ∃ i, s + step * ↑i = m

Tactic:
rintro ⟨i, w, h'⟩

Result:
case mpr.intro.intro
s step m n i : Nat
w : i < n
h' : m = s + step * i
⊢ ∃ i, s + step * ↑i = m
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem nfp_mul_zero (a : Ordinal) : nfp (a * ·) 0 = 0

Proof state:
a : Ordinal.{u_1}
n : ℕ
⊢ (fun x => a * x)^[n] 0 ≤ 0

Tactic:
induction' n with n hn

Result:
case zero
a : Ordinal.{u_1}
⊢ (fun x => a * x)^[0] 0 ≤ 0

case succ
a : Ordinal.{u_1}
n : ℕ
hn : (fun x => a * x)^[n] 0 ≤ 0
⊢ (fun x => a * x)^[n + 1] 0 ≤ 0

Proof state:
a : Ordinal.{u_1}
⊢ nfp (fun x => a * x) 0 = 0

Tactic:
rw [← Ordinal.le_zero, nfp_le_iff]

Result:
a : Ordinal.{u_1}
⊢ ∀ (n : ℕ), (fun x => a * x)^[n] 0 ≤ 0

Proof state:
case zero
a : Ordinal.{u_1}
⊢ (fun x => a * x)^[0] 0 ≤ 0

Tactic:
rfl

Result:
no goals

Proof state:
a : Ordinal.{u_1}
⊢ ∀ (n : ℕ), (fun x => a * x)^[n] 0 ≤ 0

Tactic:
intro n

Result:
a : Ordinal.{u_1}
n : ℕ
⊢ (fun x => a * x)^[n] 0 ≤ 0

Proof state:
case succ
a : Ordinal.{u_1}
n : ℕ
hn : (fun x => a * x)^[n] 0 ≤ 0
⊢ (fun x => a * x)^[n + 1] 0 ≤ 0

Tactic:
rwa [iterate_succ_apply, mul_zero]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem coe_algHomOfDvd {p q : K[X]} (hpq : q ∣ p) :
    (algHomOfDvd hpq).toFun = liftHom p (root q) (by simp only [aeval_eq, mk_eq_zero, hpq]) :=
  rfl

Proof state:
K : Type ?u.356156
L : Type ?u.356159
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p q : K[X]
hpq : q ∣ p
⊢ (aeval (root q)) p = 0

Tactic:
simp only [aeval_eq, mk_eq_zero, hpq]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isLittleO_pow_id {n : ℕ} (h : 1 < n) : (fun x : 𝕜 => x ^ n) =o[𝓝 0] fun x => x

Proof state:
case h.e'_8.h
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
n : ℕ
h : 1 < n
x✝ : 𝕜
⊢ x✝ = x✝ ^ 1

Tactic:
simp only [pow_one]

Result:
no goals

Proof state:
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
n : ℕ
h : 1 < n
⊢ (fun x => x ^ n) =o[𝓝 0] fun x => x

Tactic:
convert isLittleO_pow_pow h (𝕜 := 𝕜)

Result:
case h.e'_8.h
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
n : ℕ
h : 1 < n
x✝ : 𝕜
⊢ x✝ = x✝ ^ 1
-- Mathlib/Algebra/Homology/DerivedCategory/Basic.lean
lemma quotient_obj_mem_subcategoryAcyclic_iff_exactAt (K : CochainComplex C ℤ) :
    (subcategoryAcyclic C).P ((quotient _ _).obj K) ↔ ∀ (n : ℤ), K.ExactAt n

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
K : CochainComplex C ℤ
n : ℤ
⊢ IsZero ((homologyFunctor C (ComplexShape.up ℤ) n).obj ((quotient C (ComplexShape.up ℤ)).obj K)) ↔
    IsZero (HomologicalComplex.homology K n)

Tactic:
exact ((homologyFunctorFactors C (ComplexShape.up ℤ) n).app K).isZero_iff

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
K : CochainComplex C ℤ
⊢ (∀ (n : ℤ), IsZero ((homologyFunctor C (ComplexShape.up ℤ) n).obj ((quotient C (ComplexShape.up ℤ)).obj K))) ↔
    ∀ (n : ℤ), HomologicalComplex.ExactAt K n

Tactic:
refine forall_congr' (fun n => ?_)

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
K : CochainComplex C ℤ
n : ℤ
⊢ IsZero ((homologyFunctor C (ComplexShape.up ℤ) n).obj ((quotient C (ComplexShape.up ℤ)).obj K)) ↔
    HomologicalComplex.ExactAt K n

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
K : CochainComplex C ℤ
n : ℤ
⊢ IsZero ((homologyFunctor C (ComplexShape.up ℤ) n).obj ((quotient C (ComplexShape.up ℤ)).obj K)) ↔
    HomologicalComplex.ExactAt K n

Tactic:
simp only [HomologicalComplex.exactAt_iff_isZero_homology]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
K : CochainComplex C ℤ
n : ℤ
⊢ IsZero ((homologyFunctor C (ComplexShape.up ℤ) n).obj ((quotient C (ComplexShape.up ℤ)).obj K)) ↔
    IsZero (HomologicalComplex.homology K n)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
K : CochainComplex C ℤ
⊢ (subcategoryAcyclic C).P ((quotient C (ComplexShape.up ℤ)).obj K) ↔ ∀ (n : ℤ), HomologicalComplex.ExactAt K n

Tactic:
rw [mem_subcategoryAcyclic_iff]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
K : CochainComplex C ℤ
⊢ (∀ (n : ℤ), IsZero ((homologyFunctor C (ComplexShape.up ℤ) n).obj ((quotient C (ComplexShape.up ℤ)).obj K))) ↔
    ∀ (n : ℤ), HomologicalComplex.ExactAt K n
-- Mathlib/Algebra/DirectSum/Basic.lean
theorem coeAddMonoidHom_eq_dfinsupp_sum [DecidableEq ι]
    {M S : Type*} [DecidableEq M] [AddCommMonoid M]
    [SetLike S M] [AddSubmonoidClass S M] (A : ι → S) (x : DirectSum ι fun i => A i) :
    DirectSum.coeAddMonoidHom A x = DFinsupp.sum x fun i => (fun x : A i => ↑x)

Proof state:
ι : Type v
inst✝⁴ : DecidableEq ι
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
x : ⨁ (i : ι), ↥(A i)
⊢ (DFinsupp.sumAddHom fun i => AddSubmonoidClass.subtype (A i)) x = DFinsupp.sum x fun i x => ↑x

Tactic:
exact DFinsupp.sumAddHom_apply _ x

Result:
no goals

Proof state:
ι : Type v
inst✝⁴ : DecidableEq ι
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
x : ⨁ (i : ι), ↥(A i)
⊢ (DirectSum.coeAddMonoidHom A) x = DFinsupp.sum x fun i x => ↑x

Tactic:
simp only [DirectSum.coeAddMonoidHom, toAddMonoid, DFinsupp.liftAddHom, AddEquiv.coe_mk,
  Equiv.coe_fn_mk]

Result:
ι : Type v
inst✝⁴ : DecidableEq ι
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
x : ⨁ (i : ι), ↥(A i)
⊢ (DFinsupp.sumAddHom fun i => AddSubmonoidClass.subtype (A i)) x = DFinsupp.sum x fun i x => ↑x
-- Mathlib/Algebra/Category/Grp/ChosenFiniteProducts.lean
theorem μ_forget_apply {G H : Grp.{u}} (p : G) (q : H) :
    Functor.LaxMonoidal.μ (forget Grp.{u}) G H (p, q) = (p, q)

Proof state:
case fst
G H : Grp
p : ↑G
q : ↑H
⊢ (Functor.LaxMonoidal.μ (forget Grp) G H (p, q)).1 = (p, q).1

Tactic:
exact congrFun (Functor.Monoidal.μ_fst (forget Grp.{u}) G H) (p, q)

Result:
no goals

Proof state:
G H : Grp
p : ↑G
q : ↑H
⊢ Functor.LaxMonoidal.μ (forget Grp) G H (p, q) = (p, q)

Tactic:
apply Prod.ext

Result:
case fst
G H : Grp
p : ↑G
q : ↑H
⊢ (Functor.LaxMonoidal.μ (forget Grp) G H (p, q)).1 = (p, q).1

case snd
G H : Grp
p : ↑G
q : ↑H
⊢ (Functor.LaxMonoidal.μ (forget Grp) G H (p, q)).2 = (p, q).2

Proof state:
case snd
G H : Grp
p : ↑G
q : ↑H
⊢ (Functor.LaxMonoidal.μ (forget Grp) G H (p, q)).2 = (p, q).2

Tactic:
exact congrFun (Functor.Monoidal.μ_snd (forget Grp.{u}) G H) (p, q)

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Abs.lean
@[to_additive] lemma mabs_zpow (n : ℤ) (a : α) : |a ^ n|ₘ = |a|ₘ ^ |n|

Proof state:
α : Type u_1
inst✝ : LinearOrderedCommGroup α
n : ℤ
a : α
⊢ mabs (a ^ n) = mabs a ^ |n|

Tactic:
obtain n0 | n0 := le_total 0 n

Result:
case inl
α : Type u_1
inst✝ : LinearOrderedCommGroup α
n : ℤ
a : α
n0 : 0 ≤ n
⊢ mabs (a ^ n) = mabs a ^ |n|

case inr
α : Type u_1
inst✝ : LinearOrderedCommGroup α
n : ℤ
a : α
n0 : n ≤ 0
⊢ mabs (a ^ n) = mabs a ^ |n|

Proof state:
case inl.intro
α : Type u_1
inst✝ : LinearOrderedCommGroup α
a : α
n : ℕ
n0 : 0 ≤ ↑n
⊢ mabs (a ^ ↑n) = mabs a ^ |↑n|

Tactic:
simp only [mabs_pow, zpow_natCast, Nat.abs_cast]

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrderedCommGroup α
n : ℤ
a : α
n0 : n ≤ 0
⊢ mabs (a ^ n) = mabs a ^ |n|

Tactic:
obtain ⟨m, h⟩ := Int.eq_ofNat_of_zero_le (neg_nonneg.2 n0)

Result:
case inr.intro
α : Type u_1
inst✝ : LinearOrderedCommGroup α
n : ℤ
a : α
n0 : n ≤ 0
m : ℕ
h : -n = ↑m
⊢ mabs (a ^ n) = mabs a ^ |n|

Proof state:
case inr.intro
α : Type u_1
inst✝ : LinearOrderedCommGroup α
n : ℤ
a : α
n0 : n ≤ 0
m : ℕ
h : -n = ↑m
⊢ mabs (a ^ n) = mabs a ^ |n|

Tactic:
rw [← mabs_inv, ← zpow_neg, ← abs_neg, h, zpow_natCast, Nat.abs_cast, zpow_natCast]

Result:
case inr.intro
α : Type u_1
inst✝ : LinearOrderedCommGroup α
n : ℤ
a : α
n0 : n ≤ 0
m : ℕ
h : -n = ↑m
⊢ mabs (a ^ m) = mabs a ^ m

Proof state:
case inl
α : Type u_1
inst✝ : LinearOrderedCommGroup α
n : ℤ
a : α
n0 : 0 ≤ n
⊢ mabs (a ^ n) = mabs a ^ |n|

Tactic:
obtain ⟨n, rfl⟩ := Int.eq_ofNat_of_zero_le n0

Result:
case inl.intro
α : Type u_1
inst✝ : LinearOrderedCommGroup α
a : α
n : ℕ
n0 : 0 ≤ ↑n
⊢ mabs (a ^ ↑n) = mabs a ^ |↑n|

Proof state:
case inr.intro
α : Type u_1
inst✝ : LinearOrderedCommGroup α
n : ℤ
a : α
n0 : n ≤ 0
m : ℕ
h : -n = ↑m
⊢ mabs (a ^ m) = mabs a ^ m

Tactic:
exact mabs_pow m _

Result:
no goals
-- Mathlib/Data/Finset/Density.lean
@[simp] lemma card_mul_dens (s : Finset α) : Fintype.card α * s.dens = s.card

Proof state:
α : Type u_2
inst✝ : Fintype α
s : Finset α
⊢ ↑(Fintype.card α) * s.dens = ↑(#s)

Tactic:
cases isEmpty_or_nonempty α

Result:
case inl
α : Type u_2
inst✝ : Fintype α
s : Finset α
h✝ : IsEmpty α
⊢ ↑(Fintype.card α) * s.dens = ↑(#s)

case inr
α : Type u_2
inst✝ : Fintype α
s : Finset α
h✝ : Nonempty α
⊢ ↑(Fintype.card α) * s.dens = ↑(#s)

Proof state:
case inl
α : Type u_2
inst✝ : Fintype α
s : Finset α
h✝ : IsEmpty α
⊢ ↑(Fintype.card α) * s.dens = ↑(#s)

Tactic:
simp [Subsingleton.elim s ∅]

Result:
no goals

Proof state:
case inr.hb
α : Type u_2
inst✝ : Fintype α
s : Finset α
h✝ : Nonempty α
⊢ ↑(Fintype.card α) ≠ 0

Tactic:
exact mod_cast Fintype.card_ne_zero

Result:
no goals

Proof state:
case inr
α : Type u_2
inst✝ : Fintype α
s : Finset α
h✝ : Nonempty α
⊢ ↑(Fintype.card α) * s.dens = ↑(#s)

Tactic:
rw [dens, mul_div_cancel₀]

Result:
case inr.hb
α : Type u_2
inst✝ : Fintype α
s : Finset α
h✝ : Nonempty α
⊢ ↑(Fintype.card α) ≠ 0
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isCoseparator_op_iff (G : C) : IsCoseparator (op G) ↔ IsSeparator G

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
⊢ IsCoseparator (op G) ↔ IsSeparator G

Tactic:
rw [IsSeparator, IsCoseparator, ← isCoseparating_op_iff, Set.singleton_op]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean
theorem incMatrix_apply_mul_incMatrix_apply_of_not_adj (hab : a ≠ b) (h : ¬G.Adj a b) :
    G.incMatrix R a e * G.incMatrix R b e = 0

Proof state:
case h
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝ : MulZeroOneClass R
a b : α
e : Sym2 α
hab : a ≠ b
h : ¬G.Adj a b
⊢ e ∉ ∅

Tactic:
exact Set.not_mem_empty e

Result:
no goals

Proof state:
case h
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝ : MulZeroOneClass R
a b : α
e : Sym2 α
hab : a ≠ b
h : ¬G.Adj a b
⊢ e ∉ G.incidenceSet a ∩ G.incidenceSet b

Tactic:
rw [G.incidenceSet_inter_incidenceSet_of_not_adj h hab]

Result:
case h
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝ : MulZeroOneClass R
a b : α
e : Sym2 α
hab : a ≠ b
h : ¬G.Adj a b
⊢ e ∉ ∅

Proof state:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝ : MulZeroOneClass R
a b : α
e : Sym2 α
hab : a ≠ b
h : ¬G.Adj a b
⊢ incMatrix R G a e * incMatrix R G b e = 0

Tactic:
rw [incMatrix_apply_mul_incMatrix_apply, Set.indicator_of_not_mem]

Result:
case h
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝ : MulZeroOneClass R
a b : α
e : Sym2 α
hab : a ≠ b
h : ¬G.Adj a b
⊢ e ∉ G.incidenceSet a ∩ G.incidenceSet b
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem singleton_mul_ball_one : {x} * ball 1 δ = ball x δ

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ {x} * ball 1 δ = ball x δ

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/WittVector/InitTail.lean
theorem init_init (x : 𝕎 R) (n : ℕ) : init n (init n x) = init n x

Proof state:
p : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n i : ℕ
⊢ (if i < n then if i < n then x.coeff i else 0 else 0) = if i < n then x.coeff i else 0

Tactic:
by_cases hi : i < n <;> simp [hi]

Result:
no goals

Proof state:
p : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n i : ℕ
⊢ (init n (init n x)).coeff i = (init n x).coeff i

Tactic:
simp only [WittVector.init, WittVector.select, WittVector.coeff_mk]

Result:
p : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n i : ℕ
⊢ (if i < n then if i < n then x.coeff i else 0 else 0) = if i < n then x.coeff i else 0

Proof state:
p : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
⊢ init n (init n x) = init n x

Tactic:
rw [WittVector.ext_iff]

Result:
p : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
⊢ ∀ (n_1 : ℕ), (init n (init n x)).coeff n_1 = (init n x).coeff n_1

Proof state:
p : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
⊢ ∀ (n_1 : ℕ), (init n (init n x)).coeff n_1 = (init n x).coeff n_1

Tactic:
intro i

Result:
p : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n i : ℕ
⊢ (init n (init n x)).coeff i = (init n x).coeff i
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem commute_T (n : ℤ) (f : R[T;T⁻¹]) : Commute (T n) f :=
  f.induction_on' (fun _ _ Tp Tq => Commute.add_right Tp Tq) fun m a =>
    show T n * _ = _ by
      rw [T, T, ← single_eq_C, single_mul_single, single_mul_single, single_mul_single]
      simp [add_comm]

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℤ
f : R[T;T⁻¹]
m : ℤ
a : R
⊢ AddMonoidAlgebra.single (n + (0 + m)) (1 * (a * 1)) = AddMonoidAlgebra.single (0 + m + n) (a * 1 * 1)

Tactic:
simp [add_comm]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℤ
f : R[T;T⁻¹]
m : ℤ
a : R
⊢ T n * (C a * T m) = C a * T m * T n

Tactic:
rw [T, T, ← single_eq_C, single_mul_single, single_mul_single, single_mul_single]

Result:
R : Type u_1
inst✝ : Semiring R
n : ℤ
f : R[T;T⁻¹]
m : ℤ
a : R
⊢ AddMonoidAlgebra.single (n + (0 + m)) (1 * (a * 1)) = AddMonoidAlgebra.single (0 + m + n) (a * 1 * 1)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey_modifyKey [EquivBEq α] [Inhabited α] {k k' : α} {f : β → β} (l : List ((_ : α) × β))
    (hl : DistinctKeys l) (h : containsKey k' (modifyKey k f l)) :
    getKey k' (modifyKey k f l) h =
      if k == k' then
        k
      else
        haveI h' : containsKey k' l

Proof state:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : EquivBEq α
inst✝ : Inhabited α
k k' : α
f : β → β
l : List ((_ : α) × β)
hl : DistinctKeys l
h : containsKey k' (modifyKey k f l) = true
⊢ getKey k' (modifyKey k f l) h = if (k == k') = true then k else getKey k' l ⋯

Tactic:
simp [modifyKey_eq_alterKey, getKey_alterKey, hl]

Result:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : EquivBEq α
inst✝ : Inhabited α
k k' : α
f : β → β
l : List ((_ : α) × β)
hl : DistinctKeys l
h : containsKey k' (modifyKey k f l) = true
⊢ (if heq : (k == k') = true then k else getKey k' l ⋯) = if (k == k') = true then k else getKey k' l ⋯

Proof state:
α : Type u
β✝ : α → Type v
γ : α → Type w
β : Type v
inst✝² : BEq α
inst✝¹ : EquivBEq α
inst✝ : Inhabited α
k k' : α
f : β → β
l : List ((_ : α) × β)
hl : DistinctKeys l
h : containsKey k' (modifyKey k f l) = true
⊢ containsKey k' l = true

Tactic:
rwa [containsKey_modifyKey] at h

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : EquivBEq α
inst✝ : Inhabited α
k k' : α
f : β → β
l : List ((_ : α) × β)
hl : DistinctKeys l
h : containsKey k' (modifyKey k f l) = true
⊢ (if heq : (k == k') = true then k else getKey k' l ⋯) = if (k == k') = true then k else getKey k' l ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Slope.lean
theorem slope_sub_smul (f : k → E) {a b : k} (h : a ≠ b) :
    slope (fun x => (x - a) • f x) a b = f b

Proof state:
k : Type u_1
E : Type u_2
inst✝² : Field k
inst✝¹ : AddCommGroup E
inst✝ : Module k E
f : k → E
a b : k
h : a ≠ b
⊢ slope (fun x => (x - a) • f x) a b = f b

Tactic:
simp [slope, inv_smul_smul₀ (sub_ne_zero.2 h.symm)]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean
theorem tprod_comm' {f : β → γ → α} (h : Multipliable (Function.uncurry f))
    (h₁ : ∀ b, Multipliable (f b)) (h₂ : ∀ c, Multipliable fun b ↦ f b c) :
    ∏' (c) (b), f b c = ∏' (b) (c), f b c

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : T3Space α
f : β → γ → α
h : Multipliable (uncurry f)
h₁ : ∀ (b : β), Multipliable (f b)
h₂ : ∀ (c : γ), Multipliable fun b => f b c
⊢ ∏' (p : γ × β), uncurry f p.swap = ∏' (c : γ × β), uncurry f ((Equiv.prodComm γ β) c)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : T3Space α
f : β → γ → α
h : Multipliable (uncurry f)
h₁ : ∀ (b : β), Multipliable (f b)
h₂ : ∀ (c : γ), Multipliable fun b => f b c
⊢ ∏' (c : γ) (b : β), f b c = ∏' (b : β) (c : γ), f b c

Tactic:
erw [← tprod_prod' h h₁, ← tprod_prod' h.prod_symm h₂,
    ← (Equiv.prodComm γ β).tprod_eq (uncurry f)]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : T3Space α
f : β → γ → α
h : Multipliable (uncurry f)
h₁ : ∀ (b : β), Multipliable (f b)
h₂ : ∀ (c : γ), Multipliable fun b => f b c
⊢ ∏' (p : γ × β), uncurry f p.swap = ∏' (c : γ × β), uncurry f ((Equiv.prodComm γ β) c)
-- Mathlib/RingTheory/Radical.lean
theorem radical_zero_eq : radical (0 : M) = 1

Proof state:
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
⊢ radical 0 = 1

Tactic:
rw [radical, primeFactors, normalizedFactors_zero, Multiset.toFinset_zero, Finset.prod_empty]

Result:
no goals

Proof state:
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
⊢ radical 0 = 1

Tactic:
classical
rw [radical, primeFactors, normalizedFactors_zero, Multiset.toFinset_zero, Finset.prod_empty]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem real_inner_I_smul_self (x : E) :
    @Inner.inner ℝ E (Inner.rclikeToReal 𝕜 E) x ((I : 𝕜) • x) = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ ⟪x, I • x⟫_ℝ = 0

Tactic:
simp [real_inner_eq_re_inner 𝕜, inner_smul_right]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Ker.lean
theorem div_mem_ker_iff (f : G →* N) {x y : G} : x / y ∈ ker f ↔ f x = f y

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
x y : G
⊢ x / y ∈ f.ker ↔ f x = f y

Tactic:
rw [mem_ker, map_div, div_eq_one]

Result:
no goals
-- Mathlib/Topology/Bases.lean
theorem countable_cover_nhds [SecondCountableTopology α] {f : α → Set α} (hf : ∀ x, f x ∈ 𝓝 x) :
    ∃ s : Set α, s.Countable ∧ ⋃ x ∈ s, f x = univ

Proof state:
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
⊢ ∃ s, s.Countable ∧ ⋃ x ∈ s, f x = univ

Tactic:
rcases isOpen_iUnion_countable (fun x => interior (f x)) fun x => isOpen_interior with
  ⟨s, hsc, hsU⟩

Result:
case intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
s : Set α
hsc : s.Countable
hsU : ⋃ i ∈ s, interior (f i) = ⋃ i, interior (f i)
⊢ ∃ s, s.Countable ∧ ⋃ x ∈ s, f x = univ

Proof state:
case intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
s : Set α
hsc : s.Countable
hsU : ⋃ i ∈ s, interior (f i) = ⋃ i, interior (f i)
⊢ ∃ s, s.Countable ∧ ⋃ x ∈ s, f x = univ

Tactic:
suffices ⋃ x ∈ s, interior (f x) = univ from
  ⟨s, hsc, flip eq_univ_of_subset this <| iUnion₂_mono fun _ _ => interior_subset⟩

Result:
case intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
s : Set α
hsc : s.Countable
hsU : ⋃ i ∈ s, interior (f i) = ⋃ i, interior (f i)
⊢ ⋃ x ∈ s, interior (f x) = univ

Proof state:
case intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
s : Set α
hsc : s.Countable
hsU : ⋃ i ∈ s, interior (f i) = ⋃ i, interior (f i)
⊢ ⋃ x ∈ s, interior (f x) = univ

Tactic:
simp only [hsU, eq_univ_iff_forall, mem_iUnion]

Result:
case intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
s : Set α
hsc : s.Countable
hsU : ⋃ i ∈ s, interior (f i) = ⋃ i, interior (f i)
⊢ ∀ (x : α), ∃ i, x ∈ interior (f i)

Proof state:
case intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
s : Set α
hsc : s.Countable
hsU : ⋃ i ∈ s, interior (f i) = ⋃ i, interior (f i)
⊢ ∀ (x : α), ∃ i, x ∈ interior (f i)

Tactic:
exact fun x => ⟨x, mem_interior_iff_mem_nhds.2 (hf x)⟩

Result:
no goals