harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/GroupAction/SubMulAction/Pointwise.lean
theorem subset_coe_pow (p : SubMulAction R M) : ∀ {n : ℕ}, (p : Set M) ^ n ⊆ ↑(p ^ n)
  | 0 => by
    rw [pow_zero, pow_zero]
    exact subset_coe_one
  | n + 1 => by rw [← Nat.succ_eq_add_one, coe_pow _ n.succ_ne_zero]

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : Monoid M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
p : SubMulAction R M
⊢ ↑p ^ 0 ⊆ ↑(p ^ 0)

Tactic:
rw [pow_zero, pow_zero]

Result:
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : Monoid M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
p : SubMulAction R M
⊢ 1 ⊆ ↑1

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : Monoid M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
p : SubMulAction R M
n : ℕ
⊢ ↑p ^ (n + 1) ⊆ ↑(p ^ (n + 1))

Tactic:
rw [← Nat.succ_eq_add_one, coe_pow _ n.succ_ne_zero]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : Monoid M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
p : SubMulAction R M
⊢ 1 ⊆ ↑1

Tactic:
exact subset_coe_one

Result:
no goals
-- Mathlib/RingTheory/Coalgebra/Basic.lean
theorem counit_comp_lsingle (i : ι) : counit ∘ₗ (lsingle i : A →ₗ[R] _) = counit

Proof state:
case h
R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
i : ι
x✝ : A
⊢ (counit ∘ₗ lsingle i) x✝ = counit x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
i : ι
⊢ counit ∘ₗ lsingle i = counit

Tactic:
ext

Result:
case h
R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
i : ι
x✝ : A
⊢ (counit ∘ₗ lsingle i) x✝ = counit x✝
-- Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
theorem boundedBy_eq_ofFunction (m_empty : m ∅ = 0) (s : Set α) :
    boundedBy m s = OuterMeasure.ofFunction m m_empty s

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
this : (fun s => ⨆ (_ : s.Nonempty), m s) = m
⊢ (boundedBy m) s = (OuterMeasure.ofFunction m m_empty) s

Tactic:
simp [boundedBy, this]

Result:
no goals

Proof state:
case h
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
⊢ ⨆ (_ : t.Nonempty), m t = m t

Tactic:
rcases t.eq_empty_or_nonempty with h | h <;> simp [h, Set.not_nonempty_empty, m_empty]

Result:
no goals

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
⊢ (fun s => ⨆ (_ : s.Nonempty), m s) = m

Tactic:
ext1 t

Result:
case h
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
⊢ ⨆ (_ : t.Nonempty), m t = m t

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
⊢ (boundedBy m) s = (OuterMeasure.ofFunction m m_empty) s

Tactic:
have : (fun s : Set α => ⨆ _ : s.Nonempty, m s) = m := by
  ext1 t
  rcases t.eq_empty_or_nonempty with h | h <;> simp [h, Set.not_nonempty_empty, m_empty]

Result:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
this : (fun s => ⨆ (_ : s.Nonempty), m s) = m
⊢ (boundedBy m) s = (OuterMeasure.ofFunction m m_empty) s
-- Mathlib/Logic/Equiv/Basic.lean
theorem sumCongr_refl_swap {α β : Sort _} [DecidableEq α] [DecidableEq β] (i j : β) :
    Equiv.Perm.sumCongr (Equiv.refl α) (Equiv.swap i j) = Equiv.swap (Sum.inr i) (Sum.inr j)

Proof state:
case H.inr
α : Type u_9
β : Type u_10
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j val✝ : β
⊢ (sumCongr (Equiv.refl α) (swap i j)) (Sum.inr val✝) = (swap (Sum.inr i) (Sum.inr j)) (Sum.inr val✝)

Tactic:
simp only [Equiv.sumCongr_apply, Sum.map, coe_refl, comp_id, Sum.elim_inr, comp_apply,
  swap_apply_def, Sum.inr.injEq]

Result:
case H.inr
α : Type u_9
β : Type u_10
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j val✝ : β
⊢ Sum.inr (if val✝ = i then j else if val✝ = j then i else val✝) =
    if val✝ = i then Sum.inr j else if val✝ = j then Sum.inr i else Sum.inr val✝

Proof state:
case H.inr
α : Type u_9
β : Type u_10
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j val✝ : β
⊢ Sum.inr (if val✝ = i then j else if val✝ = j then i else val✝) =
    if val✝ = i then Sum.inr j else if val✝ = j then Sum.inr i else Sum.inr val✝

Tactic:
split_ifs <;> rfl

Result:
no goals

Proof state:
case H.inl
α : Type u_9
β : Type u_10
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j : β
val✝ : α
⊢ (sumCongr (Equiv.refl α) (swap i j)) (Sum.inl val✝) = (swap (Sum.inr i) (Sum.inr j)) (Sum.inl val✝)

Tactic:
simp [Sum.map, swap_apply_of_ne_of_ne]

Result:
no goals

Proof state:
case H
α : Type u_9
β : Type u_10
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j : β
x : α ⊕ β
⊢ (sumCongr (Equiv.refl α) (swap i j)) x = (swap (Sum.inr i) (Sum.inr j)) x

Tactic:
cases x

Result:
case H.inl
α : Type u_9
β : Type u_10
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j : β
val✝ : α
⊢ (sumCongr (Equiv.refl α) (swap i j)) (Sum.inl val✝) = (swap (Sum.inr i) (Sum.inr j)) (Sum.inl val✝)

case H.inr
α : Type u_9
β : Type u_10
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j val✝ : β
⊢ (sumCongr (Equiv.refl α) (swap i j)) (Sum.inr val✝) = (swap (Sum.inr i) (Sum.inr j)) (Sum.inr val✝)

Proof state:
α : Type u_9
β : Type u_10
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j : β
⊢ sumCongr (Equiv.refl α) (swap i j) = swap (Sum.inr i) (Sum.inr j)

Tactic:
ext x

Result:
case H
α : Type u_9
β : Type u_10
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j : β
x : α ⊕ β
⊢ (sumCongr (Equiv.refl α) (swap i j)) x = (swap (Sum.inr i) (Sum.inr j)) x
-- Mathlib/NumberTheory/EulerProduct/DirichletLSeries.lean
/-- If `χ` is a Dirichlet character and its level `M` divides `N`, then we obtain the L-series
of `χ` considered as a Dirichlet character of level `N` from the L-series of `χ` by multiplying
with `∏ p ∈ N.primeFactors, (1 - χ p * p ^ (-s))`. -/
lemma DirichletCharacter.LSeries_changeLevel {M N : ℕ} [NeZero N]
    (hMN : M ∣ N) (χ : DirichletCharacter ℂ M) {s : ℂ} (hs : 1 < s.re) :
    LSeries ↗(changeLevel hMN χ) s =
      LSeries ↗χ s * ∏ p ∈ N.primeFactors, (1 - χ p * p ^ (-s))

Proof state:
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
⊢ ∏' (x : ℕ), {p | Nat.Prime p}.mulIndicator (fun p => (1 - ((changeLevel hMN) χ) ↑p * ↑p ^ (-s))⁻¹) x =
    ∏' (b : ℕ),
      {p | Nat.Prime p}.mulIndicator (fun p => (1 - χ ↑p * ↑p ^ (-s))⁻¹) b *
        (↑N.primeFactors).mulIndicator (fun p => 1 - χ ↑p * ↑p ^ (-s)) b

case hf
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
⊢ Multipliable ({p | Nat.Prime p}.mulIndicator fun p => (1 - χ ↑p * ↑p ^ (-s))⁻¹)

case hg
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
⊢ Multipliable ((↑N.primeFactors).mulIndicator fun p => 1 - χ ↑p * ↑p ^ (-s))

Tactic:
rotate_left

Result:
case hf
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
⊢ Multipliable ({p | Nat.Prime p}.mulIndicator fun p => (1 - χ ↑p * ↑p ^ (-s))⁻¹)

case hg
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
⊢ Multipliable ((↑N.primeFactors).mulIndicator fun p => 1 - χ ↑p * ↑p ^ (-s))

M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
⊢ ∏' (x : ℕ), {p | Nat.Prime p}.mulIndicator (fun p => (1 - ((changeLevel hMN) χ) ↑p * ↑p ^ (-s))⁻¹) x =
    ∏' (b : ℕ),
      {p | Nat.Prime p}.mulIndicator (fun p => (1 - χ ↑p * ↑p ^ (-s))⁻¹) b *
        (↑N.primeFactors).mulIndicator (fun p => 1 - χ ↑p * ↑p ^ (-s)) b
-- Mathlib/Data/Matrix/RowCol.lean
theorem transpose_row (v : m → α) : (Matrix.row ι v)ᵀ = Matrix.col ι v

Proof state:
m : Type u_2
α : Type v
ι : Type u_6
v : m → α
⊢ (row ι v)ᵀ = col ι v

Tactic:
ext

Result:
case a
m : Type u_2
α : Type v
ι : Type u_6
v : m → α
i✝ : m
j✝ : ι
⊢ (row ι v)ᵀ i✝ j✝ = col ι v i✝ j✝

Proof state:
case a
m : Type u_2
α : Type v
ι : Type u_6
v : m → α
i✝ : m
j✝ : ι
⊢ (row ι v)ᵀ i✝ j✝ = col ι v i✝ j✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Basic.lean
theorem Balanced.sInter {S : Set (Set E)} (h : ∀ s ∈ S, Balanced 𝕜 s) : Balanced 𝕜 (⋂₀ S) :=
  fun _ _ => (smul_set_sInter_subset ..).trans (fun _ _ => by aesop)

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
S : Set (Set E)
h : ∀ s ∈ S, Balanced 𝕜 s
x✝³ : 𝕜
x✝² : ‖x✝³‖ ≤ 1
x✝¹ : E
x✝ : x✝¹ ∈ ⋂ s ∈ S, x✝³ • s
⊢ x✝¹ ∈ ⋂₀ S

Tactic:
aesop

Result:
no goals
-- Mathlib/Geometry/Euclidean/Triangle.lean
theorem angle_add_angle_add_angle_eq_pi {p₁ p₂ p₃ : P} (h2 : p₂ ≠ p₁) (h3 : p₃ ≠ p₁) :
    ∠ p₁ p₂ p₃ + ∠ p₂ p₃ p₁ + ∠ p₃ 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
p₁ p₂ p₃ : P
h2 : p₂ ≠ p₁
h3 : p₃ ≠ p₁
⊢ InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) + InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₃ -ᵥ p₁ - (p₂ -ᵥ p₁)) +
      InnerProductGeometry.angle (p₂ -ᵥ p₁) (p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)) =
    π

Tactic:
exact angle_add_angle_sub_add_angle_sub_eq_pi (fun he => h3 (vsub_eq_zero_iff_eq.1 he)) fun he =>
  h2 (vsub_eq_zero_iff_eq.1 he)

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
p₁ p₂ p₃ : P
h2 : p₂ ≠ p₁
h3 : p₃ ≠ p₁
⊢ ∠ p₃ p₁ p₂ + ∠ p₁ p₃ p₂ + ∠ p₁ p₂ p₃ = π

Tactic:
unfold angle

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h2 : p₂ ≠ p₁
h3 : p₃ ≠ p₁
⊢ InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) + InnerProductGeometry.angle (p₁ -ᵥ p₃) (p₂ -ᵥ p₃) +
      InnerProductGeometry.angle (p₁ -ᵥ p₂) (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
p₁ p₂ p₃ : P
h2 : p₂ ≠ p₁
h3 : p₃ ≠ p₁
⊢ ∠ p₁ p₂ p₃ + ∠ p₂ p₃ p₁ + ∠ p₃ p₁ p₂ = π

Tactic:
rw [add_assoc, add_comm, add_comm (∠ p₂ p₃ p₁), angle_comm p₂ p₃ p₁]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h2 : p₂ ≠ p₁
h3 : p₃ ≠ p₁
⊢ ∠ p₃ p₁ p₂ + ∠ p₁ p₃ p₂ + ∠ p₁ 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
p₁ p₂ p₃ : P
h2 : p₂ ≠ p₁
h3 : p₃ ≠ p₁
⊢ InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) + InnerProductGeometry.angle (p₁ -ᵥ p₃) (p₂ -ᵥ p₃) +
      InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) =
    π

Tactic:
rw [← angle_neg_neg (p₁ -ᵥ p₃), ← angle_neg_neg (p₁ -ᵥ p₂), neg_vsub_eq_vsub_rev,
  neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev, neg_vsub_eq_vsub_rev, ←
  vsub_sub_vsub_cancel_right p₃ p₂ p₁, ← vsub_sub_vsub_cancel_right p₂ p₃ p₁]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h2 : p₂ ≠ p₁
h3 : p₃ ≠ p₁
⊢ InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) + InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₃ -ᵥ p₁ - (p₂ -ᵥ p₁)) +
      InnerProductGeometry.angle (p₂ -ᵥ p₁) (p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)) =
    π
-- Mathlib/AlgebraicGeometry/Restrict.lean
theorem Γ_map_morphismRestrict {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) :
    Scheme.Γ.map (f ∣_ U).op =
      Y.presheaf.map (eqToHom U.isOpenEmbedding_obj_top.symm).op ≫
        f.app U ≫ X.presheaf.map (eqToHom (f ⁻¹ᵁ U).isOpenEmbedding_obj_top).op

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ Scheme.Γ.map (f ∣_ U).op = Y.presheaf.map (eqToHom ⋯).op ≫ Scheme.Hom.app f U ≫ X.presheaf.map (eqToHom ⋯).op

Tactic:
rw [Scheme.Γ_map_op, morphismRestrict_appTop f U, f.naturality_assoc, ← X.presheaf.map_comp]

Result:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ Scheme.Hom.app f (U.ι ''ᵁ ⊤) ≫ X.presheaf.map (eqToHom ⋯).op =
    Scheme.Hom.app f (⋯.functor.obj ⊤) ≫
      X.presheaf.map (((Opens.map f.base).map (eqToHom ⋯).op.unop).op ≫ (eqToHom ⋯).op)

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ Scheme.Hom.app f (U.ι ''ᵁ ⊤) ≫ X.presheaf.map (eqToHom ⋯).op =
    Scheme.Hom.app f (⋯.functor.obj ⊤) ≫
      X.presheaf.map (((Opens.map f.base).map (eqToHom ⋯).op.unop).op ≫ (eqToHom ⋯).op)

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Deligne.lean
lemma Gammaℝ_eq_zero_iff {s : ℂ} : Gammaℝ s = 0 ↔ ∃ n : ℕ, s = -(2 * n)

Proof state:
s : ℂ
⊢ s.Gammaℝ = 0 ↔ ∃ n, s = -(2 * ↑n)

Tactic:
simp [Gammaℝ_def, Complex.Gamma_eq_zero_iff, pi_ne_zero, div_eq_iff (two_ne_zero' ℂ), mul_comm]

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem lower_bound_le_one (hN : 1 ≤ N) (hN' : N ≤ 4096) :
    (N : ℝ) * exp (-4 * √(log N)) ≤ 1

Proof state:
case inr
N : ℕ
hN✝ : 1 ≤ N
hN' : N ≤ 4096
hN : 1 < N
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ 1

Tactic:
exact lower_bound_le_one' hN hN'

Result:
no goals

Proof state:
N : ℕ
hN : 1 ≤ N
hN' : N ≤ 4096
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ 1

Tactic:
obtain rfl | hN := hN.eq_or_lt

Result:
case inl
hN : 1 ≤ 1
hN' : 1 ≤ 4096
⊢ ↑1 * rexp (-4 * √(log ↑1)) ≤ 1

case inr
N : ℕ
hN✝ : 1 ≤ N
hN' : N ≤ 4096
hN : 1 < N
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ 1

Proof state:
case inl
hN : 1 ≤ 1
hN' : 1 ≤ 4096
⊢ ↑1 * rexp (-4 * √(log ↑1)) ≤ 1

Tactic:
norm_num

Result:
no goals
-- Mathlib/NumberTheory/Fermat.lean
theorem fermatNumber_eq_fermatNumber_sq_sub_two_mul_fermatNumber_sub_one_sq (n : ℕ) :
    fermatNumber (n + 2) = (fermatNumber (n + 1)) ^ 2 - 2 * (fermatNumber n - 1) ^ 2

Proof state:
n : ℕ
⊢ (n + 2).fermatNumber = (n + 1).fermatNumber ^ 2 - 2 * (n.fermatNumber - 1) ^ 2

Tactic:
simp only [fermatNumber, add_sub_self_right]

Result:
n : ℕ
⊢ 2 ^ 2 ^ (n + 2) + 1 = (2 ^ 2 ^ (n + 1) + 1) ^ 2 - 2 * (2 ^ 2 ^ n) ^ 2

Proof state:
n : ℕ
⊢ 2 ^ 2 ^ (n + 2) + 1 = (2 ^ 2 ^ (n + 1) + 1) ^ 2 - 2 * (2 ^ 2 ^ n) ^ 2

Tactic:
rw [← add_sub_self_right (2 ^ 2 ^ (n + 2) + 1) <| 2 * 2 ^ 2 ^ (n + 1)]

Result:
n : ℕ
⊢ 2 ^ 2 ^ (n + 2) + 1 + 2 * 2 ^ 2 ^ (n + 1) - 2 * 2 ^ 2 ^ (n + 1) = (2 ^ 2 ^ (n + 1) + 1) ^ 2 - 2 * (2 ^ 2 ^ n) ^ 2

Proof state:
n : ℕ
⊢ 2 ^ 2 ^ (n + 2) + 1 + 2 * 2 ^ 2 ^ (n + 1) - 2 * 2 ^ 2 ^ (n + 1) = (2 ^ 2 ^ (n + 1) + 1) ^ 2 - 2 * (2 ^ 2 ^ n) ^ 2

Tactic:
ring_nf

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem forIn'_toArray [Monad m] (l : List α) (b : β) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) :
    forIn' l.toArray b f = forIn' l b (fun a m b => f a (mem_toArray.mpr m) b)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
l : List α
b : β
f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)
⊢ forIn' l.toArray b f = forIn' l b fun a m b => f a ⋯ b

Tactic:
change Array.forIn' _ _ _ = List.forIn' _ _ _

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
l : List α
b : β
f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)
⊢ l.toArray.forIn' b f = l.forIn' b fun a m b => f a ⋯ b

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
l : List α
b : β
f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)
⊢ l.toArray.forIn' b f = l.forIn' b fun a m b => f a ⋯ b

Tactic:
rw [Array.forIn', forIn'_loop_toArray]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
l : List α
b : β
f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)
⊢ (forIn' (drop (l.length - l.toArray.size) l) b fun a m b => f a ⋯ b) = l.forIn' b fun a m b => f a ⋯ b

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
l : List α
b : β
f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)
⊢ (forIn' (drop (l.length - l.toArray.size) l) b fun a m b => f a ⋯ b) = l.forIn' b fun a m b => f a ⋯ b

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
theorem rangeS_algebraMap {R A : Type*} [CommSemiring R] [CommSemiring A] [Algebra R A]
    (S : Subalgebra R A) : (algebraMap S A).rangeS = S.toSubsemiring

Proof state:
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ (algebraMap (↥S) A).rangeS = S.toSubsemiring

Tactic:
rw [algebraMap_eq, Algebra.id.map_eq_id, RingHom.id_comp, ← toSubsemiring_subtype,
  Subsemiring.rangeS_subtype]

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/Supported.lean
theorem supported_inter (s t : Set α) :
    supported M R (s ∩ t) = supported M R s ⊓ supported M R t

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
⊢ supported M R (s ∩ t) = supported M R s ⊓ supported M R t

Tactic:
rw [Set.inter_eq_iInter, supported_iInter, iInf_bool_eq]

Result:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
⊢ supported M R (bif true then s else t) ⊓ supported M R (bif false then s else t) = supported M R s ⊓ supported M R t

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
⊢ supported M R (bif true then s else t) ⊓ supported M R (bif false then s else t) = supported M R s ⊓ supported M R t

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Order/Rearrangement.lean
theorem AntivaryOn.sum_smul_lt_sum_comp_perm_smul_iff (hfg : AntivaryOn f g s)
    (hσ : {x | σ x ≠ x} ⊆ s) :
    ∑ i ∈ s, f i • g i < ∑ i ∈ s, f (σ i) • g i ↔ ¬AntivaryOn (f ∘ σ) g s

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : LinearOrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : AntivaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
⊢ ∑ i ∈ s, f i • g i < ∑ i ∈ s, f (σ i) • g i ↔ ¬AntivaryOn (f ∘ ⇑σ) g ↑s

Tactic:
simp [← hfg.sum_comp_perm_smul_eq_sum_smul_iff hσ, eq_comm, lt_iff_le_and_ne,
  hfg.sum_smul_le_sum_comp_perm_smul hσ]

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem Homeomorph.mulRight_symm (a : G) :
    (Homeomorph.mulRight a).symm = Homeomorph.mulRight a⁻¹

Proof state:
case H
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
a x✝ : G
⊢ (Homeomorph.mulRight a).symm x✝ = (Homeomorph.mulRight a⁻¹) x✝

Tactic:
rfl

Result:
no goals

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
a : G
⊢ (Homeomorph.mulRight a).symm = Homeomorph.mulRight a⁻¹

Tactic:
ext

Result:
case H
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
a x✝ : G
⊢ (Homeomorph.mulRight a).symm x✝ = (Homeomorph.mulRight a⁻¹) x✝
-- Mathlib/Algebra/Lie/Solvable.lean
theorem derivedSeriesOfIdeal_add (k l : ℕ) : D (k + l) I = D k (D l I)

Proof state:
case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
l : ℕ
⊢ D (0 + l) I = D 0 (D l I)

Tactic:
rw [Nat.zero_add, derivedSeriesOfIdeal_zero]

Result:
no goals

Proof state:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
l k : ℕ
ih : D (k + l) I = D k (D l I)
⊢ D (k + 1 + l) I = D (k + 1) (D l I)

Tactic:
rw [Nat.succ_add k l, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_succ, ih]

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k l : ℕ
⊢ D (k + l) I = D k (D l I)

Tactic:
induction k with
| zero => rw [Nat.zero_add, derivedSeriesOfIdeal_zero]
| succ k ih => rw [Nat.succ_add k l, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_succ, ih]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem sumInl_toMatrix_prod_mul [Fintype n] [Fintype p] (M : Matrix n n R)
    (L : List (TransvectionStruct n R)) (N : Matrix p p R) :
    (L.map (toMatrix ∘ sumInl p)).prod * fromBlocks M 0 0 N =
      fromBlocks ((L.map toMatrix).prod * M) 0 0 N

Proof state:
case nil
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
M : Matrix n n R
N : Matrix p p R
⊢ (List.map (toMatrix ∘ sumInl p) []).prod * fromBlocks M 0 0 N = fromBlocks ((List.map toMatrix []).prod * M) 0 0 N

Tactic:
simp

Result:
no goals

Proof state:
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
M : Matrix n n R
L : List (TransvectionStruct n R)
N : Matrix p p R
⊢ (List.map (toMatrix ∘ sumInl p) L).prod * fromBlocks M 0 0 N = fromBlocks ((List.map toMatrix L).prod * M) 0 0 N

Tactic:
induction L with
| nil => simp
| cons t L IH => simp [Matrix.mul_assoc, IH, toMatrix_sumInl, fromBlocks_multiply]

Result:
no goals

Proof state:
case cons
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
M : Matrix n n R
N : Matrix p p R
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : (List.map (toMatrix ∘ sumInl p) L).prod * fromBlocks M 0 0 N = fromBlocks ((List.map toMatrix L).prod * M) 0 0 N
⊢ (List.map (toMatrix ∘ sumInl p) (t :: L)).prod * fromBlocks M 0 0 N =
    fromBlocks ((List.map toMatrix (t :: L)).prod * M) 0 0 N

Tactic:
simp [Matrix.mul_assoc, IH, toMatrix_sumInl, fromBlocks_multiply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem allOnes_shiftLeft_or_shiftLeft {x : BitVec w} {n : Nat} :
    BitVec.allOnes w <<< n ||| x <<< n = BitVec.allOnes w <<< n

Proof state:
w : Nat
x : BitVec w
n : Nat
⊢ allOnes w <<< n ||| x <<< n = allOnes w <<< n

Tactic:
simp [← shiftLeft_or_distrib]

Result:
no goals
-- Mathlib/Probability/Martingale/Basic.lean
theorem sub_supermartingale [Preorder E] [AddLeftMono E]
    (hf : Submartingale f ℱ μ) (hg : Supermartingale g ℱ μ) : Submartingale (f - g) ℱ μ

Proof state:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst✝¹ : Preorder E
inst✝ : AddLeftMono E
hf : Submartingale f ℱ μ
hg : Supermartingale g ℱ μ
⊢ Submartingale (f + -g) ℱ μ

Tactic:
exact hf.add hg.neg

Result:
no goals

Proof state:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst✝¹ : Preorder E
inst✝ : AddLeftMono E
hf : Submartingale f ℱ μ
hg : Supermartingale g ℱ μ
⊢ Submartingale (f - g) ℱ μ

Tactic:
rw [sub_eq_add_neg]

Result:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst✝¹ : Preorder E
inst✝ : AddLeftMono E
hf : Submartingale f ℱ μ
hg : Supermartingale g ℱ μ
⊢ Submartingale (f + -g) ℱ μ