harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Fold.lean
theorem all_eq_finRange_all {n : Nat} (f : (i : Nat) → i < n → Bool) :
    all n f = (List.finRange n).all (fun ⟨i, h⟩ => f i h)

Proof state:
case zero
f : (i : Nat) → i < 0 → Bool
⊢ all 0 f =
    (List.finRange 0).all fun x =>
      match x with
      | ⟨i, h⟩ => f i h

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
f : (i : Nat) → i < n → Bool
⊢ n.all f =
    (List.finRange n).all fun x =>
      match x with
      | ⟨i, h⟩ => f i h

Tactic:
induction n with
| zero => simp
| succ n ih => simp [ih, List.finRange_succ_last, List.all_map, Function.comp_def]

Result:
no goals

Proof state:
case succ
n : Nat
ih :
  ∀ (f : (i : Nat) → i < n → Bool),
    n.all f =
      (List.finRange n).all fun x =>
        match x with
        | ⟨i, h⟩ => f i h
f : (i : Nat) → i < n + 1 → Bool
⊢ (n + 1).all f =
    (List.finRange (n + 1)).all fun x =>
      match x with
      | ⟨i, h⟩ => f i h

Tactic:
simp [ih, List.finRange_succ_last, List.all_map, Function.comp_def]

Result:
no goals
-- Mathlib/Algebra/Order/Antidiag/Finsupp.lean
lemma mem_finsuppAntidiag' :
    f ∈ finsuppAntidiag s n ↔ f.sum (fun _ x ↦ x) = n ∧ f.support ⊆ s

Proof state:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι →₀ μ
⊢ f ∈ s.finsuppAntidiag n ↔ (f.sum fun x x => x) = n ∧ f.support ⊆ s

Tactic:
simp only [mem_finsuppAntidiag, and_congr_left_iff]

Result:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι →₀ μ
⊢ f.support ⊆ s → (s.sum ⇑f = n ↔ (f.sum fun x x => x) = n)

Proof state:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι →₀ μ
⊢ f.support ⊆ s → (s.sum ⇑f = n ↔ (f.sum fun x x => x) = n)

Tactic:
rintro hf

Result:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι →₀ μ
hf : f.support ⊆ s
⊢ s.sum ⇑f = n ↔ (f.sum fun x x => x) = n

Proof state:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι →₀ μ
hf : f.support ⊆ s
⊢ s.sum ⇑f = n ↔ (f.sum fun x x => x) = n

Tactic:
rw [sum_of_support_subset (N := μ) f hf (fun _ x ↦ x) fun _ _ ↦ rfl]

Result:
no goals
-- Mathlib/RingTheory/Noetherian/Basic.lean
theorem LinearIndependent.finite_of_isNoetherian [Nontrivial R] {ι} {v : ι → M}
    (hv : LinearIndependent R v) : Finite ι

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : IsNoetherian R M
inst✝ : Nontrivial R
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
⊢ Finite ι

Tactic:
refine WellFoundedGT.finite_of_iSupIndep
  hv.iSupIndep_span_singleton
  fun i contra => ?_

Result:
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : IsNoetherian R M
inst✝ : Nontrivial R
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
i : ι
contra : span R {v i} = ⊥
⊢ False

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : IsNoetherian R M
inst✝ : Nontrivial R
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
i : ι
contra : span R {v i} = ⊥
this : v i ∈ span R {v i}
⊢ v i = 0

Tactic:
rwa [contra, Submodule.mem_bot] at this

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : IsNoetherian R M
inst✝ : Nontrivial R
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
i : ι
contra : span R {v i} = ⊥
⊢ v i = 0

Tactic:
have : v i ∈ R ∙ v i := Submodule.mem_span_singleton_self (v i)

Result:
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : IsNoetherian R M
inst✝ : Nontrivial R
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
i : ι
contra : span R {v i} = ⊥
this : v i ∈ span R {v i}
⊢ v i = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : IsNoetherian R M
inst✝ : Nontrivial R
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
i : ι
contra : span R {v i} = ⊥
⊢ False

Tactic:
apply hv.ne_zero i

Result:
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : IsNoetherian R M
inst✝ : Nontrivial R
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
i : ι
contra : span R {v i} = ⊥
⊢ v i = 0
-- Mathlib/Data/List/Basic.lean
theorem Forall.imp (h : ∀ x, p x → q x) : ∀ {l : List α}, Forall p l → Forall q l
  | [] => id
  | x :: l => by
    simp only [forall_cons, and_imp]
    rw [← and_imp]
    exact And.imp (h x) (Forall.imp h)

Proof state:
α : Type u
p q : α → Prop
h : ∀ (x : α), p x → q x
x : α
l : List α
⊢ p x ∧ Forall p l → q x ∧ Forall q l

Tactic:
exact And.imp (h x) (Forall.imp h)

Result:
no goals

Proof state:
α : Type u
p q : α → Prop
h : ∀ (x : α), p x → q x
x : α
l : List α
⊢ p x → Forall p l → q x ∧ Forall q l

Tactic:
rw [← and_imp]

Result:
α : Type u
p q : α → Prop
h : ∀ (x : α), p x → q x
x : α
l : List α
⊢ p x ∧ Forall p l → q x ∧ Forall q l

Proof state:
α : Type u
p q : α → Prop
h : ∀ (x : α), p x → q x
x : α
l : List α
⊢ Forall p (x :: l) → Forall q (x :: l)

Tactic:
simp only [forall_cons, and_imp]

Result:
α : Type u
p q : α → Prop
h : ∀ (x : α), p x → q x
x : α
l : List α
⊢ p x → Forall p l → q x ∧ Forall q l
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem aleph0_le {c : Cardinal} : ℵ₀ ≤ c ↔ ∀ n : ℕ, ↑n ≤ c :=
  ⟨fun h _ => (nat_lt_aleph0 _).le.trans h, fun h =>
    le_of_not_lt fun hn => by
      rcases lt_aleph0.1 hn with ⟨n, rfl⟩
      exact (Nat.lt_succ_self _).not_le (Nat.cast_le.1 (h (n + 1)))⟩

Proof state:
case intro
n : ℕ
h : ∀ (n_1 : ℕ), ↑n_1 ≤ ↑n
hn : ↑n < ℵ₀
⊢ False

Tactic:
exact (Nat.lt_succ_self _).not_le (Nat.cast_le.1 (h (n + 1)))

Result:
no goals

Proof state:
c : Cardinal.{u_1}
h : ∀ (n : ℕ), ↑n ≤ c
hn : c < ℵ₀
⊢ False

Tactic:
rcases lt_aleph0.1 hn with ⟨n, rfl⟩

Result:
case intro
n : ℕ
h : ∀ (n_1 : ℕ), ↑n_1 ≤ ↑n
hn : ↑n < ℵ₀
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem one_sub : ∀ n, 1 - n = if n = 0 then 1 else 0
  | 0 => rfl
  | _+1 => by rw [if_neg (Nat.succ_ne_zero _), Nat.succ_sub_succ, Nat.zero_sub]

Proof state:
n✝ : Nat
⊢ 1 - (n✝ + 1) = if n✝ + 1 = 0 then 1 else 0

Tactic:
rw [if_neg (Nat.succ_ne_zero _), Nat.succ_sub_succ, Nat.zero_sub]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem suffix_cons_iff : l₁ <:+ a :: l₂ ↔ l₁ = a :: l₂ ∨ l₁ <:+ l₂

Proof state:
case mpr.inl
α✝ : Type u_1
a : α✝
l₂ : List α✝
⊢ a :: l₂ <:+ a :: l₂

Tactic:
exact (a :: l₂).suffix_refl

Result:
no goals

Proof state:
case mpr.inr
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
hl₁ : l₁ <:+ l₂
⊢ l₁ <:+ a :: l₂

Tactic:
exact hl₁.trans (l₂.suffix_cons _)

Result:
no goals

Proof state:
case mpr
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
⊢ l₁ = a :: l₂ ∨ l₁ <:+ l₂ → l₁ <:+ a :: l₂

Tactic:
rintro (rfl | hl₁)

Result:
case mpr.inl
α✝ : Type u_1
a : α✝
l₂ : List α✝
⊢ a :: l₂ <:+ a :: l₂

case mpr.inr
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
hl₁ : l₁ <:+ l₂
⊢ l₁ <:+ a :: l₂

Proof state:
case mp.intro.cons
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
head✝ : α✝
tail✝ : List α✝
hl₃ : head✝ :: (tail✝ ++ l₁) = a :: l₂
⊢ l₁ = a :: l₂ ∨ l₁ <:+ l₂

Tactic:
injection hl₃ with _ hl₄

Result:
case mp.intro.cons
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
head✝ : α✝
tail✝ : List α✝
head_eq✝ : head✝ = a
hl₄ : tail✝ ++ l₁ = l₂
⊢ l₁ = a :: l₂ ∨ l₁ <:+ l₂

Proof state:
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
⊢ l₁ <:+ a :: l₂ ↔ l₁ = a :: l₂ ∨ l₁ <:+ l₂

Tactic:
constructor

Result:
case mp
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
⊢ l₁ <:+ a :: l₂ → l₁ = a :: l₂ ∨ l₁ <:+ l₂

case mpr
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
⊢ l₁ = a :: l₂ ∨ l₁ <:+ l₂ → l₁ <:+ a :: l₂

Proof state:
case mp.intro.cons
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
head✝ : α✝
tail✝ : List α✝
head_eq✝ : head✝ = a
hl₄ : tail✝ ++ l₁ = l₂
⊢ l₁ = a :: l₂ ∨ l₁ <:+ l₂

Tactic:
exact Or.inr ⟨_, hl₄⟩

Result:
no goals

Proof state:
case mp.intro.nil
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
hl₃ : [] ++ l₁ = a :: l₂
⊢ l₁ = a :: l₂ ∨ l₁ <:+ l₂

Tactic:
exact Or.inl hl₃

Result:
no goals

Proof state:
case mp
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
⊢ l₁ <:+ a :: l₂ → l₁ = a :: l₂ ∨ l₁ <:+ l₂

Tactic:
rintro ⟨⟨hd, tl⟩, hl₃⟩

Result:
case mp.intro.nil
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
hl₃ : [] ++ l₁ = a :: l₂
⊢ l₁ = a :: l₂ ∨ l₁ <:+ l₂

case mp.intro.cons
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
head✝ : α✝
tail✝ : List α✝
hl₃ : head✝ :: tail✝ ++ l₁ = a :: l₂
⊢ l₁ = a :: l₂ ∨ l₁ <:+ l₂

Proof state:
case mp.intro.cons
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
head✝ : α✝
tail✝ : List α✝
hl₃ : head✝ :: tail✝ ++ l₁ = a :: l₂
⊢ l₁ = a :: l₂ ∨ l₁ <:+ l₂

Tactic:
simp only [cons_append] at hl₃

Result:
case mp.intro.cons
α✝ : Type u_1
l₁ : List α✝
a : α✝
l₂ : List α✝
head✝ : α✝
tail✝ : List α✝
hl₃ : head✝ :: (tail✝ ++ l₁) = a :: l₂
⊢ l₁ = a :: l₂ ∨ l₁ <:+ l₂
-- Mathlib/Data/Multiset/Fintype.lean
theorem toEmbedding_coeEquiv_trans (m : Multiset α) :
    m.coeEquiv.toEmbedding.trans (Function.Embedding.subtype _) = m.coeEmbedding

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ m.coeEquiv.toEmbedding.trans (Function.Embedding.subtype fun x => x ∈ m.toEnumFinset) = m.coeEmbedding

Tactic:
ext <;> rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
@[simp]
lemma map_b₆ : (W.map φ).b₆ = φ W.b₆

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ (W.map φ).b₆ = φ W.b₆

Tactic:
simp only [b₆, map_a₃, map_a₆]

Result:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ φ W.a₃ ^ 2 + 4 * φ W.a₆ = φ (W.a₃ ^ 2 + 4 * W.a₆)

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ φ W.a₃ ^ 2 + 4 * φ W.a₆ = φ (W.a₃ ^ 2 + 4 * W.a₆)

Tactic:
map_simp

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/AsPolynomial.lean
theorem valuation_of_mk (f : Polynomial K) {g : Polynomial K} (hg : g ≠ 0) :
    (Polynomial.idealX K).valuation _ (RatFunc.mk f g) =
      (Polynomial.idealX K).intValuation f / (Polynomial.idealX K).intValuation g

Proof state:
K : Type u_1
inst✝ : Field K
f g : K[X]
hg : g ≠ 0
⊢ (valuation (RatFunc K) (idealX K)) (RatFunc.mk f g) = (idealX K).intValuation f / (idealX K).intValuation g

Tactic:
simp only [RatFunc.mk_eq_mk' _ hg, valuation_of_mk']

Result:
no goals
-- Mathlib/Algebra/Lie/Solvable.lean
theorem derivedSeries_of_bot_eq_bot (k : ℕ) : derivedSeriesOfIdeal R L k ⊥ = ⊥

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
⊢ D k ⊥ = ⊥

Tactic:
rw [eq_bot_iff]

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
⊢ D k ⊥ ≤ ⊥

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
⊢ D k ⊥ ≤ ⊥

Tactic:
exact derivedSeriesOfIdeal_le_self ⊥ k

Result:
no goals
-- Mathlib/Data/Finmap.lean
theorem erase_union_singleton (a : α) (b : β a) (s : Finmap β) (h : s.lookup a = some b) :
    s.erase a ∪ singleton a b = s :=
  ext_lookup fun x => by
    by_cases h' : x = a
    · subst a
      rw [lookup_union_right not_mem_erase_self, lookup_singleton_eq, h]
    · have : x ∉ singleton a b

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
h' : ¬x = a
⊢ x ∉ singleton a b

Tactic:
rwa [mem_singleton]

Result:
no goals

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
h' : x = a
⊢ lookup x (erase a s ∪ singleton a b) = lookup x s

Tactic:
subst a

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finmap β
x : α
b : β x
h : lookup x s = some b
⊢ lookup x (erase x s ∪ singleton x b) = lookup x s

Proof state:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
h' : ¬x = a
this : x ∉ singleton a b
⊢ lookup x (erase a s ∪ singleton a b) = lookup x s

Tactic:
rw [lookup_union_left_of_not_in this, lookup_erase_ne h']

Result:
no goals

Proof state:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
h' : ¬x = a
⊢ lookup x (erase a s ∪ singleton a b) = lookup x s

Tactic:
have : x ∉ singleton a b := by rwa [mem_singleton]

Result:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
h' : ¬x = a
this : x ∉ singleton a b
⊢ lookup x (erase a s ∪ singleton a b) = lookup x s

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finmap β
x : α
b : β x
h : lookup x s = some b
⊢ lookup x (erase x s ∪ singleton x b) = lookup x s

Tactic:
rw [lookup_union_right not_mem_erase_self, lookup_singleton_eq, h]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
⊢ lookup x (erase a s ∪ singleton a b) = lookup x s

Tactic:
by_cases h' : x = a

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
h' : x = a
⊢ lookup x (erase a s ∪ singleton a b) = lookup x s

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
h' : ¬x = a
⊢ lookup x (erase a s ∪ singleton a b) = lookup x s
-- Mathlib/Algebra/Order/Antidiag/Pi.lean
lemma piAntidiag_cons (hi : i ∉ s) (n : μ) :
    piAntidiag (cons i s hi) n = (antidiagonal n).disjiUnion (fun p : μ × μ ↦
      (piAntidiag s p.snd).map (addRightEmbedding fun t ↦ if t = i then p.fst else 0))
        (pairwiseDisjoint_piAntidiag_map_addRightEmbedding hi _)

Proof state:
case h
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
f : ι → μ
⊢ (f i + ∑ x ∈ s, f x = n ∧ ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s) ↔
    ∃ a b,
      a + b = n ∧
        ∃ a_1,
          (s.sum a_1 = b ∧ ∀ (i : ι), ¬a_1 i = 0 → i ∈ s) ∧ (addRightEmbedding fun t => if t = i then a else 0) a_1 = f

Tactic:
constructor

Result:
case h.mp
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
f : ι → μ
⊢ (f i + ∑ x ∈ s, f x = n ∧ ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s) →
    ∃ a b,
      a + b = n ∧
        ∃ a_1,
          (s.sum a_1 = b ∧ ∀ (i : ι), ¬a_1 i = 0 → i ∈ s) ∧ (addRightEmbedding fun t => if t = i then a else 0) a_1 = f

case h.mpr
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
f : ι → μ
⊢ (∃ a b,
      a + b = n ∧
        ∃ a_1,
          (s.sum a_1 = b ∧ ∀ (i : ι), ¬a_1 i = 0 → i ∈ s) ∧
            (addRightEmbedding fun t => if t = i then a else 0) a_1 = f) →
    f i + ∑ x ∈ s, f x = n ∧ ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s

Proof state:
case h.mpr.intro.intro.intro.intro.intro.intro
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n a : μ
g : ι → μ
hg : ∀ (i : ι), ¬g i = 0 → i ∈ s
hn : a + s.sum g = n
⊢ (addRightEmbedding fun t => if t = i then a else 0) g i +
        ∑ x ∈ s, (addRightEmbedding fun t => if t = i then a else 0) g x =
      n ∧
    ∀ (i_1 : ι), ¬(addRightEmbedding fun t => if t = i then a else 0) g i_1 = 0 → i_1 = i ∨ i_1 ∈ s

Tactic:
have := hg i

Result:
case h.mpr.intro.intro.intro.intro.intro.intro
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n a : μ
g : ι → μ
hg : ∀ (i : ι), ¬g i = 0 → i ∈ s
hn : a + s.sum g = n
this : ¬g i = 0 → i ∈ s
⊢ (addRightEmbedding fun t => if t = i then a else 0) g i +
        ∑ x ∈ s, (addRightEmbedding fun t => if t = i then a else 0) g x =
      n ∧
    ∀ (i_1 : ι), ¬(addRightEmbedding fun t => if t = i then a else 0) g i_1 = 0 → i_1 = i ∨ i_1 ∈ s
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem sup_ker_aeval_eq_ker_aeval_mul_of_coprime (f : M →ₗ[R] M) {p q : R[X]}
    (hpq : IsCoprime p q) :
    LinearMap.ker (aeval f p) ⊔ LinearMap.ker (aeval f q) = LinearMap.ker (aeval f (p * q))

Proof state:
case intro.intro
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker ((aeval f) (p * q))
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ((aeval f) (q * (p * p'))) v = 0
h_eval₂_pqq' : ((aeval f) (p * (q * q'))) v = 0
⊢ ∃ y ∈ LinearMap.ker ((aeval f) p), ∃ z ∈ LinearMap.ker ((aeval f) q), y + z = v

Tactic:
rw [aeval_mul] at h_eval₂_qpp' h_eval₂_pqq'

Result:
case intro.intro
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker ((aeval f) (p * q))
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ((aeval f) q * (aeval f) (p * p')) v = 0
h_eval₂_pqq' : ((aeval f) p * (aeval f) (q * q')) v = 0
⊢ ∃ y ∈ LinearMap.ker ((aeval f) p), ∃ z ∈ LinearMap.ker ((aeval f) q), y + z = v

Proof state:
case intro.intro
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker ((aeval f) (p * q))
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ∃ y ∈ LinearMap.ker ((aeval f) p), ∃ z ∈ LinearMap.ker ((aeval f) q), y + z = v

Tactic:
have h_eval₂_qpp' :=
  calc
    aeval f (q * (p * p')) v = aeval f (p' * (p * q)) v := by
      rw [mul_comm, mul_assoc, mul_comm, mul_assoc, mul_comm q p]
    _ = 0 := by rw [aeval_mul, LinearMap.mul_apply, LinearMap.mem_ker.1 hv, LinearMap.map_zero]

Result:
case intro.intro
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker ((aeval f) (p * q))
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ((aeval f) (q * (p * p'))) v = 0
⊢ ∃ y ∈ LinearMap.ker ((aeval f) p), ∃ z ∈ LinearMap.ker ((aeval f) q), y + z = v
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem Perm.eq_of_sorted : ∀ {l₁ l₂ : List α}
    (_ : ∀ a b, a ∈ l₁ → b ∈ l₂ → le a b → le b a → a = b)
    (_ : l₁.Pairwise le) (_ : l₂.Pairwise le) (_ : l₁ ~ l₂), l₁ = l₂
  | [], [], _, _, _, _ => rfl
  | [], b :: l₂, _, _, _, h => by simp_all
  | a :: l₁, [], _, _, _, h => by simp_all
  | a :: l₁, b :: l₂, w, h₁, h₂, h => by
    have am : a ∈ b :: l₂ := h.subset (mem_cons_self _ _)
    have bm : b ∈ a :: l₁ := h.symm.subset (mem_cons_self _ _)
    have ab : a = b

Proof state:
α : Type u_1
le : α → α → Prop
a : α
l₁ l₂ : List α
h₁ : Pairwise le (a :: l₁)
w : ∀ (a_1 b : α), a_1 ∈ a :: l₁ → b ∈ a :: l₂ → le a_1 b → le b a_1 → a_1 = b
h₂ : Pairwise le (a :: l₂)
h : a :: l₁ ~ a :: l₂
am : a ∈ a :: l₂
bm : a ∈ a :: l₁
⊢ a :: l₁ = a :: l₂

Tactic:
simp only [perm_cons] at h

Result:
α : Type u_1
le : α → α → Prop
a : α
l₁ l₂ : List α
h₁ : Pairwise le (a :: l₁)
w : ∀ (a_1 b : α), a_1 ∈ a :: l₁ → b ∈ a :: l₂ → le a_1 b → le b a_1 → a_1 = b
h₂ : Pairwise le (a :: l₂)
am : a ∈ a :: l₂
bm : a ∈ a :: l₁
h : l₁ ~ l₂
⊢ a :: l₁ = a :: l₂
-- Mathlib/Data/Real/Pi/Wallis.lean
theorem W_eq_factorial_ratio (n : ℕ) :
    W n = 2 ^ (4 * n) * n ! ^ 4 / ((2 * n)! ^ 2 * (2 * n + 1))

Proof state:
case succ.refine_3
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ 2 ^ (4 * n) * (↑n ! ^ 0 * ↑n ! * ↑n ! * ↑n ! * ↑n !) * ((2 * ↑n + 2) * (2 * ↑n + 2)) *
      (((2 * ↑n + 1 + 1) * ((2 * ↑n + 1) * ↑(2 * n)!)) ^ 0 * ((2 * ↑n + 1 + 1) * ((2 * ↑n + 1) * ↑(2 * n)!)) *
          ((2 * ↑n + 1 + 1) * ((2 * ↑n + 1) * ↑(2 * n)!)) *
        (2 * (↑n + 1) + 1)) =
    2 ^ (4 * n) * 2 * 2 * 2 * 2 *
        (((↑n + 1) * ↑n !) ^ 0 * ((↑n + 1) * ↑n !) * ((↑n + 1) * ↑n !) * ((↑n + 1) * ↑n !) * ((↑n + 1) * ↑n !)) *
      (↑(2 * n)! ^ 0 * ↑(2 * n)! * ↑(2 * n)! * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3)))

Tactic:
ring_nf

Result:
no goals

Proof state:
n : ℕ
⊢ W n = 2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))

Tactic:
induction' n with n IH

Result:
case zero

⊢ W 0 = 2 ^ (4 * 0) * ↑0! ^ 4 / (↑(2 * 0)! ^ 2 * (2 * ↑0 + 1))

case succ
n : ℕ
IH : W n = 2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ W (n + 1) = 2 ^ (4 * (n + 1)) * ↑(n + 1)! ^ 4 / (↑(2 * (n + 1))! ^ 2 * (2 * ↑(n + 1) + 1))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem pow_lt_pow_succ (h : 1 < a) : a ^ n < a ^ (n + 1)

Proof state:
a n : Nat
h : 1 < a
⊢ a ^ n * 1 < a ^ n * a

Tactic:
exact Nat.mul_lt_mul_of_le_of_lt (Nat.le_refl _) h (Nat.pow_pos (Nat.lt_trans Nat.zero_lt_one h))

Result:
no goals

Proof state:
a n : Nat
h : 1 < a
⊢ a ^ n < a ^ (n + 1)

Tactic:
rw [← Nat.mul_one (a^n), Nat.pow_succ]

Result:
a n : Nat
h : 1 < a
⊢ a ^ n * 1 < a ^ n * a
-- Mathlib/Data/Nat/Sqrt.lean
private lemma AM_GM : {a b : ℕ} → (4 * a * b ≤ (a + b) * (a + b))
  | 0, _ => by rw [Nat.mul_zero, Nat.zero_mul]; exact zero_le _
  | _, 0 => by rw [Nat.mul_zero]; exact zero_le _
  | a + 1, b + 1 => by
    simpa only [Nat.mul_add, Nat.add_mul, show (4 : ℕ) = 1 + 1 + 1 + 1 from rfl, Nat.one_mul,
      Nat.mul_one, Nat.add_assoc, Nat.add_left_comm, Nat.add_le_add_iff_left]
      using Nat.add_le_add_right (@AM_GM a b) 4

Proof state:
x✝ : ℕ
⊢ 0 ≤ (0 + x✝) * (0 + x✝)

Tactic:
exact zero_le _

Result:
no goals

Proof state:
x✝ : ℕ
⊢ 4 * x✝ * 0 ≤ (x✝ + 0) * (x✝ + 0)

Tactic:
rw [Nat.mul_zero]

Result:
x✝ : ℕ
⊢ 0 ≤ (x✝ + 0) * (x✝ + 0)

Proof state:
x✝ : ℕ
⊢ 0 ≤ (x✝ + 0) * (x✝ + 0)

Tactic:
exact zero_le _

Result:
no goals

Proof state:
x✝ : ℕ
⊢ 4 * 0 * x✝ ≤ (0 + x✝) * (0 + x✝)

Tactic:
rw [Nat.mul_zero, Nat.zero_mul]

Result:
x✝ : ℕ
⊢ 0 ≤ (0 + x✝) * (0 + x✝)

Proof state:
a b : ℕ
⊢ 4 * (a + 1) * (b + 1) ≤ (a + 1 + (b + 1)) * (a + 1 + (b + 1))

Tactic:
simpa only [Nat.mul_add, Nat.add_mul, show (4 : ℕ) = 1 + 1 + 1 + 1 from rfl, Nat.one_mul,
  Nat.mul_one, Nat.add_assoc, Nat.add_left_comm, Nat.add_le_add_iff_left]
  using Nat.add_le_add_right (@AM_GM a b) 4

Result:
no goals
-- Mathlib/Algebra/BigOperators/Intervals.lean
theorem prod_range_div_prod_range {α : Type*} [CommGroup α] {f : ℕ → α} {n m : ℕ} (hnm : n ≤ m) :
    ((∏ k ∈ range m, f k) / ∏ k ∈ range n, f k) =
    ∏ k ∈ (range m).filter fun k => n ≤ k, f k

Proof state:
case e_s.h
α : Type u_3
inst✝ : CommGroup α
f : ℕ → α
n m : ℕ
hnm : n ≤ m
⊢ ∀ (a : ℕ), n ≤ a ∧ a < m ↔ a < m ∧ n ≤ a

Tactic:
tauto

Result:
no goals

Proof state:
case e_s
α : Type u_3
inst✝ : CommGroup α
f : ℕ → α
n m : ℕ
hnm : n ≤ m
⊢ Ico n m = filter (fun k => n ≤ k) (range m)

Tactic:
apply Finset.ext

Result:
case e_s.h
α : Type u_3
inst✝ : CommGroup α
f : ℕ → α
n m : ℕ
hnm : n ≤ m
⊢ ∀ (a : ℕ), a ∈ Ico n m ↔ a ∈ filter (fun k => n ≤ k) (range m)

Proof state:
case e_s.h
α : Type u_3
inst✝ : CommGroup α
f : ℕ → α
n m : ℕ
hnm : n ≤ m
⊢ ∀ (a : ℕ), a ∈ Ico n m ↔ a ∈ filter (fun k => n ≤ k) (range m)

Tactic:
simp only [mem_Ico, mem_filter, mem_range, *]

Result:
case e_s.h
α : Type u_3
inst✝ : CommGroup α
f : ℕ → α
n m : ℕ
hnm : n ≤ m
⊢ ∀ (a : ℕ), n ≤ a ∧ a < m ↔ a < m ∧ n ≤ a

Proof state:
α : Type u_3
inst✝ : CommGroup α
f : ℕ → α
n m : ℕ
hnm : n ≤ m
⊢ ∏ k ∈ Ico n m, f k = ∏ k ∈ filter (fun k => n ≤ k) (range m), f k

Tactic:
congr

Result:
case e_s
α : Type u_3
inst✝ : CommGroup α
f : ℕ → α
n m : ℕ
hnm : n ≤ m
⊢ Ico n m = filter (fun k => n ≤ k) (range m)

Proof state:
α : Type u_3
inst✝ : CommGroup α
f : ℕ → α
n m : ℕ
hnm : n ≤ m
⊢ (∏ k ∈ range m, f k) / ∏ k ∈ range n, f k = ∏ k ∈ filter (fun k => n ≤ k) (range m), f k

Tactic:
rw [← prod_Ico_eq_div f hnm]

Result:
α : Type u_3
inst✝ : CommGroup α
f : ℕ → α
n m : ℕ
hnm : n ≤ m
⊢ ∏ k ∈ Ico n m, f k = ∏ k ∈ filter (fun k => n ≤ k) (range m), f k