harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Sub/Basic.lean
lemma Even.tsub [AddLeftReflectLE α] {m n : α} (hm : Even m) (hn : Even n) :
    Even (m - n)

Proof state:
case intro
α : Type u_1
inst✝⁴ : LinearOrderedAddCommMonoid α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
n : α
hn : Even n
a : α
⊢ Even (a + a - n)

Tactic:
obtain ⟨b, rfl⟩ := hn

Result:
case intro.intro
α : Type u_1
inst✝⁴ : LinearOrderedAddCommMonoid α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
a b : α
⊢ Even (a + a - (b + b))

Proof state:
case intro.intro.inr
α : Type u_1
inst✝⁴ : LinearOrderedAddCommMonoid α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
a b : α
h : b ≤ a
⊢ a + a - (b + b) = a - b + (a - b)

Tactic:
exact (tsub_add_tsub_comm h h).symm

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : LinearOrderedAddCommMonoid α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
m n : α
hm : Even m
hn : Even n
⊢ Even (m - n)

Tactic:
obtain ⟨a, rfl⟩ := hm

Result:
case intro
α : Type u_1
inst✝⁴ : LinearOrderedAddCommMonoid α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
n : α
hn : Even n
a : α
⊢ Even (a + a - n)

Proof state:
case intro.intro.inl
α : Type u_1
inst✝⁴ : LinearOrderedAddCommMonoid α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
a b : α
h : a ≤ b
⊢ a + a - (b + b) = a - b + (a - b)

Tactic:
rw [tsub_eq_zero_of_le h, tsub_eq_zero_of_le (add_le_add h h), add_zero]

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝⁴ : LinearOrderedAddCommMonoid α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
a b : α
⊢ Even (a + a - (b + b))

Tactic:
refine ⟨a - b, ?_⟩

Result:
case intro.intro
α : Type u_1
inst✝⁴ : LinearOrderedAddCommMonoid α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
a b : α
⊢ a + a - (b + b) = a - b + (a - b)

Proof state:
case intro.intro
α : Type u_1
inst✝⁴ : LinearOrderedAddCommMonoid α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
a b : α
⊢ a + a - (b + b) = a - b + (a - b)

Tactic:
obtain h | h := le_total a b

Result:
case intro.intro.inl
α : Type u_1
inst✝⁴ : LinearOrderedAddCommMonoid α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
a b : α
h : a ≤ b
⊢ a + a - (b + b) = a - b + (a - b)

case intro.intro.inr
α : Type u_1
inst✝⁴ : LinearOrderedAddCommMonoid α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
a b : α
h : b ≤ a
⊢ a + a - (b + b) = a - b + (a - b)
-- Mathlib/Algebra/Order/Monoid/Unbundled/MinMax.lean
theorem le_or_lt_of_mul_le_mul [MulLeftMono α] [MulRightStrictMono α] {a₁ a₂ b₁ b₂ : α} :
    a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ < b₂

Proof state:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : Mul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
⊢ a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ < b₂

Tactic:
contrapose!

Result:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : Mul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
⊢ a₂ < a₁ ∧ b₂ ≤ b₁ → a₂ * b₂ < a₁ * b₁

Proof state:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : Mul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
⊢ a₂ < a₁ ∧ b₂ ≤ b₁ → a₂ * b₂ < a₁ * b₁

Tactic:
exact fun h => mul_lt_mul_of_lt_of_le h.1 h.2

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/Isometry.lean
theorem edist_map (x y : P) : edist (f x) (f y) = edist x y

Proof state:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : NormedSpace 𝕜 V
inst✝⁵ : PseudoMetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
f : P →ᵃⁱ[𝕜] P₂
x y : P
⊢ edist (f x) (f y) = edist x y

Tactic:
simp [edist_dist]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean
theorem m_pos [Nonempty α] (hPα : #P.parts * 16 ^ #P.parts ≤ card α) : 0 < m :=
  Nat.div_pos (hPα.trans' <| by unfold stepBound; gcongr; norm_num) <|
    stepBound_pos (P.parts_nonempty <| univ_nonempty.ne_empty).card_pos

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
P : Finpartition univ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
⊢ #P.parts * 4 ^ #P.parts ≤ #P.parts * 16 ^ #P.parts

Tactic:
gcongr

Result:
case bc.hab
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
P : Finpartition univ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
⊢ 4 ≤ 16

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
P : Finpartition univ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
⊢ stepBound #P.parts ≤ #P.parts * 16 ^ #P.parts

Tactic:
unfold stepBound

Result:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
P : Finpartition univ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
⊢ #P.parts * 4 ^ #P.parts ≤ #P.parts * 16 ^ #P.parts

Proof state:
case bc.hab
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
P : Finpartition univ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
⊢ 4 ≤ 16

Tactic:
norm_num

Result:
no goals
-- Mathlib/Algebra/Lie/Solvable.lean
theorem derivedSeries_map_eq (k : ℕ) (h : Function.Surjective f) :
    (derivedSeries R L' k).map f = derivedSeries R L k

Proof state:
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
k : ℕ
h : Function.Surjective ⇑f
⊢ map f (derivedSeries R L' k) = derivedSeries R L k

Tactic:
induction k with
| zero =>
  change (⊤ : LieIdeal R L').map f = ⊤
  rw [← f.idealRange_eq_map]
  exact f.idealRange_eq_top_of_surjective h
| succ k ih => simp only [derivedSeries_def, map_bracket_eq f h, ih, derivedSeriesOfIdeal_succ]

Result:
no goals

Proof state:
case zero
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
h : Function.Surjective ⇑f
⊢ map f ⊤ = ⊤

Tactic:
rw [← f.idealRange_eq_map]

Result:
case zero
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
h : Function.Surjective ⇑f
⊢ f.idealRange = ⊤

Proof state:
case zero
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
h : Function.Surjective ⇑f
⊢ f.idealRange = ⊤

Tactic:
exact f.idealRange_eq_top_of_surjective h

Result:
no goals

Proof state:
case succ
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
h : Function.Surjective ⇑f
k : ℕ
ih : map f (derivedSeries R L' k) = derivedSeries R L k
⊢ map f (derivedSeries R L' (k + 1)) = derivedSeries R L (k + 1)

Tactic:
simp only [derivedSeries_def, map_bracket_eq f h, ih, derivedSeriesOfIdeal_succ]

Result:
no goals

Proof state:
case zero
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
h : Function.Surjective ⇑f
⊢ map f (derivedSeries R L' 0) = derivedSeries R L 0

Tactic:
change (⊤ : LieIdeal R L').map f = ⊤

Result:
case zero
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L' →ₗ⁅R⁆ L
h : Function.Surjective ⇑f
⊢ map f ⊤ = ⊤
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_add_mul_I (x y : ℂ) : cos (x + y * I) = cos x * cosh y - sin x * sinh y * I

Proof state:
x y : ℂ
⊢ cos (x + y * I) = cos x * cosh y - sin x * sinh y * I

Tactic:
rw [cos_add, cos_mul_I, sin_mul_I, mul_assoc]

Result:
no goals
-- Mathlib/Data/Matrix/Block.lean
theorem blockDiagonal_add [AddZeroClass α] (M N : o → Matrix m n α) :
    blockDiagonal (M + N) = blockDiagonal M + blockDiagonal N

Proof state:
case a
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : o → Matrix m n α
i✝ : m × o
j✝ : n × o
⊢ blockDiagonal (M + N) i✝ j✝ = (blockDiagonal M + blockDiagonal N) i✝ j✝

Tactic:
simp only [blockDiagonal_apply, Pi.add_apply, add_apply]

Result:
case a
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : o → Matrix m n α
i✝ : m × o
j✝ : n × o
⊢ (if i✝.2 = j✝.2 then M i✝.2 i✝.1 j✝.1 + N i✝.2 i✝.1 j✝.1 else 0) =
    (if i✝.2 = j✝.2 then M i✝.2 i✝.1 j✝.1 else 0) + if i✝.2 = j✝.2 then N i✝.2 i✝.1 j✝.1 else 0

Proof state:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : o → Matrix m n α
⊢ blockDiagonal (M + N) = blockDiagonal M + blockDiagonal N

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : o → Matrix m n α
i✝ : m × o
j✝ : n × o
⊢ blockDiagonal (M + N) i✝ j✝ = (blockDiagonal M + blockDiagonal N) i✝ j✝

Proof state:
case a
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : o → Matrix m n α
i✝ : m × o
j✝ : n × o
⊢ (if i✝.2 = j✝.2 then M i✝.2 i✝.1 j✝.1 + N i✝.2 i✝.1 j✝.1 else 0) =
    (if i✝.2 = j✝.2 then M i✝.2 i✝.1 j✝.1 else 0) + if i✝.2 = j✝.2 then N i✝.2 i✝.1 j✝.1 else 0

Tactic:
split_ifs <;> simp

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem iterate_le_of_map_le_add_int {x : ℝ} {m : ℤ} (h : f x ≤ x + m) (n : ℕ) :
    f^[n] x ≤ x + n * m

Proof state:
f : CircleDeg1Lift
x : ℝ
m : ℤ
h : f x ≤ x + ↑m
n : ℕ
⊢ (⇑f)^[n] x ≤ x + ↑n * ↑m

Tactic:
simpa only [nsmul_eq_mul, add_right_iterate] using
  (f.commute_add_int m).iterate_le_of_map_le f.monotone (monotone_id.add_const (m : ℝ)) h n

Result:
no goals
-- Mathlib/Computability/PostTuringMachine.lean
theorem step_supports (M : Machine Γ Λ) {S : Set Λ} (ss : Supports M S) :
    ∀ {c c' : Cfg Γ Λ}, c' ∈ step M c → c.q ∈ S → c'.q ∈ S

Proof state:
Γ : Type u_1
Λ : Type u_2
inst✝¹ : Inhabited Λ
inst✝ : Inhabited Γ
M : Machine Γ Λ
S : Set Λ
ss : Supports M S
q : Λ
T : Tape Γ
c' : Cfg Γ Λ
h₁ : c' ∈ step M { q := q, Tape := T }
h₂ : { q := q, Tape := T }.q ∈ S
⊢ c'.q ∈ S

Tactic:
rcases Option.map_eq_some'.1 h₁ with ⟨⟨q', a⟩, h, rfl⟩

Result:
case intro.mk.intro
Γ : Type u_1
Λ : Type u_2
inst✝¹ : Inhabited Λ
inst✝ : Inhabited Γ
M : Machine Γ Λ
S : Set Λ
ss : Supports M S
q : Λ
T : Tape Γ
h₂ : { q := q, Tape := T }.q ∈ S
q' : Λ
a : Stmt Γ
h : M q T.head = some (q', a)
h₁ :
  (match (q', a) with
    | (q', a) =>
      { q := q',
        Tape :=
          match a with
          | Stmt.move d => Tape.move d T
          | Stmt.write a => Tape.write a T }) ∈
    step M { q := q, Tape := T }
⊢ (match (q', a) with
      | (q', a) =>
        { q := q',
          Tape :=
            match a with
            | Stmt.move d => Tape.move d T
            | Stmt.write a => Tape.write a T }).q ∈
    S

Proof state:
case intro.mk.intro
Γ : Type u_1
Λ : Type u_2
inst✝¹ : Inhabited Λ
inst✝ : Inhabited Γ
M : Machine Γ Λ
S : Set Λ
ss : Supports M S
q : Λ
T : Tape Γ
h₂ : { q := q, Tape := T }.q ∈ S
q' : Λ
a : Stmt Γ
h : M q T.head = some (q', a)
h₁ :
  (match (q', a) with
    | (q', a) =>
      { q := q',
        Tape :=
          match a with
          | Stmt.move d => Tape.move d T
          | Stmt.write a => Tape.write a T }) ∈
    step M { q := q, Tape := T }
⊢ (match (q', a) with
      | (q', a) =>
        { q := q',
          Tape :=
            match a with
            | Stmt.move d => Tape.move d T
            | Stmt.write a => Tape.write a T }).q ∈
    S

Tactic:
exact ss.2 h h₂

Result:
no goals

Proof state:
Γ : Type u_1
Λ : Type u_2
inst✝¹ : Inhabited Λ
inst✝ : Inhabited Γ
M : Machine Γ Λ
S : Set Λ
ss : Supports M S
⊢ ∀ {c c' : Cfg Γ Λ}, c' ∈ step M c → c.q ∈ S → c'.q ∈ S

Tactic:
intro ⟨q, T⟩ c' h₁ h₂

Result:
Γ : Type u_1
Λ : Type u_2
inst✝¹ : Inhabited Λ
inst✝ : Inhabited Γ
M : Machine Γ Λ
S : Set Λ
ss : Supports M S
q : Λ
T : Tape Γ
c' : Cfg Γ Λ
h₁ : c' ∈ step M { q := q, Tape := T }
h₂ : { q := q, Tape := T }.q ∈ S
⊢ c'.q ∈ S
-- Mathlib/Order/Monotone/Basic.lean
/-- A function between linear orders which is neither monotone nor antitone makes a dent upright or
downright. -/
lemma not_monotone_not_antitone_iff_exists_lt_lt :
    ¬ Monotone f ∧ ¬ Antitone f ↔ ∃ a b c, a < b ∧ b < c ∧
    (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Proof state:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ ¬Monotone f ∧ ¬Antitone f ↔ ∃ a b c, a < b ∧ b < c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Tactic:
simp_rw [not_monotone_not_antitone_iff_exists_le_le, ← and_assoc]

Result:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ (∃ a b c, (a ≤ b ∧ b ≤ c) ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)) ↔
    ∃ a b c, (a < b ∧ b < c) ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Proof state:
case refine_2
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
h : f a < f b ∧ f b < f b ∨ f b < f a ∧ f b < f b
⊢ False

Tactic:
simp at h

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ (∃ a b c, (a ≤ b ∧ b ≤ c) ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)) ↔
    ∃ a b c, (a < b ∧ b < c) ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Tactic:
refine exists₃_congr (fun a b c ↦ and_congr_left <|
  fun h ↦ (Ne.le_iff_lt ?_).and <| Ne.le_iff_lt ?_) <;>
(rintro rfl; simp at h)

Result:
no goals

Proof state:
case refine_2
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b c : α
h : f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c
⊢ b ≠ c

Tactic:
rintro rfl

Result:
case refine_2
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
h : f a < f b ∧ f b < f b ∨ f b < f a ∧ f b < f b
⊢ False
-- Mathlib/Algebra/Lie/Weights/Killing.lean
@[simp] lemma coroot_eq_zero_iff {α : Weight K H L} :
    coroot α = 0 ↔ α.IsZero

Proof state:
case refine_2
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsZero
⊢ coroot α = 0

Tactic:
simp [coroot, Weight.coe_toLinear_eq_zero_iff.mpr hα]

Result:
no goals

Proof state:
case refine_1
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : coroot α = 0
⊢ α.IsZero

Tactic:
by_contra contra

Result:
case refine_1
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : coroot α = 0
contra : ¬α.IsZero
⊢ False

Proof state:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
⊢ coroot α = 0 ↔ α.IsZero

Tactic:
refine ⟨fun hα ↦ ?_, fun hα ↦ ?_⟩

Result:
case refine_1
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : coroot α = 0
⊢ α.IsZero

case refine_2
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsZero
⊢ coroot α = 0

Proof state:
case refine_1
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : coroot α = 0
contra : ¬α.IsZero
⊢ False

Tactic:
simpa [hα, ← α.coe_coe, map_zero] using root_apply_coroot contra

Result:
no goals
-- Mathlib/Data/Real/GoldenRatio.lean
theorem gold_sq : φ ^ 2 = φ + 1

Proof state:
⊢ φ ^ 2 = φ + 1

Tactic:
rw [goldenRatio, ← sub_eq_zero]

Result:
⊢ ((1 + √5) / 2) ^ 2 - ((1 + √5) / 2 + 1) = 0

Proof state:
⊢ -5 / 4 + √5 ^ 2 * (1 / 4) = 0

Tactic:
rw [Real.sq_sqrt] <;> norm_num

Result:
no goals

Proof state:
⊢ ((1 + √5) / 2) ^ 2 - ((1 + √5) / 2 + 1) = 0

Tactic:
ring_nf

Result:
⊢ -5 / 4 + √5 ^ 2 * (1 / 4) = 0
-- Mathlib/Data/Int/Lemmas.lean
theorem natAbs_coe_sub_coe_lt_of_lt {a b n : ℕ} (a_lt_n : a < n) (b_lt_n : b < n) :
    natAbs (a - b : ℤ) < n

Proof state:
a b n : ℕ
a_lt_n : a < n
b_lt_n : b < n
⊢ (↑a - ↑b).natAbs < n

Tactic:
rw [← Nat.cast_lt (α := ℤ), natCast_natAbs]

Result:
a b n : ℕ
a_lt_n : a < n
b_lt_n : b < n
⊢ |↑a - ↑b| < ↑n

Proof state:
a b n : ℕ
a_lt_n : a < n
b_lt_n : b < n
⊢ |↑a - ↑b| < ↑n

Tactic:
exact abs_sub_lt_of_nonneg_of_lt (ofNat_nonneg a) (ofNat_lt.mpr a_lt_n)
  (ofNat_nonneg b) (ofNat_lt.mpr b_lt_n)

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[simp]
lemma liftCochain_fst :
    (liftCochain φ α β h).comp (fst φ).1 h = α

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
h : n + 1 = m
⊢ (liftCochain φ α β h).comp (↑(fst φ)) h = α

Tactic:
simp [liftCochain]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma exists_isBasis_inter_ground_isBasis_closure (M : Matroid α) (X : Set α) :
    ∃ I, M.IsBasis I (X ∩ M.E) ∧ M.IsBasis I (M.closure X)

Proof state:
α : Type u_2
M : Matroid α
X : Set α
⊢ ∃ I, M.IsBasis I (X ∩ M.E) ∧ M.IsBasis I (M.closure X)

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis (X ∩ M.E)

Result:
case intro
α : Type u_2
M : Matroid α
X I : Set α
hI : M.IsBasis I (X ∩ M.E)
⊢ ∃ I, M.IsBasis I (X ∩ M.E) ∧ M.IsBasis I (M.closure X)

Proof state:
case intro
α : Type u_2
M : Matroid α
X I : Set α
hI : M.IsBasis I (X ∩ M.E)
hI' : M.IsBasis I (M.closure X)
⊢ ∃ I, M.IsBasis I (X ∩ M.E) ∧ M.IsBasis I (M.closure X)

Tactic:
exact ⟨_, hI, hI'⟩

Result:
no goals

Proof state:
case intro
α : Type u_2
M : Matroid α
X I : Set α
hI : M.IsBasis I (X ∩ M.E)
⊢ ∃ I, M.IsBasis I (X ∩ M.E) ∧ M.IsBasis I (M.closure X)

Tactic:
have hI' := hI.isBasis_closure_right

Result:
case intro
α : Type u_2
M : Matroid α
X I : Set α
hI : M.IsBasis I (X ∩ M.E)
hI' : M.IsBasis I (M.closure (X ∩ M.E))
⊢ ∃ I, M.IsBasis I (X ∩ M.E) ∧ M.IsBasis I (M.closure X)

Proof state:
case intro
α : Type u_2
M : Matroid α
X I : Set α
hI : M.IsBasis I (X ∩ M.E)
hI' : M.IsBasis I (M.closure (X ∩ M.E))
⊢ ∃ I, M.IsBasis I (X ∩ M.E) ∧ M.IsBasis I (M.closure X)

Tactic:
rw [closure_inter_ground] at hI'

Result:
case intro
α : Type u_2
M : Matroid α
X I : Set α
hI : M.IsBasis I (X ∩ M.E)
hI' : M.IsBasis I (M.closure X)
⊢ ∃ I, M.IsBasis I (X ∩ M.E) ∧ M.IsBasis I (M.closure X)
-- Mathlib/MeasureTheory/Decomposition/Jordan.lean
theorem toSignedMeasure_zero : (0 : JordanDecomposition α).toSignedMeasure = 0

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
⊢ toSignedMeasure 0 = 0

Tactic:
ext1 i hi

Result:
case h
α : Type u_1
inst✝ : MeasurableSpace α
i : Set α
hi : MeasurableSet i
⊢ ↑(toSignedMeasure 0) i = ↑0 i

Proof state:
case h
α : Type u_1
inst✝ : MeasurableSpace α
i : Set α
hi : MeasurableSet i
⊢ ↑(toSignedMeasure 0) i = ↑0 i

Tactic:
rw [toSignedMeasure, toSignedMeasure_sub_apply hi, zero_posPart, zero_negPart, sub_self,
  VectorMeasure.coe_zero, Pi.zero_apply]

Result:
no goals
-- Mathlib/Algebra/CharP/Defs.lean
lemma char_ne_one [Nontrivial R] (p : ℕ) [hc : CharP R p] : p ≠ 1 := fun hp : p = 1 =>
  have : (1 : R) = 0

Proof state:
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
p : ℕ
hc : CharP R p
hp : p = 1
⊢ 1 = 0

Tactic:
simpa using (cast_eq_zero_iff R p 1).mpr (hp ▸ dvd_refl p)

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem zero_le_restrict_not_measurable (hi : ¬MeasurableSet i) : 0 ≤[i] v

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
v : VectorMeasure α M
i : Set α
hi : ¬MeasurableSet i
⊢ 0 ≤[i] v

Tactic:
rw [restrict_zero, restrict_not_measurable _ hi]

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean
theorem succ_nth_stream_eq_some_iff {ifp_succ_n : IntFractPair K} :
    IntFractPair.stream v (n + 1) = some ifp_succ_n ↔
      ∃ ifp_n : IntFractPair K,
        IntFractPair.stream v n = some ifp_n ∧
          ifp_n.fr ≠ 0 ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_succ_n : IntFractPair K
⊢ IntFractPair.stream v (n + 1) = some ifp_succ_n ↔
    ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr ≠ 0 ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n

Tactic:
simp [IntFractPair.stream, ite_eq_iff, Option.bind_eq_some]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Finite.lean
theorem Disjoint.orderOf {σ τ : Perm α} (hστ : Disjoint σ τ) :
    orderOf (σ * τ) = Nat.lcm (orderOf σ) (orderOf τ) :=
  haveI h : ∀ n : ℕ, (σ * τ) ^ n = 1 ↔ σ ^ n = 1 ∧ τ ^ n = 1 := fun n => by
    rw [hστ.commute.mul_pow, Disjoint.mul_eq_one_iff (hστ.pow_disjoint_pow n n)]
  Nat.dvd_antisymm hστ.commute.orderOf_mul_dvd_lcm
    (Nat.lcm_dvd
      (orderOf_dvd_of_pow_eq_one ((h (orderOf (σ * τ))).mp (pow_orderOf_eq_one (σ * τ))).1)
      (orderOf_dvd_of_pow_eq_one ((h (orderOf (σ * τ))).mp (pow_orderOf_eq_one (σ * τ))).2))

Proof state:
α : Type u
σ τ : Perm α
hστ : σ.Disjoint τ
n : ℕ
⊢ (σ * τ) ^ n = 1 ↔ σ ^ n = 1 ∧ τ ^ n = 1

Tactic:
rw [hστ.commute.mul_pow, Disjoint.mul_eq_one_iff (hστ.pow_disjoint_pow n n)]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Smeval.lean
theorem leval_eq_smeval.linearMap {R : Type*} [Semiring R] (r : R) :
    leval r = smeval.linearMap R r

Proof state:
R : Type u_3
inst✝ : Semiring R
r : R
⊢ leval r = smeval.linearMap R r

Tactic:
refine LinearMap.ext ?_

Result:
R : Type u_3
inst✝ : Semiring R
r : R
⊢ ∀ (x : R[X]), (leval r) x = (smeval.linearMap R r) x

Proof state:
R : Type u_3
inst✝ : Semiring R
r : R
x✝ : R[X]
⊢ (leval r) x✝ = (smeval.linearMap R r) x✝

Tactic:
rw [leval_apply, smeval.linearMap_apply, eval_eq_smeval]

Result:
no goals

Proof state:
R : Type u_3
inst✝ : Semiring R
r : R
⊢ ∀ (x : R[X]), (leval r) x = (smeval.linearMap R r) x

Tactic:
intro

Result:
R : Type u_3
inst✝ : Semiring R
r : R
x✝ : R[X]
⊢ (leval r) x✝ = (smeval.linearMap R r) x✝
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
theorem isClosedEmbedding_coe_ennreal : IsClosedEmbedding ((↑) : ℝ≥0∞ → EReal) :=
  ⟨isEmbedding_coe_ennreal, by rw [range_coe_ennreal]; exact isClosed_Ici⟩

Proof state:
⊢ IsClosed (range ENNReal.toEReal)

Tactic:
rw [range_coe_ennreal]

Result:
⊢ IsClosed (Ici 0)

Proof state:
⊢ IsClosed (Ici 0)

Tactic:
exact isClosed_Ici

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem preAleph_pos {o : Ordinal} : 0 < preAleph o ↔ 0 < o

Proof state:
o : Ordinal.{u_1}
⊢ 0 < preAleph o ↔ 0 < o

Tactic:
rw [← preAleph_zero, preAleph_lt_preAleph]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/ENNRealLogExp.lean
lemma exp_nmul (x : EReal) (n : ℕ) : exp (n * x) = (exp x) ^ n

Proof state:
x : EReal
n : ℕ
⊢ (↑n * x).exp = x.exp ^ n

Tactic:
simp_rw [← log_eq_iff, log_pow, log_exp]

Result:
no goals