harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/Rotate.lean
theorem reverse_rotate (l : List α) (n : ℕ) :
    (l.rotate n).reverse = l.reverse.rotate (l.length - n % l.length)

Proof state:
case zero
α : Type u
l : List α
⊢ (l.rotate 0).reverse.rotate 0 = l.reverse

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
l : List α
n : ℕ
⊢ (l.rotate n).reverse.rotate n = l.reverse

Tactic:
induction' n with n hn generalizing l

Result:
case zero
α : Type u
l : List α
⊢ (l.rotate 0).reverse.rotate 0 = l.reverse

case succ
α : Type u
n : ℕ
hn : ∀ (l : List α), (l.rotate n).reverse.rotate n = l.reverse
l : List α
⊢ (l.rotate (n + 1)).reverse.rotate (n + 1) = l.reverse

Proof state:
α : Type u
l : List α
n : ℕ
⊢ (l.rotate n).reverse = l.reverse.rotate (l.length - n % l.length)

Tactic:
rw [← length_reverse l, ← rotate_eq_iff]

Result:
α : Type u
l : List α
n : ℕ
⊢ (l.rotate n).reverse.rotate n = l.reverse

Proof state:
case succ.nil
α : Type u
n : ℕ
hn : ∀ (l : List α), (l.rotate n).reverse.rotate n = l.reverse
⊢ ([].rotate (n + 1)).reverse.rotate (n + 1) = [].reverse

Tactic:
simp

Result:
no goals

Proof state:
case succ.cons
α : Type u
n : ℕ
hn : ∀ (l : List α), (l.rotate n).reverse.rotate n = l.reverse
hd : α
tl : List α
⊢ (tl ++ [hd]).reverse.rotate 1 = (hd :: tl).reverse

Tactic:
simp

Result:
no goals

Proof state:
case succ
α : Type u
n : ℕ
hn : ∀ (l : List α), (l.rotate n).reverse.rotate n = l.reverse
l : List α
⊢ (l.rotate (n + 1)).reverse.rotate (n + 1) = l.reverse

Tactic:
rcases l with - | ⟨hd, tl⟩

Result:
case succ.nil
α : Type u
n : ℕ
hn : ∀ (l : List α), (l.rotate n).reverse.rotate n = l.reverse
⊢ ([].rotate (n + 1)).reverse.rotate (n + 1) = [].reverse

case succ.cons
α : Type u
n : ℕ
hn : ∀ (l : List α), (l.rotate n).reverse.rotate n = l.reverse
hd : α
tl : List α
⊢ ((hd :: tl).rotate (n + 1)).reverse.rotate (n + 1) = (hd :: tl).reverse

Proof state:
case succ.cons
α : Type u
n : ℕ
hn : ∀ (l : List α), (l.rotate n).reverse.rotate n = l.reverse
hd : α
tl : List α
⊢ ((hd :: tl).rotate (n + 1)).reverse.rotate (n + 1) = (hd :: tl).reverse

Tactic:
rw [rotate_cons_succ, ← rotate_rotate, hn]

Result:
case succ.cons
α : Type u
n : ℕ
hn : ∀ (l : List α), (l.rotate n).reverse.rotate n = l.reverse
hd : α
tl : List α
⊢ (tl ++ [hd]).reverse.rotate 1 = (hd :: tl).reverse
-- Mathlib/RingTheory/Filtration.lean
theorem pow_smul_le (i j : ℕ) : I ^ i • F.N j ≤ F.N (i + j)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
i j : ℕ
⊢ I ^ i • F.N j ≤ F.N (i + j)

Tactic:
induction' i with _ ih

Result:
case zero
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
j : ℕ
⊢ I ^ 0 • F.N j ≤ F.N (0 + j)

case succ
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
j n✝ : ℕ
ih : I ^ n✝ • F.N j ≤ F.N (n✝ + j)
⊢ I ^ (n✝ + 1) • F.N j ≤ F.N (n✝ + 1 + j)

Proof state:
case succ
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
j n✝ : ℕ
ih : I ^ n✝ • F.N j ≤ F.N (n✝ + j)
⊢ I • I ^ n✝ • F.N j ≤ F.N (n✝ + j + 1)

Tactic:
exact (smul_mono_right _ ih).trans (F.smul_le _)

Result:
no goals

Proof state:
case succ
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
j n✝ : ℕ
ih : I ^ n✝ • F.N j ≤ F.N (n✝ + j)
⊢ I ^ (n✝ + 1) • F.N j ≤ F.N (n✝ + 1 + j)

Tactic:
rw [pow_succ', mul_smul, add_assoc, add_comm 1, ← add_assoc]

Result:
case succ
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
j n✝ : ℕ
ih : I ^ n✝ • F.N j ≤ F.N (n✝ + j)
⊢ I • I ^ n✝ • F.N j ≤ F.N (n✝ + j + 1)

Proof state:
case zero
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
j : ℕ
⊢ I ^ 0 • F.N j ≤ F.N (0 + j)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem mul_limZero_left {f} (g : CauSeq β abv) (hg : LimZero f) : LimZero (f * g)
  | ε, ε0 =>
    let ⟨G, G0, hG⟩ := g.bounded' 0
    (hg _ <| div_pos ε0 G0).imp fun _ H j ij => by
      have := mul_lt_mul'' (H _ ij) (hG j) (abv_nonneg abv _) (abv_nonneg abv _)
      rwa [div_mul_cancel₀ _ (ne_of_gt G0), ← abv_mul] at this

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hg : f.LimZero
ε : α
ε0 : ε > 0
G : α
G0 : G > 0
hG : ∀ (i : ℕ), abv (↑g i) < G
x✝ : ℕ
H : ∀ j ≥ x✝, abv (↑f j) < ε / G
j : ℕ
ij : j ≥ x✝
this : abv (↑f j) * abv (↑g j) < ε / G * G
⊢ abv (↑(f * g) j) < ε

Tactic:
rwa [div_mul_cancel₀ _ (ne_of_gt G0), ← abv_mul] at this

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hg : f.LimZero
ε : α
ε0 : ε > 0
G : α
G0 : G > 0
hG : ∀ (i : ℕ), abv (↑g i) < G
x✝ : ℕ
H : ∀ j ≥ x✝, abv (↑f j) < ε / G
j : ℕ
ij : j ≥ x✝
⊢ abv (↑(f * g) j) < ε

Tactic:
have := mul_lt_mul'' (H _ ij) (hG j) (abv_nonneg abv _) (abv_nonneg abv _)

Result:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hg : f.LimZero
ε : α
ε0 : ε > 0
G : α
G0 : G > 0
hG : ∀ (i : ℕ), abv (↑g i) < G
x✝ : ℕ
H : ∀ j ≥ x✝, abv (↑f j) < ε / G
j : ℕ
ij : j ≥ x✝
this : abv (↑f j) * abv (↑g j) < ε / G * G
⊢ abv (↑(f * g) j) < ε
-- Mathlib/Analysis/PSeries.lean
theorem tsum_condensed_le (hf : ∀ ⦃m n⦄, 1 < m → m ≤ n → f n ≤ f m) :
    (∑' k : ℕ, 2 ^ k * f (2 ^ k)) ≤ f 1 + 2 * ∑' k, f k

Proof state:
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
⊢ ⨆ i, ∑ a ∈ range i.succ, 2 ^ a * f (2 ^ a) ≤ f 1 + 2 • ∑' (k : ℕ), f k

Tactic:
refine
  iSup_le fun n =>
    le_trans ?_
      (add_le_add_left
        (nsmul_le_nsmul_right (ENNReal.sum_le_tsum <| Finset.Ico 2 (2 ^ n + 1)) _) _)

Result:
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ a ∈ range n.succ, 2 ^ a * f (2 ^ a) ≤ f 1 + 2 • ∑ x ∈ Ico 2 (2 ^ n + 1), f x

Proof state:
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ a ∈ range n.succ, 2 ^ a * f (2 ^ a) ≤ f 1 + 2 • ∑ x ∈ Ico 2 (2 ^ n + 1), f x

Tactic:
simpa using Finset.sum_condensed_le hf n

Result:
no goals

Proof state:
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
⊢ ∑' (k : ℕ), 2 ^ k * f (2 ^ k) ≤ f 1 + 2 * ∑' (k : ℕ), f k

Tactic:
rw [ENNReal.tsum_eq_iSup_nat' (tendsto_atTop_mono Nat.le_succ tendsto_id), two_mul, ← two_nsmul]

Result:
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
⊢ ⨆ i, ∑ a ∈ range i.succ, 2 ^ a * f (2 ^ a) ≤ f 1 + 2 • ∑' (k : ℕ), f k
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Gcd.lean
theorem gcd_rec (m n : Nat) : gcd m n = gcd (n % m) m :=
  match m with
  | 0 => by have := (mod_zero n).symm; rwa [gcd, gcd_zero_right]
  | _ + 1 => by simp [gcd_succ]

Proof state:
m n : Nat
this : n = n % 0
⊢ gcd 0 n = (n % 0).gcd 0

Tactic:
rwa [gcd, gcd_zero_right]

Result:
no goals

Proof state:
m n : Nat
⊢ gcd 0 n = (n % 0).gcd 0

Tactic:
have := (mod_zero n).symm

Result:
m n : Nat
this : n = n % 0
⊢ gcd 0 n = (n % 0).gcd 0

Proof state:
m n n✝ : Nat
⊢ (n✝ + 1).gcd n = (n % (n✝ + 1)).gcd (n✝ + 1)

Tactic:
simp [gcd_succ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem eraseP_filterMap (f : α → Option β) (l : Array α) :
    (filterMap f l).eraseP p = filterMap f (l.eraseP (fun x => match f x with | some y => p y | none => false))

Proof state:
α : Type u_1
β : Type u_2
p : β → Bool
f : α → Option β
l : Array α
⊢ (filterMap f l).eraseP p =
    filterMap f
      (l.eraseP fun x =>
        match f x with
        | some y => p y
        | none => false)

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
p : β → Bool
f : α → Option β
l : List α
⊢ (filterMap f { toList := l }).eraseP p =
    filterMap f
      ({ toList := l }.eraseP fun x =>
        match f x with
        | some y => p y
        | none => false)

Proof state:
case mk
α : Type u_1
β : Type u_2
p : β → Bool
f : α → Option β
l : List α
⊢ (filterMap f { toList := l }).eraseP p =
    filterMap f
      ({ toList := l }.eraseP fun x =>
        match f x with
        | some y => p y
        | none => false)

Tactic:
simpa using List.eraseP_filterMap f l

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Periodic.lean
theorem tendsto_atBot_intervalIntegral_of_pos (h₀ : 0 < ∫ x in (0)..T, g x) (hT : 0 < T) :
    Tendsto (fun t => ∫ x in (0)..t, g x) atBot atBot

Proof state:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h₀ : 0 < ∫ (x : ℝ) in 0 ..T, g x
hT : 0 < T
h_int : IntervalIntegrable g volume 0 T
⊢ Tendsto (fun t => ∫ (x : ℝ) in 0 ..t, g x) atBot atBot

Tactic:
apply tendsto_atBot_mono (hg.integral_le_sSup_add_zsmul_of_pos h_int hT)

Result:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h₀ : 0 < ∫ (x : ℝ) in 0 ..T, g x
hT : 0 < T
h_int : IntervalIntegrable g volume 0 T
⊢ Tendsto (fun n => sSup ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Icc 0 T) + ⌊n / T⌋ • ∫ (x : ℝ) in 0 ..T, g x) atBot
    atBot

Proof state:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h₀ : 0 < ∫ (x : ℝ) in 0 ..T, g x
hT : 0 < T
⊢ Tendsto (fun t => ∫ (x : ℝ) in 0 ..t, g x) atBot atBot

Tactic:
have h_int := intervalIntegrable_of_integral_ne_zero h₀.ne'

Result:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h₀ : 0 < ∫ (x : ℝ) in 0 ..T, g x
hT : 0 < T
h_int : IntervalIntegrable g volume 0 T
⊢ Tendsto (fun t => ∫ (x : ℝ) in 0 ..t, g x) atBot atBot

Proof state:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h₀ : 0 < ∫ (x : ℝ) in 0 ..T, g x
hT : 0 < T
h_int : IntervalIntegrable g volume 0 T
⊢ Tendsto (fun n => sSup ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Icc 0 T) + ⌊n / T⌋ • ∫ (x : ℝ) in 0 ..T, g x) atBot
    atBot

Tactic:
apply atBot.tendsto_atBot_add_const_left (sSup <| (fun t => ∫ x in (0)..t, g x) '' Icc 0 T)

Result:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h₀ : 0 < ∫ (x : ℝ) in 0 ..T, g x
hT : 0 < T
h_int : IntervalIntegrable g volume 0 T
⊢ Tendsto (fun x => ⌊x / T⌋ • ∫ (x : ℝ) in 0 ..T, g x) atBot atBot

Proof state:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h₀ : 0 < ∫ (x : ℝ) in 0 ..T, g x
hT : 0 < T
h_int : IntervalIntegrable g volume 0 T
⊢ Tendsto (fun x => ⌊x / T⌋ • ∫ (x : ℝ) in 0 ..T, g x) atBot atBot

Tactic:
apply Tendsto.atBot_zsmul_const h₀

Result:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h₀ : 0 < ∫ (x : ℝ) in 0 ..T, g x
hT : 0 < T
h_int : IntervalIntegrable g volume 0 T
⊢ Tendsto (fun x => ⌊x / T⌋) atBot atBot

Proof state:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h₀ : 0 < ∫ (x : ℝ) in 0 ..T, g x
hT : 0 < T
h_int : IntervalIntegrable g volume 0 T
⊢ Tendsto (fun x => ⌊x / T⌋) atBot atBot

Tactic:
exact tendsto_floor_atBot.comp (tendsto_id.atBot_mul_const (inv_pos.mpr hT))

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean
theorem χ₄_int_three_mod_four {n : ℤ} (hn : n % 4 = 3) : χ₄ n = -1

Proof state:
n : ℤ
hn : n % 4 = 3
⊢ χ₄ ↑n = -1

Tactic:
rw [χ₄_int_mod_four, hn]

Result:
n : ℤ
hn : n % 4 = 3
⊢ χ₄ ↑3 = -1

Proof state:
n : ℤ
hn : n % 4 = 3
⊢ χ₄ ↑3 = -1

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapFinIdx_eq_ofFn {as : List α} {f : (i : Nat) → α → (h : i < as.length) → β} :
    as.mapFinIdx f = List.ofFn fun i : Fin as.length => f i as[i] i.2

Proof state:
α : Type u_1
β : Type u_2
as : List α
f : (i : Nat) → α → i < as.length → β
⊢ as.mapFinIdx f = ofFn fun i => f (↑i) as[i] ⋯

Tactic:
apply ext_getElem <;> simp

Result:
no goals
-- Mathlib/Algebra/Lie/Engel.lean
theorem isNilpotentOfIsNilpotentSpanSupEqTop (hnp : IsNilpotent <| toEnd R L M x)
    (hIM : IsNilpotent I M) : IsNilpotent L M

Proof state:
case intro.intro
R : Type u₁
L : Type u₂
M : Type u₄
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent (↥I) M
n : ℕ
hn : (toEnd R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R (↥I) M k = ⊥
hk' : I.lcs M k = ⊥
⊢ LieModule.IsNilpotent L M

Tactic:
suffices ∀ l, lowerCentralSeries R L M (l * n) ≤ I.lcs M l by
  rw [isNilpotent_iff R]
  use k * n
  simpa [hk'] using this k

Result:
case intro.intro
R : Type u₁
L : Type u₂
M : Type u₄
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent (↥I) M
n : ℕ
hn : (toEnd R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R (↥I) M k = ⊥
hk' : I.lcs M k = ⊥
⊢ ∀ (l : ℕ), lowerCentralSeries R L M (l * n) ≤ I.lcs M l

Proof state:
case intro.intro.succ
R : Type u₁
L : Type u₂
M : Type u₄
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent (↥I) M
n : ℕ
hn : (toEnd R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R (↥I) M k = ⊥
hk' : I.lcs M k = ⊥
l : ℕ
ih : lowerCentralSeries R L M (l * n) ≤ I.lcs M l
⊢ lowerCentralSeries R L M ((l + 1) * n) ≤ I.lcs M (l + 1)

Tactic:
exact (l.succ_mul n).symm ▸ lcs_le_lcs_of_is_nilpotent_span_sup_eq_top hxI hn ih

Result:
no goals

Proof state:
R : Type u₁
L : Type u₂
M : Type u₄
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent (↥I) M
n : ℕ
hn : (toEnd R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R (↥I) M k = ⊥
⊢ I.lcs M k = ⊥

Tactic:
simp only [← toSubmodule_inj, I.coe_lcs_eq, hk, bot_toSubmodule]

Result:
no goals

Proof state:
case intro.intro.zero
R : Type u₁
L : Type u₂
M : Type u₄
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent (↥I) M
n : ℕ
hn : (toEnd R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R (↥I) M k = ⊥
hk' : I.lcs M k = ⊥
⊢ lowerCentralSeries R L M (0 * n) ≤ I.lcs M 0

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem mem_box_iff [NeZero n] {ν : ι → ℤ} {x : ι → ℝ} :
    x ∈ box n ν ↔ ∀ i, ν i / n < x i ∧ x i ≤ (ν i + 1) / n

Proof state:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
ν : ι → ℤ
x : ι → ℝ
⊢ x ∈ box n ν ↔ ∀ (i : ι), ↑(ν i) / ↑n < x i ∧ x i ≤ (↑(ν i) + 1) / ↑n

Tactic:
simp_rw [Box.mem_def, box, Set.mem_Ioc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem DistinctKeys.constAlterKey [BEq α] [EquivBEq α] {β : Type v} {a : α}
    {f : Option β → Option β} {l : List ((_ : α) × β)} (hl : DistinctKeys l) :
    DistinctKeys (List.Const.alterKey a f l)

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
β : Type v
a : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
⊢ DistinctKeys
    (match f (getValue? a l) with
    | none => List.eraseKey a l
    | some v => List.insertEntry a v l)

Tactic:
split

Result:
case h_1
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
β : Type v
a : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
x✝ : Option β
heq✝ : f (getValue? a l) = none
⊢ DistinctKeys (List.eraseKey a l)

case h_2
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
β : Type v
a : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
x✝ : Option β
v✝ : β
heq✝ : f (getValue? a l) = some v✝
⊢ DistinctKeys (List.insertEntry a v✝ l)

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
β : Type v
a : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
⊢ DistinctKeys (Const.alterKey a f l)

Tactic:
dsimp only [List.Const.alterKey]

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
β : Type v
a : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
⊢ DistinctKeys
    (match f (getValue? a l) with
    | none => List.eraseKey a l
    | some v => List.insertEntry a v l)

Proof state:
case h_1
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
β : Type v
a : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
x✝ : Option β
heq✝ : f (getValue? a l) = none
⊢ DistinctKeys (List.eraseKey a l)

Tactic:
exact DistinctKeys.eraseKey hl

Result:
no goals

Proof state:
case h_2
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
β : Type v
a : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
x✝ : Option β
v✝ : β
heq✝ : f (getValue? a l) = some v✝
⊢ DistinctKeys (List.insertEntry a v✝ l)

Tactic:
exact DistinctKeys.insertEntry hl

Result:
no goals
-- Mathlib/ModelTheory/Equivalence.lean
theorem inf_iff_not_sup_not : (φ ⊓ ψ) ⇔[T] (φ.not ⊔ ψ.not).not :=
  fun M v xs => by simp

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (φ ⊓ ψ ⇔ ∼(∼φ ⊔ ∼ψ)).Realize v xs

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Dedup.lean
theorem dedup_cons_of_not_mem' {a : α} {l : List α} (h : a ∉ dedup l) :
    dedup (a :: l) = a :: dedup l :=
  pwFilter_cons_of_pos <| by simpa only [forall_mem_ne] using h

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h : a ∉ l.dedup
⊢ ∀ b ∈ pwFilter (fun x1 x2 => x1 ≠ x2) l, a ≠ b

Tactic:
simpa only [forall_mem_ne] using h

Result:
no goals
-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
theorem _root_.AlgebraicGeometry.isIso_iff_stalk_iso {X Y : Scheme.{u}} (f : X ⟶ Y) :
    IsIso f ↔ IsIso f.base ∧ ∀ x, IsIso (f.stalkMap x)

Proof state:
case refine_1
X Y : Scheme
f : X ⟶ Y
⊢ Epi f.base ∧ IsOpenEmbedding ⇑(ConcreteCategory.hom f.base) → IsIso f.base

Tactic:
rintro ⟨h₁, h₂⟩

Result:
case refine_1.intro
X Y : Scheme
f : X ⟶ Y
h₁ : Epi f.base
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom f.base)
⊢ IsIso f.base

Proof state:
case refine_2
X Y : Scheme
f : X ⟶ Y
H : IsIso f.base
⊢ Epi f.base ∧ IsOpenEmbedding ⇑(ConcreteCategory.hom f.base)

Tactic:
exact ⟨inferInstance, (TopCat.homeoOfIso (asIso f.base)).isOpenEmbedding⟩

Result:
no goals

Proof state:
case refine_2
X Y : Scheme
f : X ⟶ Y
⊢ IsIso f.base → Epi f.base ∧ IsOpenEmbedding ⇑(ConcreteCategory.hom f.base)

Tactic:
intro H

Result:
case refine_2
X Y : Scheme
f : X ⟶ Y
H : IsIso f.base
⊢ Epi f.base ∧ IsOpenEmbedding ⇑(ConcreteCategory.hom f.base)

Proof state:
X Y : Scheme
f : X ⟶ Y
⊢ ((Epi f.base ∧ IsOpenEmbedding ⇑(ConcreteCategory.hom f.base)) ∧
      ∀ (x : ↑↑X.toPresheafedSpace), IsIso (Scheme.Hom.stalkMap f x)) ↔
    IsIso f.base ∧ ∀ (x : ↑↑X.toPresheafedSpace), IsIso (Scheme.Hom.stalkMap f x)

Tactic:
refine and_congr ⟨?_, ?_⟩ Iff.rfl

Result:
case refine_1
X Y : Scheme
f : X ⟶ Y
⊢ Epi f.base ∧ IsOpenEmbedding ⇑(ConcreteCategory.hom f.base) → IsIso f.base

case refine_2
X Y : Scheme
f : X ⟶ Y
⊢ IsIso f.base → Epi f.base ∧ IsOpenEmbedding ⇑(ConcreteCategory.hom f.base)

Proof state:
X Y : Scheme
f : X ⟶ Y
⊢ IsIso f ↔ IsIso f.base ∧ ∀ (x : ↑↑X.toPresheafedSpace), IsIso (Scheme.Hom.stalkMap f x)

Tactic:
rw [isIso_iff_isOpenImmersion, IsOpenImmersion.iff_stalk_iso, and_comm, ← and_assoc]

Result:
X Y : Scheme
f : X ⟶ Y
⊢ ((Epi f.base ∧ IsOpenEmbedding ⇑(ConcreteCategory.hom f.base)) ∧
      ∀ (x : ↑↑X.toPresheafedSpace), IsIso (Scheme.Hom.stalkMap f x)) ↔
    IsIso f.base ∧ ∀ (x : ↑↑X.toPresheafedSpace), IsIso (Scheme.Hom.stalkMap f x)

Proof state:
case refine_1.intro
X Y : Scheme
f : X ⟶ Y
h₁ : Epi f.base
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom f.base)
⊢ IsIso f.base

Tactic:
convert_to
  IsIso
    (TopCat.isoOfHomeo
        (Homeomorph.homeomorphOfContinuousOpen
          (.ofBijective _ ⟨h₂.injective, (TopCat.epi_iff_surjective _).mp h₁⟩) h₂.continuous
          h₂.isOpenMap)).hom

Result:
case refine_1.intro
X Y : Scheme
f : X ⟶ Y
h₁ : Epi f.base
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom f.base)
⊢ IsIso
    (TopCat.isoOfHomeo
        (Homeomorph.homeomorphOfContinuousOpen (Equiv.ofBijective ⇑(ConcreteCategory.hom f.base) ⋯) ⋯ ⋯)).hom

Proof state:
case refine_1.intro
X Y : Scheme
f : X ⟶ Y
h₁ : Epi f.base
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom f.base)
⊢ IsIso
    (TopCat.isoOfHomeo
        (Homeomorph.homeomorphOfContinuousOpen (Equiv.ofBijective ⇑(ConcreteCategory.hom f.base) ⋯) ⋯ ⋯)).hom

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean
theorem of_s_head_aux (v : K) : (of v).s.get? 0 = (IntFractPair.stream v 1).bind (some ∘ fun p =>
    { a := 1
      b := p.b })

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
⊢ (match (IntFractPair.of v, Stream'.Seq.tail ⟨IntFractPair.stream v, ⋯⟩) with
          | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p => { a := 1, b := ↑p.b }) s }).s.get?
      0 =
    (IntFractPair.stream v 1).bind (some ∘ fun p => { a := 1, b := ↑p.b })

Tactic:
simp only [of, Stream'.Seq.map_tail, Stream'.Seq.map, Stream'.Seq.tail, Stream'.Seq.head,
  Stream'.Seq.get?, Stream'.map]

Result:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
⊢ Option.map (fun p => { a := 1, b := ↑p.b }) ((IntFractPair.stream v).tail.get 0) =
    (IntFractPair.stream v 1).bind (some ∘ fun p => { a := 1, b := ↑p.b })

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
⊢ (of v).s.get? 0 = (IntFractPair.stream v 1).bind (some ∘ fun p => { a := 1, b := ↑p.b })

Tactic:
rw [of, IntFractPair.seq1]

Result:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
⊢ (match (IntFractPair.of v, Stream'.Seq.tail ⟨IntFractPair.stream v, ⋯⟩) with
          | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p => { a := 1, b := ↑p.b }) s }).s.get?
      0 =
    (IntFractPair.stream v 1).bind (some ∘ fun p => { a := 1, b := ↑p.b })

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
⊢ (match IntFractPair.stream v (Nat.succ 0) with
    | some x => some { a := 1, b := ↑x.b }
    | none => none) =
    (IntFractPair.stream v 1).bind (some ∘ fun p => { a := 1, b := ↑p.b })

Tactic:
split <;> simp_all only [Option.some_bind, Option.none_bind, Function.comp_apply]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
⊢ Option.map (fun p => { a := 1, b := ↑p.b }) ((IntFractPair.stream v).tail.get 0) =
    (IntFractPair.stream v 1).bind (some ∘ fun p => { a := 1, b := ↑p.b })

Tactic:
rw [← Stream'.get_succ, Stream'.get, Option.map.eq_def]

Result:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
⊢ (match IntFractPair.stream v (Nat.succ 0) with
    | some x => some { a := 1, b := ↑x.b }
    | none => none) =
    (IntFractPair.stream v 1).bind (some ∘ fun p => { a := 1, b := ↑p.b })
-- Mathlib/Algebra/Ring/Commute.lean
theorem mul_self_sub_one [NonAssocRing R] (a : R) : a * a - 1 = (a + 1) * (a - 1)

Proof state:
R : Type u
inst✝ : NonAssocRing R
a : R
⊢ a * a - 1 = (a + 1) * (a - 1)

Tactic:
rw [← (Commute.one_right a).mul_self_sub_mul_self_eq, mul_one]

Result:
no goals