harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/IsPerfectClosure.lean
theorem lift_comp_lift : (lift j k p).comp (lift i j p) = lift i k p :=
  IsPRadical.injective_comp_of_perfect _ i p (by ext; simp)

Proof state:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : CommRing K
inst✝¹⁰ : CommRing L
inst✝⁹ : CommRing M
inst✝⁸ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
p : ℕ
inst✝⁷ : ExpChar M p
inst✝⁶ : ExpChar K p
inst✝⁵ : PerfectRing M p
inst✝⁴ : IsPRadical i p
inst✝³ : ExpChar L p
inst✝² : ExpChar N p
inst✝¹ : PerfectRing N p
inst✝ : IsPRadical j p
⊢ (fun f => f.comp i) ((lift j k p).comp (lift i j p)) = (fun f => f.comp i) (lift i k p)

Tactic:
ext

Result:
case a
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : CommRing K
inst✝¹⁰ : CommRing L
inst✝⁹ : CommRing M
inst✝⁸ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
p : ℕ
inst✝⁷ : ExpChar M p
inst✝⁶ : ExpChar K p
inst✝⁵ : PerfectRing M p
inst✝⁴ : IsPRadical i p
inst✝³ : ExpChar L p
inst✝² : ExpChar N p
inst✝¹ : PerfectRing N p
inst✝ : IsPRadical j p
x✝ : K
⊢ ((fun f => f.comp i) ((lift j k p).comp (lift i j p))) x✝ = ((fun f => f.comp i) (lift i k p)) x✝

Proof state:
case a
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : CommRing K
inst✝¹⁰ : CommRing L
inst✝⁹ : CommRing M
inst✝⁸ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
p : ℕ
inst✝⁷ : ExpChar M p
inst✝⁶ : ExpChar K p
inst✝⁵ : PerfectRing M p
inst✝⁴ : IsPRadical i p
inst✝³ : ExpChar L p
inst✝² : ExpChar N p
inst✝¹ : PerfectRing N p
inst✝ : IsPRadical j p
x✝ : K
⊢ ((fun f => f.comp i) ((lift j k p).comp (lift i j p))) x✝ = ((fun f => f.comp i) (lift i k p)) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean
lemma isUniform_one : P.IsUniform G (1 : 𝕜)

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ P.IsUniform G 1

Tactic:
rw [IsUniform, mul_one, Nat.cast_le]

Result:
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ #(P.nonUniforms G 1) ≤ #P.parts * (#P.parts - 1)

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ #(P.nonUniforms G 1) ≤ #P.parts * (#P.parts - 1)

Tactic:
refine (card_filter_le _
  (fun uv => ¬SimpleGraph.IsUniform G 1 (Prod.fst uv) (Prod.snd uv))).trans ?_

Result:
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ #P.parts.offDiag ≤ #P.parts * (#P.parts - 1)

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ #P.parts.offDiag ≤ #P.parts * (#P.parts - 1)

Tactic:
rw [offDiag_card, Nat.mul_sub_left_distrib, mul_one]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Field.lean
theorem tendsto_const_mul_atTop_iff [NeBot l] :
    Tendsto (fun x => r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot

Proof state:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
hr : r < 0
⊢ Tendsto (fun x => r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot

Tactic:
simp [hr, hr.not_lt, tendsto_const_mul_atTop_of_neg]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
⊢ Tendsto (fun x => r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot

Tactic:
rcases lt_trichotomy r 0 with (hr | rfl | hr)

Result:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
hr : r < 0
⊢ Tendsto (fun x => r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot

case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
inst✝ : l.NeBot
⊢ Tendsto (fun x => 0 * f x) l atTop ↔ 0 < 0 ∧ Tendsto f l atTop ∨ 0 < 0 ∧ Tendsto f l atBot

case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
hr : 0 < r
⊢ Tendsto (fun x => r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot

Proof state:
case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
hr : 0 < r
⊢ Tendsto (fun x => r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot

Tactic:
simp [hr, hr.not_lt, tendsto_const_mul_atTop_of_pos]

Result:
no goals

Proof state:
case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
inst✝ : l.NeBot
⊢ Tendsto (fun x => 0 * f x) l atTop ↔ 0 < 0 ∧ Tendsto f l atTop ∨ 0 < 0 ∧ Tendsto f l atBot

Tactic:
simp [not_tendsto_const_atTop]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
@[simp] protected lemma div_pos_iff : 0 < a / b ↔ 0 < b ∧ b ≤ a

Proof state:
a b : ℕ
⊢ 0 < a / b ↔ 0 < b ∧ b ≤ a

Tactic:
simp [Nat.pos_iff_ne_zero]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem eq_rotation_self_iff_angle_eq_zero {x : V} (hx : x ≠ 0) (θ : Real.Angle) :
    x = o.rotation θ x ↔ θ = 0

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
hx : x ≠ 0
θ : Real.Angle
⊢ x = (o.rotation θ) x ↔ θ = 0

Tactic:
rw [← o.rotation_eq_self_iff_angle_eq_zero hx, eq_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions/ComposableArrows.lean
lemma essSurj_mapComposableArrows_of_hasRightCalculusOfFractions
    [W.HasRightCalculusOfFractions] (n : ℕ) :
    (L.mapComposableArrows n).EssSurj where
  mem_essImage Y

Proof state:
case succ.intro.intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
this : L.EssSurj
n : ℕ
hn : ∀ (Y : ComposableArrows D n), (L.mapComposableArrows n).essImage Y
Y : ComposableArrows D n
Z : D
f : Z ⟶ Y.left
Y' : ComposableArrows C n
e : (L.mapComposableArrows n).obj Y' ≅ Y
f' : W.RightFraction (L.objPreimage Z) (Y'.obj 0)
hf' : (L.objObjPreimageIso Z).hom ≫ f ≫ (e.app 0).inv = f'.map L ⋯
⊢ ((L.mapComposableArrows (n + 1)).obj (Y'.precomp f'.f)).map' 0 1 ⋯ ⋯ ≫ app' e.hom 0 ⋯ =
    (isoOfHom L W f'.s ⋯ ≪≫ L.objObjPreimageIso Z).hom ≫ (Y.precomp f).map' 0 1 ⋯ ⋯

Tactic:
dsimp at hf' ⊢

Result:
case succ.intro.intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
this : L.EssSurj
n : ℕ
hn : ∀ (Y : ComposableArrows D n), (L.mapComposableArrows n).essImage Y
Y : ComposableArrows D n
Z : D
f : Z ⟶ Y.left
Y' : ComposableArrows C n
e : (L.mapComposableArrows n).obj Y' ≅ Y
f' : W.RightFraction (L.objPreimage Z) (Y'.obj 0)
hf' : (L.objObjPreimageIso Z).hom ≫ f ≫ e.inv.app 0 = f'.map L ⋯
⊢ L.map f'.f ≫ e.hom.app 0 = (L.map f'.s ≫ (L.objObjPreimageIso Z).hom) ≫ f

Proof state:
case succ.intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
this : L.EssSurj
n : ℕ
hn : ∀ (Y : ComposableArrows D n), (L.mapComposableArrows n).essImage Y
Y : ComposableArrows D n
Z : D
f : Z ⟶ Y.left
Y' : ComposableArrows C n
e : (L.mapComposableArrows n).obj Y' ≅ Y
⊢ (L.mapComposableArrows (n + 1)).essImage (Y.precomp f)

Tactic:
obtain ⟨f', hf'⟩ := exists_rightFraction L W
  ((L.objObjPreimageIso Z).hom ≫ f ≫ (e.app 0).inv)

Result:
case succ.intro.intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
this : L.EssSurj
n : ℕ
hn : ∀ (Y : ComposableArrows D n), (L.mapComposableArrows n).essImage Y
Y : ComposableArrows D n
Z : D
f : Z ⟶ Y.left
Y' : ComposableArrows C n
e : (L.mapComposableArrows n).obj Y' ≅ Y
f' : W.RightFraction (L.objPreimage Z) (Y'.obj 0)
hf' : (L.objObjPreimageIso Z).hom ≫ f ≫ (e.app 0).inv = f'.map L ⋯
⊢ (L.mapComposableArrows (n + 1)).essImage (Y.precomp f)
-- Mathlib/GroupTheory/CommutingProbability.lean
theorem Subgroup.commProb_quotient_le [H.Normal] : commProb (G ⧸ H) ≤ commProb G * Nat.card H

Proof state:
case hf
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ Function.Surjective (ConjClasses.map (QuotientGroup.mk' H))

Tactic:
exact ConjClasses.map_surjective Quotient.mk''_surjective

Result:
no goals

Proof state:
case hf
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ Function.Surjective ?f

case f
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ ConjClasses G → ConjClasses (G ⧸ H)

Tactic:
show Function.Surjective (ConjClasses.map (QuotientGroup.mk' H))

Result:
case hf
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ Function.Surjective (ConjClasses.map (QuotientGroup.mk' H))

Proof state:
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ commProb (G ⧸ H) ≤ commProb G * ↑(Nat.card ↥H)

Tactic:
rw [commProb_def', commProb_def', div_le_iff₀, mul_assoc, ← Nat.cast_mul, ← Subgroup.index,
  H.card_mul_index, div_mul_cancel₀, Nat.cast_le]

Result:
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ Nat.card (ConjClasses (G ⧸ H)) ≤ Nat.card (ConjClasses G)

case h
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ ↑(Nat.card G) ≠ 0

G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ 0 < ↑(Nat.card (G ⧸ H))

Proof state:
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ Nat.card (ConjClasses (G ⧸ H)) ≤ Nat.card (ConjClasses G)

Tactic:
apply Finite.card_le_of_surjective

Result:
case hf
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ Function.Surjective ?f

case f
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ ConjClasses G → ConjClasses (G ⧸ H)

Proof state:
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ 0 < ↑(Nat.card (G ⧸ H))

Tactic:
exact Nat.cast_pos.mpr Finite.card_pos

Result:
no goals

Proof state:
case h
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ ↑(Nat.card G) ≠ 0

Tactic:
exact Nat.cast_ne_zero.mpr Finite.card_pos.ne'

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

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

Tactic:
simp only [mem_def, toList_map, List.mem_map]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKeyD_modifyKey [EquivBEq α] {k k' fallback : α} {f : β → β} (l : List ((_ : α) × β))
    (hl : DistinctKeys l) :
    getKeyD k' (modifyKey k f l) fallback =
      if k == k' then
        if containsKey k l then k else fallback
      else
        getKeyD k' l fallback

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k k' fallback : α
f : β → β
l : List ((_ : α) × β)
hl : DistinctKeys l
⊢ getKeyD k' (modifyKey k f l) fallback =
    if (k == k') = true then if containsKey k l = true then k else fallback else getKeyD k' l fallback

Tactic:
simp [modifyKey_eq_alterKey, getKeyD_alterKey, containsKey_eq_isSome_getValue?, hl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Lemmas.lean
theorem mkAtom_decl_eq (aig : AIG α) (var : α) (idx : Nat) {h : idx < aig.decls.size} {hbound} :
    (aig.mkAtom var).aig.decls[idx]'hbound = aig.decls[idx]

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkAtom var).aig.decls.size
⊢ (if h : idx < aig.decls.size then aig.decls[idx] else Decl.atom var) = aig.decls[idx]

Tactic:
split

Result:
case isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkAtom var).aig.decls.size
h✝ : idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]

case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkAtom var).aig.decls.size
h✝ : ¬idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]

Proof state:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkAtom var).aig.decls.size
h✝ : ¬idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]

Tactic:
contradiction

Result:
no goals

Proof state:
case isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkAtom var).aig.decls.size
h✝ : idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]

Tactic:
rfl

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkAtom var).aig.decls.size
⊢ (aig.mkAtom var).aig.decls[idx] = aig.decls[idx]

Tactic:
simp only [mkAtom, Array.getElem_push]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
idx : Nat
h : idx < aig.decls.size
hbound : idx < (aig.mkAtom var).aig.decls.size
⊢ (if h : idx < aig.decls.size then aig.decls[idx] else Decl.atom var) = aig.decls[idx]
-- Mathlib/Algebra/Jordan/Basic.lean
theorem two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add [IsCommJordan A] (a b : A) :
    2 • (⁅L a, L (a * b)⁆ + ⁅L b, L (b * a)⁆) = ⁅L (a * a), L b⁆ + ⁅L (b * b), L a⁆

Proof state:
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b : A
⊢ 2 • ⁅L a, L (a * b)⁆ + 2 • ⁅L b, L (b * a)⁆ + ⁅L b, L (a * a)⁆ + ⁅L a, L (b * b)⁆ = 0

Tactic:
convert (commute_lmul_lmul_sq (a + b)).lie_eq using 1

Result:
case h.e'_2
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b : A
⊢ 2 • ⁅L a, L (a * b)⁆ + 2 • ⁅L b, L (b * a)⁆ + ⁅L b, L (a * a)⁆ + ⁅L a, L (b * b)⁆ = ⁅L (a + b), L ((a + b) * (a + b))⁆

Proof state:
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b : A
⊢ 2 • (⁅L a, L (a * b)⁆ + ⁅L b, L (b * a)⁆) = ⁅L (a * a), L b⁆ + ⁅L (b * b), L a⁆

Tactic:
suffices 2 • ⁅L a, L (a * b)⁆ + 2 • ⁅L b, L (b * a)⁆ + ⁅L b, L (a * a)⁆ + ⁅L a, L (b * b)⁆ = 0 by
  rwa [← sub_eq_zero, ← sub_sub, sub_eq_add_neg, sub_eq_add_neg, lie_skew, lie_skew, nsmul_add]

Result:
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b : A
⊢ 2 • ⁅L a, L (a * b)⁆ + 2 • ⁅L b, L (b * a)⁆ + ⁅L b, L (a * a)⁆ + ⁅L a, L (b * b)⁆ = 0

Proof state:
case h.e'_2
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b : A
⊢ 2 • ⁅L a, L (a * b)⁆ + 2 • ⁅L b, L (b * a)⁆ + ⁅L b, L (a * a)⁆ + ⁅L a, L (b * b)⁆ = ⁅L (a + b), L ((a + b) * (a + b))⁆

Tactic:
simp only [add_mul, mul_add, map_add, lie_add, add_lie, mul_comm b a,
  (commute_lmul_lmul_sq a).lie_eq, (commute_lmul_lmul_sq b).lie_eq, zero_add, add_zero, two_smul]

Result:
case h.e'_2
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b : A
⊢ ⁅L a, L (a * b)⁆ + ⁅L a, L (a * b)⁆ + (⁅L b, L (a * b)⁆ + ⁅L b, L (a * b)⁆) + ⁅L b, L (a * a)⁆ + ⁅L a, L (b * b)⁆ =
    ⁅L b, L (a * a)⁆ + (⁅L a, L (a * b)⁆ + ⁅L b, L (a * b)⁆) + (⁅L a, L (a * b)⁆ + ⁅L b, L (a * b)⁆ + ⁅L a, L (b * b)⁆)

Proof state:
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b : A
this : 2 • ⁅L a, L (a * b)⁆ + 2 • ⁅L b, L (b * a)⁆ + ⁅L b, L (a * a)⁆ + ⁅L a, L (b * b)⁆ = 0
⊢ 2 • (⁅L a, L (a * b)⁆ + ⁅L b, L (b * a)⁆) = ⁅L (a * a), L b⁆ + ⁅L (b * b), L a⁆

Tactic:
rwa [← sub_eq_zero, ← sub_sub, sub_eq_add_neg, sub_eq_add_neg, lie_skew, lie_skew, nsmul_add]

Result:
no goals

Proof state:
case h.e'_2
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b : A
⊢ ⁅L a, L (a * b)⁆ + ⁅L a, L (a * b)⁆ + (⁅L b, L (a * b)⁆ + ⁅L b, L (a * b)⁆) + ⁅L b, L (a * a)⁆ + ⁅L a, L (b * b)⁆ =
    ⁅L b, L (a * a)⁆ + (⁅L a, L (a * b)⁆ + ⁅L b, L (a * b)⁆) + (⁅L a, L (a * b)⁆ + ⁅L b, L (a * b)⁆ + ⁅L a, L (b * b)⁆)

Tactic:
abel

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_eq (z : ℂ) : cos z = cos z.re * cosh z.im - sin z.re * sinh z.im * I

Proof state:
z : ℂ
⊢ cos z = cos ↑z.re * cosh ↑z.im - sin ↑z.re * sinh ↑z.im * I

Tactic:
convert cos_add_mul_I z.re z.im

Result:
case h.e'_2.h.e'_1
z : ℂ
⊢ z = ↑z.re + ↑z.im * I

Proof state:
case h.e'_2.h.e'_1
z : ℂ
⊢ z = ↑z.re + ↑z.im * I

Tactic:
exact (re_add_im z).symm

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
theorem measurableSpace_iSup_eq (m : ι → MeasurableSpace α) :
    ⨆ n, m n = generateFrom { s | ∃ n, MeasurableSet[m n] s }

Proof state:
case h
α : Type u_1
ι : Sort u_6
m : ι → MeasurableSpace α
s : Set α
⊢ MeasurableSet s ↔ MeasurableSet s

Tactic:
rw [measurableSet_iSup]

Result:
case h
α : Type u_1
ι : Sort u_6
m : ι → MeasurableSpace α
s : Set α
⊢ GenerateMeasurable {s | ∃ i, MeasurableSet s} s ↔ MeasurableSet s

Proof state:
α : Type u_1
ι : Sort u_6
m : ι → MeasurableSpace α
⊢ ⨆ n, m n = generateFrom {s | ∃ n, MeasurableSet s}

Tactic:
ext s

Result:
case h
α : Type u_1
ι : Sort u_6
m : ι → MeasurableSpace α
s : Set α
⊢ MeasurableSet s ↔ MeasurableSet s

Proof state:
case h
α : Type u_1
ι : Sort u_6
m : ι → MeasurableSpace α
s : Set α
⊢ GenerateMeasurable {s | ∃ i, MeasurableSet s} s ↔ MeasurableSet s

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/RelClasses.lean
theorem eq_empty_relation (r) [IsIrrefl α r] [Subsingleton α] : r = EmptyRelation :=
  funext₂ <| by simpa using not_rel_of_subsingleton r

Proof state:
α : Type u
r : α → α → Prop
inst✝¹ : IsIrrefl α r
inst✝ : Subsingleton α
⊢ ∀ (a b : α), r a b = EmptyRelation a b

Tactic:
simpa using not_rel_of_subsingleton r

Result:
no goals
-- Mathlib/Analysis/Polynomial/Basic.lean
theorem abs_div_tendsto_atTop_of_degree_gt (hdeg : Q.degree < P.degree) (hQ : Q ≠ 0) :
    Tendsto (fun x => |eval x P / eval x Q|) atTop atTop

Proof state:
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : Q.degree < P.degree
hQ : Q ≠ 0
h : P.leadingCoeff / Q.leadingCoeff < 0
⊢ Tendsto (fun x => |eval x P / eval x Q|) atTop atTop

Tactic:
exact tendsto_abs_atBot_atTop.comp (P.div_tendsto_atBot_of_degree_gt Q hdeg hQ h.le)

Result:
no goals

Proof state:
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : Q.degree < P.degree
hQ : Q ≠ 0
h : ¬0 ≤ P.leadingCoeff / Q.leadingCoeff
⊢ Tendsto (fun x => |eval x P / eval x Q|) atTop atTop

Tactic:
push_neg at h

Result:
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : Q.degree < P.degree
hQ : Q ≠ 0
h : P.leadingCoeff / Q.leadingCoeff < 0
⊢ Tendsto (fun x => |eval x P / eval x Q|) atTop atTop

Proof state:
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : Q.degree < P.degree
hQ : Q ≠ 0
h : 0 ≤ P.leadingCoeff / Q.leadingCoeff
⊢ Tendsto (fun x => |eval x P / eval x Q|) atTop atTop

Tactic:
exact tendsto_abs_atTop_atTop.comp (P.div_tendsto_atTop_of_degree_gt Q hdeg hQ h)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : Q.degree < P.degree
hQ : Q ≠ 0
⊢ Tendsto (fun x => |eval x P / eval x Q|) atTop atTop

Tactic:
by_cases h : 0 ≤ P.leadingCoeff / Q.leadingCoeff

Result:
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : Q.degree < P.degree
hQ : Q ≠ 0
h : 0 ≤ P.leadingCoeff / Q.leadingCoeff
⊢ Tendsto (fun x => |eval x P / eval x Q|) atTop atTop

case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : Q.degree < P.degree
hQ : Q ≠ 0
h : ¬0 ≤ P.leadingCoeff / Q.leadingCoeff
⊢ Tendsto (fun x => |eval x P / eval x Q|) atTop atTop
-- Mathlib/Data/Stream/Init.lean
theorem even_cons_cons (a₁ a₂ : α) (s : Stream' α) : even (a₁::a₂::s) = a₁::even s

Proof state:
α : Type u
a₁ a₂ : α
s : Stream' α
⊢ corec head (fun s => s.tail.tail) (a₁ :: a₂ :: s) = a₁ :: corec head (fun s => s.tail.tail) s

Tactic:
rw [corec_eq]

Result:
α : Type u
a₁ a₂ : α
s : Stream' α
⊢ (a₁ :: a₂ :: s).head :: corec head (fun s => s.tail.tail) (a₁ :: a₂ :: s).tail.tail =
    a₁ :: corec head (fun s => s.tail.tail) s

Proof state:
α : Type u
a₁ a₂ : α
s : Stream' α
⊢ (a₁ :: a₂ :: s).head :: corec head (fun s => s.tail.tail) (a₁ :: a₂ :: s).tail.tail =
    a₁ :: corec head (fun s => s.tail.tail) s

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
a₁ a₂ : α
s : Stream' α
⊢ (a₁ :: a₂ :: s).even = a₁ :: s.even

Tactic:
unfold even

Result:
α : Type u
a₁ a₂ : α
s : Stream' α
⊢ corec head (fun s => s.tail.tail) (a₁ :: a₂ :: s) = a₁ :: corec head (fun s => s.tail.tail) s
-- Mathlib/Order/Filter/Bases.lean
theorem HasBasis.sup_pure (hl : l.HasBasis p s) (x : α) :
    (l ⊔ pure x).HasBasis p fun i => s i ∪ {x}

Proof state:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
x : α
⊢ (l ⊔ pure x).HasBasis p fun i => s i ∪ {x}

Tactic:
simp only [← principal_singleton, hl.sup_principal]

Result:
no goals
-- Mathlib/Data/Finset/Sort.lean
theorem orderEmbOfFin_unique {s : Finset α} {k : ℕ} (h : s.card = k) {f : Fin k → α}
    (hfs : ∀ x, f x ∈ s) (hmono : StrictMono f) : f = s.orderEmbOfFin h

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ image f univ = s

Tactic:
refine eq_of_subset_of_card_le (fun x hx => ?_) ?_

Result:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
x : α
hx : x ∈ image f univ
⊢ x ∈ s

case refine_2
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ #s ≤ #(image f univ)

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ f = ⇑(s.orderEmbOfFin h)

Tactic:
rw [← hmono.range_inj (s.orderEmbOfFin h).strictMono, range_orderEmbOfFin, ← Set.image_univ,
  ← coe_univ, ← coe_image, coe_inj]

Result:
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ image f univ = s

Proof state:
case refine_2
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ #s ≤ #(image f univ)

Tactic:
rw [h, card_image_of_injective _ hmono.injective, card_univ, Fintype.card_fin]

Result:
no goals

Proof state:
case refine_1.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
x : Fin k
left✝ : x ∈ univ
hx : f x ∈ image f univ
⊢ f x ∈ s

Tactic:
exact hfs x

Result:
no goals

Proof state:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
x : α
hx : x ∈ image f univ
⊢ x ∈ s

Tactic:
rcases mem_image.1 hx with ⟨x, _, rfl⟩

Result:
case refine_1.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
x : Fin k
left✝ : x ∈ univ
hx : f x ∈ image f univ
⊢ f x ∈ s