harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem tendsto_card_div_pow₃ (hs₁ : IsBounded s)
    (hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s) :
    ∀ᶠ x : ℝ in atTop, (Nat.card ↑(s ∩ (⌊x⌋₊ : ℝ)⁻¹ • L) : ℝ) / x ^ card ι ≤
      (Nat.card ↑(s ∩ x⁻¹ • L) : ℝ) / x ^ card ι

Proof state:
case h
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x : ℝ
hx : 1 ≤ x
⊢ ↑(Nat.card ↑(s ∩ (↑⌊x⌋₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι ≤
    ↑(Nat.card ↑(s ∩ x⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι

Tactic:
gcongr

Result:
case h.hab.h
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x : ℝ
hx : 1 ≤ x
⊢ Nat.card ↑(s ∩ (↑⌊x⌋₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))) ≤
    Nat.card ↑(s ∩ x⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))

Proof state:
case h.hab.h
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x : ℝ
hx : 1 ≤ x
⊢ Nat.card ↑(s ∩ (↑⌊x⌋₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))) ≤
    Nat.card ↑(s ∩ x⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))

Tactic:
exact tendsto_card_div_pow₂ s hs₁ hs₄ (Nat.cast_pos.mpr (Nat.floor_pos.mpr hx))
  (Nat.floor_le (zero_le_one.trans hx))

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ ∀ᶠ (x : ℝ) in atTop,
    ↑(Nat.card ↑(s ∩ (↑⌊x⌋₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι ≤
      ↑(Nat.card ↑(s ∩ x⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι

Tactic:
filter_upwards [eventually_ge_atTop 1] with x hx

Result:
case h
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x : ℝ
hx : 1 ≤ x
⊢ ↑(Nat.card ↑(s ∩ (↑⌊x⌋₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι ≤
    ↑(Nat.card ↑(s ∩ x⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem head?_dropWhile_not (p : α → Bool) (l : List α) :
    match (l.dropWhile p).head? with | some x => p x = false | none => True

Proof state:
case nil
α : Type u_1
p : α → Bool
⊢ match (dropWhile p []).head? with
  | some x => p x = false
  | none => True

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  match (dropWhile p xs).head? with
  | some x => p x = false
  | none => True
⊢ match (dropWhile p (x :: xs)).head? with
  | some x => p x = false
  | none => True

Tactic:
simp only [dropWhile_cons]

Result:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  match (dropWhile p xs).head? with
  | some x => p x = false
  | none => True
⊢ match (if p x = true then dropWhile p xs else x :: xs).head? with
  | some x => p x = false
  | none => True

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ match (dropWhile p l).head? with
  | some x => p x = false
  | none => True

Tactic:
induction l with
| nil => simp
| cons x xs ih =>
  simp only [dropWhile_cons]
  split <;> rename_i h <;> split at h <;> simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  match (dropWhile p xs).head? with
  | some x => p x = false
  | none => True
⊢ match (if p x = true then dropWhile p xs else x :: xs).head? with
  | some x => p x = false
  | none => True

Tactic:
split <;> rename_i h <;> split at h <;> simp_all

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
theorem prod_eq_one_iff_of_one_le' :
    (∀ i ∈ s, 1 ≤ f i) → ((∏ i ∈ s, f i) = 1 ↔ ∀ i ∈ s, f i = 1)

Proof state:
ι : Type u_1
N : Type u_5
inst✝ : OrderedCommMonoid N
f : ι → N
s✝ : Finset ι
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, 1 ≤ f i) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)
H : ∀ i ∈ insert a s, 1 ≤ f i
this : ∀ i ∈ s, 1 ≤ f i
⊢ ∏ i ∈ insert a s, f i = 1 ↔ ∀ i ∈ insert a s, f i = 1

Tactic:
rw [prod_insert ha, mul_eq_one_iff_of_one_le (H _ <| mem_insert_self _ _) (one_le_prod' this),
  forall_mem_insert, ih this]

Result:
no goals

Proof state:
ι : Type u_1
N : Type u_5
inst✝ : OrderedCommMonoid N
f : ι → N
s : Finset ι
⊢ (∀ i ∈ s, 1 ≤ f i) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)

Tactic:
classical
  refine Finset.induction_on s
    (fun _ ↦ ⟨fun _ _ h ↦ False.elim (Finset.not_mem_empty _ h), fun _ ↦ rfl⟩) ?_
  intro a s ha ih H
  have : ∀ i ∈ s, 1 ≤ f i := fun _ ↦ H _ ∘ mem_insert_of_mem
  rw [prod_insert ha, mul_eq_one_iff_of_one_le (H _ <| mem_insert_self _ _) (one_le_prod' this),
    forall_mem_insert, ih this]

Result:
no goals

Proof state:
ι : Type u_1
N : Type u_5
inst✝ : OrderedCommMonoid N
f : ι → N
s : Finset ι
⊢ (∀ i ∈ s, 1 ≤ f i) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)

Tactic:
refine Finset.induction_on s
  (fun _ ↦ ⟨fun _ _ h ↦ False.elim (Finset.not_mem_empty _ h), fun _ ↦ rfl⟩) ?_

Result:
ι : Type u_1
N : Type u_5
inst✝ : OrderedCommMonoid N
f : ι → N
s : Finset ι
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    a ∉ s →
      ((∀ i ∈ s, 1 ≤ f i) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)) →
        (∀ i ∈ insert a s, 1 ≤ f i) → (∏ i ∈ insert a s, f i = 1 ↔ ∀ i ∈ insert a s, f i = 1)

Proof state:
ι : Type u_1
N : Type u_5
inst✝ : OrderedCommMonoid N
f : ι → N
s : Finset ι
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    a ∉ s →
      ((∀ i ∈ s, 1 ≤ f i) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)) →
        (∀ i ∈ insert a s, 1 ≤ f i) → (∏ i ∈ insert a s, f i = 1 ↔ ∀ i ∈ insert a s, f i = 1)

Tactic:
intro a s ha ih H

Result:
ι : Type u_1
N : Type u_5
inst✝ : OrderedCommMonoid N
f : ι → N
s✝ : Finset ι
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, 1 ≤ f i) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)
H : ∀ i ∈ insert a s, 1 ≤ f i
⊢ ∏ i ∈ insert a s, f i = 1 ↔ ∀ i ∈ insert a s, f i = 1

Proof state:
ι : Type u_1
N : Type u_5
inst✝ : OrderedCommMonoid N
f : ι → N
s✝ : Finset ι
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, 1 ≤ f i) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)
H : ∀ i ∈ insert a s, 1 ≤ f i
⊢ ∏ i ∈ insert a s, f i = 1 ↔ ∀ i ∈ insert a s, f i = 1

Tactic:
have : ∀ i ∈ s, 1 ≤ f i := fun _ ↦ H _ ∘ mem_insert_of_mem

Result:
ι : Type u_1
N : Type u_5
inst✝ : OrderedCommMonoid N
f : ι → N
s✝ : Finset ι
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, 1 ≤ f i) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)
H : ∀ i ∈ insert a s, 1 ≤ f i
this : ∀ i ∈ s, 1 ≤ f i
⊢ ∏ i ∈ insert a s, f i = 1 ↔ ∀ i ∈ insert a s, f i = 1
-- Mathlib/RingTheory/PowerSeries/Order.lean
theorem min_order_le_order_add (φ ψ : R⟦X⟧) : min (order φ) (order ψ) ≤ order (φ + ψ)

Proof state:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
⊢ ∀ (i : ℕ), ↑i < φ.order ⊓ ψ.order → (coeff R i) (φ + ψ) = 0

Tactic:
simp +contextual [coeff_of_lt_order]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
⊢ φ.order ⊓ ψ.order ≤ (φ + ψ).order

Tactic:
refine le_order _ _ ?_

Result:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
⊢ ∀ (i : ℕ), ↑i < φ.order ⊓ ψ.order → (coeff R i) (φ + ψ) = 0
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isSeparator_op_iff (G : C) : IsSeparator (op G) ↔ IsCoseparator G

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

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

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

Proof state:
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
⊢ f x = f y ↔ y⁻¹ * x ∈ f.ker

Tactic:
constructor <;> intro h

Result:
case mp
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : f x = f y
⊢ y⁻¹ * x ∈ f.ker

case mpr
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : y⁻¹ * x ∈ f.ker
⊢ f x = f y

Proof state:
case mpr
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : y⁻¹ * x ∈ f.ker
⊢ f x = f y

Tactic:
rw [← one_mul x, ← mul_inv_cancel y, mul_assoc, map_mul, mem_ker.1 h, mul_one]

Result:
no goals

Proof state:
case mp
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : f x = f y
⊢ y⁻¹ * x ∈ f.ker

Tactic:
rw [mem_ker, map_mul, h, ← map_mul, inv_mul_cancel, map_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lcm.lean
theorem lcm_ne_zero (hm : m ≠ 0) (hn : n ≠ 0) : lcm m n ≠ 0

Proof state:
m n : Nat
hm : m ≠ 0
hn : n ≠ 0
h : m.lcm n = 0
h1 : 0 = m * n
hn1 : n = 0
⊢ False

Tactic:
exact hn hn1

Result:
no goals

Proof state:
m n : Nat
hm : m ≠ 0
hn : n ≠ 0
h : m.lcm n = 0
h1 : 0 = m * n
⊢ False

Tactic:
match mul_eq_zero.1 h1.symm with
| .inl hm1 => exact hm hm1
| .inr hn1 => exact hn hn1

Result:
no goals

Proof state:
m n : Nat
hm : m ≠ 0
hn : n ≠ 0
h : m.lcm n = 0
⊢ False

Tactic:
have h1 := gcd_mul_lcm m n

Result:
m n : Nat
hm : m ≠ 0
hn : n ≠ 0
h : m.lcm n = 0
h1 : m.gcd n * m.lcm n = m * n
⊢ False

Proof state:
m n : Nat
hm : m ≠ 0
hn : n ≠ 0
⊢ m.lcm n ≠ 0

Tactic:
intro h

Result:
m n : Nat
hm : m ≠ 0
hn : n ≠ 0
h : m.lcm n = 0
⊢ False

Proof state:
m n : Nat
hm : m ≠ 0
hn : n ≠ 0
h : m.lcm n = 0
h1 : 0 = m * n
hm1 : m = 0
⊢ False

Tactic:
exact hm hm1

Result:
no goals

Proof state:
m n : Nat
hm : m ≠ 0
hn : n ≠ 0
h : m.lcm n = 0
h1 : m.gcd n * m.lcm n = m * n
⊢ False

Tactic:
rw [h, Nat.mul_zero] at h1

Result:
m n : Nat
hm : m ≠ 0
hn : n ≠ 0
h : m.lcm n = 0
h1 : 0 = m * n
⊢ False
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem apply_eq_of_lt_firstDiff {x y : ∀ n, E n} {n : ℕ} (hn : n < firstDiff x y) : x n = y n

Proof state:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hn : n < if h : x ≠ y then Nat.find ⋯ else 0
⊢ x n = y n

Tactic:
split_ifs at hn with h

Result:
case pos
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : x ≠ y
hn : n < Nat.find ⋯
⊢ x n = y n

case neg
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : ¬x ≠ y
hn : n < 0
⊢ x n = y n

Proof state:
case neg
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : ¬x ≠ y
hn : n < 0
⊢ x n = y n

Tactic:
exact (not_lt_zero' hn).elim

Result:
no goals

Proof state:
case a
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : x ≠ y
hn : n < Nat.find ⋯
⊢ x n = y n ↔ ¬x n ≠ y n

Tactic:
simp

Result:
no goals

Proof state:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hn : n < firstDiff x y
⊢ x n = y n

Tactic:
rw [firstDiff_def] at hn

Result:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hn : n < if h : x ≠ y then Nat.find ⋯ else 0
⊢ x n = y n

Proof state:
case pos
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : x ≠ y
hn : n < Nat.find ⋯
⊢ x n = y n

Tactic:
convert Nat.find_min (ne_iff.1 h) hn

Result:
case a
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : x ≠ y
hn : n < Nat.find ⋯
⊢ x n = y n ↔ ¬x n ≠ y n
-- Mathlib/RingTheory/Valuation/ValuationRing.lean
theorem _root_.PreValuationRing.iff_ideal_total [CommRing R] :
    PreValuationRing R ↔ IsTotal (Ideal R) (· ≤ ·)

Proof state:
R : Type u_1
inst✝ : CommRing R
H : IsTotal (Ideal R) fun x1 x2 => x1 ≤ x2
a b : R
this : b ∣ a ∨ a ∣ b
⊢ a ∣ b ∨ b ∣ a

Tactic:
exact this.symm

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ PreValuationRing R ↔ IsTotal (Ideal R) fun x1 x2 => x1 ≤ x2

Tactic:
refine ⟨fun _ => ⟨le_total⟩, fun H => PreValuationRing.iff_dvd_total.mpr ⟨fun a b => ?_⟩⟩

Result:
R : Type u_1
inst✝ : CommRing R
H : IsTotal (Ideal R) fun x1 x2 => x1 ≤ x2
a b : R
⊢ a ∣ b ∨ b ∣ a

Proof state:
R : Type u_1
inst✝ : CommRing R
H : IsTotal (Ideal R) fun x1 x2 => x1 ≤ x2
a b : R
⊢ a ∣ b ∨ b ∣ a

Tactic:
have := @IsTotal.total _ _ H (Ideal.span {a}) (Ideal.span {b})

Result:
R : Type u_1
inst✝ : CommRing R
H : IsTotal (Ideal R) fun x1 x2 => x1 ≤ x2
a b : R
this : Ideal.span {a} ≤ Ideal.span {b} ∨ Ideal.span {b} ≤ Ideal.span {a}
⊢ a ∣ b ∨ b ∣ a

Proof state:
R : Type u_1
inst✝ : CommRing R
H : IsTotal (Ideal R) fun x1 x2 => x1 ≤ x2
a b : R
this : Ideal.span {a} ≤ Ideal.span {b} ∨ Ideal.span {b} ≤ Ideal.span {a}
⊢ a ∣ b ∨ b ∣ a

Tactic:
simp_rw [Ideal.span_singleton_le_span_singleton] at this

Result:
R : Type u_1
inst✝ : CommRing R
H : IsTotal (Ideal R) fun x1 x2 => x1 ≤ x2
a b : R
this : b ∣ a ∨ a ∣ b
⊢ a ∣ b ∨ b ∣ a

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ PreValuationRing R ↔ IsTotal (Ideal R) fun x1 x2 => x1 ≤ x2

Tactic:
classical
refine ⟨fun _ => ⟨le_total⟩, fun H => PreValuationRing.iff_dvd_total.mpr ⟨fun a b => ?_⟩⟩
have := @IsTotal.total _ _ H (Ideal.span {a}) (Ideal.span {b})
simp_rw [Ideal.span_singleton_le_span_singleton] at this
exact this.symm

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem box_index_tag_eq_self {B I : Box ι} (hI : I ∈ (prepartition n B).boxes) :
    box n (index n ((prepartition n B).tag I)) = I

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B I : Box ι
hI : I ∈ (prepartition n B).boxes
⊢ box n (index n ((prepartition n B).tag I)) = I

Tactic:
obtain ⟨ν, hν, rfl⟩ := mem_prepartition_boxes_iff.mp hI

Result:
case intro.intro
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ (prepartition n B).boxes
⊢ box n (index n ((prepartition n B).tag (box n ν))) = box n ν

Proof state:
case intro.intro
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B : Box ι
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ (prepartition n B).boxes
⊢ box n (index n ((prepartition n B).tag (box n ν))) = box n ν

Tactic:
rw [prepartition_tag n hν, index_tag]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Basic.lean
theorem size_eraseIdx (a : Array α) (i : Nat) (h) : (a.eraseIdx i h).size = a.size - 1

Proof state:
case case1
α : Type u
a✝ : Array α
i✝ : Nat
a : Array α
i : Nat
h : autoParam (i < a.size) _auto✝
h' : i + 1 < a.size
a' : Array α := a.swap (i + 1) i h' h
ih : (a'.eraseIdx (i + 1) ⋯).size = a'.size - 1
⊢ (if h' : i + 1 < a.size then
        let a' := a.swap (i + 1) i h' h;
        a'.eraseIdx (i + 1) ⋯
      else a.pop).size =
    a.size - 1

Tactic:
simp +zetaDelta [h', a', ih]

Result:
no goals

Proof state:
case case1
α : Type u
a✝ : Array α
i✝ : Nat
a : Array α
i : Nat
h : autoParam (i < a.size) _auto✝
h' : i + 1 < a.size
a' : Array α := a.swap (i + 1) i h' h
ih : (a'.eraseIdx (i + 1) ⋯).size = a'.size - 1
⊢ (a.eraseIdx i h).size = a.size - 1

Tactic:
unfold eraseIdx

Result:
case case1
α : Type u
a✝ : Array α
i✝ : Nat
a : Array α
i : Nat
h : autoParam (i < a.size) _auto✝
h' : i + 1 < a.size
a' : Array α := a.swap (i + 1) i h' h
ih : (a'.eraseIdx (i + 1) ⋯).size = a'.size - 1
⊢ (if h' : i + 1 < a.size then
        let a' := a.swap (i + 1) i h' h;
        a'.eraseIdx (i + 1) ⋯
      else a.pop).size =
    a.size - 1

Proof state:
case case2
α : Type u
a✝ : Array α
i✝ : Nat
a : Array α
i : Nat
h : autoParam (i < a.size) _auto✝
h' : ¬i + 1 < a.size
⊢ (a.eraseIdx i h).size = a.size - 1

Tactic:
unfold eraseIdx

Result:
case case2
α : Type u
a✝ : Array α
i✝ : Nat
a : Array α
i : Nat
h : autoParam (i < a.size) _auto✝
h' : ¬i + 1 < a.size
⊢ (if h' : i + 1 < a.size then
        let a' := a.swap (i + 1) i h' h;
        a'.eraseIdx (i + 1) ⋯
      else a.pop).size =
    a.size - 1

Proof state:
α : Type u
a : Array α
i : Nat
h : i < a.size
⊢ (a.eraseIdx i h).size = a.size - 1

Tactic:
induction a, i, h using Array.eraseIdx.induct with
| @case1 a i h h' a' ih =>
  unfold eraseIdx
  simp +zetaDelta [h', a', ih]
| case2 a i h h' =>
  unfold eraseIdx
  simp [h']

Result:
no goals

Proof state:
case case2
α : Type u
a✝ : Array α
i✝ : Nat
a : Array α
i : Nat
h : autoParam (i < a.size) _auto✝
h' : ¬i + 1 < a.size
⊢ (if h' : i + 1 < a.size then
        let a' := a.swap (i + 1) i h' h;
        a'.eraseIdx (i + 1) ⋯
      else a.pop).size =
    a.size - 1

Tactic:
simp [h']

Result:
no goals
-- Mathlib/RingTheory/Idempotents.lean
lemma OrthogonalIdempotents.isIdempotentElem_sum (he : OrthogonalIdempotents e) {s : Finset I} :
    IsIdempotentElem (∑ i ∈ s, e i)

Proof state:
R : Type u_1
inst✝ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
s : Finset I
⊢ IsIdempotentElem (∑ i ∈ s, e i)

Tactic:
simp [IsIdempotentElem, Finset.sum_mul, Finset.mul_sum, he.mul_eq]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
s : Finset I
⊢ IsIdempotentElem (∑ i ∈ s, e i)

Tactic:
classical
simp [IsIdempotentElem, Finset.sum_mul, Finset.mul_sum, he.mul_eq]

Result:
no goals
-- Mathlib/SetTheory/Game/Domineering.lean
theorem moveLeft_card {b : Board} {m : ℤ × ℤ} (h : m ∈ left b) :
    Finset.card (moveLeft b m) + 2 = Finset.card b

Proof state:
b : Board
m : ℤ × ℤ
h : m ∈ left b
⊢ Finset.card (moveLeft b m) + 2 = Finset.card b

Tactic:
dsimp only [moveLeft]

Result:
b : Board
m : ℤ × ℤ
h : m ∈ left b
⊢ ((Finset.erase b m).erase (m.1, m.2 - 1)).card + 2 = Finset.card b

Proof state:
b : Board
m : ℤ × ℤ
h : m ∈ left b
⊢ (Finset.erase b m).card - 1 + 2 = Finset.card b

Tactic:
rw [Finset.card_erase_of_mem (Finset.mem_of_mem_inter_left h)]

Result:
b : Board
m : ℤ × ℤ
h : m ∈ left b
⊢ Finset.card b - 1 - 1 + 2 = Finset.card b

Proof state:
b : Board
m : ℤ × ℤ
h : m ∈ left b
⊢ ((Finset.erase b m).erase (m.1, m.2 - 1)).card + 2 = Finset.card b

Tactic:
rw [Finset.card_erase_of_mem (snd_pred_mem_erase_of_mem_left h)]

Result:
b : Board
m : ℤ × ℤ
h : m ∈ left b
⊢ (Finset.erase b m).card - 1 + 2 = Finset.card b

Proof state:
b : Board
m : ℤ × ℤ
h : m ∈ left b
⊢ Finset.card b - 1 - 1 + 2 = Finset.card b

Tactic:
exact tsub_add_cancel_of_le (card_of_mem_left h)

Result:
no goals
-- Mathlib/Algebra/Lie/Quotient.lean
theorem mk'_ker : (mk' N).ker = N

Proof state:
case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
m✝ : M
⊢ m✝ ∈ (mk' N).ker ↔ m✝ ∈ N

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
⊢ (mk' N).ker = N

Tactic:
ext

Result:
case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
m✝ : M
⊢ m✝ ∈ (mk' N).ker ↔ m✝ ∈ N
-- Mathlib/LinearAlgebra/PerfectPairing/Basic.lean
@[simp] lemma flip_flip (h : IsReflexive R N := isReflexive_of_equiv_dual_of_isReflexive e) :
    e.flip.flip = e

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
h : optParam (IsReflexive R N) ⋯
⊢ e.flip.flip = e

Tactic:
ext

Result:
case h.h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
h : optParam (IsReflexive R N) ⋯
x✝¹ : N
x✝ : M
⊢ (e.flip.flip x✝¹) x✝ = (e x✝¹) x✝

Proof state:
case h.h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
h : optParam (IsReflexive R N) ⋯
x✝¹ : N
x✝ : M
⊢ (e.flip.flip x✝¹) x✝ = (e x✝¹) x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean
@[simp]
lemma ranAdjunction_counit : (L.ranAdjunction H).counit = L.ranCounit

Proof state:
case w.h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_6, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{u_5, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
F : C ⥤ H
⊢ (L.ranAdjunction H).counit.app F = L.ranCounit.app F

Tactic:
dsimp [ranAdjunction, homEquivOfIsRightKanExtension]

Result:
case w.h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_6, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{u_5, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
F : C ⥤ H
⊢ 𝟙 (L ⋙ L.ran.obj F) ≫ L.ranCounit.app F = L.ranCounit.app F

Proof state:
case w.h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_6, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{u_5, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
F : C ⥤ H
⊢ 𝟙 (L ⋙ L.ran.obj F) ≫ L.ranCounit.app F = L.ranCounit.app F

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_6, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{u_5, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
⊢ (L.ranAdjunction H).counit = L.ranCounit

Tactic:
ext F : 2

Result:
case w.h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_6, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{u_5, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
F : C ⥤ H
⊢ (L.ranAdjunction H).counit.app F = L.ranCounit.app F
-- Mathlib/RingTheory/Radical.lean
theorem divRadical_mul {a b : E} (hab : IsCoprime a b) :
    divRadical (a * b) = divRadical a * divRadical b

Proof state:
E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a b : E
hab : IsCoprime a b
⊢ divRadical (a * b) = divRadical a * divRadical b

Tactic:
symm

Result:
E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a b : E
hab : IsCoprime a b
⊢ divRadical a * divRadical b = divRadical (a * b)

Proof state:
case h
E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a b : E
hab : IsCoprime a b
⊢ radical (a * b) * (divRadical a * divRadical b) = a * b

Tactic:
rw [radical_mul hab]

Result:
case h
E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a b : E
hab : IsCoprime a b
⊢ radical a * radical b * (divRadical a * divRadical b) = a * b

Proof state:
case h
E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a b : E
hab : IsCoprime a b
⊢ radical a * radical b * (divRadical a * divRadical b) = a * b

Tactic:
rw [mul_mul_mul_comm, radical_mul_divRadical, radical_mul_divRadical]

Result:
no goals

Proof state:
E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a b : E
hab : IsCoprime a b
⊢ divRadical a * divRadical b = divRadical (a * b)

Tactic:
apply eq_divRadical

Result:
case h
E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a b : E
hab : IsCoprime a b
⊢ radical (a * b) * (divRadical a * divRadical b) = a * b
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem map_neighborFinset_induce (v : s) :
    ((G.induce s).neighborFinset v).map (.subtype s)
      = G.neighborFinset v ∩ s.toFinset

Proof state:
case h
V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x => x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : ↑s
a✝ : V
⊢ a✝ ∈ map (Embedding.subtype s) ((induce s G).neighborFinset v) ↔ a✝ ∈ G.neighborFinset ↑v ∩ s.toFinset

Tactic:
simp [Set.mem_def]

Result:
no goals

Proof state:
V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x => x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : ↑s
⊢ map (Embedding.subtype s) ((induce s G).neighborFinset v) = G.neighborFinset ↑v ∩ s.toFinset

Tactic:
ext

Result:
case h
V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x => x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : ↑s
a✝ : V
⊢ a✝ ∈ map (Embedding.subtype s) ((induce s G).neighborFinset v) ↔ a✝ ∈ G.neighborFinset ↑v ∩ s.toFinset