harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast_append {l : List α} (h : l ++ l' ≠ []) :
    (l ++ l').getLast h =
      if h' : l'.isEmpty then
        l.getLast (by simp_all [isEmpty_iff])
      else
        l'.getLast (by simp_all [isEmpty_iff])

Proof state:
case isTrue
α : Type u_1
l' l : List α
h : l ++ l' ≠ []
h'✝ : l'.isEmpty = true
h' : l' = []
⊢ (l ++ l').getLast h = l.getLast ⋯

Tactic:
subst h'

Result:
case isTrue
α : Type u_1
l : List α
h : l ++ [] ≠ []
h' : [].isEmpty = true
⊢ (l ++ []).getLast h = l.getLast ⋯

Proof state:
case isTrue
α : Type u_1
l' l : List α
h : l ++ l' ≠ []
h' : l'.isEmpty = true
⊢ (l ++ l').getLast h = l.getLast ⋯

Tactic:
simp only [isEmpty_iff] at h'

Result:
case isTrue
α : Type u_1
l' l : List α
h : l ++ l' ≠ []
h'✝ : l'.isEmpty = true
h' : l' = []
⊢ (l ++ l').getLast h = l.getLast ⋯

Proof state:
case isFalse
α : Type u_1
l' l : List α
h : l ++ l' ≠ []
h' : ¬l'.isEmpty = true
⊢ (l ++ l').getLast h = l'.getLast ⋯

Tactic:
simp [isEmpty_iff] at h'

Result:
case isFalse
α : Type u_1
l' l : List α
h : l ++ l' ≠ []
h'✝ : ¬l'.isEmpty = true
h' : ¬l' = []
⊢ (l ++ l').getLast h = l'.getLast ⋯

Proof state:
α : Type ?u.313829
l' l : List α
h : l ++ l' ≠ []
h' : ¬l'.isEmpty = true
⊢ l' ≠ []

Tactic:
simp_all [isEmpty_iff]

Result:
no goals

Proof state:
case isFalse
α : Type u_1
l' l : List α
h : l ++ l' ≠ []
h'✝ : ¬l'.isEmpty = true
h' : ¬l' = []
⊢ (l ++ l').getLast h = l'.getLast ⋯

Tactic:
simp [h']

Result:
no goals

Proof state:
α : Type u_1
l' l : List α
h : l ++ l' ≠ []
⊢ (l ++ l').getLast h = if h' : l'.isEmpty = true then l.getLast ⋯ else l'.getLast ⋯

Tactic:
split <;> rename_i h'

Result:
case isTrue
α : Type u_1
l' l : List α
h : l ++ l' ≠ []
h' : l'.isEmpty = true
⊢ (l ++ l').getLast h = l.getLast ⋯

case isFalse
α : Type u_1
l' l : List α
h : l ++ l' ≠ []
h' : ¬l'.isEmpty = true
⊢ (l ++ l').getLast h = l'.getLast ⋯

Proof state:
case isTrue
α : Type u_1
l : List α
h : l ++ [] ≠ []
h' : [].isEmpty = true
⊢ (l ++ []).getLast h = l.getLast ⋯

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.313829
l' l : List α
h : l ++ l' ≠ []
h' : l'.isEmpty = true
⊢ l ≠ []

Tactic:
simp_all [isEmpty_iff]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Dickson.lean
theorem dickson_add_two (n : ℕ) :
    dickson k a (n + 2) = X * dickson k a (n + 1) - C a * dickson k a n

Proof state:
R : Type u_1
inst✝ : CommRing R
k : ℕ
a : R
n : ℕ
⊢ dickson k a (n + 2) = X * dickson k a (n + 1) - C a * dickson k a n

Tactic:
rw [dickson]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Equiv.lean
theorem finSuccEquiv_apply (p : MvPolynomial (Fin (n + 1)) R) :
    finSuccEquiv R n p =
      eval₂Hom (Polynomial.C.comp (C : R →+* MvPolynomial (Fin n) R))
        (fun i : Fin (n + 1) => Fin.cases Polynomial.X (fun k => Polynomial.C (X k)) i) p

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
⊢ (finSuccEquiv R n) p =
    (eval₂Hom (Polynomial.C.comp C) fun i => Fin.cases Polynomial.X (fun k => Polynomial.C (X k)) i) p

Tactic:
rw [← finSuccEquiv_eq, RingHom.coe_coe]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem rootSet_mapsTo {p : T[X]} {S S'} [CommRing S] [IsDomain S] [Algebra T S] [CommRing S']
    [IsDomain S'] [Algebra T S'] [NoZeroSMulDivisors T S'] (f : S →ₐ[T] S') :
    (p.rootSet S).MapsTo f (p.rootSet S')

Proof state:
T : Type w
inst✝⁷ : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra T S
inst✝³ : CommRing S'
inst✝² : IsDomain S'
inst✝¹ : Algebra T S'
inst✝ : NoZeroSMulDivisors T S'
f : S →ₐ[T] S'
h₀ : map (algebraMap T S') p = 0
⊢ map (algebraMap T S) p = 0

Tactic:
obtain rfl : p = 0 :=
  map_injective _ (FaithfulSMul.algebraMap_injective T S') (by rwa [Polynomial.map_zero])

Result:
T : Type w
inst✝⁷ : CommRing T
S : Type u_1
S' : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra T S
inst✝³ : CommRing S'
inst✝² : IsDomain S'
inst✝¹ : Algebra T S'
inst✝ : NoZeroSMulDivisors T S'
f : S →ₐ[T] S'
h₀ : map (algebraMap T S') 0 = 0
⊢ map (algebraMap T S) 0 = 0

Proof state:
T : Type w
inst✝⁷ : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra T S
inst✝³ : CommRing S'
inst✝² : IsDomain S'
inst✝¹ : Algebra T S'
inst✝ : NoZeroSMulDivisors T S'
f : S →ₐ[T] S'
⊢ Set.MapsTo (⇑f) (p.rootSet S) (p.rootSet S')

Tactic:
refine rootSet_maps_to' (fun h₀ => ?_) f

Result:
T : Type w
inst✝⁷ : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra T S
inst✝³ : CommRing S'
inst✝² : IsDomain S'
inst✝¹ : Algebra T S'
inst✝ : NoZeroSMulDivisors T S'
f : S →ₐ[T] S'
h₀ : map (algebraMap T S') p = 0
⊢ map (algebraMap T S) p = 0

Proof state:
T : Type w
inst✝⁷ : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra T S
inst✝³ : CommRing S'
inst✝² : IsDomain S'
inst✝¹ : Algebra T S'
inst✝ : NoZeroSMulDivisors T S'
f : S →ₐ[T] S'
h₀ : map (algebraMap T S') p = 0
⊢ map (algebraMap T S') p = map (algebraMap T S') 0

Tactic:
rwa [Polynomial.map_zero]

Result:
no goals

Proof state:
T : Type w
inst✝⁷ : CommRing T
S : Type u_1
S' : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra T S
inst✝³ : CommRing S'
inst✝² : IsDomain S'
inst✝¹ : Algebra T S'
inst✝ : NoZeroSMulDivisors T S'
f : S →ₐ[T] S'
h₀ : map (algebraMap T S') 0 = 0
⊢ map (algebraMap T S) 0 = 0

Tactic:
exact Polynomial.map_zero _

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma b_relation : 4 * W.b₈ = W.b₂ * W.b₆ - W.b₄ ^ 2

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ 4 * (W.a₁ ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2) =
    (W.a₁ ^ 2 + 4 * W.a₂) * (W.a₃ ^ 2 + 4 * W.a₆) - (2 * W.a₄ + W.a₁ * W.a₃) ^ 2

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ 4 * W.b₈ = W.b₂ * W.b₆ - W.b₄ ^ 2

Tactic:
simp only [b₂, b₄, b₆, b₈]

Result:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ 4 * (W.a₁ ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2) =
    (W.a₁ ^ 2 + 4 * W.a₂) * (W.a₃ ^ 2 + 4 * W.a₆) - (2 * W.a₄ + W.a₁ * W.a₃) ^ 2
-- Mathlib/Algebra/Vertex/VertexOperator.lean
theorem coeff_eq_zero_of_lt_order (A : VertexOperator R V) (n : ℤ) (x : V)
    (h : n < HahnSeries.order ((HahnModule.of R).symm (A x))) : coeff A n x = 0

Proof state:
R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
A : VertexOperator R V
n : ℤ
x : V
h : n < ((HahnModule.of R).symm (A x)).order
⊢ (coeff A n) x = 0

Tactic:
rw [coeff_eq_ncoeff, ncoeff_eq_zero_of_lt_order A (-n - 1) x]

Result:
R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
A : VertexOperator R V
n : ℤ
x : V
h : n < ((HahnModule.of R).symm (A x)).order
⊢ -(-n - 1) - 1 < ((HahnModule.of R).symm (A x)).order

Proof state:
R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
A : VertexOperator R V
n : ℤ
x : V
h : n < ((HahnModule.of R).symm (A x)).order
⊢ -(-n - 1) - 1 < ((HahnModule.of R).symm (A x)).order

Tactic:
omega

Result:
no goals
-- Mathlib/GroupTheory/IndexNormal.lean
theorem normal_of_index_eq_minFac_card (hHp : H.index = (Nat.card G).minFac) :
    H.Normal

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
⊢ H.normalCore.index ∣ H.index !

Tactic:
rw [normalCore_eq_ker, index_ker, index_eq_card, ← Nat.card_perm]

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
⊢ Nat.card ↥(toPermHom G (G ⧸ H)).range ∣ Nat.card (Equiv.Perm (G ⧸ H))

Proof state:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = 1
hG0 : ¬Nat.card G = 0
hG1 : Nat.card G = 1
⊢ H.Normal

Tactic:
exact normal_of_index_eq_one hHp

Result:
no goals

Proof state:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
⊢ H.normalCore.index = H.index

Tactic:
have h : H.normalCore.index ∣ H.index ! := by
  rw [normalCore_eq_ker, index_ker, index_eq_card, ← Nat.card_perm]
  exact card_subgroup_dvd_card (toPermHom G (G ⧸ H)).range

Result:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
h : H.normalCore.index ∣ H.index !
⊢ H.normalCore.index = H.index

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
h : H.normalCore.index ∣ H.index !
hr1 : H.normalCore.index ≠ 1
⊢ H.normalCore.index.Coprime (H.index - 1)!

Tactic:
rw [Nat.coprime_factorial_iff hr1]

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
h : H.normalCore.index ∣ H.index !
hr1 : H.normalCore.index ≠ 1
⊢ H.index - 1 < H.normalCore.index.minFac
-- Mathlib/Analysis/Analytic/Basic.lean
theorem HasFPowerSeriesWithinOnBall.uniform_geometric_approx {r' : ℝ≥0}
    (hf : HasFPowerSeriesWithinOnBall f p s x r) (h : (r' : ℝ≥0∞) < r) :
    ∃ a ∈ Ioo (0 : ℝ) 1,
      ∃ C > 0, ∀ y ∈ Metric.ball (0 : E) r', ∀ n, x + y ∈ insert x s →
      ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n

Proof state:
case intro.intro.intro.intro.h.hab
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ↑r' < r
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : C > 0
hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n
y : E
hy : y ∈ Metric.ball 0 ↑r'
n : ℕ
ys : x + y ∈ insert x s
yr' : ‖y‖ < ↑r'
this : 0 ≤ a
⊢ a * (‖y‖ / ↑r') ≤ a

Tactic:
exact mul_le_of_le_one_right ha.1.le (div_le_one_of_le₀ yr'.le r'.coe_nonneg)

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem MonoidHom.map_finprod_plift (f : M →* N) (g : α → M)
    (h : (mulSupport <| g ∘ PLift.down).Finite) : f (∏ᶠ x, g x) = ∏ᶠ x, f (g x)

Proof state:
M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
g : α → M
h : (mulSupport (g ∘ PLift.down)).Finite
⊢ mulSupport ((fun x => f (g x)) ∘ PLift.down) ⊆ ↑h.toFinset

Tactic:
rw [h.coe_toFinset]

Result:
M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
g : α → M
h : (mulSupport (g ∘ PLift.down)).Finite
⊢ mulSupport ((fun x => f (g x)) ∘ PLift.down) ⊆ mulSupport (g ∘ PLift.down)

Proof state:
M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
g : α → M
h : (mulSupport (g ∘ PLift.down)).Finite
⊢ mulSupport ((fun x => f (g x)) ∘ PLift.down) ⊆ mulSupport (g ∘ PLift.down)

Tactic:
exact mulSupport_comp_subset f.map_one (g ∘ PLift.down)

Result:
no goals

Proof state:
M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
g : α → M
h : (mulSupport (g ∘ PLift.down)).Finite
⊢ f (∏ᶠ (x : α), g x) = ∏ᶠ (x : α), f (g x)

Tactic:
rw [finprod_eq_prod_plift_of_mulSupport_subset h.coe_toFinset.ge,
  finprod_eq_prod_plift_of_mulSupport_subset, map_prod]

Result:
M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
g : α → M
h : (mulSupport (g ∘ PLift.down)).Finite
⊢ mulSupport ((fun x => f (g x)) ∘ PLift.down) ⊆ ↑h.toFinset
-- Mathlib/Algebra/Algebra/Spectrum.lean
theorem add_mem_add_iff {a : A} {r s : R} : r + s ∈ σ (↑ₐ s + a) ↔ r ∈ σ a

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r s : R
⊢ r + s ∈ σ (↑ₐ s + a) ↔ r ∈ σ a

Tactic:
rw [add_mem_iff, neg_add_cancel_left]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Primitive.lean
theorem isSimpleOrder_blockMem_iff_isPreprimitive [IsPretransitive G X] [Nontrivial X] (a : X) :
    IsSimpleOrder (BlockMem G a) ↔ IsPreprimitive G X

Proof state:
case mp.inr.h
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
h : IsSimpleOrder (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = ↑⊤
⊢ ↑⊤ = Set.univ

Tactic:
rfl

Result:
no goals

Proof state:
case mp
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
h : IsSimpleOrder (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
⊢ ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B

Tactic:
intro B haB hB

Result:
case mp
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
h : IsSimpleOrder (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
⊢ IsTrivialBlock B

Proof state:
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
⊢ IsSimpleOrder (BlockMem G a) ↔ IsPreprimitive G X

Tactic:
constructor

Result:
case mp
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
⊢ IsSimpleOrder (BlockMem G a) → IsPreprimitive G X

case mpr
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
⊢ IsPreprimitive G X → IsSimpleOrder (BlockMem G a)

Proof state:
case mpr.eq_bot_or_eq_top
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
hGX' : IsPreprimitive G X
⊢ ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤

Tactic:
rintro ⟨B, haB, hB⟩

Result:
case mpr.eq_bot_or_eq_top.mk.intro
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
⊢ ⟨B, ⋯⟩ = ⊥ ∨ ⟨B, ⋯⟩ = ⊤

Proof state:
case mp.inr.h
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
h : IsSimpleOrder (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = ↑⊤
⊢ B = Set.univ

Tactic:
rw [hB']

Result:
case mp.inr.h
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
h : IsSimpleOrder (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = ↑⊤
⊢ ↑⊤ = Set.univ
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem sum_integral_adjacent_intervals_Ico {a : ℕ → ℝ} {m n : ℕ} (hmn : m ≤ n)
    (hint : ∀ k ∈ Ico m n, IntervalIntegrable f μ (a k) (a <| k + 1)) :
    ∑ k ∈ Finset.Ico m n, ∫ x in a k..a <| k + 1, f x ∂μ = ∫ x in a m..a n, f x ∂μ

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
hint : ∀ k ∈ Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))
⊢ ∑ k ∈ Finset.Ico m n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a n, f x ∂μ

Tactic:
revert hint

Result:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
⊢ (∀ k ∈ Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))) →
    ∑ k ∈ Finset.Ico m n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a n, f x ∂μ

Proof state:
case refine_2
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
⊢ ∀ (n : ℕ),
    m ≤ n →
      ((∀ k ∈ Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))) →
          ∑ k ∈ Finset.Ico m n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a n, f x ∂μ) →
        (∀ k ∈ Ico m (n + 1), IntervalIntegrable f μ (a k) (a (k + 1))) →
          ∑ k ∈ Finset.Ico m (n + 1), ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a (n + 1), f x ∂μ

Tactic:
intro p hmp IH h

Result:
case refine_2
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  (∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))) →
    ∑ k ∈ Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a p, f x ∂μ
h : ∀ k ∈ Ico m (p + 1), IntervalIntegrable f μ (a k) (a (k + 1))
⊢ ∑ k ∈ Finset.Ico m (p + 1), ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a (p + 1), f x ∂μ
-- Mathlib/Analysis/InnerProductSpace/Dual.lean
theorem ext_inner_right_basis {ι : Type*} {x y : E} (b : Basis ι 𝕜 E)
    (h : ∀ i : ι, ⟪x, b i⟫ = ⟪y, b i⟫) : x = y

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪x, b i⟫_𝕜 = ⟪y, b i⟫_𝕜
i : ι
⊢ (starRingEnd 𝕜) ⟪x, b i⟫_𝕜 = ⟪b i, y⟫_𝕜

Tactic:
conv_rhs => rw [← inner_conj_symm]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪x, b i⟫_𝕜 = ⟪y, b i⟫_𝕜
i : ι
⊢ (starRingEnd 𝕜) ⟪x, b i⟫_𝕜 = (starRingEnd 𝕜) ⟪y, b i⟫_𝕜

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪x, b i⟫_𝕜 = ⟪y, b i⟫_𝕜
i : ι
⊢ ⟪b i, x⟫_𝕜 = ⟪b i, y⟫_𝕜

Tactic:
rw [← inner_conj_symm]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪x, b i⟫_𝕜 = ⟪y, b i⟫_𝕜
i : ι
⊢ (starRingEnd 𝕜) ⟪x, b i⟫_𝕜 = ⟪b i, y⟫_𝕜

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪x, b i⟫_𝕜 = ⟪y, b i⟫_𝕜
⊢ x = y

Tactic:
refine ext_inner_left_basis b fun i => ?_

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪x, b i⟫_𝕜 = ⟪y, b i⟫_𝕜
i : ι
⊢ ⟪b i, x⟫_𝕜 = ⟪b i, y⟫_𝕜

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪x, b i⟫_𝕜 = ⟪y, b i⟫_𝕜
i : ι
⊢ (starRingEnd 𝕜) ⟪x, b i⟫_𝕜 = (starRingEnd 𝕜) ⟪y, b i⟫_𝕜

Tactic:
exact congr_arg conj (h i)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem flatMap_reverse {β} (l : Array α) (f : α → Array β) :
    (l.reverse.flatMap f) = (l.flatMap (reverse ∘ f)).reverse

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : α → Array β
⊢ flatMap f l.reverse = (flatMap (reverse ∘ f) l).reverse

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
f : α → Array β
toList✝ : List α
⊢ flatMap f { toList := toList✝ }.reverse = (flatMap (reverse ∘ f) { toList := toList✝ }).reverse

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → Array β
toList✝ : List α
⊢ flatMap f { toList := toList✝ }.reverse = (flatMap (reverse ∘ f) { toList := toList✝ }).reverse

Tactic:
simp [List.flatMap_reverse, Function.comp_def]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma baseChange_addX (P Q : Fin 3 → A) : (W'.baseChange B).toJacobian.addX (f ∘ P) (f ∘ Q) =
    f ((W'.baseChange A).toJacobian.addX P Q)

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Jacobian R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P Q : Fin 3 → A
⊢ (baseChange W' B).toJacobian.addX (⇑f ∘ P) (⇑f ∘ Q) = f ((baseChange W' A).toJacobian.addX P Q)

Tactic:
rw [← RingHom.coe_coe, ← map_addX, map_baseChange]

Result:
no goals
-- Mathlib/Data/List/DropRight.lean
theorem rdropWhile_concat (x : α) :
    rdropWhile p (l ++ [x]) = if p x then rdropWhile p l else l ++ [x]

Proof state:
α : Type u_1
p : α → Bool
l : List α
x : α
⊢ (match p x with
      | true => dropWhile p l.reverse
      | false => x :: l.reverse).reverse =
    if p x = true then (dropWhile p l.reverse).reverse else l ++ [x]

Tactic:
split_ifs with h <;> simp [h]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : List α
x : α
⊢ rdropWhile p (l ++ [x]) = if p x = true then rdropWhile p l else l ++ [x]

Tactic:
simp only [rdropWhile, dropWhile, reverse_append, reverse_singleton, singleton_append]

Result:
α : Type u_1
p : α → Bool
l : List α
x : α
⊢ (match p x with
      | true => dropWhile p l.reverse
      | false => x :: l.reverse).reverse =
    if p x = true then (dropWhile p l.reverse).reverse else l ++ [x]
-- Mathlib/Order/SuccPred/Basic.lean
theorem succ_eq_csInf [ConditionallyCompleteLattice α] [SuccOrder α] [NoMaxOrder α] (a : α) :
    succ a = sInf (Set.Ioi a)

Proof state:
α : Type u_1
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
⊢ sInf (Ioi a) ≤ succ a

Tactic:
exact csInf_le ⟨a, fun b => le_of_lt⟩ <| lt_succ a

Result:
no goals

Proof state:
α : Type u_1
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
⊢ succ a = sInf (Ioi a)

Tactic:
apply (le_csInf nonempty_Ioi fun b => succ_le_of_lt).antisymm

Result:
α : Type u_1
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
⊢ sInf (Ioi a) ≤ succ a
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem norm_div_tan_oangle_add_right_of_oangle_eq_pi_div_two {x y : V}
    (h : o.oangle x y = ↑(π / 2)) : ‖y‖ / Real.Angle.tan (o.oangle x (x + y)) = ‖x‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle x (x + y)).sign = 1
⊢ ‖y‖ / (o.oangle x (x + y)).tan = ‖x‖

Tactic:
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
  InnerProductGeometry.norm_div_tan_angle_add_of_inner_eq_zero
    (o.inner_eq_zero_of_oangle_eq_pi_div_two h)
    (Or.inr (o.right_ne_zero_of_oangle_eq_pi_div_two h))]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle x (x + y)).sign = 1

Tactic:
rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ ‖y‖ / (o.oangle x (x + y)).tan = ‖x‖

Tactic:
have hs : (o.oangle x (x + y)).sign = 1 := by
  rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle x (x + y)).sign = 1
⊢ ‖y‖ / (o.oangle x (x + y)).tan = ‖x‖