harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Determinant.lean
theorem is_basis_iff_det {v : ι → M} :
    LinearIndependent R v ∧ span R (Set.range v) = ⊤ ↔ IsUnit (e.det v)

Proof state:
case mpr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
h : IsUnit ((toMatrix e e) ((e.constr ℕ) v)).det
v' : Basis ι R M := e.map (LinearEquiv.ofIsUnitDet h)
v'_def : v' = e.map (LinearEquiv.ofIsUnitDet h)
this : ⇑v' = v
⊢ LinearIndependent R v ∧ span R (Set.range v) = ⊤

Tactic:
rw [← this]

Result:
case mpr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
h : IsUnit ((toMatrix e e) ((e.constr ℕ) v)).det
v' : Basis ι R M := e.map (LinearEquiv.ofIsUnitDet h)
v'_def : v' = e.map (LinearEquiv.ofIsUnitDet h)
this : ⇑v' = v
⊢ LinearIndependent R ⇑v' ∧ span R (Set.range ⇑v') = ⊤

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
⊢ LinearIndependent R v ∧ span R (Set.range v) = ⊤ ↔ IsUnit (e.det v)

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
⊢ LinearIndependent R v ∧ span R (Set.range v) = ⊤ → IsUnit (e.det v)

case mpr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
⊢ IsUnit (e.det v) → LinearIndependent R v ∧ span R (Set.range v) = ⊤

Proof state:
case mp
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
⊢ LinearIndependent R v ∧ span R (Set.range v) = ⊤ → IsUnit (e.det v)

Tactic:
rintro ⟨hli, hspan⟩

Result:
case mp.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hspan : span R (Set.range v) = ⊤
⊢ IsUnit (e.det v)
-- Mathlib/Data/Set/Pointwise/SMul.lean
@[to_additive]
lemma smul_graphOn (x : α × β) (s : Set α) (f : F) :
    x • s.graphOn f = (x.1 • s).graphOn fun a ↦ x.2 / f x.1 * f a

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : CommGroup β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
x : α × β
s : Set α
f : F
⊢ x • graphOn (⇑f) s = graphOn (fun a => x.2 / f x.1 * f a) (x.1 • s)

Tactic:
ext ⟨a, b⟩

Result:
case h.mk
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : CommGroup β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
x : α × β
s : Set α
f : F
a : α
b : β
⊢ (a, b) ∈ x • graphOn (⇑f) s ↔ (a, b) ∈ graphOn (fun a => x.2 / f x.1 * f a) (x.1 • s)

Proof state:
case h.mk
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : CommGroup β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
x : α × β
s : Set α
f : F
a : α
b : β
⊢ (a, b) ∈ x • graphOn (⇑f) s ↔ (a, b) ∈ graphOn (fun a => x.2 / f x.1 * f a) (x.1 • s)

Tactic:
simp [mem_smul_set_iff_inv_smul_mem, Prod.ext_iff, and_comm (a := _ = a), inv_mul_eq_iff_eq_mul,
  mul_left_comm _ _⁻¹, eq_inv_mul_iff_mul_eq, ← mul_div_right_comm, div_eq_iff_eq_mul, mul_comm b]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem ofReal_le_enorm (r : ℝ) : ENNReal.ofReal r ≤ ‖r‖ₑ

Proof state:
case h
r : ℝ
⊢ r ≤ |r|

Tactic:
exact le_abs_self _

Result:
no goals

Proof state:
r : ℝ
⊢ ENNReal.ofReal r ≤ ENNReal.ofReal |r|

Tactic:
gcongr

Result:
case h
r : ℝ
⊢ r ≤ |r|

Proof state:
r : ℝ
⊢ ENNReal.ofReal r ≤ ‖r‖ₑ

Tactic:
rw [enorm_eq_ofReal_abs]

Result:
r : ℝ
⊢ ENNReal.ofReal r ≤ ENNReal.ofReal |r|
-- Mathlib/Data/Real/EReal.lean
private lemma exists_lt_add_right {a b c : EReal} (hc : c < a + b) : ∃ b' < b, c < a + b'

Proof state:
a b c : EReal
hc : c < a + b
⊢ ∃ b' < b, c < a + b'

Tactic:
simp_rw [add_comm a] at hc ⊢

Result:
a b c : EReal
hc : c < b + a
⊢ ∃ b' < b, c < b' + a

Proof state:
a b c : EReal
hc : c < b + a
⊢ ∃ b' < b, c < b' + a

Tactic:
exact exists_lt_add_left hc

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isLittleO_iff_exists_eq_mul :
    u =o[l] v ↔ ∃ φ : α → 𝕜, Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v

Proof state:
case mp
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
⊢ u =o[l] v → ∃ φ, Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v

Tactic:
exact fun h => ⟨fun x => u x / v x, h.tendsto_div_nhds_zero, h.eventually_mul_div_cancel.symm⟩

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
⊢ u =o[l] v ↔ ∃ φ, Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v

Tactic:
constructor

Result:
case mp
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
⊢ u =o[l] v → ∃ φ, Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v

case mpr
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
⊢ (∃ φ, Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v) → u =o[l] v

Proof state:
case mpr.intro.intro
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v φ : α → 𝕜
hφ : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖φ x‖ < ε
huvφ : u =ᶠ[l] φ * v
c : ℝ
hpos : 0 < c
⊢ IsBigOWith c l u v

Tactic:
exact isBigOWith_of_eq_mul _ ((hφ c hpos).mono fun x => le_of_lt) huvφ

Result:
no goals

Proof state:
case mpr
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
⊢ (∃ φ, Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v) → u =o[l] v

Tactic:
simp only [IsLittleO_def]

Result:
case mpr
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
⊢ (∃ φ, Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v) → ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l u v

Proof state:
case mpr
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
⊢ (∃ φ, Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v) → ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l u v

Tactic:
rintro ⟨φ, hφ, huvφ⟩ c hpos

Result:
case mpr.intro.intro
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v φ : α → 𝕜
hφ : Tendsto φ l (𝓝 0)
huvφ : u =ᶠ[l] φ * v
c : ℝ
hpos : 0 < c
⊢ IsBigOWith c l u v

Proof state:
case mpr.intro.intro
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v φ : α → 𝕜
hφ : Tendsto φ l (𝓝 0)
huvφ : u =ᶠ[l] φ * v
c : ℝ
hpos : 0 < c
⊢ IsBigOWith c l u v

Tactic:
rw [NormedAddCommGroup.tendsto_nhds_zero] at hφ

Result:
case mpr.intro.intro
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v φ : α → 𝕜
hφ : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖φ x‖ < ε
huvφ : u =ᶠ[l] φ * v
c : ℝ
hpos : 0 < c
⊢ IsBigOWith c l u v
-- Mathlib/Order/Interval/Set/OrdConnected.lean
theorem image_Ioc (e : α ↪o β) (he : OrdConnected (range e)) (x y : α) :
    e '' Ioc x y = Ioc (e x) (e y)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : (range ⇑e).OrdConnected
x y : α
⊢ ⇑e '' Ioc x y = Ioc (e x) (e y)

Tactic:
rw [← e.preimage_Ioc, image_preimage_eq_inter_range,
  inter_eq_left.2 <| Ioc_subset_Icc_self.trans <| he.out ⟨_, rfl⟩ ⟨_, rfl⟩]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/Relabel.lean
theorem relabel_relabel' : relabel r1 ∘ relabel r2 = relabel (r1 ∘ r2)

Proof state:
case h
α✝² : Type u_1
α✝¹ : Type u_2
r1 : α✝² → α✝¹
α✝ : Type u_3
r2 : α✝ → α✝²
i : Clause α✝
⊢ (relabel r1 ∘ relabel r2) i = relabel (r1 ∘ r2) i

Tactic:
simp only [Function.comp_apply, relabel, List.map_map]

Result:
case h
α✝² : Type u_1
α✝¹ : Type u_2
r1 : α✝² → α✝¹
α✝ : Type u_3
r2 : α✝ → α✝²
i : Clause α✝
⊢ List.map ((fun x => (r1 x.fst, x.snd)) ∘ fun x => (r2 x.fst, x.snd)) i = List.map (fun x => (r1 (r2 x.fst), x.snd)) i

Proof state:
case h
α✝² : Type u_1
α✝¹ : Type u_2
r1 : α✝² → α✝¹
α✝ : Type u_3
r2 : α✝ → α✝²
i : Clause α✝
⊢ List.map ((fun x => (r1 x.fst, x.snd)) ∘ fun x => (r2 x.fst, x.snd)) i = List.map (fun x => (r1 (r2 x.fst), x.snd)) i

Tactic:
rfl

Result:
no goals

Proof state:
α✝² : Type u_1
α✝¹ : Type u_2
r1 : α✝² → α✝¹
α✝ : Type u_3
r2 : α✝ → α✝²
⊢ relabel r1 ∘ relabel r2 = relabel (r1 ∘ r2)

Tactic:
funext i

Result:
case h
α✝² : Type u_1
α✝¹ : Type u_2
r1 : α✝² → α✝¹
α✝ : Type u_3
r2 : α✝ → α✝²
i : Clause α✝
⊢ (relabel r1 ∘ relabel r2) i = relabel (r1 ∘ r2) i
-- Mathlib/Order/BooleanAlgebra.lean
theorem inf_sdiff : (x ⊓ y) \ z = x \ z ⊓ y \ z :=
  sdiff_unique
    (calc
      x ⊓ y ⊓ z ⊔ x \ z ⊓ y \ z = (x ⊓ y ⊓ z ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z)

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y ⊓ (z ⊓ x \ z) ⊓ y \ z = ⊥

Tactic:
rw [inf_sdiff_self_right, inf_bot_eq, bot_inf_eq]

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y ⊓ z ⊓ (x \ z ⊓ y \ z) = x ⊓ y ⊓ (z ⊓ x \ z) ⊓ y \ z

Tactic:
ac_rfl

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x ⊓ y ⊓ z ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z) = (x ⊓ y ⊓ (z ⊔ x) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z)

Tactic:
rw [sup_inf_right, sup_sdiff_self_right, inf_sup_right, inf_sdiff_sup_right]

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y ⊓ z ⊔ x \ z ⊓ y \ z = (x ⊓ y ⊓ z ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z)

Tactic:
rw [sup_inf_left]

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (y ⊓ x ⊔ x \ z) ⊓ (x ⊓ y ⊔ y \ z) = x ⊓ y ⊔ x \ z ⊓ y \ z

Tactic:
rw [inf_comm y, sup_inf_left]

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (y ⊓ (x ⊓ (x ⊔ z)) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z) = (y ⊓ x ⊔ x \ z) ⊓ (x ⊓ y ⊔ y \ z)

Tactic:
rw [inf_sup_self, sup_inf_inf_sdiff]

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x ⊓ y ⊓ (z ⊔ x) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z) = (y ⊓ (x ⊓ (x ⊔ z)) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z)

Tactic:
ac_rfl

Result:
no goals
-- Mathlib/Tactic/NormNum/OfScientific.lean
theorem isNat_ofScientific_of_false [DivisionRing α] : {m e nm ne n : ℕ} →
    IsNat m nm → IsNat e ne → n = Nat.mul nm ((10 : ℕ) ^ ne) →
    IsNat (OfScientific.ofScientific m false e : α) n
  | _, _, _, _, _, ⟨rfl⟩, ⟨rfl⟩, h => ⟨by
    rw [← Rat.cast_ofScientific, ← Rat.ofScientific_eq_ofScientific]
    simp only [Nat.cast_id, Rat.ofScientific_false_def, Nat.cast_mul, Nat.cast_pow,
      Nat.cast_ofNat, h, Nat.mul_eq]
    norm_cast⟩

Proof state:
α : Type u_1
inst✝ : DivisionRing α
n✝¹ n✝ x✝ : ℕ
h : x✝ = n✝¹.mul (10 ^ n✝)
⊢ ↑(Rat.ofScientific (OfNat.ofNat ↑n✝¹) false (OfNat.ofNat ↑n✝)) = ↑x✝

Tactic:
simp only [Nat.cast_id, Rat.ofScientific_false_def, Nat.cast_mul, Nat.cast_pow,
  Nat.cast_ofNat, h, Nat.mul_eq]

Result:
α : Type u_1
inst✝ : DivisionRing α
n✝¹ n✝ x✝ : ℕ
h : x✝ = n✝¹.mul (10 ^ n✝)
⊢ ↑(↑(OfNat.ofNat n✝¹) * 10 ^ OfNat.ofNat n✝) = ↑n✝¹ * 10 ^ n✝

Proof state:
α : Type u_1
inst✝ : DivisionRing α
n✝¹ n✝ x✝ : ℕ
h : x✝ = n✝¹.mul (10 ^ n✝)
⊢ ↑(↑(OfNat.ofNat n✝¹) * 10 ^ OfNat.ofNat n✝) = ↑n✝¹ * 10 ^ n✝

Tactic:
norm_cast

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DivisionRing α
n✝¹ n✝ x✝ : ℕ
h : x✝ = n✝¹.mul (10 ^ n✝)
⊢ OfScientific.ofScientific (↑n✝¹) false ↑n✝ = ↑x✝

Tactic:
rw [← Rat.cast_ofScientific, ← Rat.ofScientific_eq_ofScientific]

Result:
α : Type u_1
inst✝ : DivisionRing α
n✝¹ n✝ x✝ : ℕ
h : x✝ = n✝¹.mul (10 ^ n✝)
⊢ ↑(Rat.ofScientific (OfNat.ofNat ↑n✝¹) false (OfNat.ofNat ↑n✝)) = ↑x✝
-- Mathlib/Algebra/Order/Ring/Basic.lean
protected lemma Even.add_pow_le (hn : Even n) :
    (a + b) ^ n ≤ 2 ^ (n - 1) * (a ^ n + b ^ n)

Proof state:
case succ
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
n✝ : ℕ
⊢ 2 ^ (n✝ + 1 + (n✝ + 1 - 1)) * (a ^ (2 * (n✝ + 1)) + b ^ (2 * (n✝ + 1))) =
    2 ^ (2 * (n✝ + 1) - 1) * (a ^ (2 * (n✝ + 1)) + b ^ (2 * (n✝ + 1)))

Tactic:
simp [Nat.two_mul]

Result:
no goals

Proof state:
case intro
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
n : ℕ
⊢ (a + b) ^ (n + n) ≤ 2 ^ (n + n - 1) * (a ^ (n + n) + b ^ (n + n))

Tactic:
rw [← two_mul, pow_mul]

Result:
case intro
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
n : ℕ
⊢ ((a + b) ^ 2) ^ n ≤ 2 ^ (2 * n - 1) * (a ^ (2 * n) + b ^ (2 * n))

Proof state:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Even n
⊢ (a + b) ^ n ≤ 2 ^ (n - 1) * (a ^ n + b ^ n)

Tactic:
obtain ⟨n, rfl⟩ := hn

Result:
case intro
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
n : ℕ
⊢ (a + b) ^ (n + n) ≤ 2 ^ (n + n - 1) * (a ^ (n + n) + b ^ (n + n))

Proof state:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
n : ℕ
⊢ (2 * (a ^ 2 + b ^ 2)) ^ n = 2 ^ n * (a ^ 2 + b ^ 2) ^ n

Tactic:
rw [Commute.mul_pow]

Result:
case h
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
n : ℕ
⊢ Commute 2 (a ^ 2 + b ^ 2)

Proof state:
case h
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
n : ℕ
⊢ Commute 2 (a ^ 2 + b ^ 2)

Tactic:
simp [Commute, SemiconjBy, two_mul, mul_two]

Result:
no goals

Proof state:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
n : ℕ
⊢ 2 ^ n * (2 ^ (n - 1) * ((a ^ 2) ^ n + (b ^ 2) ^ n)) = 2 ^ (2 * n - 1) * (a ^ (2 * n) + b ^ (2 * n))

Tactic:
simp only [← mul_assoc, ← pow_add, ← pow_mul]

Result:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
n : ℕ
⊢ 2 ^ (n + (n - 1)) * (a ^ (2 * n) + b ^ (2 * n)) = 2 ^ (2 * n - 1) * (a ^ (2 * n) + b ^ (2 * n))

Proof state:
case zero
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
⊢ 2 ^ (0 + (0 - 1)) * (a ^ (2 * 0) + b ^ (2 * 0)) = 2 ^ (2 * 0 - 1) * (a ^ (2 * 0) + b ^ (2 * 0))

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
n : ℕ
⊢ 2 ^ (n + (n - 1)) * (a ^ (2 * n) + b ^ (2 * n)) = 2 ^ (2 * n - 1) * (a ^ (2 * n) + b ^ (2 * n))

Tactic:
cases n

Result:
case zero
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
⊢ 2 ^ (0 + (0 - 1)) * (a ^ (2 * 0) + b ^ (2 * 0)) = 2 ^ (2 * 0 - 1) * (a ^ (2 * 0) + b ^ (2 * 0))

case succ
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
n✝ : ℕ
⊢ 2 ^ (n✝ + 1 + (n✝ + 1 - 1)) * (a ^ (2 * (n✝ + 1)) + b ^ (2 * (n✝ + 1))) =
    2 ^ (2 * (n✝ + 1) - 1) * (a ^ (2 * (n✝ + 1)) + b ^ (2 * (n✝ + 1)))
-- Mathlib/ModelTheory/Substructures.lean
theorem range_le_iff_comap {f : M →[L] N} {p : L.Substructure N} : range f ≤ p ↔ comap f p = ⊤

Proof state:
L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M →[L] N
p : L.Substructure N
⊢ f.range ≤ p ↔ comap f p = ⊤

Tactic:
rw [range_eq_map, map_le_iff_le_comap, eq_top_iff]

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem isCompact_singleton {x : X} : IsCompact ({x} : Set X) := fun _ hf hfa =>
  ⟨x, rfl, ClusterPt.of_le_nhds'
    (hfa.trans <| by simpa only [principal_singleton] using pure_le_nhds x) hf⟩

Proof state:
X : Type u
inst✝ : TopologicalSpace X
x : X
x✝ : Filter X
hf : x✝.NeBot
hfa : x✝ ≤ 𝓟 {x}
⊢ 𝓟 {x} ≤ 𝓝 x

Tactic:
simpa only [principal_singleton] using pure_le_nhds x

Result:
no goals
-- Mathlib/Data/List/Intervals.lean
theorem filter_le_of_le {n m l : ℕ} (hnl : n ≤ l) :
    ((Ico n m).filter fun x => l ≤ x) = Ico l m

Proof state:
case inr
n m l : ℕ
hnl : n ≤ l
hml : m ≤ l
⊢ filter (fun x => decide (l ≤ x)) (Ico n m) = Ico l m

Tactic:
rw [eq_nil_of_le hml, filter_le_of_top_le hml]

Result:
no goals

Proof state:
case inl
n m l : ℕ
hnl : n ≤ l
hlm : l ≤ m
⊢ filter (fun x => decide (l ≤ x)) (Ico n m) = Ico l m

Tactic:
rw [← append_consecutive hnl hlm, filter_append, filter_le_of_top_le (le_refl l),
  filter_le_of_le_bot (le_refl l), nil_append]

Result:
no goals

Proof state:
n m l : ℕ
hnl : n ≤ l
⊢ filter (fun x => decide (l ≤ x)) (Ico n m) = Ico l m

Tactic:
rcases le_total l m with hlm | hml

Result:
case inl
n m l : ℕ
hnl : n ≤ l
hlm : l ≤ m
⊢ filter (fun x => decide (l ≤ x)) (Ico n m) = Ico l m

case inr
n m l : ℕ
hnl : n ≤ l
hml : m ≤ l
⊢ filter (fun x => decide (l ≤ x)) (Ico n m) = Ico l m
-- Mathlib/Topology/Algebra/Monoid.lean
theorem continuous_finprod_cond {f : ι → X → M} {p : ι → Prop} (hc : ∀ i, p i → Continuous (f i))
    (hf : LocallyFinite fun i => mulSupport (f i)) :
    Continuous fun x => ∏ᶠ (i) (_ : p i), f i x

Proof state:
ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
p : ι → Prop
hc : ∀ (i : ι), p i → Continuous (f i)
hf : LocallyFinite fun i => mulSupport (f i)
⊢ Continuous fun x => ∏ᶠ (j : Subtype p), f (↑j) x

Tactic:
exact continuous_finprod (fun i => hc i i.2) (hf.comp_injective Subtype.coe_injective)

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
p : ι → Prop
hc : ∀ (i : ι), p i → Continuous (f i)
hf : LocallyFinite fun i => mulSupport (f i)
⊢ Continuous fun x => ∏ᶠ (i : ι) (_ : p i), f i x

Tactic:
simp only [← finprod_subtype_eq_finprod_cond]

Result:
ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
p : ι → Prop
hc : ∀ (i : ι), p i → Continuous (f i)
hf : LocallyFinite fun i => mulSupport (f i)
⊢ Continuous fun x => ∏ᶠ (j : Subtype p), f (↑j) x
-- Mathlib/Data/Nat/Digits.lean
theorem modEq_eleven_digits_sum (n : ℕ) :
    n ≡ ((digits 10 n).map fun n : ℕ => (n : ℤ)).alternatingSum [ZMOD 11]

Proof state:
n : ℕ
⊢ ↑n ≡ (List.map (fun n => ↑n) (digits 10 n)).alternatingSum [ZMOD 11]

Tactic:
have t := zmodeq_ofDigits_digits 11 10 (-1 : ℤ) (by unfold Int.ModEq; rfl) n

Result:
n : ℕ
t : ↑n ≡ ofDigits (-1) (digits 10 n) [ZMOD ↑11]
⊢ ↑n ≡ (List.map (fun n => ↑n) (digits 10 n)).alternatingSum [ZMOD 11]

Proof state:
n : ℕ
t : ↑n ≡ ofDigits (-1) (digits 10 n) [ZMOD ↑11]
⊢ ↑n ≡ (List.map (fun n => ↑n) (digits 10 n)).alternatingSum [ZMOD 11]

Tactic:
rwa [ofDigits_neg_one] at t

Result:
no goals

Proof state:
n : ℕ
⊢ ↑10 ≡ -1 [ZMOD ↑11]

Tactic:
unfold Int.ModEq

Result:
n : ℕ
⊢ ↑10 % ↑11 = -1 % ↑11

Proof state:
n : ℕ
⊢ ↑10 % ↑11 = -1 % ↑11

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/WittVector/Verschiebung.lean
theorem verschiebungFun_coeff (x : 𝕎 R) (n : ℕ) :
    (verschiebungFun x).coeff n = if n = 0 then 0 else x.coeff (n - 1)

Proof state:
p : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
⊢ x.verschiebungFun.coeff n = if n = 0 then 0 else x.coeff (n - 1)

Tactic:
simp only [verschiebungFun]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem tail_range' (n : Nat) : (range' s n step).tail = range' (s + step) (n - 1) step

Proof state:
case zero
s step : Nat
⊢ (range' s 0 step).tail = range' (s + step) (0 - 1) step

Tactic:
simp

Result:
no goals

Proof state:
s step n : Nat
⊢ (range' s n step).tail = range' (s + step) (n - 1) step

Tactic:
cases n with
| zero => simp
| succ n => simp [range'_succ]

Result:
no goals

Proof state:
case succ
s step n : Nat
⊢ (range' s (n + 1) step).tail = range' (s + step) (n + 1 - 1) step

Tactic:
simp [range'_succ]

Result:
no goals
-- Mathlib/Topology/Order/PartialSups.lean
protected lemma ContinuousAt.partialSups (hf : ∀ k ≤ n, ContinuousAt (f k) x) :
    ContinuousAt (partialSups f n) x

Proof state:
L : Type u_1
inst✝³ : SemilatticeSup L
inst✝² : TopologicalSpace L
inst✝¹ : ContinuousSup L
X : Type u_2
inst✝ : TopologicalSpace X
f : ℕ → X → L
n : ℕ
x : X
hf : ∀ k ≤ n, ContinuousAt (f k) x
⊢ ContinuousAt ((partialSups f) n) x

Tactic:
simpa only [← Pi.partialSups_apply] using ContinuousAt.partialSups_apply hf

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem oangle_left_eq_arcsin_of_oangle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∡ p₁ p₂ p₃ = ↑(π / 2)) :
    ∡ p₃ p₁ p₂ = Real.arcsin (dist p₃ p₂ / dist p₁ p₃)

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ ∡ p₃ p₁ p₂ = ↑(Real.arcsin (dist p₃ p₂ / dist p₁ p₃))

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm,
  angle_eq_arcsin_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
    (Or.inr (left_ne_of_oangle_eq_pi_div_two h)),
  dist_comm p₁ p₃]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ ∡ p₃ p₁ p₂ = ↑(Real.arcsin (dist p₃ p₂ / dist p₁ p₃))

Tactic:
have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ ∡ p₃ p₁ p₂ = ↑(Real.arcsin (dist p₃ p₂ / dist p₁ p₃))

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₃ p₁ p₂).sign = 1

Tactic:
rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals
-- Mathlib/Algebra/Group/ForwardDiff.lean
theorem shift_eq_sum_fwdDiff_iter (f : M → G) (n : ℕ) (y : M) :
    f (y + n • h) = ∑ k ∈ range (n + 1), n.choose k • Δ_[h]^[k] f y

Proof state:
case h.e'_3
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
⊢ ∑ k ∈ range (n + 1), n.choose k • Δ_[h]^[k] f y =
    (∑ m ∈ range (n + 1), fwdDiffₗ M G h ^ m * 1 ^ (n - m) * ↑(n.choose m)) f y

Tactic:
simp only [LinearMap.sum_apply, sum_apply, one_pow, mul_one, LinearMap.mul_apply,
  Module.End.natCast_apply, map_nsmul, Pi.smul_apply, LinearMap.pow_apply, coe_fwdDiffₗ]

Result:
no goals

Proof state:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
⊢ f (y + n • h) = ∑ k ∈ range (n + 1), n.choose k • Δ_[h]^[k] f y

Tactic:
convert congr_fun (LinearMap.congr_fun
    ((Commute.one_right (fwdDiffₗ M G h)).add_pow n) f) y using 1

Result:
case h.e'_2
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
⊢ f (y + n • h) = ((fwdDiffₗ M G h + 1) ^ n) f y

case h.e'_3
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
⊢ ∑ k ∈ range (n + 1), n.choose k • Δ_[h]^[k] f y =
    (∑ m ∈ range (n + 1), fwdDiffₗ M G h ^ m * 1 ^ (n - m) * ↑(n.choose m)) f y

Proof state:
case h.e'_2
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
⊢ f (y + n • h) = ((fwdDiffₗ M G h + 1) ^ n) f y

Tactic:
rw [← shiftₗ_pow_apply h f, shiftₗ]

Result:
no goals