harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Prod.lean
theorem offDiag_union (h : Disjoint s t) :
    (s ∪ t).offDiag = s.offDiag ∪ t.offDiag ∪ s ×ˢ t ∪ t ×ˢ s :=
  coe_injective <| by
    push_cast
    exact Set.offDiag_union (disjoint_coe.2 h)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : Disjoint s t
⊢ ↑(s ∪ t).offDiag = ↑(s.offDiag ∪ t.offDiag ∪ s ×ˢ t ∪ t ×ˢ s)

Tactic:
push_cast

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : Disjoint s t
⊢ (↑s ∪ ↑t).offDiag = (↑s).offDiag ∪ (↑t).offDiag ∪ ↑s ×ˢ ↑t ∪ ↑t ×ˢ ↑s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : Disjoint s t
⊢ (↑s ∪ ↑t).offDiag = (↑s).offDiag ∪ (↑t).offDiag ∪ ↑s ×ˢ ↑t ∪ ↑t ×ˢ ↑s

Tactic:
exact Set.offDiag_union (disjoint_coe.2 h)

Result:
no goals
-- Mathlib/Topology/Compactification/OnePoint.lean
theorem nhds_infty_eq : 𝓝 (∞ : OnePoint X) = map (↑) (coclosedCompact X) ⊔ pure ∞

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ 𝓝 ∞ = map some (coclosedCompact X) ⊔ pure ∞

Tactic:
rw [← nhdsWithin_compl_infty_eq, nhdsWithin_compl_singleton_sup_pure]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem set_comm (a b : α)
    {i j : Nat} (as : Array α) {hi : i < as.size} {hj : j < (as.set i a).size} (h : i ≠ j) :
    (as.set i a).set j b = (as.set j b (by simpa using hj)).set i a (by simpa using hi)

Proof state:
α : Type u_1
a b : α
i j : Nat
as : Array α
hi : i < as.size
hj : j < (as.set i a hi).size
h : i ≠ j
⊢ (as.set i a hi).set j b hj = (as.set j b ⋯).set i a ⋯

Tactic:
cases as

Result:
case mk
α : Type u_1
a b : α
i j : Nat
h : i ≠ j
toList✝ : List α
hi : i < { toList := toList✝ }.size
hj : j < ({ toList := toList✝ }.set i a hi).size
⊢ ({ toList := toList✝ }.set i a hi).set j b hj = ({ toList := toList✝ }.set j b ⋯).set i a ⋯

Proof state:
α : Type ?u.126148
a b : α
i j : Nat
as : Array α
hi : i < as.size
hj : j < (as.set i a hi).size
h : i ≠ j
⊢ j < as.size

Tactic:
simpa using hj

Result:
no goals

Proof state:
α : Type ?u.126148
a b : α
i j : Nat
as : Array α
hi : i < as.size
hj : j < (as.set i a hi).size
h : i ≠ j
⊢ i < (as.set j b ⋯).size

Tactic:
simpa using hi

Result:
no goals

Proof state:
case mk
α : Type u_1
a b : α
i j : Nat
h : i ≠ j
toList✝ : List α
hi : i < { toList := toList✝ }.size
hj : j < ({ toList := toList✝ }.set i a hi).size
⊢ ({ toList := toList✝ }.set i a hi).set j b hj = ({ toList := toList✝ }.set j b ⋯).set i a ⋯

Tactic:
simp [List.set_comm _ _ _ h]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive zsmul_zero, simp]
lemma one_zpow : ∀ n : ℤ, (1 : α) ^ n = 1
  | (n : ℕ)    => by rw [zpow_natCast, one_pow]
  | .negSucc n => by rw [zpow_negSucc, one_pow, inv_one]

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
n : ℕ
⊢ 1 ^ Int.negSucc n = 1

Tactic:
rw [zpow_negSucc, one_pow, inv_one]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
n : ℕ
⊢ 1 ^ ↑n = 1

Tactic:
rw [zpow_natCast, one_pow]

Result:
no goals
-- Mathlib/Order/CompleteBooleanAlgebra.lean
lemma inf_iSup_eq (a : α) (f : ι → α) : (a ⊓ ⨆ i, f i) = ⨆ i, a ⊓ f i

Proof state:
α : Type u
ι : Sort w
minAx : MinimalAxioms α
a : α
f : ι → α
⊢ a ⊓ ⨆ i, f i = ⨆ i, a ⊓ f i

Tactic:
simpa only [inf_comm] using minAx.iSup_inf_eq f a

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem extractLsb'_or {x y : BitVec w} {start len : Nat} :
   (x ||| y).extractLsb' start len = (x.extractLsb' start len) ||| (y.extractLsb' start len)

Proof state:
w : Nat
x y : BitVec w
start len : Nat
⊢ extractLsb' start len (x ||| y) = extractLsb' start len x ||| extractLsb' start len y

Tactic:
ext i hi

Result:
case pred
w : Nat
x y : BitVec w
start len i : Nat
hi : i < len
⊢ (extractLsb' start len (x ||| y)).getLsbD i = (extractLsb' start len x ||| extractLsb' start len y).getLsbD i

Proof state:
case pred
w : Nat
x y : BitVec w
start len i : Nat
hi : i < len
⊢ (extractLsb' start len (x ||| y)).getLsbD i = (extractLsb' start len x ||| extractLsb' start len y).getLsbD i

Tactic:
simp [hi]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/ZMod.lean
lemma completedLFunction_def_odd (hΦ : Φ.Odd) (s : ℂ) :
    completedLFunction Φ s = N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaOdd (toAddCircle j) s

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
⊢ completedLFunction Φ s = ↑N ^ (-s) * ∑ j : ZMod N, Φ j * completedHurwitzZetaOdd (toAddCircle j) s

Tactic:
suffices ∑ j, Φ j * completedHurwitzZetaEven (toAddCircle j) s = 0 by
  rw [completedLFunction, this, mul_zero, zero_add]

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
⊢ ∑ j : ZMod N, Φ j * completedHurwitzZetaEven (toAddCircle j) s = 0

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
this : ∑ j : ZMod N, Φ j * completedHurwitzZetaEven (toAddCircle j) s = 0
⊢ completedLFunction Φ s = ↑N ^ (-s) * ∑ j : ZMod N, Φ j * completedHurwitzZetaOdd (toAddCircle j) s

Tactic:
rw [completedLFunction, this, mul_zero, zero_add]

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
⊢ ∑ j : ZMod N, Φ j * completedHurwitzZetaEven (toAddCircle j) s = 0

Tactic:
refine (hΦ.mul_even fun j ↦ ?_).sum_eq_zero

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
j : ZMod N
⊢ completedHurwitzZetaEven (toAddCircle (-j)) s = completedHurwitzZetaEven (toAddCircle j) s

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
j : ZMod N
⊢ completedHurwitzZetaEven (toAddCircle (-j)) s = completedHurwitzZetaEven (toAddCircle j) s

Tactic:
rw [map_neg, completedHurwitzZetaEven_neg]

Result:
no goals
-- Mathlib/Data/Matrix/Basis.lean
theorem mem_range_scalar_iff_commute_stdBasisMatrix' {M : Matrix n n α} :
    M ∈ Set.range (Matrix.scalar n) ↔ ∀ (i j : n), Commute (stdBasisMatrix i j 1) M

Proof state:
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
⊢ M ∈ Set.range ⇑(scalar n) ↔ ∀ (i j : n), Commute (stdBasisMatrix i j 1) M

Tactic:
refine ⟨fun ⟨r, hr⟩ i j => hr ▸ Commute.symm ?_,
  fun hM => mem_range_scalar_iff_commute_stdBasisMatrix.mpr <| fun i j _ => hM i j⟩

Result:
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
x✝ : M ∈ Set.range ⇑(scalar n)
i j : n
r : α
hr : (scalar n) r = M
⊢ Commute ((scalar n) r) (stdBasisMatrix i j 1)

Proof state:
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
x✝ : M ∈ Set.range ⇑(scalar n)
i j : n
r : α
hr : (scalar n) r = M
⊢ Commute ((scalar n) r) (stdBasisMatrix i j 1)

Tactic:
rw [scalar_commute_iff]

Result:
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
x✝ : M ∈ Set.range ⇑(scalar n)
i j : n
r : α
hr : (scalar n) r = M
⊢ r • stdBasisMatrix i j 1 = MulOpposite.op r • stdBasisMatrix i j 1

Proof state:
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
x✝ : M ∈ Set.range ⇑(scalar n)
i j : n
r : α
hr : (scalar n) r = M
⊢ r • stdBasisMatrix i j 1 = MulOpposite.op r • stdBasisMatrix i j 1

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/AddChar.lean
lemma _root_.MonoidHom.compAddChar_injective_left (ψ : AddChar A M) (hψ : Surjective ψ) :
    Injective fun f : M →* N ↦ f.compAddChar ψ

Proof state:
A : Type u_1
M : Type u_3
N : Type u_4
inst✝² : AddMonoid A
inst✝¹ : Monoid M
inst✝ : Monoid N
ψ : AddChar A M
hψ : Surjective ⇑ψ
f g : M →* N
h : ⇑((fun f => f.compAddChar ψ) f) = ⇑((fun f => f.compAddChar ψ) g)
⊢ ⇑f = ⇑g

Tactic:
exact hψ.injective_comp_right h

Result:
no goals

Proof state:
A : Type u_1
M : Type u_3
N : Type u_4
inst✝² : AddMonoid A
inst✝¹ : Monoid M
inst✝ : Monoid N
ψ : AddChar A M
hψ : Surjective ⇑ψ
f g : M →* N
h : (fun f => f.compAddChar ψ) f = (fun f => f.compAddChar ψ) g
⊢ f = g

Tactic:
rw [DFunLike.ext'_iff] at h ⊢

Result:
A : Type u_1
M : Type u_3
N : Type u_4
inst✝² : AddMonoid A
inst✝¹ : Monoid M
inst✝ : Monoid N
ψ : AddChar A M
hψ : Surjective ⇑ψ
f g : M →* N
h : ⇑((fun f => f.compAddChar ψ) f) = ⇑((fun f => f.compAddChar ψ) g)
⊢ ⇑f = ⇑g

Proof state:
A : Type u_1
M : Type u_3
N : Type u_4
inst✝² : AddMonoid A
inst✝¹ : Monoid M
inst✝ : Monoid N
ψ : AddChar A M
hψ : Surjective ⇑ψ
⊢ Injective fun f => f.compAddChar ψ

Tactic:
rintro f g h

Result:
A : Type u_1
M : Type u_3
N : Type u_4
inst✝² : AddMonoid A
inst✝¹ : Monoid M
inst✝ : Monoid N
ψ : AddChar A M
hψ : Surjective ⇑ψ
f g : M →* N
h : (fun f => f.compAddChar ψ) f = (fun f => f.compAddChar ψ) g
⊢ f = g
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem sub_eq_zero_iff_le {a b : Ordinal} : a - b = 0 ↔ a ≤ b :=
  ⟨fun h => by simpa only [h, add_zero] using le_add_sub a b, fun h => by
    rwa [← Ordinal.le_zero, sub_le, add_zero]⟩

Proof state:
a b : Ordinal.{u_4}
h : a ≤ b
⊢ a - b = 0

Tactic:
rwa [← Ordinal.le_zero, sub_le, add_zero]

Result:
no goals

Proof state:
a b : Ordinal.{u_4}
h : a - b = 0
⊢ a ≤ b

Tactic:
simpa only [h, add_zero] using le_add_sub a b

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
@[reassoc (attr := simp), elementwise (attr := simp)]
lemma toCocycles_comp_isoOneCocycles_hom :
    toCocycles A 0 1 ≫ (isoOneCocycles A).hom =
      (zeroCochainsLequiv A).toModuleIso.hom ≫
        ModuleCat.ofHom (shortComplexH1 A).moduleCatToCycles

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ toCocycles A 0 1 ≫ (isoOneCocycles A).hom =
    (zeroCochainsLequiv A).toModuleIso.hom ≫ ModuleCat.ofHom (shortComplexH1 A).moduleCatToCycles

Tactic:
simp [isoOneCocycles]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem three_le {α : Type*} (h : 3 ≤ #α) (x : α) (y : α) : ∃ z : α, z ≠ x ∧ z ≠ y

Proof state:
α : Type u_1
h : 3 ≤ #α
x y : α
this : ↑3 ≤ #α
⊢ ↑2 < #α

Tactic:
rwa [← succ_le_iff, ← Cardinal.nat_succ]

Result:
no goals

Proof state:
α : Type u_1
h : 3 ≤ #α
x y : α
this : ↑3 ≤ #α
⊢ ∃ z, z ≠ x ∧ z ≠ y

Tactic:
have : ↑(2 : ℕ) < #α := by rwa [← succ_le_iff, ← Cardinal.nat_succ]

Result:
α : Type u_1
h : 3 ≤ #α
x y : α
this✝ : ↑3 ≤ #α
this : ↑2 < #α
⊢ ∃ z, z ≠ x ∧ z ≠ y

Proof state:
α : Type u_1
h : 3 ≤ #α
x y : α
this✝¹ : ↑3 ≤ #α
this✝ : ↑2 < #α
this : ∃ z, z ∉ [x, y]
⊢ ∃ z, z ≠ x ∧ z ≠ y

Tactic:
simpa [not_or] using this

Result:
no goals

Proof state:
α : Type u_1
h : 3 ≤ #α
x y : α
⊢ ∃ z, z ≠ x ∧ z ≠ y

Tactic:
have : ↑(3 : ℕ) ≤ #α := by simpa using h

Result:
α : Type u_1
h : 3 ≤ #α
x y : α
this : ↑3 ≤ #α
⊢ ∃ z, z ≠ x ∧ z ≠ y

Proof state:
α : Type u_1
h : 3 ≤ #α
x y : α
this✝ : ↑3 ≤ #α
this : ↑2 < #α
⊢ ∃ z, z ≠ x ∧ z ≠ y

Tactic:
have := exists_not_mem_of_length_lt [x, y] this

Result:
α : Type u_1
h : 3 ≤ #α
x y : α
this✝¹ : ↑3 ≤ #α
this✝ : ↑2 < #α
this : ∃ z, z ∉ [x, y]
⊢ ∃ z, z ≠ x ∧ z ≠ y

Proof state:
α : Type u_1
h : 3 ≤ #α
x y : α
⊢ ↑3 ≤ #α

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Geometry/Euclidean/MongePoint.lean
theorem affineSpan_of_orthocentricSystem {s : Set P} (ho : OrthocentricSystem s) {p : Fin 3 → P}
    (hps : Set.range p ⊆ s) (hpi : Function.Injective p) :
    affineSpan ℝ (Set.range p) = affineSpan ℝ s

Proof state:
case intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
ha : AffineIndependent ℝ p
t : Triangle ℝ P
left✝ : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
hs : affineSpan ℝ s = affineSpan ℝ (Set.range t.points)
hfd this : FiniteDimensional ℝ ↥(affineSpan ℝ s).direction
⊢ (affineSpan ℝ (Set.range p)).direction = (affineSpan ℝ s).direction

Tactic:
refine Submodule.eq_of_le_of_finrank_eq (direction_le (affineSpan_mono ℝ hps)) ?_

Result:
case intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
ha : AffineIndependent ℝ p
t : Triangle ℝ P
left✝ : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
hs : affineSpan ℝ s = affineSpan ℝ (Set.range t.points)
hfd this : FiniteDimensional ℝ ↥(affineSpan ℝ s).direction
⊢ finrank ℝ ↥(affineSpan ℝ (Set.range p)).direction = finrank ℝ ↥(affineSpan ℝ s).direction

Proof state:
case intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
ha : AffineIndependent ℝ p
t : Triangle ℝ P
left✝ : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
hs : affineSpan ℝ s = affineSpan ℝ (Set.range t.points)
⊢ affineSpan ℝ (Set.range p) = affineSpan ℝ s

Tactic:
refine ext_of_direction_eq ?_
  ⟨p 0, mem_affineSpan ℝ (Set.mem_range_self _), mem_affineSpan ℝ (hps (Set.mem_range_self _))⟩

Result:
case intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
ha : AffineIndependent ℝ p
t : Triangle ℝ P
left✝ : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
hs : affineSpan ℝ s = affineSpan ℝ (Set.range t.points)
⊢ (affineSpan ℝ (Set.range p)).direction = (affineSpan ℝ s).direction
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/PullbackCone.lean
theorem condition_one (t : PullbackCone f g) : t.π.app WalkingCospan.one = t.fst ≫ f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
⊢ t.π.app WalkingCospan.one = t.fst ≫ f

Tactic:
have w := t.π.naturality WalkingCospan.Hom.inl

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
w :
  ((Functor.const WalkingCospan).obj t.pt).map inl ≫ t.π.app WalkingCospan.one =
    t.π.app WalkingCospan.left ≫ (cospan f g).map inl
⊢ t.π.app WalkingCospan.one = t.fst ≫ f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
w :
  ((Functor.const WalkingCospan).obj t.pt).map inl ≫ t.π.app WalkingCospan.one =
    t.π.app WalkingCospan.left ≫ (cospan f g).map inl
⊢ t.π.app WalkingCospan.one = t.fst ≫ f

Tactic:
dsimp at w

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
w : 𝟙 t.pt ≫ t.π.app WalkingCospan.one = t.fst ≫ f
⊢ t.π.app WalkingCospan.one = t.fst ≫ f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
w : 𝟙 t.pt ≫ t.π.app WalkingCospan.one = t.fst ≫ f
⊢ t.π.app WalkingCospan.one = t.fst ≫ f

Tactic:
simpa using w

Result:
no goals
-- Mathlib/Topology/Instances/Int.lean
theorem dist_eq' (m n : ℤ) : dist m n = |m - n|

Proof state:
m n : ℤ
⊢ dist m n = ↑|m - n|

Tactic:
rw [dist_eq]

Result:
m n : ℤ
⊢ |↑m - ↑n| = ↑|m - n|

Proof state:
m n : ℤ
⊢ |↑m - ↑n| = ↑|m - n|

Tactic:
norm_cast

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
/-- The `n`-th coefficient of the `k`-th power of a power series. -/
lemma coeff_pow (k n : ℕ) (φ : R⟦X⟧) :
    coeff R n (φ ^ k) = ∑ l ∈ finsuppAntidiag (range k) n, ∏ i ∈ range k, coeff R (l i) φ

Proof state:
R : Type u_2
inst✝ : CommSemiring R
k n : ℕ
φ : R⟦X⟧
⊢ (coeff R n) (φ ^ k) = ∑ l ∈ (range k).finsuppAntidiag n, ∏ i ∈ range k, (coeff R (l i)) φ

Tactic:
have h₁ (i : ℕ) : Function.const ℕ φ i = φ := rfl

Result:
R : Type u_2
inst✝ : CommSemiring R
k n : ℕ
φ : R⟦X⟧
h₁ : ∀ (i : ℕ), Function.const ℕ φ i = φ
⊢ (coeff R n) (φ ^ k) = ∑ l ∈ (range k).finsuppAntidiag n, ∏ i ∈ range k, (coeff R (l i)) φ

Proof state:
R : Type u_2
inst✝ : CommSemiring R
k n : ℕ
φ : R⟦X⟧
h₁ : ∀ (i : ℕ), Function.const ℕ φ i = φ
h₂ : ∀ (i : ℕ), ∏ j ∈ range i, Function.const ℕ φ j = φ ^ i
⊢ (coeff R n) (∏ j ∈ range k, Function.const ℕ (Function.const ℕ φ k) j) =
    ∑ l ∈ (range k).finsuppAntidiag n, ∏ i ∈ range k, (coeff R (l i)) (Function.const ℕ φ k)

Tactic:
apply coeff_prod (f := Function.const ℕ φ) (d := n) (s := range k)

Result:
no goals

Proof state:
R : Type u_2
inst✝ : CommSemiring R
k n : ℕ
φ : R⟦X⟧
h₁ : ∀ (i : ℕ), Function.const ℕ φ i = φ
h₂ : ∀ (i : ℕ), ∏ j ∈ range i, Function.const ℕ φ j = φ ^ i
⊢ (coeff R n) (φ ^ k) = ∑ l ∈ (range k).finsuppAntidiag n, ∏ i ∈ range k, (coeff R (l i)) φ

Tactic:
rw [← h₂, ← h₁ k]

Result:
R : Type u_2
inst✝ : CommSemiring R
k n : ℕ
φ : R⟦X⟧
h₁ : ∀ (i : ℕ), Function.const ℕ φ i = φ
h₂ : ∀ (i : ℕ), ∏ j ∈ range i, Function.const ℕ φ j = φ ^ i
⊢ (coeff R n) (∏ j ∈ range k, Function.const ℕ (Function.const ℕ φ k) j) =
    ∑ l ∈ (range k).finsuppAntidiag n, ∏ i ∈ range k, (coeff R (l i)) (Function.const ℕ φ k)

Proof state:
R : Type u_2
inst✝ : CommSemiring R
k n : ℕ
φ : R⟦X⟧
h₁ : ∀ (i : ℕ), Function.const ℕ φ i = φ
i : ℕ
⊢ ∏ j ∈ range i, Function.const ℕ φ j = φ ^ i

Tactic:
apply prod_range_induction (fun _ => φ) (fun i => φ ^ i) rfl (congrFun rfl) i

Result:
no goals

Proof state:
R : Type u_2
inst✝ : CommSemiring R
k n : ℕ
φ : R⟦X⟧
h₁ : ∀ (i : ℕ), Function.const ℕ φ i = φ
⊢ (coeff R n) (φ ^ k) = ∑ l ∈ (range k).finsuppAntidiag n, ∏ i ∈ range k, (coeff R (l i)) φ

Tactic:
have h₂ (i : ℕ) : ∏ j ∈ range i, Function.const ℕ φ j = φ ^ i := by
  apply prod_range_induction (fun _ => φ) (fun i => φ ^ i) rfl (congrFun rfl) i

Result:
R : Type u_2
inst✝ : CommSemiring R
k n : ℕ
φ : R⟦X⟧
h₁ : ∀ (i : ℕ), Function.const ℕ φ i = φ
h₂ : ∀ (i : ℕ), ∏ j ∈ range i, Function.const ℕ φ j = φ ^ i
⊢ (coeff R n) (φ ^ k) = ∑ l ∈ (range k).finsuppAntidiag n, ∏ i ∈ range k, (coeff R (l i)) φ
-- Mathlib/Data/List/Flatten.lean
theorem drop_take_succ_flatten_eq_getElem' (L : List (List α)) (i : Nat) (h : i <  L.length) :
    (L.flatten.take (Nat.sum ((L.map length).take (i + 1)))).drop
      (Nat.sum ((L.map length).take i)) = L[i]

Proof state:
α : Type u_1
L : List (List α)
i : ℕ
h : i < L.length
⊢ drop (Nat.sum (take i (map length L))) (take (Nat.sum (take (i + 1) (map length L))) L.flatten) = L[i]

Tactic:
have : (L.map length).take i = ((L.take (i + 1)).map length).take i := by
  simp [map_take, take_take, Nat.min_eq_left]

Result:
α : Type u_1
L : List (List α)
i : ℕ
h : i < L.length
this : take i (map length L) = take i (map length (take (i + 1) L))
⊢ drop (Nat.sum (take i (map length L))) (take (Nat.sum (take (i + 1) (map length L))) L.flatten) = L[i]

Proof state:
α : Type u_1
L : List (List α)
i : ℕ
h : i < L.length
this : take i (map length L) = take i (map length (take (i + 1) L))
⊢ drop (Nat.sum (take i (map length L))) (take (Nat.sum (take (i + 1) (map length L))) L.flatten) = L[i]

Tactic:
simp only [this, length_map, take_sum_flatten', drop_sum_flatten',
  drop_take_succ_eq_cons_getElem, h, flatten, append_nil]

Result:
no goals

Proof state:
α : Type u_1
L : List (List α)
i : ℕ
h : i < L.length
⊢ take i (map length L) = take i (map length (take (i + 1) L))

Tactic:
simp [map_take, take_take, Nat.min_eq_left]

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/Defs.lean
theorem of_comp (f : A →ₐ[R] A') (hfv : AlgebraicIndependent R (f ∘ x)) :
    AlgebraicIndependent R x

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
A' : Type u_6
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hfv : Injective (⇑f ∘ ⇑(aeval x))
this : aeval (⇑f ∘ x) = f.comp (aeval x)
⊢ AlgebraicIndependent R x

Tactic:
exact hfv.of_comp

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
A' : Type u_6
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hfv : AlgebraicIndependent R (⇑f ∘ x)
⊢ aeval (⇑f ∘ x) = f.comp (aeval x)

Tactic:
ext

Result:
case hf
ι : Type u_1
R : Type u_3
A : Type u_5
A' : Type u_6
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hfv : AlgebraicIndependent R (⇑f ∘ x)
i✝ : ι
⊢ (aeval (⇑f ∘ x)) (X i✝) = (f.comp (aeval x)) (X i✝)

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
A' : Type u_6
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hfv : AlgebraicIndependent R (⇑f ∘ x)
⊢ AlgebraicIndependent R x

Tactic:
have : aeval (f ∘ x) = f.comp (aeval x) := by ext; simp

Result:
ι : Type u_1
R : Type u_3
A : Type u_5
A' : Type u_6
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hfv : AlgebraicIndependent R (⇑f ∘ x)
this : aeval (⇑f ∘ x) = f.comp (aeval x)
⊢ AlgebraicIndependent R x

Proof state:
case hf
ι : Type u_1
R : Type u_3
A : Type u_5
A' : Type u_6
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hfv : AlgebraicIndependent R (⇑f ∘ x)
i✝ : ι
⊢ (aeval (⇑f ∘ x)) (X i✝) = (f.comp (aeval x)) (X i✝)

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
A' : Type u_6
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hfv : AlgebraicIndependent R (⇑f ∘ x)
this : aeval (⇑f ∘ x) = f.comp (aeval x)
⊢ AlgebraicIndependent R x

Tactic:
rw [AlgebraicIndependent, this, AlgHom.coe_comp] at hfv

Result:
ι : Type u_1
R : Type u_3
A : Type u_5
A' : Type u_6
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hfv : Injective (⇑f ∘ ⇑(aeval x))
this : aeval (⇑f ∘ x) = f.comp (aeval x)
⊢ AlgebraicIndependent R x
-- Mathlib/Data/DFinsupp/Defs.lean
theorem extendWith_zero [DecidableEq ι] [∀ i, Zero (α i)] (x : α none) :
    (0 : Π₀ i, α (some i)).extendWith x = single none x

Proof state:
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
x : α none
⊢ extendWith x 0 = single none x

Tactic:
ext (_ | j)

Result:
case h.none
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
x : α none
⊢ (extendWith x 0) none = (single none x) none

case h.some
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
x : α none
j : ι
⊢ (extendWith x 0) (some j) = (single none x) (some j)

Proof state:
case h.none
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
x : α none
⊢ (extendWith x 0) none = (single none x) none

Tactic:
rw [extendWith_none, single_eq_same]

Result:
no goals

Proof state:
case h.some
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
x : α none
j : ι
⊢ (extendWith x 0) (some j) = (single none x) (some j)

Tactic:
rw [extendWith_some, single_eq_of_ne (Option.some_ne_none _).symm, zero_apply]

Result:
no goals