harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem sqLe_cancel {c d x y z w : ℕ} (zw : SqLe y d x c) (h : SqLe (x + z) c (y + w) d) :
    SqLe z c w d

Proof state:
case a
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
l : c * z * z > d * w * w
⊢ c * (x + z) * (x + z) > d * (y + w) * (y + w)

Tactic:
simp only [SqLe, mul_add, mul_comm, mul_left_comm, add_assoc, gt_iff_lt]

Result:
case a
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
l : c * z * z > d * w * w
⊢ d * (y * y) + (d * (y * w) + (d * (y * w) + d * (w * w))) < c * (x * x) + (c * (x * z) + (c * (x * z) + c * (z * z)))

Proof state:
case a
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
l : c * z * z > d * w * w
hm : d * (y * w) ≤ c * (x * z)
⊢ d * (y * y) + (d * (y * w) + (d * (y * w) + d * (w * w))) < c * (x * x) + (c * (x * z) + (c * (x * z) + c * (z * z)))

Tactic:
simp only [SqLe, mul_assoc, gt_iff_lt] at l zw

Result:
case a
c d x y z w : ℕ
h : SqLe (x + z) c (y + w) d
hm : d * (y * w) ≤ c * (x * z)
l : d * (w * w) < c * (z * z)
zw : d * (y * y) ≤ c * (x * x)
⊢ d * (y * y) + (d * (y * w) + (d * (y * w) + d * (w * w))) < c * (x * x) + (c * (x * z) + (c * (x * z) + c * (z * z)))

Proof state:
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
⊢ SqLe z c w d

Tactic:
apply le_of_not_gt

Result:
case a
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
⊢ ¬c * z * z > d * w * w

Proof state:
case a
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
l : c * z * z > d * w * w
⊢ d * (y * y) + (d * (y * w) + (d * (y * w) + d * (w * w))) < c * (x * x) + (c * (x * z) + (c * (x * z) + c * (z * z)))

Tactic:
have hm := sqLe_add_mixed zw (le_of_lt l)

Result:
case a
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
l : c * z * z > d * w * w
hm : d * (y * w) ≤ c * (x * z)
⊢ d * (y * y) + (d * (y * w) + (d * (y * w) + d * (w * w))) < c * (x * x) + (c * (x * z) + (c * (x * z) + c * (z * z)))

Proof state:
case a
c d x y z w : ℕ
h : SqLe (x + z) c (y + w) d
hm : d * (y * w) ≤ c * (x * z)
l : d * (w * w) < c * (z * z)
zw : d * (y * y) ≤ c * (x * x)
⊢ d * (y * y) + (d * (y * w) + (d * (y * w) + d * (w * w))) < c * (x * x) + (c * (x * z) + (c * (x * z) + c * (z * z)))

Tactic:
exact
  lt_of_le_of_lt (add_le_add_right zw _)
    (add_lt_add_left (add_lt_add_of_le_of_lt hm (add_lt_add_of_le_of_lt hm l)) _)

Result:
no goals

Proof state:
case a
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
l : c * z * z > d * w * w
⊢ False

Tactic:
refine not_le_of_gt ?_ h

Result:
case a
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
l : c * z * z > d * w * w
⊢ c * (x + z) * (x + z) > d * (y + w) * (y + w)

Proof state:
case a
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
⊢ ¬c * z * z > d * w * w

Tactic:
intro l

Result:
case a
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
l : c * z * z > d * w * w
⊢ False
-- Mathlib/GroupTheory/Abelianization.lean
theorem mem_commutatorSet_of_isConj_sq {g : G} (hg : IsConj g (g ^ 2)) :
    g ∈ commutatorSet G

Proof state:
case intro
G : Type u
inst✝ : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h) g (g ^ 2)
⊢ g ∈ commutatorSet G

Tactic:
use h, g

Result:
case h
G : Type u
inst✝ : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h) g (g ^ 2)
⊢ ⁅↑h, g⁆ = g

Proof state:
case h
G : Type u
inst✝ : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h) g (g ^ 2)
⊢ g ^ 2 * ↑h * (↑h)⁻¹ * g⁻¹ = g

Tactic:
simp only [IsUnit.mul_inv_cancel_right, Units.isUnit, mul_inv_eq_iff_eq_mul, pow_two]

Result:
no goals

Proof state:
case h
G : Type u
inst✝ : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h) g (g ^ 2)
⊢ ⁅↑h, g⁆ = g

Tactic:
rw [commutatorElement_def, hg]

Result:
case h
G : Type u
inst✝ : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h) g (g ^ 2)
⊢ g ^ 2 * ↑h * (↑h)⁻¹ * g⁻¹ = g

Proof state:
G : Type u
inst✝ : Group G
g : G
hg : IsConj g (g ^ 2)
⊢ g ∈ commutatorSet G

Tactic:
obtain ⟨h, hg⟩ := hg

Result:
case intro
G : Type u
inst✝ : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h) g (g ^ 2)
⊢ g ∈ commutatorSet G
-- Mathlib/Algebra/Polynomial/Degree/SmallDegree.lean
theorem eq_X_add_C_of_degree_le_one (h : degree p ≤ 1) : p = C (p.coeff 1) * X + C (p.coeff 0) :=
  ext fun n =>
    Nat.casesOn n (by simp) fun n =>
      Nat.casesOn n (by simp [coeff_C]) fun m => by
        -- Porting note: `by decide` → `Iff.mpr ..`
        have : degree p < m.succ.succ := lt_of_le_of_lt h
          (Iff.mpr WithBot.coe_lt_coe <| Nat.succ_lt_succ <| Nat.zero_lt_succ m)
        simp [coeff_eq_zero_of_degree_lt this, coeff_C, Nat.succ_ne_zero, coeff_X, Nat.succ_inj',
          @eq_comm ℕ 0]

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.degree ≤ 1
n✝ n m : ℕ
⊢ p.coeff m.succ.succ = (C (p.coeff 1) * X + C (p.coeff 0)).coeff m.succ.succ

Tactic:
have : degree p < m.succ.succ := lt_of_le_of_lt h
  (Iff.mpr WithBot.coe_lt_coe <| Nat.succ_lt_succ <| Nat.zero_lt_succ m)

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.degree ≤ 1
n✝ n m : ℕ
this : p.degree < ↑m.succ.succ
⊢ p.coeff m.succ.succ = (C (p.coeff 1) * X + C (p.coeff 0)).coeff m.succ.succ

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.degree ≤ 1
n✝ n m : ℕ
this : p.degree < ↑m.succ.succ
⊢ p.coeff m.succ.succ = (C (p.coeff 1) * X + C (p.coeff 0)).coeff m.succ.succ

Tactic:
simp [coeff_eq_zero_of_degree_lt this, coeff_C, Nat.succ_ne_zero, coeff_X, Nat.succ_inj',
  @eq_comm ℕ 0]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.degree ≤ 1
n : ℕ
⊢ p.coeff Nat.zero = (C (p.coeff 1) * X + C (p.coeff 0)).coeff Nat.zero

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.degree ≤ 1
n✝ n : ℕ
⊢ p.coeff Nat.zero.succ = (C (p.coeff 1) * X + C (p.coeff 0)).coeff Nat.zero.succ

Tactic:
simp [coeff_C]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem support_X [Nontrivial R] : (X n : MvPolynomial σ R).support = {Finsupp.single n 1}

Proof state:
case hnc
R : Type u
σ : Type u_1
n : σ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ ¬1 = 0

Tactic:
exact one_ne_zero

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
n : σ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ (X n).support = {Finsupp.single n 1}

Tactic:
rw [X, support_monomial, if_neg]

Result:
case hnc
R : Type u
σ : Type u_1
n : σ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ ¬1 = 0

Proof state:
R : Type u
σ : Type u_1
n : σ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ (X n).support = {Finsupp.single n 1}

Tactic:
classical rw [X, support_monomial, if_neg]; exact one_ne_zero

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Injective/Resolution.lean
lemma ofCocomplex_d_0_1 :
    (ofCocomplex Z).d 0 1 = d (Injective.ι Z)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ (ofCocomplex Z).d 0 1 = d (Injective.ι Z)

Tactic:
simp [ofCocomplex]

Result:
no goals
-- Mathlib/Algebra/Group/Ext.lean
theorem RightCancelMonoid.toMonoid_injective {M : Type u} :
    Function.Injective (@RightCancelMonoid.toMonoid M)

Proof state:
M : Type u
⊢ Injective (@toMonoid M)

Tactic:
rintro @⟨@⟨⟩⟩ @⟨@⟨⟩⟩ h

Result:
case mk.mk.mk.mk
M : Type u
toSemigroup✝¹ : Semigroup M
toOne✝¹ : One M
one_mul✝¹ : ∀ (a : M), 1 * a = a
mul_one✝¹ : ∀ (a : M), a * 1 = a
npow✝¹ : ℕ → M → M
npow_zero✝¹ : ∀ (x : M), npow✝¹ 0 x = 1
npow_succ✝¹ : ∀ (n : ℕ) (x : M), npow✝¹ (n + 1) x = npow✝¹ n x * x
mul_right_cancel✝¹ : ∀ (a b c : M), a * b = c * b → a = c
toSemigroup✝ : Semigroup M
toOne✝ : One M
one_mul✝ : ∀ (a : M), 1 * a = a
mul_one✝ : ∀ (a : M), a * 1 = a
npow✝ : ℕ → M → M
npow_zero✝ : ∀ (x : M), npow✝ 0 x = 1
npow_succ✝ : ∀ (n : ℕ) (x : M), npow✝ (n + 1) x = npow✝ n x * x
mul_right_cancel✝ : ∀ (a b c : M), a * b = c * b → a = c
h : toMonoid = toMonoid
⊢ mk mul_right_cancel✝¹ = mk mul_right_cancel✝

Proof state:
case mk.mk.mk.mk
M : Type u
toSemigroup✝¹ : Semigroup M
toOne✝¹ : One M
one_mul✝¹ : ∀ (a : M), 1 * a = a
mul_one✝¹ : ∀ (a : M), a * 1 = a
npow✝¹ : ℕ → M → M
npow_zero✝¹ : ∀ (x : M), npow✝¹ 0 x = 1
npow_succ✝¹ : ∀ (n : ℕ) (x : M), npow✝¹ (n + 1) x = npow✝¹ n x * x
mul_right_cancel✝¹ : ∀ (a b c : M), a * b = c * b → a = c
toSemigroup✝ : Semigroup M
toOne✝ : One M
one_mul✝ : ∀ (a : M), 1 * a = a
mul_one✝ : ∀ (a : M), a * 1 = a
npow✝ : ℕ → M → M
npow_zero✝ : ∀ (x : M), npow✝ 0 x = 1
npow_succ✝ : ∀ (n : ℕ) (x : M), npow✝ (n + 1) x = npow✝ n x * x
mul_right_cancel✝ : ∀ (a b c : M), a * b = c * b → a = c
h : toMonoid = toMonoid
⊢ mk mul_right_cancel✝¹ = mk mul_right_cancel✝

Tactic:
congr <;> injection h

Result:
no goals
-- Mathlib/Logic/Equiv/Set.lean
theorem prod_assoc_symm_image {α β γ} {s : Set α} {t : Set β} {u : Set γ} :
    (Equiv.prodAssoc α β γ).symm '' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
u : Set γ
⊢ ⇑(prodAssoc α β γ).symm '' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u

Tactic:
simpa only [Equiv.image_eq_preimage] using prod_assoc_preimage

Result:
no goals
-- Mathlib/NumberTheory/Padics/RingHoms.lean
theorem nthHom_zero : nthHom f 0 = 0

Proof state:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
⊢ nthHom f 0 = 0

Tactic:
simp (config := { unfoldPartialApp := true }) [nthHom]

Result:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
⊢ (fun n => 0) = 0

Proof state:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
⊢ (fun n => 0) = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem PseudoMetricSpace.replaceBornology_eq {α} [m : PseudoMetricSpace α] [B : Bornology α]
    (H : ∀ s, @IsBounded _ B s ↔ @IsBounded _ PseudoMetricSpace.toBornology s) :
    PseudoMetricSpace.replaceBornology _ H = m

Proof state:
case h.dist.h.h
α : Type u_3
m : PseudoMetricSpace α
B : Bornology α
H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s
x✝¹ x✝ : α
⊢ dist x✝¹ x✝ = dist x✝¹ x✝

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_3
m : PseudoMetricSpace α
B : Bornology α
H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s
⊢ m.replaceBornology H = m

Tactic:
ext

Result:
case h.dist.h.h
α : Type u_3
m : PseudoMetricSpace α
B : Bornology α
H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s
x✝¹ x✝ : α
⊢ dist x✝¹ x✝ = dist x✝¹ x✝
-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
lemma coroot'_reflection_perm {i j : ι} :
    P.coroot' (P.reflection_perm i j) = P.coroot' j ∘ₗ P.reflection i

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 : ι
⊢ P.coroot' ((P.reflection_perm i) j) = P.coroot' j ∘ₗ ↑(P.reflection i)

Tactic:
ext y

Result:
case h
ι : 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 : ι
y : M
⊢ (P.coroot' ((P.reflection_perm i) j)) y = (P.coroot' j ∘ₗ ↑(P.reflection i)) y

Proof state:
case h
ι : 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 : ι
y : M
⊢ (P.coroot' ((P.reflection_perm i) j)) y = (P.coroot' j ∘ₗ ↑(P.reflection i)) y

Tactic:
simp [coreflection_apply_coroot, reflection_apply, map_sub, mul_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem laverage_lt_top (hf : ∫⁻ x, f x ∂μ ≠ ∞) : ⨍⁻ x, f x ∂μ < ∞

Proof state:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hμ : μ ≠ 0
⊢ (∫⁻ (x : α), f x ∂μ) / μ univ < ⊤

Tactic:
exact div_lt_top hf (measure_univ_ne_zero.2 hμ)

Result:
no goals

Proof state:
case inl
α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂0 ≠ ⊤
⊢ ⨍⁻ (x : α), f x ∂0 < ⊤

Tactic:
simp

Result:
no goals

Proof state:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hμ : μ ≠ 0
⊢ ⨍⁻ (x : α), f x ∂μ < ⊤

Tactic:
rw [laverage_eq]

Result:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hμ : μ ≠ 0
⊢ (∫⁻ (x : α), f x ∂μ) / μ univ < ⊤

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
⊢ ⨍⁻ (x : α), f x ∂μ < ⊤

Tactic:
obtain rfl | hμ := eq_or_ne μ 0

Result:
case inl
α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂0 ≠ ⊤
⊢ ⨍⁻ (x : α), f x ∂0 < ⊤

case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hμ : μ ≠ 0
⊢ ⨍⁻ (x : α), f x ∂μ < ⊤
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem pow_le {κ μ : Cardinal.{u}} (H1 : ℵ₀ ≤ κ) (H2 : μ < ℵ₀) : κ ^ μ ≤ κ :=
  let ⟨n, H3⟩ := lt_aleph0.1 H2
  H3.symm ▸
    Quotient.inductionOn κ
      (fun α H1 =>
        Nat.recOn n
          (lt_of_lt_of_le
              (by
                rw [Nat.cast_zero, power_zero]
                exact one_lt_aleph0)
              H1).le
          fun n ih =>
          le_of_le_of_eq
            (by
              rw [Nat.cast_succ, power_add, power_one]
              exact mul_le_mul_right' ih _)
            (mul_eq_self H1))
      H1

Proof state:
κ μ : Cardinal.{u}
H1✝ : ℵ₀ ≤ κ
H2 : μ < ℵ₀
n✝ : ℕ
H3 : μ = ↑n✝
α : Type u
H1 : ℵ₀ ≤ ⟦α⟧
n : ℕ
ih : ⟦α⟧ ^ ↑n ≤ ⟦α⟧
⊢ ⟦α⟧ ^ ↑n.succ ≤ ⟦α⟧ * ⟦α⟧

Tactic:
rw [Nat.cast_succ, power_add, power_one]

Result:
κ μ : Cardinal.{u}
H1✝ : ℵ₀ ≤ κ
H2 : μ < ℵ₀
n✝ : ℕ
H3 : μ = ↑n✝
α : Type u
H1 : ℵ₀ ≤ ⟦α⟧
n : ℕ
ih : ⟦α⟧ ^ ↑n ≤ ⟦α⟧
⊢ ⟦α⟧ ^ ↑n * ⟦α⟧ ≤ ⟦α⟧ * ⟦α⟧

Proof state:
κ μ : Cardinal.{u}
H1✝ : ℵ₀ ≤ κ
H2 : μ < ℵ₀
n✝ : ℕ
H3 : μ = ↑n✝
α : Type u
H1 : ℵ₀ ≤ ⟦α⟧
n : ℕ
ih : ⟦α⟧ ^ ↑n ≤ ⟦α⟧
⊢ ⟦α⟧ ^ ↑n * ⟦α⟧ ≤ ⟦α⟧ * ⟦α⟧

Tactic:
exact mul_le_mul_right' ih _

Result:
no goals

Proof state:
κ μ : Cardinal.{u}
H1✝ : ℵ₀ ≤ κ
H2 : μ < ℵ₀
n : ℕ
H3 : μ = ↑n
α : Type u
H1 : ℵ₀ ≤ ⟦α⟧
⊢ ⟦α⟧ ^ ↑Nat.zero < ℵ₀

Tactic:
rw [Nat.cast_zero, power_zero]

Result:
κ μ : Cardinal.{u}
H1✝ : ℵ₀ ≤ κ
H2 : μ < ℵ₀
n : ℕ
H3 : μ = ↑n
α : Type u
H1 : ℵ₀ ≤ ⟦α⟧
⊢ 1 < ℵ₀

Proof state:
κ μ : Cardinal.{u}
H1✝ : ℵ₀ ≤ κ
H2 : μ < ℵ₀
n : ℕ
H3 : μ = ↑n
α : Type u
H1 : ℵ₀ ≤ ⟦α⟧
⊢ 1 < ℵ₀

Tactic:
exact one_lt_aleph0

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lex/Lemmas.lean
theorem lex_eq_false_iff_ge [DecidableEq α] [LT α] [DecidableLT α]
    {l₁ l₂ : Array α} : lex l₁ l₂ = false ↔ l₂ ≤ l₁

Proof state:
case mk.mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
toList✝¹ toList✝ : List α
⊢ ({ toList := toList✝¹ }.lex { toList := toList✝ } fun x1 x2 => decide (x1 < x2)) = false ↔
    { toList := toList✝ } ≤ { toList := toList✝¹ }

Tactic:
simp [List.not_lt_iff_ge]

Result:
no goals

Proof state:
case mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
l₂ : Array α
toList✝ : List α
⊢ ({ toList := toList✝ }.lex l₂ fun x1 x2 => decide (x1 < x2)) = false ↔ l₂ ≤ { toList := toList✝ }

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
toList✝¹ toList✝ : List α
⊢ ({ toList := toList✝¹ }.lex { toList := toList✝ } fun x1 x2 => decide (x1 < x2)) = false ↔
    { toList := toList✝ } ≤ { toList := toList✝¹ }

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
l₁ l₂ : Array α
⊢ (l₁.lex l₂ fun x1 x2 => decide (x1 < x2)) = false ↔ l₂ ≤ l₁

Tactic:
cases l₁

Result:
case mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
l₂ : Array α
toList✝ : List α
⊢ ({ toList := toList✝ }.lex l₂ fun x1 x2 => decide (x1 < x2)) = false ↔ l₂ ≤ { toList := toList✝ }
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Equal.lean
theorem BitVec.add_right_inj (a b c : BitVec w) : (c + a == c + b) = (a == b)

Proof state:
w : Nat
a b c : BitVec w
⊢ (c + a == c + b) = (a == b)

Tactic:
rw [Bool.eq_iff_iff]

Result:
w : Nat
a b c : BitVec w
⊢ (c + a == c + b) = true ↔ (a == b) = true

Proof state:
w : Nat
a b c : BitVec w
⊢ (c + a == c + b) = true ↔ (a == b) = true

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Manifold/LocalDiffeomorph.lean
/-- A `C^n` local diffeomorphism at `x` is `C^n` differentiable at `x`. -/
lemma IsLocalDiffeomorphAt.contMDiffAt (hf : IsLocalDiffeomorphAt I J n f x) :
    ContMDiffAt I J n f x

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H : Type u_4
inst✝⁵ : TopologicalSpace H
G : Type u_5
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
x : M
Φ : PartialDiffeomorph I J M N n
hx : x ∈ Φ.source
heq : EqOn f (↑Φ.toPartialEquiv) Φ.source
⊢ ContMDiffAt I J n f x

Tactic:
exact ((Φ.contMDiffOn_toFun).congr heq).contMDiffAt (Φ.open_source.mem_nhds hx)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H : Type u_4
inst✝⁵ : TopologicalSpace H
G : Type u_5
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
⊢ ContMDiffAt I J n f x

Tactic:
choose Φ hx heq using hf

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H : Type u_4
inst✝⁵ : TopologicalSpace H
G : Type u_5
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
x : M
Φ : PartialDiffeomorph I J M N n
hx : x ∈ Φ.source
heq : EqOn f (↑Φ.toPartialEquiv) Φ.source
⊢ ContMDiffAt I J n f x
-- Mathlib/Topology/Homeomorph.lean
theorem _root_.Fin.continuous_append (m n : ℕ) :
    Continuous fun (p : (Fin m → X) × (Fin n → X)) ↦ Fin.append p.1 p.2

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
m n : ℕ
this : Continuous ⇑(Fin.appendEquiv m n)
⊢ Continuous fun p => Fin.append p.1 p.2

Tactic:
exact this

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
m n : ℕ
⊢ Continuous ⇑(Fin.appendEquiv m n)

Tactic:
rw [Fin.appendEquiv_eq_Homeomorph]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
m n : ℕ
⊢ Continuous ⇑(sumArrowHomeomorphProdArrow.symm.trans (piCongrLeft finSumFinEquiv)).toEquiv

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
m n : ℕ
⊢ Continuous ⇑(sumArrowHomeomorphProdArrow.symm.trans (piCongrLeft finSumFinEquiv)).toEquiv

Tactic:
exact Homeomorph.continuous_toFun _

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
m n : ℕ
⊢ Continuous fun p => Fin.append p.1 p.2

Tactic:
suffices Continuous (Fin.appendEquiv m n) by exact this

Result:
X : Type u_1
inst✝ : TopologicalSpace X
m n : ℕ
⊢ Continuous ⇑(Fin.appendEquiv m n)
-- Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
theorem cokernelIsoOfEq_hom_comp_desc {Z} {f g : X ⟶ Y} [HasCokernel f] [HasCokernel g] (h : f = g)
    (e : Y ⟶ Z) (he) :
    (cokernelIsoOfEq h).hom ≫ cokernel.desc _ e he = cokernel.desc _ e (by simp [h, he])

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y Z : C
f g : X ⟶ Y
inst✝¹ : HasCokernel f
inst✝ : HasCokernel g
h : f = g
e : Y ⟶ Z
he : g ≫ e = 0
⊢ (cokernelIsoOfEq h).hom ≫ cokernel.desc g e he = cokernel.desc f e ⋯

Tactic:
cases h

Result:
case refl
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
inst✝¹ : HasCokernel f
e : Y ⟶ Z
inst✝ : HasCokernel f
he : f ≫ e = 0
⊢ (cokernelIsoOfEq ⋯).hom ≫ cokernel.desc f e he = cokernel.desc f e ⋯

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f✝ : X ⟶ Y
inst✝² : HasCokernel f✝
Z : C
f g : X ⟶ Y
inst✝¹ : HasCokernel f
inst✝ : HasCokernel g
h : f = g
e : Y ⟶ Z
he : g ≫ e = 0
⊢ f ≫ e = 0

Tactic:
simp [h, he]

Result:
no goals

Proof state:
case refl
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
inst✝¹ : HasCokernel f
e : Y ⟶ Z
inst✝ : HasCokernel f
he : f ≫ e = 0
⊢ (cokernelIsoOfEq ⋯).hom ≫ cokernel.desc f e he = cokernel.desc f e ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean
theorem posLog_nonneg {x : ℝ} : 0 ≤ log⁺ x

Proof state:
x : ℝ
⊢ 0 ≤ log⁺ x

Tactic:
simp [posLog]

Result:
no goals
-- Mathlib/Computability/PartrecCode.lean
theorem encode_lt_pair (cf cg) :
    encode cf < encode (pair cf cg) ∧ encode cg < encode (pair cf cg)

Proof state:
cf cg : Code
⊢ encode cf < encode (cf.pair cg) ∧ encode cg < encode (cf.pair cg)

Tactic:
simp only [encodeCode_eq, encodeCode]

Result:
cf cg : Code
⊢ cf.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4 ∧
    cg.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4

Proof state:
cf cg : Code
this : 1 * Nat.pair cf.encodeCode cg.encodeCode ≤ 2 * 2 * Nat.pair cf.encodeCode cg.encodeCode
⊢ cf.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4 ∧
    cg.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4

Tactic:
rw [one_mul, mul_assoc] at this

Result:
cf cg : Code
this : Nat.pair cf.encodeCode cg.encodeCode ≤ 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode)
⊢ cf.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4 ∧
    cg.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4

Proof state:
cf cg : Code
⊢ 1 ≤ 2 * 2

Tactic:
decide

Result:
no goals

Proof state:
cf cg : Code
this✝ : Nat.pair cf.encodeCode cg.encodeCode ≤ 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode)
this : Nat.pair cf.encodeCode cg.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4
⊢ cf.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4 ∧
    cg.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4

Tactic:
exact ⟨lt_of_le_of_lt (Nat.left_le_pair _ _) this, lt_of_le_of_lt (Nat.right_le_pair _ _) this⟩

Result:
no goals

Proof state:
cf cg : Code
⊢ cf.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4 ∧
    cg.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4

Tactic:
have := Nat.mul_le_mul_right (Nat.pair cf.encodeCode cg.encodeCode) (by decide : 1 ≤ 2 * 2)

Result:
cf cg : Code
this : 1 * Nat.pair cf.encodeCode cg.encodeCode ≤ 2 * 2 * Nat.pair cf.encodeCode cg.encodeCode
⊢ cf.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4 ∧
    cg.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4

Proof state:
cf cg : Code
this : Nat.pair cf.encodeCode cg.encodeCode ≤ 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode)
⊢ 0 < 4

Tactic:
decide

Result:
no goals

Proof state:
cf cg : Code
this : Nat.pair cf.encodeCode cg.encodeCode ≤ 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode)
⊢ cf.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4 ∧
    cg.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4

Tactic:
have := lt_of_le_of_lt this (lt_add_of_pos_right _ (by decide : 0 < 4))

Result:
cf cg : Code
this✝ : Nat.pair cf.encodeCode cg.encodeCode ≤ 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode)
this : Nat.pair cf.encodeCode cg.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4
⊢ cf.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4 ∧
    cg.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4