harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Category/Grp/EpiMono.lean
theorem surjective_of_epi [Epi f] : Function.Surjective f

Proof state:
A B : Grp
f : A ⟶ B
inst✝ : Epi f
r : ¬Function.Surjective ⇑(ConcreteCategory.hom f)
⊢ False

Tactic:
dsimp [Function.Surjective] at r

Result:
A B : Grp
f : A ⟶ B
inst✝ : Epi f
r : ¬∀ (b : ↑B), ∃ a, (ConcreteCategory.hom f) a = b
⊢ False

Proof state:
A B : Grp
f : A ⟶ B
inst✝ : Epi f
r : ∃ b, ∀ (a : ↑A), (ConcreteCategory.hom f) a ≠ b
⊢ False

Tactic:
rcases r with ⟨b, hb⟩

Result:
case intro
A B : Grp
f : A ⟶ B
inst✝ : Epi f
b : ↑B
hb : ∀ (a : ↑A), (ConcreteCategory.hom f) a ≠ b
⊢ False

Proof state:
A B : Grp
f : A ⟶ B
inst✝ : Epi f
⊢ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
by_contra r

Result:
A B : Grp
f : A ⟶ B
inst✝ : Epi f
r : ¬Function.Surjective ⇑(ConcreteCategory.hom f)
⊢ False

Proof state:
case intro
A B : Grp
f : A ⟶ B
inst✝ : Epi f
b : ↑B
hb : ∀ (a : ↑A), (ConcreteCategory.hom f) a ≠ b
⊢ False

Tactic:
exact
  SurjectiveOfEpiAuxs.g_ne_h f b (fun ⟨c, hc⟩ => hb _ hc)
    (congr_arg Grp.Hom.hom ((cancel_epi f).1 (SurjectiveOfEpiAuxs.comp_eq f)))

Result:
no goals

Proof state:
A B : Grp
f : A ⟶ B
inst✝ : Epi f
r : ¬∀ (b : ↑B), ∃ a, (ConcreteCategory.hom f) a = b
⊢ False

Tactic:
push_neg at r

Result:
A B : Grp
f : A ⟶ B
inst✝ : Epi f
r : ∃ b, ∀ (a : ↑A), (ConcreteCategory.hom f) a ≠ b
⊢ False
-- Mathlib/Data/Real/EReal.lean
lemma strictMono_div_right_of_pos (h : 0 < b) (h' : b ≠ ⊤) : StrictMono fun a ↦ a / b

Proof state:
b : EReal
h : 0 < b
h' : b ≠ ⊤
a a' : EReal
a_lt_a' : a < a'
⊢ (fun a => a / b) a < (fun a => a / b) a'

Tactic:
apply lt_of_le_of_ne <| div_le_div_right_of_nonneg (le_of_lt h) (le_of_lt a_lt_a')

Result:
b : EReal
h : 0 < b
h' : b ≠ ⊤
a a' : EReal
a_lt_a' : a < a'
⊢ a / b ≠ a' / b

Proof state:
b : EReal
h : 0 < b
h' : b ≠ ⊤
a a' : EReal
a_lt_a' : a < a'
hyp : a / b = a' / b
⊢ False

Tactic:
apply ne_of_lt a_lt_a'

Result:
b : EReal
h : 0 < b
h' : b ≠ ⊤
a a' : EReal
a_lt_a' : a < a'
hyp : a / b = a' / b
⊢ a = a'

Proof state:
b : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ StrictMono fun a => a / b

Tactic:
intro a a' a_lt_a'

Result:
b : EReal
h : 0 < b
h' : b ≠ ⊤
a a' : EReal
a_lt_a' : a < a'
⊢ (fun a => a / b) a < (fun a => a / b) a'

Proof state:
b : EReal
h : 0 < b
h' : b ≠ ⊤
a a' : EReal
a_lt_a' : a < a'
hyp : a / b = a' / b
⊢ a = a'

Tactic:
rw [← @EReal.mul_div_cancel a b (ne_bot_of_gt h) h' (ne_of_gt h), hyp,
  @EReal.mul_div_cancel a' b (ne_bot_of_gt h) h' (ne_of_gt h)]

Result:
no goals

Proof state:
b : EReal
h : 0 < b
h' : b ≠ ⊤
a a' : EReal
a_lt_a' : a < a'
⊢ a / b ≠ a' / b

Tactic:
intro hyp

Result:
b : EReal
h : 0 < b
h' : b ≠ ⊤
a a' : EReal
a_lt_a' : a < a'
hyp : a / b = a' / b
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Int.lean
theorem add_le_zero_iff_le_neg' {a b : Int} : a + b ≤ 0 ↔ b ≤ -a

Proof state:
a b : Int
⊢ a + b ≤ 0 ↔ b ≤ -a

Tactic:
rw [Int.add_comm, add_le_zero_iff_le_neg]

Result:
no goals
-- Mathlib/RingTheory/Idempotents.lean
lemma OrthogonalIdempotents.lift_of_isNilpotent_ker_aux
    (h : ∀ x ∈ RingHom.ker f, IsNilpotent x)
    {n} {e : Fin n → S} (he : OrthogonalIdempotents e) (he' : ∀ i, e i ∈ f.range) :
    ∃ e' : Fin n → R, OrthogonalIdempotents e' ∧ f ∘ e' = e

Proof state:
case succ.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
n : ℕ
IH :
  ∀ {e : Fin n → S},
    OrthogonalIdempotents e → (∀ (i : Fin n), e i ∈ f.range) → ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), e i ∈ f.range
e' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fin.succEmb n)
h₂' : ∀ (i : Fin n), f (e' i) = e i.succ
⊢ ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

Tactic:
obtain ⟨e₀, h₃, h₄, h₅, h₆⟩ :=
  exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent f h _ (he' 0) (he.idem 0) _
  h₁.isIdempotentElem_sum
  (by simp [Finset.mul_sum, h₂', he.mul_eq, Fin.succ_ne_zero, eq_comm])
  (by simp [Finset.sum_mul, h₂', he.mul_eq, Fin.succ_ne_zero])

Result:
case succ.intro.intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
n : ℕ
IH :
  ∀ {e : Fin n → S},
    OrthogonalIdempotents e → (∀ (i : Fin n), e i ∈ f.range) → ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), e i ∈ f.range
e' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fin.succEmb n)
h₂' : ∀ (i : Fin n), f (e' i) = e i.succ
e₀ : R
h₃ : IsIdempotentElem e₀
h₄ : f e₀ = e 0
h₅ : e₀ * ∑ i ∈ ?m.144356, e' i = 0
h₆ : (∑ i ∈ ?m.144356, e' i) * e₀ = 0
⊢ ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/DecidableEq.lean
theorem isEqv_iff_rel {a b : Vector α n} {r} :
    Vector.isEqv a b r ↔ ∀ (i : Nat) (h' : i < n), r a[i] b[i]

Proof state:
α : Type u_1
n : Nat
a b : Vector α n
r : α → α → Bool
⊢ a.isEqv b r = true ↔ ∀ (i : Nat) (h' : i < n), r a[i] b[i] = true

Tactic:
rcases a with ⟨a, rfl⟩

Result:
case mk
α : Type u_1
r : α → α → Bool
a : Array α
b : Vector α a.size
⊢ { toArray := a, size_toArray := ⋯ }.isEqv b r = true ↔
    ∀ (i : Nat) (h' : i < a.size), r { toArray := a, size_toArray := ⋯ }[i] b[i] = true

Proof state:
case mk
α : Type u_1
r : α → α → Bool
a : Array α
b : Vector α a.size
⊢ { toArray := a, size_toArray := ⋯ }.isEqv b r = true ↔
    ∀ (i : Nat) (h' : i < a.size), r { toArray := a, size_toArray := ⋯ }[i] b[i] = true

Tactic:
rcases b with ⟨b, h⟩

Result:
case mk.mk
α : Type u_1
r : α → α → Bool
a b : Array α
h : b.size = a.size
⊢ { toArray := a, size_toArray := ⋯ }.isEqv { toArray := b, size_toArray := h } r = true ↔
    ∀ (i : Nat) (h' : i < a.size),
      r { toArray := a, size_toArray := ⋯ }[i] { toArray := b, size_toArray := h }[i] = true

Proof state:
case mk.mk
α : Type u_1
r : α → α → Bool
a b : Array α
h : b.size = a.size
⊢ { toArray := a, size_toArray := ⋯ }.isEqv { toArray := b, size_toArray := h } r = true ↔
    ∀ (i : Nat) (h' : i < a.size),
      r { toArray := a, size_toArray := ⋯ }[i] { toArray := b, size_toArray := h }[i] = true

Tactic:
simp [Array.isEqv_iff_rel, h]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
theorem adjoint_comp (A : F →ₗ[𝕜] G) (B : E →ₗ[𝕜] F) :
    LinearMap.adjoint (A ∘ₗ B) = LinearMap.adjoint B ∘ₗ LinearMap.adjoint A

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
A : F →ₗ[𝕜] G
B : E →ₗ[𝕜] F
v : G
w : E
⊢ ⟪w, (adjoint (A ∘ₗ B)) v⟫_𝕜 = ⟪w, (adjoint B ∘ₗ adjoint A) v⟫_𝕜

Tactic:
simp only [adjoint_inner_right, LinearMap.coe_comp, Function.comp_apply]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
A : F →ₗ[𝕜] G
B : E →ₗ[𝕜] F
⊢ adjoint (A ∘ₗ B) = adjoint B ∘ₗ adjoint A

Tactic:
ext v

Result:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
A : F →ₗ[𝕜] G
B : E →ₗ[𝕜] F
v : G
⊢ (adjoint (A ∘ₗ B)) v = (adjoint B ∘ₗ adjoint A) v

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
A : F →ₗ[𝕜] G
B : E →ₗ[𝕜] F
v : G
⊢ (adjoint (A ∘ₗ B)) v = (adjoint B ∘ₗ adjoint A) v

Tactic:
refine ext_inner_left 𝕜 fun w => ?_

Result:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
A : F →ₗ[𝕜] G
B : E →ₗ[𝕜] F
v : G
w : E
⊢ ⟪w, (adjoint (A ∘ₗ B)) v⟫_𝕜 = ⟪w, (adjoint B ∘ₗ adjoint A) v⟫_𝕜
-- Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean
lemma eval_minpolyDiv_of_aeval_eq_zero [IsDomain S] [DecidableEq S]
    {y} (hy : aeval y (minpoly R x) = 0) :
    (minpolyDiv R x).eval y = if x = y then aeval x (derivative <| minpoly R x) else 0

Proof state:
case hy
R : Type u_2
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
x : S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
y : S
hy : (aeval y) (minpoly R x) = 0
⊢ eval₂ ((RingHom.id S).comp (algebraMap R S)) y (minpoly R x) = 0

Tactic:
simpa [aeval_def] using hy

Result:
no goals

Proof state:
R : Type u_2
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
x : S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
y : S
hy : (aeval y) (minpoly R x) = 0
⊢ eval y (minpolyDiv R x) = if x = y then (aeval x) (derivative (minpoly R x)) else 0

Tactic:
rw [eval, eval₂_minpolyDiv_of_eval₂_eq_zero, RingHom.id_apply, RingHom.id_apply]

Result:
case hy
R : Type u_2
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
x : S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
y : S
hy : (aeval y) (minpoly R x) = 0
⊢ eval₂ ((RingHom.id S).comp (algebraMap R S)) y (minpoly R x) = 0
-- Mathlib/Data/Finset/Card.lean
theorem injOn_of_card_image_eq [DecidableEq β] (H : #(s.image f) = #s) : Set.InjOn f s

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
H : (Multiset.map f s.val).dedup.card = s.val.card
⊢ (Multiset.map f s.val).card ≤ (Multiset.map f s.val).dedup.card

Tactic:
simp only [H, Multiset.card_map, le_rfl]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
H : { val := (Multiset.map f s.val).dedup, nodup := ⋯ }.val.card = s.val.card
⊢ Set.InjOn f ↑s

Tactic:
dsimp only at H

Result:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
H : (Multiset.map f s.val).dedup.card = s.val.card
⊢ Set.InjOn f ↑s

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
H : (Multiset.map f s.val).dedup.card = s.val.card
this : (Multiset.map f s.val).dedup = Multiset.map f s.val
⊢ Set.InjOn f ↑s

Tactic:
rw [Multiset.dedup_eq_self] at this

Result:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
H : (Multiset.map f s.val).dedup.card = s.val.card
this : (Multiset.map f s.val).Nodup
⊢ Set.InjOn f ↑s

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
H : (Multiset.map f s.val).dedup.card = s.val.card
this : (Multiset.map f s.val).Nodup
⊢ Set.InjOn f ↑s

Tactic:
exact inj_on_of_nodup_map this

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
H : #(image f s) = #s
⊢ Set.InjOn f ↑s

Tactic:
rw [card_def, card_def, image, toFinset] at H

Result:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
H : { val := (Multiset.map f s.val).dedup, nodup := ⋯ }.val.card = s.val.card
⊢ Set.InjOn f ↑s

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
H : (Multiset.map f s.val).dedup.card = s.val.card
⊢ (Multiset.map f s.val).dedup = Multiset.map f s.val

Tactic:
refine Multiset.eq_of_le_of_card_le (Multiset.dedup_le _) ?_

Result:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
H : (Multiset.map f s.val).dedup.card = s.val.card
⊢ (Multiset.map f s.val).card ≤ (Multiset.map f s.val).dedup.card

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
H : (Multiset.map f s.val).dedup.card = s.val.card
⊢ Set.InjOn f ↑s

Tactic:
have : (s.1.map f).dedup = s.1.map f := by
  refine Multiset.eq_of_le_of_card_le (Multiset.dedup_le _) ?_
  simp only [H, Multiset.card_map, le_rfl]

Result:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
H : (Multiset.map f s.val).dedup.card = s.val.card
this : (Multiset.map f s.val).dedup = Multiset.map f s.val
⊢ Set.InjOn f ↑s
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem eq_pow_find_of_dvd_irreducible_pow {a p : Associates α} (hp : Irreducible p)
    [∀ n : ℕ, Decidable (a ∣ p ^ n)] {n : ℕ} (h : a ∣ p ^ n) :
    a = p ^ @Nat.find (fun n => a ∣ p ^ n) _ ⟨n, h⟩

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
a p : Associates α
hp : Irreducible p
inst✝ : (n : ℕ) → Decidable (a ∣ p ^ n)
n : ℕ
h : a ∣ p ^ n
⊢ a ∣ p ^ ?m.169457

α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
a p : Associates α
hp : Irreducible p
inst✝ : (n : ℕ) → Decidable (a ∣ p ^ n)
n : ℕ
h : a ∣ p ^ n
⊢ ℕ

Tactic:
exact h

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
a p : Associates α
hp : Irreducible p
inst✝ : (n : ℕ) → Decidable (a ∣ p ^ n)
n : ℕ
h : a ∣ p ^ n
⊢ a = p ^ Nat.find ⋯

Tactic:
rw [count_factors_eq_find_of_dvd_pow hp, ← eq_pow_count_factors_of_dvd_pow hp h]

Result:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
a p : Associates α
hp : Irreducible p
inst✝ : (n : ℕ) → Decidable (a ∣ p ^ n)
n : ℕ
h : a ∣ p ^ n
⊢ a ∣ p ^ ?m.169457

α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
a p : Associates α
hp : Irreducible p
inst✝ : (n : ℕ) → Decidable (a ∣ p ^ n)
n : ℕ
h : a ∣ p ^ n
⊢ ℕ

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
a p : Associates α
hp : Irreducible p
inst✝ : (n : ℕ) → Decidable (a ∣ p ^ n)
n : ℕ
h : a ∣ p ^ n
⊢ a = p ^ Nat.find ⋯

Tactic:
classical rw [count_factors_eq_find_of_dvd_pow hp, ← eq_pow_count_factors_of_dvd_pow hp h]

Result:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
a p : Associates α
hp : Irreducible p
inst✝ : (n : ℕ) → Decidable (a ∣ p ^ n)
n : ℕ
h : a ∣ p ^ n
⊢ a ∣ p ^ ?m.169457

α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
a p : Associates α
hp : Irreducible p
inst✝ : (n : ℕ) → Decidable (a ∣ p ^ n)
n : ℕ
h : a ∣ p ^ n
⊢ ℕ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem getLast_take {l : List α} (h : l.take n ≠ []) :
    (l.take n).getLast h = l[n - 1]?.getD (l.getLast (by simp_all))

Proof state:
α : Type ?u.6389
n : Nat
l : List α
h : take n l ≠ []
⊢ l ≠ []

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : List α
h : take n l ≠ []
⊢ (take n l).getLast h = l[n - 1]?.getD (l.getLast ⋯)

Tactic:
rw [getLast_eq_getElem, getElem_take]

Result:
α : Type u_1
n : Nat
l : List α
h : take n l ≠ []
⊢ l[(take n l).length - 1] = l[n - 1]?.getD (l.getLast ⋯)

Proof state:
α : Type u_1
n : Nat
l : List α
h : take n l ≠ []
⊢ l[(take n l).length - 1] = l[n - 1]?.getD (l.getLast ⋯)

Tactic:
simp [length_take, Nat.min_def]

Result:
α : Type u_1
n : Nat
l : List α
h : take n l ≠ []
⊢ l[(if n ≤ l.length then n else l.length) - 1] = l[n - 1]?.getD (l.getLast ⋯)

Proof state:
α : Type u_1
n : Nat
l : List α
h✝¹ : take n l ≠ []
h : ¬n = 0 ∧ ¬l = []
h✝ : n ≤ l.length
⊢ n - 1 < l.length

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : List α
h✝¹ : take n l ≠ []
h : ¬n = 0 ∧ ¬l = []
h✝ : ¬n ≤ l.length
⊢ l.length ≤ n - 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : List α
h : take n l ≠ []
⊢ l[(if n ≤ l.length then n else l.length) - 1] = l[n - 1]?.getD (l.getLast ⋯)

Tactic:
simp at h

Result:
α : Type u_1
n : Nat
l : List α
h✝ : take n l ≠ []
h : ¬n = 0 ∧ ¬l = []
⊢ l[(if n ≤ l.length then n else l.length) - 1] = l[n - 1]?.getD (l.getLast ⋯)

Proof state:
case isFalse
α : Type u_1
n : Nat
l : List α
h✝¹ : take n l ≠ []
h : ¬n = 0 ∧ ¬l = []
h✝ : ¬n ≤ l.length
⊢ l[l.length - 1] = none.getD l[l.length - 1]

Tactic:
simp

Result:
no goals

Proof state:
case isFalse
α : Type u_1
n : Nat
l : List α
h✝¹ : take n l ≠ []
h : ¬n = 0 ∧ ¬l = []
h✝ : ¬n ≤ l.length
⊢ l[l.length - 1] = l[n - 1]?.getD (l.getLast ⋯)

Tactic:
rw [getElem?_eq_none (by omega), getLast_eq_getElem]

Result:
case isFalse
α : Type u_1
n : Nat
l : List α
h✝¹ : take n l ≠ []
h : ¬n = 0 ∧ ¬l = []
h✝ : ¬n ≤ l.length
⊢ l[l.length - 1] = none.getD l[l.length - 1]

Proof state:
case isTrue
α : Type u_1
n : Nat
l : List α
h✝¹ : take n l ≠ []
h : ¬n = 0 ∧ ¬l = []
h✝ : n ≤ l.length
⊢ l[n - 1] = l[n - 1]?.getD (l.getLast ⋯)

Tactic:
rw [getElem?_eq_getElem (by omega)]

Result:
case isTrue
α : Type u_1
n : Nat
l : List α
h✝¹ : take n l ≠ []
h : ¬n = 0 ∧ ¬l = []
h✝ : n ≤ l.length
⊢ l[n - 1] = (some l[n - 1]).getD (l.getLast ⋯)

Proof state:
case isTrue
α : Type u_1
n : Nat
l : List α
h✝¹ : take n l ≠ []
h : ¬n = 0 ∧ ¬l = []
h✝ : n ≤ l.length
⊢ l[n - 1] = (some l[n - 1]).getD (l.getLast ⋯)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : List α
h✝ : take n l ≠ []
h : ¬n = 0 ∧ ¬l = []
⊢ l[(if n ≤ l.length then n else l.length) - 1] = l[n - 1]?.getD (l.getLast ⋯)

Tactic:
split

Result:
case isTrue
α : Type u_1
n : Nat
l : List α
h✝¹ : take n l ≠ []
h : ¬n = 0 ∧ ¬l = []
h✝ : n ≤ l.length
⊢ l[n - 1] = l[n - 1]?.getD (l.getLast ⋯)

case isFalse
α : Type u_1
n : Nat
l : List α
h✝¹ : take n l ≠ []
h : ¬n = 0 ∧ ¬l = []
h✝ : ¬n ≤ l.length
⊢ l[l.length - 1] = l[n - 1]?.getD (l.getLast ⋯)
-- Mathlib/Algebra/Field/Rat.lean
protected lemma inv_nonneg {a : ℚ} (ha : 0 ≤ a) : 0 ≤ a⁻¹

Proof state:
a : ℚ
ha : 0 ≤ a
⊢ 0 ≤ a⁻¹

Tactic:
rw [inv_def']

Result:
a : ℚ
ha : 0 ≤ a
⊢ 0 ≤ ↑a.den /. a.num

Proof state:
a : ℚ
ha : 0 ≤ a
⊢ 0 ≤ ↑a.den /. a.num

Tactic:
exact divInt_nonneg (Int.ofNat_nonneg a.den) (num_nonneg.mpr ha)

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem principal_mono {s t : Set α} : 𝓟 s ≤ 𝓟 t ↔ s ⊆ t

Proof state:
α : Type u
s t : Set α
⊢ 𝓟 s ≤ 𝓟 t ↔ s ⊆ t

Tactic:
simp only [le_principal_iff, mem_principal]

Result:
no goals
-- Mathlib/Data/Multiset/AddSub.lean
theorem Rel.add {s t u v} (hst : Rel r s t) (huv : Rel r u v) : Rel r (s + u) (t + v)

Proof state:
case zero
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
huv : Rel r u v
⊢ Rel r (0 + u) (0 + v)

Tactic:
simpa using huv

Result:
no goals

Proof state:
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
hst : Rel r s t
huv : Rel r u v
⊢ Rel r (s + u) (t + v)

Tactic:
induction hst with
| zero => simpa using huv
| cons hab hst ih => simpa using ih.cons hab

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
huv : Rel r u v
a✝ : α
b✝ : β
as✝ : Multiset α
bs✝ : Multiset β
hab : r a✝ b✝
hst : Rel r as✝ bs✝
ih : Rel r (as✝ + u) (bs✝ + v)
⊢ Rel r (a✝ ::ₘ as✝ + u) (b✝ ::ₘ bs✝ + v)

Tactic:
simpa using ih.cons hab

Result:
no goals
-- Mathlib/NumberTheory/Multiplicity.lean
theorem pow_two_pow_sub_pow_two_pow [CommRing R] {x y : R} (n : ℕ) :
    x ^ 2 ^ n - y ^ 2 ^ n = (∏ i ∈ Finset.range n, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)

Proof state:
case succ
R : Type u_1
inst✝ : CommRing R
x y : R
d : ℕ
hd : x ^ 2 ^ d - y ^ 2 ^ d = (∏ i ∈ range d, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)
⊢ x ^ 2 ^ (d + 1) - y ^ 2 ^ (d + 1) = (x ^ 2 ^ d + y ^ 2 ^ d) * (x ^ 2 ^ d - y ^ 2 ^ d)

Tactic:
ring

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
x y : R
d : ℕ
hd : x ^ 2 ^ d - y ^ 2 ^ d = (∏ i ∈ range d, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)
this : x ^ 2 ^ d.succ - y ^ 2 ^ d.succ = (x ^ 2 ^ d + y ^ 2 ^ d) * (x ^ 2 ^ d - y ^ 2 ^ d)
⊢ x ^ 2 ^ (d + 1) - y ^ 2 ^ (d + 1) = (∏ i ∈ range (d + 1), (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)

Tactic:
rw [this, hd, Finset.prod_range_succ, ← mul_assoc, mul_comm (x ^ 2 ^ d + y ^ 2 ^ d)]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
x y : R
n : ℕ
⊢ x ^ 2 ^ n - y ^ 2 ^ n = (∏ i ∈ range n, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)

Tactic:
induction n with
| zero => simp only [pow_zero, pow_one, range_zero, prod_empty, one_mul]
| succ d hd =>
  suffices x ^ 2 ^ d.succ - y ^ 2 ^ d.succ = (x ^ 2 ^ d + y ^ 2 ^ d) * (x ^ 2 ^ d - y ^ 2 ^ d) by
    rw [this, hd, Finset.prod_range_succ, ← mul_assoc, mul_comm (x ^ 2 ^ d + y ^ 2 ^ d)]
  rw [Nat.succ_eq_add_one]
  ring

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝ : CommRing R
x y : R
d : ℕ
hd : x ^ 2 ^ d - y ^ 2 ^ d = (∏ i ∈ range d, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)
⊢ x ^ 2 ^ d.succ - y ^ 2 ^ d.succ = (x ^ 2 ^ d + y ^ 2 ^ d) * (x ^ 2 ^ d - y ^ 2 ^ d)

Tactic:
rw [Nat.succ_eq_add_one]

Result:
case succ
R : Type u_1
inst✝ : CommRing R
x y : R
d : ℕ
hd : x ^ 2 ^ d - y ^ 2 ^ d = (∏ i ∈ range d, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)
⊢ x ^ 2 ^ (d + 1) - y ^ 2 ^ (d + 1) = (x ^ 2 ^ d + y ^ 2 ^ d) * (x ^ 2 ^ d - y ^ 2 ^ d)

Proof state:
case succ
R : Type u_1
inst✝ : CommRing R
x y : R
d : ℕ
hd : x ^ 2 ^ d - y ^ 2 ^ d = (∏ i ∈ range d, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)
⊢ x ^ 2 ^ (d + 1) - y ^ 2 ^ (d + 1) = (∏ i ∈ range (d + 1), (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)

Tactic:
suffices x ^ 2 ^ d.succ - y ^ 2 ^ d.succ = (x ^ 2 ^ d + y ^ 2 ^ d) * (x ^ 2 ^ d - y ^ 2 ^ d) by
  rw [this, hd, Finset.prod_range_succ, ← mul_assoc, mul_comm (x ^ 2 ^ d + y ^ 2 ^ d)]

Result:
case succ
R : Type u_1
inst✝ : CommRing R
x y : R
d : ℕ
hd : x ^ 2 ^ d - y ^ 2 ^ d = (∏ i ∈ range d, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)
⊢ x ^ 2 ^ d.succ - y ^ 2 ^ d.succ = (x ^ 2 ^ d + y ^ 2 ^ d) * (x ^ 2 ^ d - y ^ 2 ^ d)

Proof state:
case zero
R : Type u_1
inst✝ : CommRing R
x y : R
⊢ x ^ 2 ^ 0 - y ^ 2 ^ 0 = (∏ i ∈ range 0, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)

Tactic:
simp only [pow_zero, pow_one, range_zero, prod_empty, one_mul]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval₂_sub {S} [Ring S] (f : R →+* S) {x : S} :
    (p - q).eval₂ f x = p.eval₂ f x - q.eval₂ f x

Proof state:
R : Type u
inst✝¹ : Ring R
p q : R[X]
S : Type u_1
inst✝ : Ring S
f : R →+* S
x : S
⊢ eval₂ f x (p - q) = eval₂ f x p - eval₂ f x q

Tactic:
rw [sub_eq_add_neg, eval₂_add, eval₂_neg, sub_eq_add_neg]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Membership.lean
theorem closure_eq_mrange (s : Set M) : closure s = mrange (FreeMonoid.lift ((↑) : s → M))

Proof state:
M : Type u_1
inst✝ : Monoid M
s : Set M
⊢ closure s = mrange (FreeMonoid.lift Subtype.val)

Tactic:
rw [FreeMonoid.mrange_lift, Subtype.range_coe]

Result:
no goals