harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Solvable.lean
theorem IsSimpleGroup.derivedSeries_succ {n : ℕ} : derivedSeries G n.succ = commutator G

Proof state:
case succ.inr
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
n : ℕ
ih : derivedSeries G n.succ = _root_.commutator G
h : ⁅⊤, ⊤⁆ = ⊤
⊢ ⁅⁅⊤, ⊤⁆, ⁅⊤, ⊤⁆⁆ = ⁅⊤, ⊤⁆

Tactic:
rwa [h]

Result:
no goals

Proof state:
case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
n : ℕ
ih : derivedSeries G n.succ = _root_.commutator G
⊢ derivedSeries G (n + 1).succ = _root_.commutator G

Tactic:
rw [_root_.derivedSeries_succ, ih, _root_.commutator]

Result:
case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
n : ℕ
ih : derivedSeries G n.succ = _root_.commutator G
⊢ ⁅⁅⊤, ⊤⁆, ⁅⊤, ⊤⁆⁆ = ⁅⊤, ⊤⁆

Proof state:
case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
n : ℕ
ih : derivedSeries G n.succ = _root_.commutator G
⊢ ⁅⁅⊤, ⊤⁆, ⁅⊤, ⊤⁆⁆ = ⁅⊤, ⊤⁆

Tactic:
rcases (commutator_normal (⊤ : Subgroup G) (⊤ : Subgroup G)).eq_bot_or_eq_top with h | h

Result:
case succ.inl
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
n : ℕ
ih : derivedSeries G n.succ = _root_.commutator G
h : ⁅⊤, ⊤⁆ = ⊥
⊢ ⁅⁅⊤, ⊤⁆, ⁅⊤, ⊤⁆⁆ = ⁅⊤, ⊤⁆

case succ.inr
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
n : ℕ
ih : derivedSeries G n.succ = _root_.commutator G
h : ⁅⊤, ⊤⁆ = ⊤
⊢ ⁅⁅⊤, ⊤⁆, ⁅⊤, ⊤⁆⁆ = ⁅⊤, ⊤⁆

Proof state:
case succ.inl
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
n : ℕ
ih : derivedSeries G n.succ = _root_.commutator G
h : ⁅⊤, ⊤⁆ = ⊥
⊢ ⁅⁅⊤, ⊤⁆, ⁅⊤, ⊤⁆⁆ = ⁅⊤, ⊤⁆

Tactic:
rw [h, commutator_bot_left]

Result:
no goals

Proof state:
case zero
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
⊢ derivedSeries G (Nat.succ 0) = _root_.commutator G

Tactic:
exact derivedSeries_one G

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem HasDerivWithinAt.const_mul (c : 𝔸) (hd : HasDerivWithinAt d d' s x) :
    HasDerivWithinAt (fun y => c * d y) (c * d') s x

Proof state:
case h.e'_9
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
d : 𝕜 → 𝔸
d' c : 𝔸
hd : HasDerivWithinAt d d' s x
⊢ c * d' = 0 * d x + c * d'

Tactic:
rw [zero_mul, zero_add]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
d : 𝕜 → 𝔸
d' c : 𝔸
hd : HasDerivWithinAt d d' s x
⊢ HasDerivWithinAt (fun y => c * d y) (c * d') s x

Tactic:
convert (hasDerivWithinAt_const x s c).mul hd using 1

Result:
case h.e'_9
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
d : 𝕜 → 𝔸
d' c : 𝔸
hd : HasDerivWithinAt d d' s x
⊢ c * d' = 0 * d x + c * d'
-- Mathlib/Order/Interval/Set/Basic.lean
@[simp] lemma Ici_True : Ici True = {True}

Proof state:
⊢ Ici True = {True}

Tactic:
aesop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem reverse_append (as bs : List α) : (as ++ bs).reverse = bs.reverse ++ as.reverse

Proof state:
α : Type u_1
as bs : List α
⊢ (as ++ bs).reverse = bs.reverse ++ as.reverse

Tactic:
induction as <;> simp_all

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem isCoprime_map [Field k] (f : R →+* k) : IsCoprime (p.map f) (q.map f) ↔ IsCoprime p q

Proof state:
R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
⊢ IsCoprime (map f p) (map f q) ↔ IsCoprime p q

Tactic:
classical
rw [← EuclideanDomain.gcd_isUnit_iff, ← EuclideanDomain.gcd_isUnit_iff, gcd_map, isUnit_map]

Result:
no goals

Proof state:
R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
⊢ IsCoprime (map f p) (map f q) ↔ IsCoprime p q

Tactic:
rw [← EuclideanDomain.gcd_isUnit_iff, ← EuclideanDomain.gcd_isUnit_iff, gcd_map, isUnit_map]

Result:
no goals
-- Mathlib/Algebra/Group/Conj.lean
theorem isConj_iff_eq {α : Type*} [CommMonoid α] {a b : α} : IsConj a b ↔ a = b :=
  ⟨fun ⟨c, hc⟩ => by
    rw [SemiconjBy, mul_comm, ← Units.mul_inv_eq_iff_eq_mul, mul_assoc, c.mul_inv, mul_one] at hc
    exact hc, fun h => by rw [h]⟩

Proof state:
α : Type u_1
inst✝ : CommMonoid α
a b : α
h : a = b
⊢ IsConj a b

Tactic:
rw [h]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommMonoid α
a b : α
x✝ : IsConj a b
c : αˣ
hc : a = b
⊢ a = b

Tactic:
exact hc

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommMonoid α
a b : α
x✝ : IsConj a b
c : αˣ
hc : SemiconjBy (↑c) a b
⊢ a = b

Tactic:
rw [SemiconjBy, mul_comm, ← Units.mul_inv_eq_iff_eq_mul, mul_assoc, c.mul_inv, mul_one] at hc

Result:
α : Type u_1
inst✝ : CommMonoid α
a b : α
x✝ : IsConj a b
c : αˣ
hc : a = b
⊢ a = b
-- Mathlib/Data/Complex/Trigonometric.lean
theorem tanh_mul_I : tanh (x * I) = tan x * I

Proof state:
x : ℂ
⊢ tanh (x * I) = tan x * I

Tactic:
rw [tanh_eq_sinh_div_cosh, cosh_mul_I, sinh_mul_I, mul_div_right_comm, tan]

Result:
no goals
-- Mathlib/Combinatorics/Colex.lean
private lemma antisymm_aux (hst : toColex s ≤ toColex t) (hts : toColex t ≤ toColex s) : s ⊆ t

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
hst : { ofColex := s } ≤ { ofColex := t }
hts : { ofColex := t } ≤ { ofColex := s }
a : α
has : a ∈ s
hat : a ∉ t
⊢ False

Tactic:
have ⟨_b, hb₁, hb₂, _⟩ := trans_aux hst hts has hat

Result:
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
hst : { ofColex := s } ≤ { ofColex := t }
hts : { ofColex := t } ≤ { ofColex := s }
a : α
has : a ∈ s
hat : a ∉ t
_b : α
hb₁ : _b ∈ s
hb₂ : _b ∉ s
right✝ : a ≤ _b
⊢ False

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
hst : { ofColex := s } ≤ { ofColex := t }
hts : { ofColex := t } ≤ { ofColex := s }
⊢ s ⊆ t

Tactic:
intro a has

Result:
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
hst : { ofColex := s } ≤ { ofColex := t }
hts : { ofColex := t } ≤ { ofColex := s }
a : α
has : a ∈ s
⊢ a ∈ t

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
hst : { ofColex := s } ≤ { ofColex := t }
hts : { ofColex := t } ≤ { ofColex := s }
a : α
has : a ∈ s
hat : a ∉ t
_b : α
hb₁ : _b ∈ s
hb₂ : _b ∉ s
right✝ : a ≤ _b
⊢ False

Tactic:
exact hb₂ hb₁

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
hst : { ofColex := s } ≤ { ofColex := t }
hts : { ofColex := t } ≤ { ofColex := s }
a : α
has : a ∈ s
⊢ a ∈ t

Tactic:
by_contra! hat

Result:
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
hst : { ofColex := s } ≤ { ofColex := t }
hts : { ofColex := t } ≤ { ofColex := s }
a : α
has : a ∈ s
hat : a ∉ t
⊢ False
-- Mathlib/Order/Antisymmetrization.lean
theorem le_iff_lt_or_antisymmRel : a ≤ b ↔ a < b ∨ AntisymmRel (· ≤ ·) a b

Proof state:
α : Type u_1
a b : α
inst✝ : Preorder α
⊢ a ≤ b ↔ a < b ∨ AntisymmRel (fun x1 x2 => x1 ≤ x2) a b

Tactic:
rw [lt_iff_le_not_le, AntisymmRel]

Result:
α : Type u_1
a b : α
inst✝ : Preorder α
⊢ a ≤ b ↔ a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a

Proof state:
α : Type u_1
a b : α
inst✝ : Preorder α
⊢ a ≤ b ↔ a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a

Tactic:
tauto

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem isoPullback_hom_fst (h : IsPullback fst snd f g) [HasPullback f g] :
    h.isoPullback.hom ≫ pullback.fst _ _ = fst

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : HasPullback f g
⊢ (limit.isoLimitCone { cone := PullbackCone.mk fst snd ⋯, isLimit := h.isLimit }).inv ≫ pullback.fst f g = fst

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : HasPullback f g
⊢ h.isoPullback.hom ≫ pullback.fst f g = fst

Tactic:
dsimp [isoPullback, cone, CommSq.cone]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : HasPullback f g
⊢ (limit.isoLimitCone { cone := PullbackCone.mk fst snd ⋯, isLimit := h.isLimit }).inv ≫ pullback.fst f g = fst
-- Mathlib/Algebra/Order/BigOperators/Expect.lean
lemma exists_lt_of_lt_expect (hs : s.Nonempty) (h : a < 𝔼 i ∈ s, f i) : ∃ x ∈ s, a < f x

Proof state:
ι : Type u_1
α : Type u_2
inst✝² : LinearOrderedAddCommMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulMono ℚ≥0 α
s : Finset ι
f : ι → α
a : α
hs : s.Nonempty
h : a < 𝔼 i ∈ s, f i
⊢ ∃ x ∈ s, a < f x

Tactic:
contrapose! h

Result:
ι : Type u_1
α : Type u_2
inst✝² : LinearOrderedAddCommMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulMono ℚ≥0 α
s : Finset ι
f : ι → α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, f x ≤ a
⊢ 𝔼 i ∈ s, f i ≤ a

Proof state:
ι : Type u_1
α : Type u_2
inst✝² : LinearOrderedAddCommMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulMono ℚ≥0 α
s : Finset ι
f : ι → α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, f x ≤ a
⊢ 𝔼 i ∈ s, f i ≤ a

Tactic:
exact expect_le hs h

Result:
no goals
-- Mathlib/Order/Monotone/Basic.lean
theorem Monotone.ne_of_lt_of_lt_int {f : ℤ → α} (hf : Monotone f) (n : ℤ) {x : α} (h1 : f n < x)
    (h2 : x < f (n + 1)) (a : ℤ) : f a ≠ x

Proof state:
α : Type u
inst✝ : Preorder α
f : ℤ → α
hf : Monotone f
n : ℤ
x : α
h1 : f n < x
h2 : x < f (n + 1)
a : ℤ
⊢ f a ≠ x

Tactic:
rintro rfl

Result:
α : Type u
inst✝ : Preorder α
f : ℤ → α
hf : Monotone f
n a : ℤ
h1 : f n < f a
h2 : f a < f (n + 1)
⊢ False

Proof state:
α : Type u
inst✝ : Preorder α
f : ℤ → α
hf : Monotone f
n a : ℤ
h1 : f n < f a
h2 : f a < f (n + 1)
⊢ False

Tactic:
exact (hf.reflect_lt h1).not_le (Int.le_of_lt_add_one <| hf.reflect_lt h2)

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem derivWithin_inter (ht : t ∈ 𝓝 x) : derivWithin f (s ∩ t) x = derivWithin f s x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s t : Set 𝕜
ht : t ∈ 𝓝 x
⊢ derivWithin f (s ∩ t) x = derivWithin f s x

Tactic:
unfold derivWithin

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s t : Set 𝕜
ht : t ∈ 𝓝 x
⊢ (fderivWithin 𝕜 f (s ∩ t) x) 1 = (fderivWithin 𝕜 f s x) 1

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s t : Set 𝕜
ht : t ∈ 𝓝 x
⊢ (fderivWithin 𝕜 f (s ∩ t) x) 1 = (fderivWithin 𝕜 f s x) 1

Tactic:
rw [fderivWithin_inter ht]

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean
@[reassoc (attr := simp)]
lemma pullbackAwayιIso_inv_fst :
    (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).inv ≫ Limits.pullback.fst _ _ =
      Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx))

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
⊢ (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).inv ≫ Limits.pullback.fst (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm') =
    Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx))

Tactic:
rw [← pullbackAwayιIso_hom_SpecMap_awayMap_left, Iso.inv_hom_id_assoc]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem Δ_of_isCharNeTwoNF : W.Δ = -64 * W.a₂ ^ 3 * W.a₆ + 16 * W.a₂ ^ 2 * W.a₄ ^ 2 - 64 * W.a₄ ^ 3
    - 432 * W.a₆ ^ 2 + 288 * W.a₂ * W.a₄ * W.a₆

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ W.Δ = -64 * W.a₂ ^ 3 * W.a₆ + 16 * W.a₂ ^ 2 * W.a₄ ^ 2 - 64 * W.a₄ ^ 3 - 432 * W.a₆ ^ 2 + 288 * W.a₂ * W.a₄ * W.a₆

Tactic:
rw [Δ, b₂_of_isCharNeTwoNF, b₄_of_isCharNeTwoNF, b₆_of_isCharNeTwoNF, b₈_of_isCharNeTwoNF]

Result:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ -(4 * W.a₂) ^ 2 * (4 * W.a₂ * W.a₆ - W.a₄ ^ 2) - 8 * (2 * W.a₄) ^ 3 - 27 * (4 * W.a₆) ^ 2 +
      9 * (4 * W.a₂) * (2 * W.a₄) * (4 * W.a₆) =
    -64 * W.a₂ ^ 3 * W.a₆ + 16 * W.a₂ ^ 2 * W.a₄ ^ 2 - 64 * W.a₄ ^ 3 - 432 * W.a₆ ^ 2 + 288 * W.a₂ * W.a₄ * W.a₆

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ -(4 * W.a₂) ^ 2 * (4 * W.a₂ * W.a₆ - W.a₄ ^ 2) - 8 * (2 * W.a₄) ^ 3 - 27 * (4 * W.a₆) ^ 2 +
      9 * (4 * W.a₂) * (2 * W.a₄) * (4 * W.a₆) =
    -64 * W.a₂ ^ 3 * W.a₆ + 16 * W.a₂ ^ 2 * W.a₄ ^ 2 - 64 * W.a₄ ^ 3 - 432 * W.a₆ ^ 2 + 288 * W.a₂ * W.a₄ * W.a₆

Tactic:
ring1

Result:
no goals
-- Mathlib/Data/List/SplitLengths.lean
theorem splitLengths_length_getElem {α : Type*} (l : List α) (sz : List ℕ)
    (h : sz.sum ≤ l.length) (i : ℕ) (hi : i < (sz.splitLengths l).length) :
    (sz.splitLengths l)[i].length = sz[i]'(by simpa using hi)

Proof state:
α : Type u_2
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
i : ℕ
hi : i < (sz.splitLengths l).length
⊢ (sz.splitLengths l)[i].length = sz[i]

Tactic:
have := map_splitLengths_length l sz h

Result:
α : Type u_2
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
i : ℕ
hi : i < (sz.splitLengths l).length
this : map length (sz.splitLengths l) = sz
⊢ (sz.splitLengths l)[i].length = sz[i]

Proof state:
α : Type u_2
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
i : ℕ
hi : i < (sz.splitLengths l).length
this : map length (sz.splitLengths l) = sz
⊢ (map length (sz.splitLengths l))[i] = sz[i]

Tactic:
simp [this]

Result:
no goals

Proof state:
α : Type u_2
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
i : ℕ
hi : i < (sz.splitLengths l).length
this : map length (sz.splitLengths l) = sz
⊢ (sz.splitLengths l)[i].length = sz[i]

Tactic:
rw [← List.getElem_map List.length]

Result:
α : Type u_2
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
i : ℕ
hi : i < (sz.splitLengths l).length
this : map length (sz.splitLengths l) = sz
⊢ (map length (sz.splitLengths l))[i] = sz[i]

α : Type u_2
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
i : ℕ
hi : i < (sz.splitLengths l).length
this : map length (sz.splitLengths l) = sz
⊢ i < (map length (sz.splitLengths l)).length

Proof state:
α : Type u_2
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
i : ℕ
hi : i < (sz.splitLengths l).length
this : map length (sz.splitLengths l) = sz
⊢ i < (map length (sz.splitLengths l)).length

Tactic:
simpa using hi

Result:
no goals

Proof state:
α✝ : Type u_1
l✝ : List α✝
sz✝ : List ℕ
α : Type u_2
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
i : ℕ
hi : i < (sz.splitLengths l).length
⊢ i < sz.length

Tactic:
simpa using hi

Result:
no goals
-- Mathlib/Data/Real/Basic.lean
theorem ofCauchy_sup (a b) : (⟨⟦a ⊔ b⟧⟩ : ℝ) = ⟨⟦a⟧⟩ ⊔ ⟨⟦b⟧⟩ :=
  show _ = sup _ _ by
    rw [sup_def]
    rfl

Proof state:
a b : CauSeq ℚ abs
⊢ { cauchy := ⟦a ⊔ b⟧ } = Real.sup { cauchy := ⟦a⟧ } { cauchy := ⟦b⟧ }

Tactic:
rw [sup_def]

Result:
a b : CauSeq ℚ abs
⊢ { cauchy := ⟦a ⊔ b⟧ } =
    match { cauchy := ⟦a⟧ }, { cauchy := ⟦b⟧ } with
    | { cauchy := x }, { cauchy := y } => { cauchy := Quotient.map₂ (fun x1 x2 => x1 ⊔ x2) ⋯ x y }

Proof state:
a b : CauSeq ℚ abs
⊢ { cauchy := ⟦a ⊔ b⟧ } =
    match { cauchy := ⟦a⟧ }, { cauchy := ⟦b⟧ } with
    | { cauchy := x }, { cauchy := y } => { cauchy := Quotient.map₂ (fun x1 x2 => x1 ⊔ x2) ⋯ x y }

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_eq_iff_eq_mul_self (hx : 0 ≤ x) (hy : 0 ≤ y) : √x = y ↔ y * y = x

Proof state:
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ √x = y ↔ y * y = x

Tactic:
rw [sqrt_eq_iff_mul_self_eq hx hy, eq_comm]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/Monoid.lean
theorem Ico_add_bij : BijOn (· + d) (Ico a b) (Ico (a + d) (b + d))

Proof state:
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun x => x + d) (Ico a b) (Ico (a + d) (b + d))

Tactic:
rw [← Ici_inter_Iio, ← Ici_inter_Iio]

Result:
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun x => x + d) (Ici a ∩ Iio b) (Ici (a + d) ∩ Iio (b + d))

Proof state:
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun x => x + d) (Ici a ∩ Iio b) (Ici (a + d) ∩ Iio (b + d))

Tactic:
exact
  (Ici_add_bij a d).inter_mapsTo (fun x hx => add_lt_add_right hx _) fun x hx =>
    lt_of_add_lt_add_right hx.2

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@[simp]
lemma leftShift_smul (a n' : ℤ) (hn' : n + a = n') (x : R) :
    (x • γ).leftShift a n' hn' = x • γ.leftShift a n' hn'

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
x : R
p q : ℤ
hpq : p + n' = q
⊢ p + a + n = q

Tactic:
omega

Result:
no goals

Proof state:
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
x : R
p q : ℤ
hpq : p + n' = q
⊢ ((x • γ).leftShift a n' hn').v p q hpq = (x • γ.leftShift a n' hn').v p q hpq

Tactic:
dsimp

Result:
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
x : R
p q : ℤ
hpq : p + n' = q
⊢ ((x • γ).leftShift a n' hn').v p q hpq = x • (γ.leftShift a n' hn').v p q hpq

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
x : R
⊢ (x • γ).leftShift a n' hn' = x • γ.leftShift a n' hn'

Tactic:
ext p q hpq

Result:
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
x : R
p q : ℤ
hpq : p + n' = q
⊢ ((x • γ).leftShift a n' hn').v p q hpq = (x • γ.leftShift a n' hn').v p q hpq

Proof state:
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
x : R
p q : ℤ
hpq : p + n' = q
⊢ ((x • γ).leftShift a n' hn').v p q hpq = x • (γ.leftShift a n' hn').v p q hpq

Tactic:
simp only [leftShift_v _ a n' hn' p q hpq (p + a) (by omega), smul_v, Linear.comp_smul,
  smul_comm x]

Result:
no goals
-- Mathlib/Probability/Independence/ZeroOne.lean
theorem Kernel.indep_limsup_atTop_self (h_le : ∀ n, s n ≤ m0) (h_indep : iIndep s κ μα) :
    Indep (limsup s atTop) (limsup s atTop) κ μα

Proof state:
case refine_1.intro.intro
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}
b : ι
hb : a < b
c : ι
hc : c ≥ b
hct : c ∈ t
⊢ False

Tactic:
suffices ∀ i ∈ t, i < c from lt_irrefl c (this c hct)

Result:
case refine_1.intro.intro
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}
b : ι
hb : a < b
c : ι
hc : c ≥ b
hct : c ∈ t
⊢ ∀ i ∈ t, i < c

Proof state:
case refine_1.intro.intro
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}
b : ι
hb : a < b
⊢ ∃ a, ∀ b ≥ a, b ∉ t

Tactic:
refine ⟨b, fun c hc hct => ?_⟩

Result:
case refine_1.intro.intro
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}
b : ι
hb : a < b
c : ι
hc : c ≥ b
hct : c ∈ t
⊢ False
-- Mathlib/Computability/Primrec.lean
theorem list_length : Primrec (@List.length α) :=
  (list_foldr (@Primrec.id (List α) _) (const 0) <| to₂ <| (succ.comp <| snd.comp snd).to₂).of_eq
    fun l => by dsimp; induction l <;> simp [*]

Proof state:
α : Type u_1
inst✝ : Primcodable α
l : List α
⊢ List.foldr (fun b s => s + 1) 0 l = l.length

Tactic:
induction l <;> simp [*]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Primcodable α
l : List α
⊢ List.foldr (fun b s => (fun a b => (a, b).2.2.succ) (l, b, s).1 (l, b, s).2) 0 (id l) = l.length

Tactic:
dsimp

Result:
α : Type u_1
inst✝ : Primcodable α
l : List α
⊢ List.foldr (fun b s => s + 1) 0 l = l.length
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_eq_zero {M₀ : Type*} [CommMonoidWithZero M₀] (f : α → M₀) (x : α) (hx : f x = 0)
    (hf : (mulSupport f).Finite) : ∏ᶠ x, f x = 0

Proof state:
α : Type u_1
M₀ : Type u_7
inst✝ : CommMonoidWithZero M₀
f : α → M₀
x : α
hx : f x = 0
hf : (mulSupport f).Finite
a✝ : Nontrivial M₀
⊢ ∏ i ∈ hf.toFinset, f i = 0

Tactic:
refine Finset.prod_eq_zero (hf.mem_toFinset.2 ?_) hx

Result:
α : Type u_1
M₀ : Type u_7
inst✝ : CommMonoidWithZero M₀
f : α → M₀
x : α
hx : f x = 0
hf : (mulSupport f).Finite
a✝ : Nontrivial M₀
⊢ x ∈ mulSupport f

Proof state:
α : Type u_1
M₀ : Type u_7
inst✝ : CommMonoidWithZero M₀
f : α → M₀
x : α
hx : f x = 0
hf : (mulSupport f).Finite
a✝ : Nontrivial M₀
⊢ x ∈ mulSupport f

Tactic:
simp [hx]

Result:
no goals

Proof state:
α : Type u_1
M₀ : Type u_7
inst✝ : CommMonoidWithZero M₀
f : α → M₀
x : α
hx : f x = 0
hf : (mulSupport f).Finite
a✝ : Nontrivial M₀
⊢ ∏ᶠ (x : α), f x = 0

Tactic:
rw [finprod_eq_prod f hf]

Result:
α : Type u_1
M₀ : Type u_7
inst✝ : CommMonoidWithZero M₀
f : α → M₀
x : α
hx : f x = 0
hf : (mulSupport f).Finite
a✝ : Nontrivial M₀
⊢ ∏ i ∈ hf.toFinset, f i = 0

Proof state:
α : Type u_1
M₀ : Type u_7
inst✝ : CommMonoidWithZero M₀
f : α → M₀
x : α
hx : f x = 0
hf : (mulSupport f).Finite
⊢ ∏ᶠ (x : α), f x = 0

Tactic:
nontriviality

Result:
α : Type u_1
M₀ : Type u_7
inst✝ : CommMonoidWithZero M₀
f : α → M₀
x : α
hx : f x = 0
hf : (mulSupport f).Finite
a✝ : Nontrivial M₀
⊢ ∏ᶠ (x : α), f x = 0
-- Mathlib/Data/Fin/Basic.lean
lemma cast_injective {k l : ℕ} (h : k = l) : Injective (Fin.cast h) :=
  fun a b hab ↦ by simpa [← val_eq_val] using hab

Proof state:
k l : ℕ
h : k = l
a b : Fin k
hab : Fin.cast h a = Fin.cast h b
⊢ a = b

Tactic:
simpa [← val_eq_val] using hab

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_eq_zero : s.encard = 0 ↔ s = ∅

Proof state:
α : Type u_1
s : Set α
⊢ s.encard = 0 ↔ s = ∅

Tactic:
rw [encard, ENat.card_eq_zero_iff_empty, isEmpty_subtype, eq_empty_iff_forall_not_mem]

Result:
no goals