harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/PNat/Factors.lean
theorem factorMultiset_le_iff {m n : ℕ+} : factorMultiset m ≤ factorMultiset n ↔ m ∣ n

Proof state:
case mp
m n : ℕ+
h : m.factorMultiset ≤ n.factorMultiset
⊢ m.factorMultiset.prod.factorMultiset.prod * (n.factorMultiset - m.factorMultiset).prod = n

Tactic:
rw [← PrimeMultiset.prod_add, PrimeMultiset.factorMultiset_prod, add_tsub_cancel_of_le h,
  prod_factorMultiset]

Result:
no goals

Proof state:
case mp
m n : ℕ+
h : m.factorMultiset ≤ n.factorMultiset
⊢ m.factorMultiset.prod.factorMultiset.prod ∣ n

Tactic:
apply Dvd.intro (n.factorMultiset - m.factorMultiset).prod

Result:
case mp
m n : ℕ+
h : m.factorMultiset ≤ n.factorMultiset
⊢ m.factorMultiset.prod.factorMultiset.prod * (n.factorMultiset - m.factorMultiset).prod = n

Proof state:
case mpr
m n : ℕ+
⊢ m ∣ n → m.factorMultiset ≤ n.factorMultiset

Tactic:
intro h

Result:
case mpr
m n : ℕ+
h : m ∣ n
⊢ m.factorMultiset ≤ n.factorMultiset

Proof state:
case mpr
m n : ℕ+
h : m ∣ n
⊢ m.factorMultiset ≤ m.factorMultiset + (n.divExact m).factorMultiset

Tactic:
exact le_self_add

Result:
no goals

Proof state:
case mpr
m n : ℕ+
h : m ∣ n
⊢ m.factorMultiset ≤ n.factorMultiset

Tactic:
rw [← mul_div_exact h, factorMultiset_mul]

Result:
case mpr
m n : ℕ+
h : m ∣ n
⊢ m.factorMultiset ≤ m.factorMultiset + (n.divExact m).factorMultiset

Proof state:
m n : ℕ+
⊢ m.factorMultiset ≤ n.factorMultiset ↔ m ∣ n

Tactic:
constructor

Result:
case mp
m n : ℕ+
⊢ m.factorMultiset ≤ n.factorMultiset → m ∣ n

case mpr
m n : ℕ+
⊢ m ∣ n → m.factorMultiset ≤ n.factorMultiset

Proof state:
case mp
m n : ℕ+
h : m.factorMultiset ≤ n.factorMultiset
⊢ m ∣ n

Tactic:
rw [← prod_factorMultiset m, ← prod_factorMultiset m]

Result:
case mp
m n : ℕ+
h : m.factorMultiset ≤ n.factorMultiset
⊢ m.factorMultiset.prod.factorMultiset.prod ∣ n

Proof state:
case mp
m n : ℕ+
⊢ m.factorMultiset ≤ n.factorMultiset → m ∣ n

Tactic:
intro h

Result:
case mp
m n : ℕ+
h : m.factorMultiset ≤ n.factorMultiset
⊢ m ∣ n
-- Mathlib/RingTheory/Smooth/Kaehler.lean
lemma sectionOfRetractionKerToTensorAux_prop (x y) (h : algebraMap P S x = algebraMap P S y) :
    x - l (1 ⊗ₜ .D _ _ x) = y - l (1 ⊗ₜ .D _ _ y)

Proof state:
R P S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing P
inst✝² : CommRing S
inst✝¹ : Algebra R P
inst✝ : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
x y : P
h : (algebraMap P S) x = (algebraMap P S) y
⊢ x - y = ↑(l (1 ⊗ₜ[P] (D R P) (x - y)))

Tactic:
exact congr_arg Subtype.val (LinearMap.congr_fun hl.symm ⟨x - y, by simp [RingHom.mem_ker, h]⟩)

Result:
no goals

Proof state:
R P S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing P
inst✝² : CommRing S
inst✝¹ : Algebra R P
inst✝ : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
x y : P
h : (algebraMap P S) x = (algebraMap P S) y
⊢ x - y ∈ RingHom.ker (algebraMap P S)

Tactic:
simp [RingHom.mem_ker, h]

Result:
no goals

Proof state:
R P S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing P
inst✝² : CommRing S
inst✝¹ : Algebra R P
inst✝ : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
x y : P
h : (algebraMap P S) x = (algebraMap P S) y
⊢ x - ↑(l (1 ⊗ₜ[P] (D R P) x)) = y - ↑(l (1 ⊗ₜ[P] (D R P) y))

Tactic:
rw [sub_eq_iff_eq_add, sub_add_comm, ← sub_eq_iff_eq_add, ← Submodule.coe_sub,
  ← map_sub, ← tmul_sub, ← map_sub]

Result:
R P S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing P
inst✝² : CommRing S
inst✝¹ : Algebra R P
inst✝ : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
x y : P
h : (algebraMap P S) x = (algebraMap P S) y
⊢ x - y = ↑(l (1 ⊗ₜ[P] (D R P) (x - y)))
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivative_eval₂_C (p q : R[X]) :
    derivative (p.eval₂ C q) = p.derivative.eval₂ C q * derivative q :=
  Polynomial.induction_on p (fun r => by rw [eval₂_C, derivative_C, eval₂_zero, zero_mul])
    (fun p₁ p₂ ih₁ ih₂ => by
      rw [eval₂_add, derivative_add, ih₁, ih₂, derivative_add, eval₂_add, add_mul])
    fun n r ih => by
    rw [pow_succ, ← mul_assoc, eval₂_mul, eval₂_X, derivative_mul, ih, @derivative_mul _ _ _ X,
      derivative_X, mul_one, eval₂_add, @eval₂_mul _ _ _ _ X, eval₂_X, add_mul, mul_right_comm]

Proof state:
R : Type u
inst✝ : CommSemiring R
p q p₁ p₂ : R[X]
ih₁ : derivative (eval₂ C q p₁) = eval₂ C q (derivative p₁) * derivative q
ih₂ : derivative (eval₂ C q p₂) = eval₂ C q (derivative p₂) * derivative q
⊢ derivative (eval₂ C q (p₁ + p₂)) = eval₂ C q (derivative (p₁ + p₂)) * derivative q

Tactic:
rw [eval₂_add, derivative_add, ih₁, ih₂, derivative_add, eval₂_add, add_mul]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
p q : R[X]
r : R
⊢ derivative (eval₂ C q (C r)) = eval₂ C q (derivative (C r)) * derivative q

Tactic:
rw [eval₂_C, derivative_C, eval₂_zero, zero_mul]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
p q : R[X]
n : ℕ
r : R
ih : derivative (eval₂ C q (C r * X ^ n)) = eval₂ C q (derivative (C r * X ^ n)) * derivative q
⊢ derivative (eval₂ C q (C r * X ^ (n + 1))) = eval₂ C q (derivative (C r * X ^ (n + 1))) * derivative q

Tactic:
rw [pow_succ, ← mul_assoc, eval₂_mul, eval₂_X, derivative_mul, ih, @derivative_mul _ _ _ X,
  derivative_X, mul_one, eval₂_add, @eval₂_mul _ _ _ _ X, eval₂_X, add_mul, mul_right_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Int.lean
theorem of_not_lex {α} {r : α → α → Prop} [DecidableEq α] {β} {s : β → β → Prop}
    {p q : α × β} (w : ¬ Prod.Lex r s p q) :
    ¬ r p.fst q.fst ∧ (p.fst ≠ q.fst ∨ ¬ s p.snd q.snd)

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : DecidableEq α
β : Type u_2
s : β → β → Prop
p q : α × β
w : ¬r p.fst q.fst ∧ (¬p.fst = q.fst ∨ ¬s p.snd q.snd)
⊢ ¬r p.fst q.fst ∧ (p.fst ≠ q.fst ∨ ¬s p.snd q.snd)

Tactic:
exact w

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : DecidableEq α
β : Type u_2
s : β → β → Prop
p q : α × β
w : ¬Prod.Lex r s p q
⊢ ¬r p.fst q.fst ∧ (p.fst ≠ q.fst ∨ ¬s p.snd q.snd)

Tactic:
rw [Prod.lex_def, not_or, Decidable.not_and_iff_or_not_not] at w

Result:
α : Type u_1
r : α → α → Prop
inst✝ : DecidableEq α
β : Type u_2
s : β → β → Prop
p q : α × β
w : ¬r p.fst q.fst ∧ (¬p.fst = q.fst ∨ ¬s p.snd q.snd)
⊢ ¬r p.fst q.fst ∧ (p.fst ≠ q.fst ∨ ¬s p.snd q.snd)
-- Mathlib/Combinatorics/SimpleGraph/Density.lean
theorem edgeDensity_empty_left (t : Finset β) : edgeDensity r ∅ t = 0

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
t : Finset β
⊢ edgeDensity r ∅ t = 0

Tactic:
rw [edgeDensity, Finset.card_empty, Nat.cast_zero, zero_mul, div_zero]

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Alternating/Centralizer.lean
theorem card_of_cycleType_mul_eq (m : Multiset ℕ) :
    #({ g |  g.val.cycleType = m} : Finset (alternatingGroup α)) *
        ((Fintype.card α - m.sum)! * m.prod * (∏ n ∈ m.toFinset, (m.count n)!)) =
          if ((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + Multiset.card m))
          then (Fintype.card α)!
          else 0

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
⊢ (if Even (m.sum + m.card) then
      #(filter (fun g => g.cycleType = m) univ) *
        ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
    else 0) =
    if Even (m.sum + m.card) ∧ m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then (Fintype.card α)! else 0

Tactic:
rw [ite_and, Equiv.Perm.card_of_cycleType_mul_eq]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
⊢ #(filter (fun g => (↑g).cycleType = m) univ) *
      ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) =
    if (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card) then (Fintype.card α)! else 0

Tactic:
rw [← Finset.card_map, map_subtype_of_cycleType, apply_ite Finset.card,
  Finset.card_empty, ite_mul, zero_mul]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
⊢ (if Even (m.sum + m.card) then
      #(filter (fun g => g.cycleType = m) univ) *
        ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
    else 0) =
    if (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card) then (Fintype.card α)! else 0

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
⊢ (if Even (m.sum + m.card) then
      #(filter (fun g => g.cycleType = m) univ) *
        ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
    else 0) =
    if (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card) then (Fintype.card α)! else 0

Tactic:
simp only [and_comm (b := Even _)]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
⊢ (if Even (m.sum + m.card) then
      #(filter (fun g => g.cycleType = m) univ) *
        ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
    else 0) =
    if Even (m.sum + m.card) ∧ m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then (Fintype.card α)! else 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem isPrefixOfAux_toArray_succ' [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) (i : Nat) :
    Array.isPrefixOfAux l₁.toArray l₂.toArray hle (i + 1) =
      Array.isPrefixOfAux (l₁.drop (i+1)).toArray (l₂.drop (i+1)).toArray (by simp; omega) 0

Proof state:
α : Type ?u.80401
inst✝ : BEq α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
i : Nat
⊢ (drop (i + 1) l₁).toArray.size ≤ (drop (i + 1) l₂).toArray.size

Tactic:
simp

Result:
α : Type ?u.80401
inst✝ : BEq α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
i : Nat
⊢ l₁.length - (i + 1) ≤ l₂.length - (i + 1)

Proof state:
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
i : Nat
⊢ l₁.toArray.isPrefixOfAux l₂.toArray hle (i + 1) =
    (drop (i + 1) l₁).toArray.isPrefixOfAux (drop (i + 1) l₂).toArray ⋯ 0

Tactic:
induction i generalizing l₁ l₂ with
| zero => simp [isPrefixOfAux_toArray_succ]
| succ i ih =>
  rw [isPrefixOfAux_toArray_succ, ih]
  simp

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝ : BEq α
i : Nat
ih :
  ∀ (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length),
    l₁.toArray.isPrefixOfAux l₂.toArray hle (i + 1) =
      (drop (i + 1) l₁).toArray.isPrefixOfAux (drop (i + 1) l₂).toArray ⋯ 0
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
⊢ l₁.toArray.isPrefixOfAux l₂.toArray hle (i + 1 + 1) =
    (drop (i + 1 + 1) l₁).toArray.isPrefixOfAux (drop (i + 1 + 1) l₂).toArray ⋯ 0

Tactic:
rw [isPrefixOfAux_toArray_succ, ih]

Result:
case succ
α : Type u_1
inst✝ : BEq α
i : Nat
ih :
  ∀ (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length),
    l₁.toArray.isPrefixOfAux l₂.toArray hle (i + 1) =
      (drop (i + 1) l₁).toArray.isPrefixOfAux (drop (i + 1) l₂).toArray ⋯ 0
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
⊢ (drop (i + 1) l₁.tail).toArray.isPrefixOfAux (drop (i + 1) l₂.tail).toArray ⋯ 0 =
    (drop (i + 1 + 1) l₁).toArray.isPrefixOfAux (drop (i + 1 + 1) l₂).toArray ⋯ 0

Proof state:
case succ
α : Type u_1
inst✝ : BEq α
i : Nat
ih :
  ∀ (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length),
    l₁.toArray.isPrefixOfAux l₂.toArray hle (i + 1) =
      (drop (i + 1) l₁).toArray.isPrefixOfAux (drop (i + 1) l₂).toArray ⋯ 0
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
⊢ (drop (i + 1) l₁.tail).toArray.isPrefixOfAux (drop (i + 1) l₂.tail).toArray ⋯ 0 =
    (drop (i + 1 + 1) l₁).toArray.isPrefixOfAux (drop (i + 1 + 1) l₂).toArray ⋯ 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.80401
inst✝ : BEq α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
i : Nat
⊢ l₁.length - (i + 1) ≤ l₂.length - (i + 1)

Tactic:
omega

Result:
no goals

Proof state:
case zero
α : Type u_1
inst✝ : BEq α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
⊢ l₁.toArray.isPrefixOfAux l₂.toArray hle (0 + 1) =
    (drop (0 + 1) l₁).toArray.isPrefixOfAux (drop (0 + 1) l₂).toArray ⋯ 0

Tactic:
simp [isPrefixOfAux_toArray_succ]

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Defs.lean
theorem toLinearMap_injective {f g : M →ₑ+[σ.toMonoidHom] M₂}
    (h : (f : M →ₛₗ[σ] M₂) = (g : M →ₛₗ[σ] M₂)) :
    f = g

Proof state:
case a
R : Type u_1
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Semiring R
inst✝² : Module R M
inst✝¹ : Semiring S
inst✝ : Module S M₂
σ : R →+* S
f g : M →ₑ+[↑σ] M₂
h : ↑f = ↑g
m : M
⊢ f m = g m

Tactic:
exact LinearMap.congr_fun h m

Result:
no goals

Proof state:
R : Type u_1
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Semiring R
inst✝² : Module R M
inst✝¹ : Semiring S
inst✝ : Module S M₂
σ : R →+* S
f g : M →ₑ+[↑σ] M₂
h : ↑f = ↑g
⊢ f = g

Tactic:
ext m

Result:
case a
R : Type u_1
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Semiring R
inst✝² : Module R M
inst✝¹ : Semiring S
inst✝ : Module S M₂
σ : R →+* S
f g : M →ₑ+[↑σ] M₂
h : ↑f = ↑g
m : M
⊢ f m = g m
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem sub_ofNat' [NeZero n] (x : Fin n) (y : Nat) :
    x - Fin.ofNat' n y = Fin.ofNat' n ((n - y % n) + x.val)

Proof state:
case a
n : Nat
inst✝ : NeZero n
x : Fin n
y : Nat
⊢ ↑(x - Fin.ofNat' n y) = ↑(Fin.ofNat' n (n - y % n + ↑x))

Tactic:
simp [Fin.ofNat', Fin.sub_def]

Result:
no goals

Proof state:
n : Nat
inst✝ : NeZero n
x : Fin n
y : Nat
⊢ x - Fin.ofNat' n y = Fin.ofNat' n (n - y % n + ↑x)

Tactic:
apply Fin.eq_of_val_eq

Result:
case a
n : Nat
inst✝ : NeZero n
x : Fin n
y : Nat
⊢ ↑(x - Fin.ofNat' n y) = ↑(Fin.ofNat' n (n - y % n + ↑x))
-- Mathlib/RingTheory/Localization/FractionRing.lean
theorem lift_fieldRange_eq_of_range_eq (hg : Injective g)
    {s : Set L} (hs : g.range = Subring.closure s) :
    (lift hg : K →+* L).fieldRange = Subfield.closure s :=
  ringHom_fieldRange_eq_of_comp_eq_of_range_eq (by ext; simp) hs

Proof state:
A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
hg : Injective ⇑g
s : Set L
hs : g.range = Subring.closure s
⊢ (lift hg).comp (algebraMap A K) = g

Tactic:
ext

Result:
case a
A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
hg : Injective ⇑g
s : Set L
hs : g.range = Subring.closure s
x✝ : A
⊢ ((lift hg).comp (algebraMap A K)) x✝ = g x✝

Proof state:
case a
A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
hg : Injective ⇑g
s : Set L
hs : g.range = Subring.closure s
x✝ : A
⊢ ((lift hg).comp (algebraMap A K)) x✝ = g x✝

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Integral.lean
theorem Algebra.isAlgebraic_iff_isIntegral :
    Algebra.IsAlgebraic K A ↔ Algebra.IsIntegral K A

Proof state:
K : Type u
A : Type v
inst✝² : Field K
inst✝¹ : Ring A
inst✝ : Algebra K A
⊢ Algebra.IsAlgebraic K A ↔ Algebra.IsIntegral K A

Tactic:
rw [Algebra.isAlgebraic_def, Algebra.isIntegral_def,
    forall_congr' fun _ ↦ isAlgebraic_iff_isIntegral]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_of_append {l l₁ l₂ : Array α} (eq : l = l₁.push a ++ l₂) (h : l₁.size = i) :
    l[i]'(eq ▸ h ▸ by simp_arith) = a := Option.some.inj <| by
  rw [← getElem?_eq_getElem, eq, getElem?_append_left (by simp; omega), ← h]
  simp

Proof state:
α : Type ?u.237674
a : α
i : Nat
l l₁ l₂ : Array α
eq : l = l₁.push a ++ l₂
h : l₁.size = i
⊢ l₁.size < (l₁.push a ++ l₂).size

Tactic:
simp_arith

Result:
no goals

Proof state:
α : Type u_1
a : α
i : Nat
l l₁ l₂ : Array α
eq : l = l₁.push a ++ l₂
h : l₁.size = i
⊢ some l[i] = some a

Tactic:
rw [← getElem?_eq_getElem, eq, getElem?_append_left (by simp; omega), ← h]

Result:
α : Type u_1
a : α
i : Nat
l l₁ l₂ : Array α
eq : l = l₁.push a ++ l₂
h : l₁.size = i
⊢ (l₁.push a)[l₁.size]? = some a

Proof state:
α : Type u_1
a : α
i : Nat
l l₁ l₂ : Array α
eq : l = l₁.push a ++ l₂
h : l₁.size = i
⊢ i < l₁.size + 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
a : α
i : Nat
l l₁ l₂ : Array α
eq : l = l₁.push a ++ l₂
h : l₁.size = i
⊢ (l₁.push a)[l₁.size]? = some a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a : α
i : Nat
l l₁ l₂ : Array α
eq : l = l₁.push a ++ l₂
h : l₁.size = i
⊢ i < (l₁.push a).size

Tactic:
simp

Result:
α : Type u_1
a : α
i : Nat
l l₁ l₂ : Array α
eq : l = l₁.push a ++ l₂
h : l₁.size = i
⊢ i < l₁.size + 1
-- Mathlib/Analysis/RCLike/Lemmas.lean
theorem proper_rclike [FiniteDimensional K E] : ProperSpace E

Proof state:
K : Type u_1
E : Type u_2
inst✝³ : RCLike K
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace K E
inst✝ : FiniteDimensional K E
⊢ ProperSpace E

Tactic:
letI : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ K E

Result:
K : Type u_1
E : Type u_2
inst✝³ : RCLike K
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace K E
inst✝ : FiniteDimensional K E
this : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ K E
⊢ ProperSpace E

Proof state:
K : Type u_1
E : Type u_2
inst✝³ : RCLike K
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace K E
inst✝ : FiniteDimensional K E
this✝ : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ K E
this : FiniteDimensional ℝ E := trans ℝ K E
⊢ ProperSpace E

Tactic:
infer_instance

Result:
no goals

Proof state:
K : Type u_1
E : Type u_2
inst✝³ : RCLike K
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace K E
inst✝ : FiniteDimensional K E
this : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ K E
⊢ ProperSpace E

Tactic:
letI : FiniteDimensional ℝ E := FiniteDimensional.trans ℝ K E

Result:
K : Type u_1
E : Type u_2
inst✝³ : RCLike K
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace K E
inst✝ : FiniteDimensional K E
this✝ : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ K E
this : FiniteDimensional ℝ E := trans ℝ K E
⊢ ProperSpace E
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem inv_inr (m : M) : (inr m)⁻¹ = (0 : tsze R M)

Proof state:
case h2
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
m : M
⊢ (inr m)⁻¹.snd = snd 0

Tactic:
rw [snd_inv, snd_inr, fst_inr, inv_zero, op_zero, zero_smul, snd_zero, neg_zero]

Result:
no goals

Proof state:
case h1
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
m : M
⊢ (inr m)⁻¹.fst = fst 0

Tactic:
rw [fst_inv, fst_inr, fst_zero, inv_zero]

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
m : M
⊢ (inr m)⁻¹ = 0

Tactic:
ext

Result:
case h1
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
m : M
⊢ (inr m)⁻¹.fst = fst 0

case h2
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
m : M
⊢ (inr m)⁻¹.snd = snd 0
-- Mathlib/Algebra/Homology/Embedding/TruncGE.lean
@[reassoc (attr := simp)]
lemma d_comp_d (i j k : ι) : d K e i j ≫ d K e j k = 0

Proof state:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hij : c.Rel i j
hjk : ¬c.Rel j k
⊢ ((if hij : c.Rel i j then
        if hi : e.BoundaryGE i then (XIsoOpcycles K e hi).hom ≫ K.fromOpcycles (e.f i) (e.f j) ≫ (XIso K e ⋯).inv
        else (XIso K e hi).hom ≫ K.d (e.f i) (e.f j) ≫ (XIso K e ⋯).inv
      else 0) ≫
      if hij : c.Rel j k then
        if hi : e.BoundaryGE j then (XIsoOpcycles K e hi).hom ≫ K.fromOpcycles (e.f j) (e.f k) ≫ (XIso K e ⋯).inv
        else (XIso K e hi).hom ≫ K.d (e.f j) (e.f k) ≫ (XIso K e ⋯).inv
      else 0) =
    0

Tactic:
rw [dif_neg hjk, comp_zero]

Result:
no goals

Proof state:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hij : ¬c.Rel i j
⊢ ((if hij : c.Rel i j then
        if hi : e.BoundaryGE i then (XIsoOpcycles K e hi).hom ≫ K.fromOpcycles (e.f i) (e.f j) ≫ (XIso K e ⋯).inv
        else (XIso K e hi).hom ≫ K.d (e.f i) (e.f j) ≫ (XIso K e ⋯).inv
      else 0) ≫
      if hij : c.Rel j k then
        if hi : e.BoundaryGE j then (XIsoOpcycles K e hi).hom ≫ K.fromOpcycles (e.f j) (e.f k) ≫ (XIso K e ⋯).inv
        else (XIso K e hi).hom ≫ K.d (e.f j) (e.f k) ≫ (XIso K e ⋯).inv
      else 0) =
    0

Tactic:
rw [dif_neg hij, zero_comp]

Result:
no goals

Proof state:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ (if hi : e.BoundaryGE i then (XIsoOpcycles K e hi).hom ≫ K.fromOpcycles (e.f i) (e.f j) ≫ (XIso K e ⋯).inv
      else (XIso K e hi).hom ≫ K.d (e.f i) (e.f j) ≫ (XIso K e ⋯).inv) ≫
      (XIso K e ⋯).hom ≫ K.d (e.f j) (e.f k) ≫ (XIso K e ⋯).inv =
    0

Tactic:
split_ifs <;> simp

Result:
no goals
-- Mathlib/NumberTheory/LSeries/DirichletContinuation.lean
lemma deriv_LFunction_eq_deriv_LSeries (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) :
    deriv (LFunction χ) s = deriv (LSeries (χ ·)) s

Proof state:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
h : {z | 1 < z.re} ∈ 𝓝 s
⊢ LFunction χ =ᶠ[𝓝 s] LSeries fun x => χ ↑x

Tactic:
filter_upwards [h] with z hz

Result:
case h
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
h : {z | 1 < z.re} ∈ 𝓝 s
z : ℂ
hz : 1 < z.re
⊢ LFunction χ z = LSeries (fun x => χ ↑x) z

Proof state:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ deriv (LFunction χ) s = deriv (LSeries fun x => χ ↑x) s

Tactic:
refine Filter.EventuallyEq.deriv_eq ?_

Result:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ LFunction χ =ᶠ[𝓝 s] LSeries fun x => χ ↑x

Proof state:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ LFunction χ =ᶠ[𝓝 s] LSeries fun x => χ ↑x

Tactic:
have h : {z | 1 < z.re} ∈ nhds s :=
  (isOpen_lt continuous_const continuous_re).mem_nhds hs

Result:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
h : {z | 1 < z.re} ∈ 𝓝 s
⊢ LFunction χ =ᶠ[𝓝 s] LSeries fun x => χ ↑x

Proof state:
case h
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
h : {z | 1 < z.re} ∈ 𝓝 s
z : ℂ
hz : 1 < z.re
⊢ LFunction χ z = LSeries (fun x => χ ↑x) z

Tactic:
exact LFunction_eq_LSeries χ hz

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
lemma leftHomologyMap_comm [S₁.HasLeftHomology] [S₂.HasLeftHomology] :
    leftHomologyMap φ ≫ h₂.leftHomologyIso.hom = h₁.leftHomologyIso.hom ≫ γ.φH

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ leftHomologyMap φ ≫ h₂.leftHomologyIso.hom = h₁.leftHomologyIso.hom ≫ γ.φH

Tactic:
simp only [γ.leftHomologyMap_eq, assoc, Iso.inv_hom_id, comp_id]

Result:
no goals