harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/Young/YoungDiagram.lean
theorem rowLen_ofRowLens {w : List ℕ} {hw : w.Sorted (· ≥ ·)} (i : Fin w.length) :
    (ofRowLens w hw).rowLen i = w[i]

Proof state:
w : List ℕ
hw : List.Sorted (fun x1 x2 => x1 ≥ x2) w
i : Fin w.length
⊢ (ofRowLens w hw).rowLen ↑i = w[i]

Tactic:
simp [rowLen, Nat.find_eq_iff, mem_ofRowLens]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Reduced.lean
/-- See also `RootPairing.pairingIn_neg_two_neg_two_iff`. -/
@[simp]
lemma pairing_neg_two_neg_two_iff :
    P.pairing i j = -2 ∧ P.pairing j i = -2 ↔ P.root i = -P.root j

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
i j : ι
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
⊢ P.pairing i j = -2 ∧ P.pairing j i = -2 ↔ P.root i = -P.root j

Tactic:
simp only [← neg_eq_iff_eq_neg]

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
i j : ι
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
⊢ -P.pairing i j = 2 ∧ -P.pairing j i = 2 ↔ -P.root i = P.root j

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
i j : ι
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
⊢ -P.pairing i j = 2 ∧ -P.pairing j i = 2 ↔ -P.root i = P.root j

Tactic:
simpa [eq_comm (a := -P.root i), root_eq_neg_iff] using
  P.pairing_two_two_iff i (P.reflection_perm j j)

Result:
no goals
-- Mathlib/RingTheory/OreLocalization/Basic.lean
theorem oreDiv_add_oreDiv {r r' : X} {s s' : S} :
    r /ₒ s + r' /ₒ s' =
      (oreDenom (s : R) s' • r + oreNum (s : R) s' • r') /ₒ (oreDenom (s : R) s' * s)

Proof state:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r r' : X
s s' : ↥S
⊢ r /ₒ s + r' /ₒ s' = (oreDenom (↑s) s' • r + oreNum (↑s) s' • r') /ₒ (oreDenom (↑s) s' * s)

Tactic:
with_unfolding_all rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r r' : X
s s' : ↥S
⊢ r /ₒ s + r' /ₒ s' = (oreDenom (↑s) s' • r + oreNum (↑s) s' • r') /ₒ (oreDenom (↑s) s' * s)

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Finset/Sort.lean
/-- Any finite linear order order-embeds into any infinite linear order. -/
lemma nonempty_orderEmbedding_of_finite_infinite
    (α : Type*) [LinearOrder α] [hα : Finite α]
    (β : Type*) [LinearOrder β] [hβ : Infinite β] : Nonempty (α ↪o β)

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
hα : Finite α
β : Type u_2
inst✝ : LinearOrder β
hβ : Infinite β
⊢ Nonempty (α ↪o β)

Tactic:
haveI := Fintype.ofFinite α

Result:
α : Type u_1
inst✝¹ : LinearOrder α
hα : Finite α
β : Type u_2
inst✝ : LinearOrder β
hβ : Infinite β
this : Fintype α
⊢ Nonempty (α ↪o β)

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
hα : Finite α
β : Type u_2
inst✝ : LinearOrder β
hβ : Infinite β
this : Fintype α
⊢ Nonempty (α ↪o β)

Tactic:
obtain ⟨s, hs⟩ := Infinite.exists_subset_card_eq β (Fintype.card α)

Result:
case intro
α : Type u_1
inst✝¹ : LinearOrder α
hα : Finite α
β : Type u_2
inst✝ : LinearOrder β
hβ : Infinite β
this : Fintype α
s : Finset β
hs : s.card = Fintype.card α
⊢ Nonempty (α ↪o β)

Proof state:
case intro
α : Type u_1
inst✝¹ : LinearOrder α
hα : Finite α
β : Type u_2
inst✝ : LinearOrder β
hβ : Infinite β
this : Fintype α
s : Finset β
hs : s.card = Fintype.card α
⊢ Nonempty (α ↪o β)

Tactic:
exact ⟨((Fintype.orderIsoFinOfCardEq α rfl).symm.toOrderEmbedding).trans (s.orderEmbOfFin hs)⟩

Result:
no goals
-- Mathlib/RingTheory/Nilpotent/Basic.lean
theorem IsNilpotent.isUnit_one_sub [Ring R] {r : R} (hnil : IsNilpotent r) : IsUnit (1 - r)

Proof state:
R : Type u_1
inst✝ : Ring R
r : R
hnil : IsNilpotent r
⊢ IsUnit (1 - r)

Tactic:
rw [← IsUnit.neg_iff, neg_sub]

Result:
R : Type u_1
inst✝ : Ring R
r : R
hnil : IsNilpotent r
⊢ IsUnit (r - 1)

Proof state:
R : Type u_1
inst✝ : Ring R
r : R
hnil : IsNilpotent r
⊢ IsUnit (r - 1)

Tactic:
exact isUnit_sub_one hnil

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma pow_nonneg {a : A} (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : autoParam (0 ≤ a) _auto✝
n : ℕ
⊢ 0 ≤ a ^ n

Tactic:
rw [← cfc_pow_id (R := ℝ≥0) a]

Result:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : autoParam (0 ≤ a) _auto✝
n : ℕ
⊢ 0 ≤ cfc (fun x => x ^ n) a

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : autoParam (0 ≤ a) _auto✝
n : ℕ
⊢ 0 ≤ cfc (fun x => x ^ n) a

Tactic:
exact cfc_nonneg_of_predicate

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isBigO_one_iff : f =O[l] (fun _x => 1 : α → F) ↔
    IsBoundedUnder (· ≤ ·) l fun x => ‖f x‖

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝³ : Norm E
inst✝² : Norm F
f : α → E
l : Filter α
inst✝¹ : One F
inst✝ : NormOneClass F
⊢ (f =O[l] fun _x => 1) ↔ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖f x‖

Tactic:
simp only [isBigO_iff, norm_one, mul_one, IsBoundedUnder, IsBounded, eventually_map]

Result:
no goals
-- Mathlib/Computability/PartrecCode.lean
theorem evaln_bound : ∀ {k c n x}, x ∈ evaln k c n → n < k
  | 0, c, n, x, h => by simp [evaln] at h
  | k + 1, c, n, x, h => by
    suffices ∀ {o : Option ℕ}, x ∈ do { guard (n ≤ k); o } → n < k + 1 by
      cases c <;> rw [evaln] at h <;> exact this h
    simpa [Option.bind_eq_some] using Nat.lt_succ_of_le

Proof state:
c : Code
n x : ℕ
h : x ∈ evaln 0 c n
⊢ n < 0

Tactic:
simp [evaln] at h

Result:
no goals

Proof state:
k : ℕ
c : Code
n x : ℕ
h : x ∈ evaln (k + 1) c n
⊢ ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1

Tactic:
simpa [Option.bind_eq_some] using Nat.lt_succ_of_le

Result:
no goals

Proof state:
k : ℕ
c : Code
n x : ℕ
h : x ∈ evaln (k + 1) c n
⊢ n < k + 1

Tactic:
suffices ∀ {o : Option ℕ}, x ∈ do { guard (n ≤ k); o } → n < k + 1 by
  cases c <;> rw [evaln] at h <;> exact this h

Result:
k : ℕ
c : Code
n x : ℕ
h : x ∈ evaln (k + 1) c n
⊢ ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1

Proof state:
k : ℕ
c : Code
n x : ℕ
h : x ∈ evaln (k + 1) c n
this :
  ∀ {o : Option ℕ},
    (x ∈ do
        guard (n ≤ k)
        o) →
      n < k + 1
⊢ n < k + 1

Tactic:
cases c <;> rw [evaln] at h <;> exact this h

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem einfsep_triple (hxy : x ≠ y) (hyz : y ≠ z) (hxz : x ≠ z) :
    einfsep ({x, y, z} : Set α) = edist x y ⊓ edist x z ⊓ edist y z

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
hxy : x ≠ y
hyz : y ≠ z
hxz : x ≠ z
⊢ {x, y, z}.einfsep = edist x y ⊓ edist x z ⊓ edist y z

Tactic:
simp_rw [einfsep_insert, iInf_insert, iInf_singleton, einfsep_singleton, inf_top_eq,
  ciInf_pos hxy, ciInf_pos hyz, ciInf_pos hxz]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Quotient.lean
theorem IsQuotient.norm_le {f : NormedAddGroupHom M N} (hquot : IsQuotient f) (m : M) :
    ‖f m‖ ≤ ‖m‖

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
m : M
⊢ sInf ((fun m_1 => ‖m + m_1‖) '' ↑f.ker) ≤ ‖m‖

Tactic:
apply csInf_le

Result:
case h₁
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
m : M
⊢ BddBelow ((fun m_1 => ‖m + m_1‖) '' ↑f.ker)

case h₂
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
m : M
⊢ ‖m‖ ∈ (fun m_1 => ‖m + m_1‖) '' ↑f.ker

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
m : M
⊢ (fun m_1 => ‖m + m_1‖) 0 = ‖m‖

Tactic:
simp

Result:
no goals

Proof state:
case h
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
m : M
⊢ 0 ∈ lowerBounds ((fun m_1 => ‖m + m_1‖) '' ↑f.ker)

Tactic:
rintro _ ⟨m', -, rfl⟩

Result:
case h.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
m m' : M
⊢ 0 ≤ (fun m_1 => ‖m + m_1‖) m'

Proof state:
case h.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
m m' : M
⊢ 0 ≤ (fun m_1 => ‖m + m_1‖) m'

Tactic:
apply norm_nonneg

Result:
no goals

Proof state:
case h₁
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
m : M
⊢ BddBelow ((fun m_1 => ‖m + m_1‖) '' ↑f.ker)

Tactic:
use 0

Result:
case h
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
m : M
⊢ 0 ∈ lowerBounds ((fun m_1 => ‖m + m_1‖) '' ↑f.ker)

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
m : M
⊢ ‖f m‖ ≤ ‖m‖

Tactic:
rw [hquot.norm]

Result:
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
m : M
⊢ sInf ((fun m_1 => ‖m + m_1‖) '' ↑f.ker) ≤ ‖m‖

Proof state:
case h₂
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
m : M
⊢ ‖m‖ ∈ (fun m_1 => ‖m + m_1‖) '' ↑f.ker

Tactic:
exact ⟨0, f.ker.zero_mem, by simp⟩

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_union_eq (h : Disjoint s t) : (s ∪ t).encard = s.encard + t.encard

Proof state:
α : Type u_1
s t : Set α
h : Disjoint s t
⊢ (s ∪ t).encard = s.encard + t.encard

Tactic:
simp [encard, ENat.card_congr (Equiv.Set.union h)]

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
h : Disjoint s t
⊢ (s ∪ t).encard = s.encard + t.encard

Tactic:
classical
simp [encard, ENat.card_congr (Equiv.Set.union h)]

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
theorem one_sub_dvd_one_sub_pow [Ring α] (x : α) (n : ℕ) :
    1 - x ∣ 1 - x ^ n

Proof state:
α : Type u
inst✝ : Ring α
x : α
n : ℕ
⊢ 1 - x ∣ 1 ^ n - x ^ n

Tactic:
exact (Commute.one_left x).sub_dvd_pow_sub_pow n

Result:
no goals

Proof state:
α : Type u
inst✝ : Ring α
x : α
n : ℕ
⊢ 1 - x ∣ 1 - x ^ n

Tactic:
conv_rhs => rw [← one_pow n]

Result:
α : Type u
inst✝ : Ring α
x : α
n : ℕ
⊢ 1 - x ∣ 1 ^ n - x ^ n
-- Mathlib/SetTheory/Game/Birthday.lean
theorem birthday_moveLeft_lt {x : PGame} (i : x.LeftMoves) :
    (x.moveLeft i).birthday < x.birthday

Proof state:
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : (mk α✝ β✝ a✝¹ a✝).LeftMoves
⊢ ((mk α✝ β✝ a✝¹ a✝).moveLeft i).birthday < (lsub fun i => (a✝¹ i).birthday) ⊔ lsub fun i => (a✝ i).birthday

Tactic:
exact lt_max_of_lt_left (lt_lsub _ i)

Result:
no goals

Proof state:
x : PGame
i : x.LeftMoves
⊢ (x.moveLeft i).birthday < x.birthday

Tactic:
cases x

Result:
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : (mk α✝ β✝ a✝¹ a✝).LeftMoves
⊢ ((mk α✝ β✝ a✝¹ a✝).moveLeft i).birthday < (mk α✝ β✝ a✝¹ a✝).birthday

Proof state:
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : (mk α✝ β✝ a✝¹ a✝).LeftMoves
⊢ ((mk α✝ β✝ a✝¹ a✝).moveLeft i).birthday < (mk α✝ β✝ a✝¹ a✝).birthday

Tactic:
rw [birthday]

Result:
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : (mk α✝ β✝ a✝¹ a✝).LeftMoves
⊢ ((mk α✝ β✝ a✝¹ a✝).moveLeft i).birthday < (lsub fun i => (a✝¹ i).birthday) ⊔ lsub fun i => (a✝ i).birthday
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem fst_map (f : M →ₗ[R'] N) (x : TrivSqZeroExt R' M) : fst (map f x) = fst x

Proof state:
R' : Type u
M : Type v
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R' M
inst✝⁵ : Module R'ᵐᵒᵖ M
inst✝⁴ : IsCentralScalar R' M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R' N
inst✝¹ : Module R'ᵐᵒᵖ N
inst✝ : IsCentralScalar R' N
f : M →ₗ[R'] N
x : tsze R' M
⊢ ((map f) x).fst = x.fst

Tactic:
simp [map, lift_def, Algebra.ofId_apply, algebraMap_eq_inl]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
lemma pairing_reflection_perm (i j k : ι) :
    P.pairing j (P.reflection_perm i k) = P.pairing (P.reflection_perm i j) k

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j k : ι
⊢ (P.toLin (P.root j)) (P.coroot k) - P.pairing i k * (P.toLin (P.root j)) (P.coroot i) =
    (P.toLin (P.root j)) (P.coroot k) - P.pairing j i * (P.toLin (P.root i)) (P.coroot k)

Tactic:
simp only [PerfectPairing.toLin_apply, root'_coroot_eq_pairing, sub_right_inj, mul_comm]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j k : ι
⊢ (P.toPerfectPairing (P.root j)) ((P.coreflection i) (P.coroot k)) =
    (P.toPerfectPairing ((P.reflection i) (P.root j))) (P.coroot k)

Tactic:
simp only [coreflection_apply_coroot, map_sub, map_smul, smul_eq_mul,
  reflection_apply_root]

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j k : ι
⊢ (P.toPerfectPairing (P.root j)) (P.coroot k) - P.pairing i k * (P.toPerfectPairing (P.root j)) (P.coroot i) =
    (P.toPerfectPairing (P.root j) - P.pairing j i • P.toPerfectPairing (P.root i)) (P.coroot k)

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j k : ι
⊢ (P.toPerfectPairing (P.root j)) (P.coroot k) - P.pairing i k * (P.toPerfectPairing (P.root j)) (P.coroot i) =
    (P.toPerfectPairing (P.root j) - P.pairing j i • P.toPerfectPairing (P.root i)) (P.coroot k)

Tactic:
simp only [← toLin_toPerfectPairing, map_smul, LinearMap.smul_apply, map_sub, map_smul,
  LinearMap.sub_apply, smul_eq_mul]

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j k : ι
⊢ (P.toLin (P.root j)) (P.coroot k) - P.pairing i k * (P.toLin (P.root j)) (P.coroot i) =
    (P.toLin (P.root j)) (P.coroot k) - P.pairing j i * (P.toLin (P.root i)) (P.coroot k)

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j k : ι
⊢ P.pairing j ((P.reflection_perm i) k) = P.pairing ((P.reflection_perm i) j) k

Tactic:
simp only [pairing, root', coroot_reflection_perm, root_reflection_perm]

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j k : ι
⊢ (P.toPerfectPairing (P.root j)) ((P.coreflection i) (P.coroot k)) =
    (P.toPerfectPairing ((P.reflection i) (P.root j))) (P.coroot k)
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem Monic.pow {f : MvPolynomial σ R} {n : ℕ} (hf : m.Monic f) :
    m.Monic (f ^ n)

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hf : m.Monic f
a✝ : Nontrivial R
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

Result:
no goals

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hf : m.Monic f
a✝ : Nontrivial R
⊢ m.leadingCoeff f ^ n ≠ 0

Tactic:
rw [hf.leadingCoeff_eq_one, one_pow]

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hf : m.Monic f
a✝ : Nontrivial R
⊢ 1 ≠ 0

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hf : m.Monic f
⊢ m.Monic (f ^ n)

Tactic:
nontriviality R

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hf : m.Monic f
a✝ : Nontrivial R
⊢ m.Monic (f ^ n)

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hf : m.Monic f
a✝ : Nontrivial R
⊢ m.Monic (f ^ n)

Tactic:
rw [Monic, leadingCoeff_pow_of_pow_leadingCoeff_ne_zero, hf.leadingCoeff_eq_one, one_pow]

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hf : m.Monic f
a✝ : Nontrivial R
⊢ m.leadingCoeff f ^ n ≠ 0
-- Mathlib/Algebra/Order/Ring/WithTop.lean
lemma mul_def (a b : WithBot α) :
    a * b = if a = 0 ∨ b = 0 then 0 else WithBot.map₂ (· * ·) a b

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
⊢ a * b = if a = 0 ∨ b = 0 then 0 else map₂ (fun x1 x2 => x1 * x2) a b

Tactic:
cases a <;> cases b <;> aesop

Result:
no goals
-- Mathlib/RingTheory/LaurentSeries.lean
theorem Cauchy.eventually_mem_nhds {ℱ : Filter K⸨X⸩} (hℱ : Cauchy ℱ)
    {U : Set K⸨X⸩} (hU : U ∈ 𝓝 (Cauchy.limit hℱ)) : ∀ᶠ f in ℱ, f ∈ U

Proof state:
case intro
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : ℤₘ₀ˣ
hU₁ : {y | Valued.v (y - limit hℱ) < ↑γ} ⊆ U
D : ℤ := -(toAdd (WithZero.unzero ⋯) - 1)
hD₀ : D = -(toAdd (WithZero.unzero ⋯) - 1)
hD : ↑(ofAdd (-D)) < ↑γ
x✝ : K⸨X⸩
hf : ∀ d < D, coeff hℱ d = x✝.coeff d
⊢ x✝ ∈ {y | Valued.v (y - limit hℱ) < ↑γ}

Tactic:
apply lt_of_le_of_lt (valuation_le_iff_coeff_lt_eq_zero K |>.mpr _) hD

Result:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : ℤₘ₀ˣ
hU₁ : {y | Valued.v (y - limit hℱ) < ↑γ} ⊆ U
D : ℤ := -(toAdd (WithZero.unzero ⋯) - 1)
hD₀ : D = -(toAdd (WithZero.unzero ⋯) - 1)
hD : ↑(ofAdd (-D)) < ↑γ
x✝ : K⸨X⸩
hf : ∀ d < D, coeff hℱ d = x✝.coeff d
⊢ ∀ n < D, (x✝ - limit hℱ).coeff n = 0
-- Mathlib/Order/Partition/Finpartition.lean
theorem sum_card_parts : ∑ i ∈ P.parts, #i = #s

Proof state:
case h.e'_2
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
⊢ ∑ i ∈ P.parts, #i = #(P.parts.biUnion id)

Tactic:
rw [card_biUnion P.supIndep.pairwiseDisjoint]

Result:
case h.e'_2
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
⊢ ∑ i ∈ P.parts, #i = ∑ u ∈ P.parts, #(id u)

Proof state:
case h.e'_2
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
⊢ ∑ i ∈ P.parts, #i = ∑ u ∈ P.parts, #(id u)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
⊢ ∑ i ∈ P.parts, #i = #s

Tactic:
convert congr_arg Finset.card P.biUnion_parts

Result:
case h.e'_2
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
⊢ ∑ i ∈ P.parts, #i = #(P.parts.biUnion id)
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem prod_trunc {M : Type*} [CommMonoid M] {a b : ℕ} (f : Fin (a + b) → M)
    (hf : ∀ j : Fin b, f (natAdd a j) = 1) :
    (∏ i : Fin (a + b), f i) = ∏ i : Fin a, f (castLE (Nat.le.intro rfl) i)

Proof state:
M : Type u_3
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
hf : ∀ (j : Fin b), f (natAdd a j) = 1
⊢ ∏ i : Fin (a + b), f i = ∏ i : Fin a, f (castLE ⋯ i)

Tactic:
rw [prod_univ_add, Fintype.prod_eq_one _ hf, mul_one]

Result:
M : Type u_3
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
hf : ∀ (j : Fin b), f (natAdd a j) = 1
⊢ ∏ i : Fin a, f (castAdd b i) = ∏ i : Fin a, f (castLE ⋯ i)

Proof state:
M : Type u_3
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
hf : ∀ (j : Fin b), f (natAdd a j) = 1
⊢ ∏ i : Fin a, f (castAdd b i) = ∏ i : Fin a, f (castLE ⋯ i)

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem le_of_forall_sub_le (h : ∀ ε > 0, b - ε ≤ a) : b ≤ a

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
h : ∀ ε > 0, b - ε ≤ a
⊢ b ≤ a

Tactic:
contrapose! h

Result:
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
h : a < b
⊢ ∃ ε > 0, a < b - ε

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
h : a < b
⊢ ∃ ε > 0, a < b - ε

Tactic:
simpa only [@and_comm ((0 : α) < _), lt_sub_iff_add_lt, gt_iff_lt] using
  exists_add_lt_and_pos_of_lt h

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Prod.lean
theorem Tendsto.prod_atTop [Preorder α] [Preorder γ] {f g : α → γ}
    (hf : Tendsto f atTop atTop) (hg : Tendsto g atTop atTop) :
    Tendsto (Prod.map f g) atTop atTop

Proof state:
α : Type u_3
γ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder γ
f g : α → γ
hf : Tendsto f atTop atTop
hg : Tendsto g atTop atTop
⊢ Tendsto (Prod.map f g) atTop atTop

Tactic:
rw [← prod_atTop_atTop_eq]

Result:
α : Type u_3
γ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder γ
f g : α → γ
hf : Tendsto f atTop atTop
hg : Tendsto g atTop atTop
⊢ Tendsto (Prod.map f g) (atTop ×ˢ atTop) atTop

Proof state:
α : Type u_3
γ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder γ
f g : α → γ
hf : Tendsto f atTop atTop
hg : Tendsto g atTop atTop
⊢ Tendsto (Prod.map f g) (atTop ×ˢ atTop) atTop

Tactic:
exact hf.prod_map_prod_atTop hg

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Equiv.lean
theorem ring_inverse_equiv (e : M ≃L[R] M) : Ring.inverse ↑e = inverse (e : M →L[R] M)

Proof state:
R : Type u_3
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : M ≃L[R] M
this : Ring.inverse ↑((ContinuousLinearEquiv.unitsEquiv R M).symm e) = (↑e).inverse
⊢ Ring.inverse ↑e = (↑e).inverse

Tactic:
convert this

Result:
no goals

Proof state:
R : Type u_3
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : M ≃L[R] M
⊢ ↑((ContinuousLinearEquiv.unitsEquiv R M).symm e)⁻¹ = ↑e.symm

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_3
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : M ≃L[R] M
⊢ Ring.inverse ↑((ContinuousLinearEquiv.unitsEquiv R M).symm e) = (↑e).inverse

Tactic:
simp

Result:
R : Type u_3
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : M ≃L[R] M
⊢ ↑((ContinuousLinearEquiv.unitsEquiv R M).symm e)⁻¹ = ↑e.symm

Proof state:
R : Type u_3
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : M ≃L[R] M
⊢ Ring.inverse ↑e = (↑e).inverse

Tactic:
suffices Ring.inverse ((ContinuousLinearEquiv.unitsEquiv _ _).symm e : M →L[R] M) = inverse ↑e by
  convert this

Result:
R : Type u_3
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : M ≃L[R] M
⊢ Ring.inverse ↑((ContinuousLinearEquiv.unitsEquiv R M).symm e) = (↑e).inverse