harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Exponent.lean
theorem Commute.of_orderOf_dvd_two [IsCancelMul G] (h : ∀ g : G, orderOf g ∣ 2) (a b : G) :
    Commute a b

Proof state:
G : Type u
inst✝¹ : Monoid G
inst✝ : IsCancelMul G
a b : G
h : ∀ (g : G), g ^ 2 = 1
⊢ a ^ 2 * b ^ 2 = 1

Tactic:
rw [h, h, mul_one]

Result:
no goals

Proof state:
G : Type u
inst✝¹ : Monoid G
inst✝ : IsCancelMul G
a b : G
h : ∀ (g : G), g ^ 2 = 1
⊢ a * (a * b) * b = a ^ 2 * b ^ 2

Tactic:
simp [pow_two, mul_assoc]

Result:
no goals

Proof state:
G : Type u
inst✝¹ : Monoid G
inst✝ : IsCancelMul G
a b : G
h : ∀ (g : G), g ^ 2 = 1
⊢ (a * b) ^ 2 = a * (b * a) * b

Tactic:
simp [pow_two, mul_assoc]

Result:
no goals

Proof state:
G : Type u
inst✝¹ : Monoid G
inst✝ : IsCancelMul G
a b : G
h : ∀ (g : G), g ^ 2 = 1
⊢ a * (a * b) * b = a * (b * a) * b

Tactic:
calc
  a * (a * b) * b = a ^ 2 * b ^ 2 := by simp [pow_two, mul_assoc]
  _ = 1 := by rw [h, h, mul_one]
  _ = (a * b) ^ 2 := by rw [h]
  _ = a * (b * a) * b := by simp [pow_two, mul_assoc]

Result:
no goals

Proof state:
G : Type u
inst✝¹ : Monoid G
inst✝ : IsCancelMul G
h : ∀ (g : G), orderOf g ∣ 2
a b : G
⊢ Commute a b

Tactic:
simp_rw [orderOf_dvd_iff_pow_eq_one] at h

Result:
G : Type u
inst✝¹ : Monoid G
inst✝ : IsCancelMul G
a b : G
h : ∀ (g : G), g ^ 2 = 1
⊢ Commute a b

Proof state:
G : Type u
inst✝¹ : Monoid G
inst✝ : IsCancelMul G
a b : G
h : ∀ (g : G), g ^ 2 = 1
⊢ 1 = (a * b) ^ 2

Tactic:
rw [h]

Result:
no goals

Proof state:
G : Type u
inst✝¹ : Monoid G
inst✝ : IsCancelMul G
a b : G
h : ∀ (g : G), g ^ 2 = 1
⊢ Commute a b

Tactic:
rw [commute_iff_eq, ← mul_right_inj a, ← mul_left_inj b]

Result:
G : Type u
inst✝¹ : Monoid G
inst✝ : IsCancelMul G
a b : G
h : ∀ (g : G), g ^ 2 = 1
⊢ a * (a * b) * b = a * (b * a) * b
-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
theorem Gamma_integrand_deriv_integrable_B {s : ℂ} (hs : 0 < s.re) {Y : ℝ} (hY : 0 ≤ Y) :
    IntervalIntegrable (fun x : ℝ => (-x).exp * (s * x ^ (s - 1)) : ℝ → ℂ) volume 0 Y

Proof state:
case left.hcont
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))
x : ℝ
hx : x ∈ Ioc 0 Y
⊢ ContinuousAt (fun x => x ^ (s - 1)) ↑x

Tactic:
exact continuousAt_cpow_const <| ofReal_mem_slitPlane.2 hx.1

Result:
no goals

Proof state:
case right
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ HasFiniteIntegral (fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))) (volume.restrict (Ioc 0 Y))

Tactic:
rw [← hasFiniteIntegral_norm_iff]

Result:
case right
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ HasFiniteIntegral (fun a => ‖s * (↑(rexp (-a)) * ↑a ^ (s - 1))‖) (volume.restrict (Ioc 0 Y))

Proof state:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ IntervalIntegrable (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) volume 0 Y

Tactic:
rw [this, intervalIntegrable_iff_integrableOn_Ioc_of_le hY]

Result:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ IntegrableOn (fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))) (Ioc 0 Y) volume

Proof state:
case h
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
x✝ : ℝ
⊢ ↑(rexp (-x✝)) * (s * ↑x✝ ^ (s - 1)) = s * (↑(rexp (-x✝)) * ↑x✝ ^ (s - 1))

Tactic:
ring

Result:
no goals
-- Mathlib/Data/Multiset/Fintype.lean
theorem card_coe (m : Multiset α) : Fintype.card m = Multiset.card m

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ Fintype.card m.ToType = m.card

Tactic:
rw [Fintype.card_congr m.coeEquiv]

Result:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ Fintype.card { x // x ∈ m.toEnumFinset } = m.card

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ Fintype.card { x // x ∈ m.toEnumFinset } = m.card

Tactic:
simp only [Fintype.card_coe, card_toEnumFinset]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Scheme.lean
@[ext (iff := false)]
protected lemma ext {f g : X ⟶ Y} (h_base : f.base = g.base)
    (h_app : ∀ U, f.app U ≫ X.presheaf.map
      (eqToHom congr((Opens.map $h_base.symm).obj U)).op = g.app U) : f = g

Proof state:
X Y : Scheme
toHom_1✝¹ toHom_1✝ : X.Hom Y.toLocallyRingedSpace
h_base : { toHom_1 := toHom_1✝¹ }.base = { toHom_1 := toHom_1✝ }.base
h_app : ∀ (U : Y.Opens), { toHom_1 := toHom_1✝¹ }.app U ≫ X.presheaf.map (eqToHom ⋯).op = { toHom_1 := toHom_1✝ }.app U
U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace
⊢ (toHom_1✝¹.toShHom.c ≫ whiskerRight (eqToHom ⋯) X.presheaf).app (op U) = toHom_1✝.toShHom.c.app (op U)

Tactic:
simpa using h_app U

Result:
no goals

Proof state:
case mk.mk
X Y : Scheme
toHom_1✝¹ toHom_1✝ : X.Hom Y.toLocallyRingedSpace
h_base : { toHom_1 := toHom_1✝¹ }.base = { toHom_1 := toHom_1✝ }.base
h_app : ∀ (U : Y.Opens), { toHom_1 := toHom_1✝¹ }.app U ≫ X.presheaf.map (eqToHom ⋯).op = { toHom_1 := toHom_1✝ }.app U
⊢ { toHom_1 := toHom_1✝¹ } = { toHom_1 := toHom_1✝ }

Tactic:
congr 1

Result:
case mk.mk.e_toHom_1
X Y : Scheme
toHom_1✝¹ toHom_1✝ : X.Hom Y.toLocallyRingedSpace
h_base : { toHom_1 := toHom_1✝¹ }.base = { toHom_1 := toHom_1✝ }.base
h_app : ∀ (U : Y.Opens), { toHom_1 := toHom_1✝¹ }.app U ≫ X.presheaf.map (eqToHom ⋯).op = { toHom_1 := toHom_1✝ }.app U
⊢ toHom_1✝¹ = toHom_1✝

Proof state:
case mk
X Y : Scheme
g : X ⟶ Y
toHom_1✝ : X.Hom Y.toLocallyRingedSpace
h_base : { toHom_1 := toHom_1✝ }.base = g.base
h_app : ∀ (U : Y.Opens), { toHom_1 := toHom_1✝ }.app U ≫ X.presheaf.map (eqToHom ⋯).op = app g U
⊢ { toHom_1 := toHom_1✝ } = g

Tactic:
cases g

Result:
case mk.mk
X Y : Scheme
toHom_1✝¹ toHom_1✝ : X.Hom Y.toLocallyRingedSpace
h_base : { toHom_1 := toHom_1✝¹ }.base = { toHom_1 := toHom_1✝ }.base
h_app : ∀ (U : Y.Opens), { toHom_1 := toHom_1✝¹ }.app U ≫ X.presheaf.map (eqToHom ⋯).op = { toHom_1 := toHom_1✝ }.app U
⊢ { toHom_1 := toHom_1✝¹ } = { toHom_1 := toHom_1✝ }

Proof state:
case mk.mk.e_toHom_1
X Y : Scheme
toHom_1✝¹ toHom_1✝ : X.Hom Y.toLocallyRingedSpace
h_base : { toHom_1 := toHom_1✝¹ }.base = { toHom_1 := toHom_1✝ }.base
h_app : ∀ (U : Y.Opens), { toHom_1 := toHom_1✝¹ }.app U ≫ X.presheaf.map (eqToHom ⋯).op = { toHom_1 := toHom_1✝ }.app U
⊢ toHom_1✝¹ = toHom_1✝

Tactic:
exact LocallyRingedSpace.Hom.ext' <| SheafedSpace.ext _ _ h_base
  (TopCat.Presheaf.ext fun U ↦ by simpa using h_app U)

Result:
no goals

Proof state:
X Y : Scheme
f g : X ⟶ Y
h_base : f.base = g.base
h_app : ∀ (U : Y.Opens), app f U ≫ X.presheaf.map (eqToHom ⋯).op = app g U
⊢ f = g

Tactic:
cases f

Result:
case mk
X Y : Scheme
g : X ⟶ Y
toHom_1✝ : X.Hom Y.toLocallyRingedSpace
h_base : { toHom_1 := toHom_1✝ }.base = g.base
h_app : ∀ (U : Y.Opens), { toHom_1 := toHom_1✝ }.app U ≫ X.presheaf.map (eqToHom ⋯).op = app g U
⊢ { toHom_1 := toHom_1✝ } = g
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem one_le_lift_iff {a : Cardinal.{u}} :
    (1 : Cardinal) ≤ lift.{v} a ↔ 1 ≤ a

Proof state:
a : Cardinal.{u}
⊢ 1 ≤ lift.{v, u} a ↔ 1 ≤ a

Tactic:
simpa using nat_le_lift_iff (n := 1)

Result:
no goals
-- Mathlib/RingTheory/Coprime/Lemmas.lean
theorem Nat.Coprime.cast {R : Type*} [CommRing R] {a b : ℕ} (h : Nat.Coprime a b) :
    IsCoprime (a : R) (b : R)

Proof state:
R : Type u_1
inst✝ : CommRing R
a b : ℕ
h : IsCoprime ↑a ↑b
⊢ IsCoprime ↑a ↑b

Tactic:
rw [← Int.cast_natCast a, ← Int.cast_natCast b]

Result:
R : Type u_1
inst✝ : CommRing R
a b : ℕ
h : IsCoprime ↑a ↑b
⊢ IsCoprime ↑↑a ↑↑b

Proof state:
R : Type u_1
inst✝ : CommRing R
a b : ℕ
h : IsCoprime ↑a ↑b
⊢ IsCoprime ↑↑a ↑↑b

Tactic:
exact IsCoprime.intCast h

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
a b : ℕ
h : a.Coprime b
⊢ IsCoprime ↑a ↑b

Tactic:
rw [← isCoprime_iff_coprime] at h

Result:
R : Type u_1
inst✝ : CommRing R
a b : ℕ
h : IsCoprime ↑a ↑b
⊢ IsCoprime ↑a ↑b
-- Mathlib/Tactic/ReduceModChar.lean
lemma CharP.neg_eq_sub_one_mul {α : Type _} [Ring α] (n : ℕ) (inst : CharP α n) (b : α)
    (a : ℕ) (a' : α) (p : IsNat (n - 1 : α) a) (pa : a = a') :
    -b = a' * b

Proof state:
α : Type u_1
inst✝ : Ring α
n : ℕ
inst : CharP α n
b : α
a : ℕ
a' : α
p : IsNat (↑n - 1) a
pa : ↑a = a'
⊢ -1 * b = (↑n - 1) * b

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Ring α
n : ℕ
inst : CharP α n
b : α
a : ℕ
a' : α
p : IsNat (↑n - 1) a
pa : ↑a = a'
⊢ -b = a' * b

Tactic:
rw [← pa, ← p.out, ← neg_one_mul]

Result:
α : Type u_1
inst✝ : Ring α
n : ℕ
inst : CharP α n
b : α
a : ℕ
a' : α
p : IsNat (↑n - 1) a
pa : ↑a = a'
⊢ -1 * b = (↑n - 1) * b
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem norm_image_sub_le_of_norm_hasFDerivWithin_le
    (hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (bound : ∀ x ∈ s, ‖f' x‖ ≤ C) (hs : Convex ℝ s)
    (xs : x ∈ s) (ys : y ∈ s) : ‖f y - f x‖ ≤ C * ‖y - x‖

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
⊢ ‖f y - f x‖ ≤ C * ‖y - x‖

Tactic:
letI : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜

Result:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
⊢ ‖f y - f x‖ ≤ C * ‖y - x‖

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
C : ℝ
s : Set E
x y : E
f' : E → E →L[𝕜] G
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖ ≤ C
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
this✝ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ G := RestrictScalars.normedSpace ℝ 𝕜 G
g : ℝ → E := ⇑(AffineMap.lineMap x y)
segm : MapsTo g (Icc 0 1) s
t : ℝ
ht : t ∈ Icc 0 1
⊢ HasDerivWithinAt (f ∘ g) ((f' (g t)) (y - x)) (Icc 0 1) t

Tactic:
simpa using ((hf (g t) (segm ht)).restrictScalars ℝ).comp_hasDerivWithinAt _
  AffineMap.hasDerivWithinAt_lineMap segm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem reverseAux_reverseAux (as bs cs : List α) : reverseAux (reverseAux as bs) cs = reverseAux bs (reverseAux (reverseAux as []) cs)

Proof state:
α : Type u
as bs cs : List α
⊢ (as.reverseAux bs).reverseAux cs = bs.reverseAux ((as.reverseAux nil).reverseAux cs)

Tactic:
induction as generalizing bs cs with
| nil => rfl
| cons a as ih => simp [reverseAux, ih (a::bs), ih [a]]

Result:
no goals

Proof state:
case cons
α : Type u
a : α
as : List α
ih : ∀ (bs cs : List α), (as.reverseAux bs).reverseAux cs = bs.reverseAux ((as.reverseAux nil).reverseAux cs)
bs cs : List α
⊢ ((a :: as).reverseAux bs).reverseAux cs = bs.reverseAux (((a :: as).reverseAux nil).reverseAux cs)

Tactic:
simp [reverseAux, ih (a::bs), ih [a]]

Result:
no goals

Proof state:
case nil
α : Type u
bs cs : List α
⊢ (nil.reverseAux bs).reverseAux cs = bs.reverseAux ((nil.reverseAux nil).reverseAux cs)

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
theorem Odd.add_dvd_pow_add_pow [CommRing α] (x y : α) {n : ℕ} (h : Odd n) :
    x + y ∣ x ^ n + y ^ n

Proof state:
α : Type u
inst✝ : CommRing α
x y : α
n : ℕ
h : Odd n
h₁ : (∑ i ∈ range n, x ^ i * (-y) ^ (n - 1 - i)) * (x - -y) = x ^ n - (-y) ^ n
⊢ x + y ∣ x ^ n + y ^ n

Tactic:
rw [Odd.neg_pow h y, sub_neg_eq_add, sub_neg_eq_add] at h₁

Result:
α : Type u
inst✝ : CommRing α
x y : α
n : ℕ
h : Odd n
h₁ : (∑ i ∈ range n, x ^ i * (-y) ^ (n - 1 - i)) * (x + y) = x ^ n + y ^ n
⊢ x + y ∣ x ^ n + y ^ n

Proof state:
α : Type u
inst✝ : CommRing α
x y : α
n : ℕ
h : Odd n
⊢ x + y ∣ x ^ n + y ^ n

Tactic:
have h₁ := geom_sum₂_mul x (-y) n

Result:
α : Type u
inst✝ : CommRing α
x y : α
n : ℕ
h : Odd n
h₁ : (∑ i ∈ range n, x ^ i * (-y) ^ (n - 1 - i)) * (x - -y) = x ^ n - (-y) ^ n
⊢ x + y ∣ x ^ n + y ^ n

Proof state:
α : Type u
inst✝ : CommRing α
x y : α
n : ℕ
h : Odd n
h₁ : (∑ i ∈ range n, x ^ i * (-y) ^ (n - 1 - i)) * (x + y) = x ^ n + y ^ n
⊢ x + y ∣ x ^ n + y ^ n

Tactic:
exact Dvd.intro_left _ h₁

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem neg_mul (x y : BitVec w) : -x * y = -(x * y)

Proof state:
w : Nat
x y : BitVec w
⊢ -x * y = -(x * y)

Tactic:
apply eq_of_toInt_eq

Result:
case a
w : Nat
x y : BitVec w
⊢ (-x * y).toInt = (-(x * y)).toInt

Proof state:
case a
w : Nat
x y : BitVec w
⊢ (-x * y).toInt = (-(x * y)).toInt

Tactic:
simp [toInt_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mem_filterMap {f : α → Option β} {l : Array α} {b : β} :
    b ∈ filterMap f l ↔ ∃ a, a ∈ l ∧ f a = some b

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : Array α
b : β
⊢ b ∈ filterMap f l ↔ ∃ a, a ∈ l ∧ f a = some b

Tactic:
simp only [mem_def, toList_filterMap, List.mem_filterMap]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem sup_direction_le (s₁ s₂ : AffineSubspace k P) :
    s₁.direction ⊔ s₂.direction ≤ (s₁ ⊔ s₂).direction

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
⊢ Submodule.span k (↑s₁ -ᵥ ↑s₁) ⊔ Submodule.span k (↑s₂ -ᵥ ↑s₂) ≤ Submodule.span k (↑(s₁ ⊔ s₂) -ᵥ ↑(s₁ ⊔ s₂))

Tactic:
exact
  sup_le
    (sInf_le_sInf fun p hp => Set.Subset.trans (vsub_self_mono (le_sup_left : s₁ ≤ s₁ ⊔ s₂)) hp)
    (sInf_le_sInf fun p hp => Set.Subset.trans (vsub_self_mono (le_sup_right : s₂ ≤ s₁ ⊔ s₂)) hp)

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
⊢ s₁.direction ⊔ s₂.direction ≤ (s₁ ⊔ s₂).direction

Tactic:
simp only [direction_eq_vectorSpan, vectorSpan_def]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
⊢ Submodule.span k (↑s₁ -ᵥ ↑s₁) ⊔ Submodule.span k (↑s₂ -ᵥ ↑s₂) ≤ Submodule.span k (↑(s₁ ⊔ s₂) -ᵥ ↑(s₁ ⊔ s₂))
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem update_eq_add_sub_coeff {R : Type*} [Ring R] (p : R[X]) (n : ℕ) (a : R) :
    p.update n a = p + Polynomial.C (a - p.coeff n) * Polynomial.X ^ n

Proof state:
case a
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
a : R
n✝ : ℕ
⊢ (if n✝ = n then a else p.coeff n✝) = p.coeff n✝ + if n✝ = n then a - p.coeff n else 0

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

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
a : R
⊢ p.update n a = p + C (a - p.coeff n) * X ^ n

Tactic:
ext

Result:
case a
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
a : R
n✝ : ℕ
⊢ (p.update n a).coeff n✝ = (p + C (a - p.coeff n) * X ^ n).coeff n✝

Proof state:
case a
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
a : R
n✝ : ℕ
⊢ (p.update n a).coeff n✝ = (p + C (a - p.coeff n) * X ^ n).coeff n✝

Tactic:
rw [coeff_update_apply, coeff_add, coeff_C_mul_X_pow]

Result:
case a
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
a : R
n✝ : ℕ
⊢ (if n✝ = n then a else p.coeff n✝) = p.coeff n✝ + if n✝ = n then a - p.coeff n else 0
-- Mathlib/Topology/Order/LowerUpperTopology.lean
lemma isTopologicalSpace_basis (U : Set α) : IsOpen U ↔ U = univ ∨ ∃ a, (Ici a)ᶜ = U

Proof state:
case a.mpr
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
⊢ (∃ S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}, U = ⋃₀ S) → ∃ a, (Ici a)ᶜ = U

Tactic:
intro ⟨S, hS1, hS2⟩

Result:
case a.mpr
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
⊢ ∃ a, (Ici a)ᶜ = U

Proof state:
case a.mp
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
a : α
ha : (Ici a)ᶜ = U
⊢ ∃ S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}, U = ⋃₀ S

Tactic:
use {U}

Result:
case h
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
a : α
ha : (Ici a)ᶜ = U
⊢ {U} ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s} ∧ U = ⋃₀ {U}

Proof state:
case neg
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
⊢ IsOpen U ↔ U = univ ∨ ∃ a, (Ici a)ᶜ = U

Tactic:
refine ⟨?_, isTopologicalBasis_insert_univ_subbasis.isOpen⟩

Result:
case neg
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
⊢ IsOpen U → U = univ ∨ ∃ a, (Ici a)ᶜ = U

Proof state:
case h.left
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
a : α
ha : (Ici a)ᶜ = U
⊢ {U} ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}

Tactic:
apply subset_trans (singleton_subset_iff.mpr _) (subset_insert _ _)

Result:
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
a : α
ha : (Ici a)ᶜ = U
⊢ U ∈ {s | ∃ a, (Ici a)ᶜ = s}

Proof state:
case neg
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
⊢ IsOpen U → U = univ ∨ ∃ a, (Ici a)ᶜ = U

Tactic:
intro hO

Result:
case neg
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
⊢ U = univ ∨ ∃ a, (Ici a)ᶜ = U

Proof state:
case h.a
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
b : α
hb : b ∈ Ici (sSup {a | (Ici a)ᶜ ∈ S})
⊢ ∀ i ∈ S, b ∉ i

Tactic:
intro s hs

Result:
case h.a
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen U
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
b : α
hb : b ∈ Ici (sSup {a | (Ici a)ᶜ ∈ S})
s : Set α
hs : s ∈ S
⊢ b ∉ s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findSome?_append {l₁ l₂ : List α} : (l₁ ++ l₂).findSome? f = (l₁.findSome? f).or (l₂.findSome? f)

Proof state:
case nil
α : Type u_1
α✝ : Type u_2
f : α → Option α✝
l₂ : List α
⊢ findSome? f ([] ++ l₂) = (findSome? f []).or (findSome? f l₂)

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
α✝ : Type u_2
f : α → Option α✝
l₂ : List α
x : α
xs : List α
ih : findSome? f (xs ++ l₂) = (findSome? f xs).or (findSome? f l₂)
⊢ (match f x with
    | some b => some b
    | none => findSome? f (xs ++ l₂)) =
    (match f x with
        | some b => some b
        | none => findSome? f xs).or
      (findSome? f l₂)

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
α : Type u_1
α✝ : Type u_2
f : α → Option α✝
l₁ l₂ : List α
⊢ findSome? f (l₁ ++ l₂) = (findSome? f l₁).or (findSome? f l₂)

Tactic:
induction l₁ with
| nil => simp
| cons x xs ih =>
  simp only [cons_append, findSome?]
  split <;> simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
α✝ : Type u_2
f : α → Option α✝
l₂ : List α
x : α
xs : List α
ih : findSome? f (xs ++ l₂) = (findSome? f xs).or (findSome? f l₂)
⊢ findSome? f (x :: xs ++ l₂) = (findSome? f (x :: xs)).or (findSome? f l₂)

Tactic:
simp only [cons_append, findSome?]

Result:
case cons
α : Type u_1
α✝ : Type u_2
f : α → Option α✝
l₂ : List α
x : α
xs : List α
ih : findSome? f (xs ++ l₂) = (findSome? f xs).or (findSome? f l₂)
⊢ (match f x with
    | some b => some b
    | none => findSome? f (xs ++ l₂)) =
    (match f x with
        | some b => some b
        | none => findSome? f xs).or
      (findSome? f l₂)
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma polynomialX_eq : W'.polynomialX =
    C W'.a₁ * X 1 * X 2 - (C 3 * X 0 ^ 2 + C (2 * W'.a₂) * X 0 * X 2 ^ 2 + C W'.a₄ * X 2 ^ 4)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
⊢ W'.polynomialX = C W'.a₁ * X y * X z - (C 3 * X x ^ 2 + C (2 * W'.a₂) * X x * X z ^ 2 + C W'.a₄ * X z ^ 4)

Tactic:
rw [polynomialX, polynomial]

Result:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
⊢ (pderiv x)
      (X y ^ 2 + C W'.a₁ * X x * X y * X z + C W'.a₃ * X y * X z ^ 3 -
        (X x ^ 3 + C W'.a₂ * X x ^ 2 * X z ^ 2 + C W'.a₄ * X x * X z ^ 4 + C W'.a₆ * X z ^ 6)) =
    C W'.a₁ * X y * X z - (C 3 * X x ^ 2 + C (2 * W'.a₂) * X x * X z ^ 2 + C W'.a₄ * X z ^ 4)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
⊢ ↑2 * X y ^ (2 - 1) * 0 + (((0 * X x + C W'.a₁ * 1) * X y + C W'.a₁ * X x * 0) * X z + C W'.a₁ * X x * X y * 0) +
        ((0 * X y + C W'.a₃ * 0) * X z ^ 3 + C W'.a₃ * X y * (↑3 * X z ^ (3 - 1) * 0)) -
      (↑3 * X x ^ (3 - 1) * 1 +
            ((0 * X x ^ 2 + C W'.a₂ * (↑2 * X x ^ (2 - 1) * 1)) * X z ^ 2 +
              C W'.a₂ * X x ^ 2 * (↑2 * X z ^ (2 - 1) * 0)) +
          ((0 * X x + C W'.a₄ * 1) * X z ^ 4 + C W'.a₄ * X x * (↑4 * X z ^ (4 - 1) * 0)) +
        (0 * X z ^ 6 + C W'.a₆ * (↑6 * X z ^ (6 - 1) * 0))) =
    C W'.a₁ * X y * X z - (3 * X x ^ 2 + 2 * C W'.a₂ * X x * X z ^ 2 + C W'.a₄ * X z ^ 4)

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
⊢ (pderiv x)
      (X y ^ 2 + C W'.a₁ * X x * X y * X z + C W'.a₃ * X y * X z ^ 3 -
        (X x ^ 3 + C W'.a₂ * X x ^ 2 * X z ^ 2 + C W'.a₄ * X x * X z ^ 4 + C W'.a₆ * X z ^ 6)) =
    C W'.a₁ * X y * X z - (C 3 * X x ^ 2 + C (2 * W'.a₂) * X x * X z ^ 2 + C W'.a₄ * X z ^ 4)

Tactic:
pderiv_simp

Result:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
⊢ ↑2 * X y ^ (2 - 1) * 0 + (((0 * X x + C W'.a₁ * 1) * X y + C W'.a₁ * X x * 0) * X z + C W'.a₁ * X x * X y * 0) +
        ((0 * X y + C W'.a₃ * 0) * X z ^ 3 + C W'.a₃ * X y * (↑3 * X z ^ (3 - 1) * 0)) -
      (↑3 * X x ^ (3 - 1) * 1 +
            ((0 * X x ^ 2 + C W'.a₂ * (↑2 * X x ^ (2 - 1) * 1)) * X z ^ 2 +
              C W'.a₂ * X x ^ 2 * (↑2 * X z ^ (2 - 1) * 0)) +
          ((0 * X x + C W'.a₄ * 1) * X z ^ 4 + C W'.a₄ * X x * (↑4 * X z ^ (4 - 1) * 0)) +
        (0 * X z ^ 6 + C W'.a₆ * (↑6 * X z ^ (6 - 1) * 0))) =
    C W'.a₁ * X y * X z - (3 * X x ^ 2 + 2 * C W'.a₂ * X x * X z ^ 2 + C W'.a₄ * X z ^ 4)
-- Mathlib/Data/Finset/Sum.lean
@[simp] lemma toLeft_insert_inl : (insert (inl a) u).toLeft = insert a u.toLeft

Proof state:
case h
α : Type u_1
β : Type u_2
a : α
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
y : α
⊢ y ∈ (insert (inl a) u).toLeft ↔ y ∈ insert a u.toLeft

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
a : α
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (insert (inl a) u).toLeft = insert a u.toLeft

Tactic:
ext y

Result:
case h
α : Type u_1
β : Type u_2
a : α
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
y : α
⊢ y ∈ (insert (inl a) u).toLeft ↔ y ∈ insert a u.toLeft
-- Mathlib/Topology/Category/LightProfinite/AsLimit.lean
lemma proj_comp_transitionMapLE' {n m : ℕ} (h : n ≤ m) :
    S.transitionMapLE h ∘ S.proj m  = S.proj n

Proof state:
S : LightProfinite
n m : ℕ
h : n ≤ m
⊢ ⇑(ConcreteCategory.hom (S.transitionMapLE h)) ∘ ⇑(ConcreteCategory.hom (S.proj m)) =
    ⇑(ConcreteCategory.hom (S.proj n))

Tactic:
rw [← S.proj_comp_transitionMapLE h]

Result:
S : LightProfinite
n m : ℕ
h : n ≤ m
⊢ ⇑(ConcreteCategory.hom (S.transitionMapLE h)) ∘ ⇑(ConcreteCategory.hom (S.proj m)) =
    ⇑(ConcreteCategory.hom (S.proj m ≫ S.diagram.map (Opposite.op (homOfLE h))))

Proof state:
S : LightProfinite
n m : ℕ
h : n ≤ m
⊢ ⇑(ConcreteCategory.hom (S.transitionMapLE h)) ∘ ⇑(ConcreteCategory.hom (S.proj m)) =
    ⇑(ConcreteCategory.hom (S.proj m ≫ S.diagram.map (Opposite.op (homOfLE h))))

Tactic:
rfl

Result:
no goals