harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean
/-- A commutative square involving the morphisms `mor₃` of two distinguished triangles
can be extended as morphism of triangles -/
lemma complete_distinguished_triangle_morphism₂ (T₁ T₂ : Triangle C)
    (hT₁ : T₁ ∈ distTriang C) (hT₂ : T₂ ∈ distTriang C) (a : T₁.obj₁ ⟶ T₂.obj₁)
    (c : T₁.obj₃ ⟶ T₂.obj₃) (comm : T₁.mor₃ ≫ a⟦(1 : ℤ)⟧' = c ≫ T₂.mor₃) :
    ∃ (b : T₁.obj₂ ⟶ T₂.obj₂), T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₂ ≫ c = b ≫ T₂.mor₂

Proof state:
case intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a✝ : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a✝ = c ≫ T₂.mor₃
a : T₁.invRotate.obj₃ ⟶ T₂.invRotate.obj₃
ha₁ : T₁.invRotate.mor₂ ≫ a = a✝ ≫ T₂.invRotate.mor₂
ha₂ : T₁.invRotate.mor₃ ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map c) = a ≫ T₂.invRotate.mor₃
⊢ ∃ b, T₁.mor₁ ≫ b = a✝ ≫ T₂.mor₁ ∧ T₁.mor₂ ≫ c = b ≫ T₂.mor₂

Tactic:
refine ⟨a, ⟨ha₁, ?_⟩⟩

Result:
case intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a✝ : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a✝ = c ≫ T₂.mor₃
a : T₁.invRotate.obj₃ ⟶ T₂.invRotate.obj₃
ha₁ : T₁.invRotate.mor₂ ≫ a = a✝ ≫ T₂.invRotate.mor₂
ha₂ : T₁.invRotate.mor₃ ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map c) = a ≫ T₂.invRotate.mor₃
⊢ T₁.mor₂ ≫ c = a ≫ T₂.mor₂
-- Mathlib/LinearAlgebra/Matrix/Basis.lean
theorem toMatrix_eq_toMatrix_constr [Fintype ι] [DecidableEq ι] (v : ι → M) :
    e.toMatrix v = LinearMap.toMatrix e e (e.constr ℕ v)

Proof state:
ι : Type u_1
R : Type u_5
M : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
e : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
v : ι → M
⊢ e.toMatrix v = (LinearMap.toMatrix e e) ((e.constr ℕ) v)

Tactic:
ext

Result:
case a
ι : Type u_1
R : Type u_5
M : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
e : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
v : ι → M
i✝ j✝ : ι
⊢ e.toMatrix v i✝ j✝ = (LinearMap.toMatrix e e) ((e.constr ℕ) v) i✝ j✝

Proof state:
case a
ι : Type u_1
R : Type u_5
M : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
e : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
v : ι → M
i✝ j✝ : ι
⊢ e.toMatrix v i✝ j✝ = (LinearMap.toMatrix e e) ((e.constr ℕ) v) i✝ j✝

Tactic:
rw [Basis.toMatrix_apply, LinearMap.toMatrix_apply, Basis.constr_basis]

Result:
no goals
-- Mathlib/Algebra/Group/Operations.lean
@[to_additive]
lemma dite_div (a : P → α) (b : ¬ P → α) (c : α) :
    (if h : P then a h else b h) / c = if h : P then a h / c else b h / c

Proof state:
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : P → α
b : ¬P → α
c : α
⊢ (if h : P then a h else b h) / c = if h : P then a h / c else b h / c

Tactic:
split <;> rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Final.lean
/-- The functor `Grothendieck.map α` for a natural transformation `α : F ⟶ G`, with
`F G : C ⥤ Cat`, is final if for each `X : C`, the functor `α.app X` is final. -/
lemma Grothendieck.final_map {F G : C ⥤ Cat.{v₂, u₂}} (α : F ⟶ G) [hα : ∀ X, Final (α.app X)] :
    Final (map α)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), Final (α.app X)
sC : C ≌ AsSmall C := AsSmall.equiv
F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor
G' : AsSmall C ⥤ Cat := sC.inverse ⋙ G ⋙ Cat.asSmallFunctor
α' : F' ⟶ G' := whiskerLeft sC.inverse (whiskerRight α Cat.asSmallFunctor)
this : ∀ (X : AsSmall C), Final (α'.app X)
⊢ (map α).Final

Tactic:
have hα' : (map α').Final := final_map_small _

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), Final (α.app X)
sC : C ≌ AsSmall C := AsSmall.equiv
F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor
G' : AsSmall C ⥤ Cat := sC.inverse ⋙ G ⋙ Cat.asSmallFunctor
α' : F' ⟶ G' := whiskerLeft sC.inverse (whiskerRight α Cat.asSmallFunctor)
this : ∀ (X : AsSmall C), Final (α'.app X)
hα' : (map α').Final
⊢ (map α).Final

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), Final (α.app X)
sC : C ≌ AsSmall C := AsSmall.equiv
F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor
G' : AsSmall C ⥤ Cat := sC.inverse ⋙ G ⋙ Cat.asSmallFunctor
α' : F' ⟶ G' := whiskerLeft sC.inverse (whiskerRight α Cat.asSmallFunctor)
this : ∀ (X : AsSmall C), Final (α'.app X)
hα' : (map α').Final
⊢ (map α).Final

Tactic:
dsimp only [α', ← Equivalence.symm_functor] at hα'

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), Final (α.app X)
sC : C ≌ AsSmall C := AsSmall.equiv
F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor
G' : AsSmall C ⥤ Cat := sC.inverse ⋙ G ⋙ Cat.asSmallFunctor
α' : F' ⟶ G' := whiskerLeft sC.inverse (whiskerRight α Cat.asSmallFunctor)
this : ∀ (X : AsSmall C), Final (α'.app X)
hα' : (map (whiskerLeft sC.symm.functor (whiskerRight α Cat.asSmallFunctor))).Final
⊢ (map α).Final

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), Final (α.app X)
sC : C ≌ AsSmall C := AsSmall.equiv
F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor
G' : AsSmall C ⥤ Cat := sC.inverse ⋙ G ⋙ Cat.asSmallFunctor
⊢ (map α).Final

Tactic:
let α' : F' ⟶ G' := whiskerLeft _ (whiskerRight α _)

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), Final (α.app X)
sC : C ≌ AsSmall C := AsSmall.equiv
F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor
G' : AsSmall C ⥤ Cat := sC.inverse ⋙ G ⋙ Cat.asSmallFunctor
α' : F' ⟶ G' := whiskerLeft sC.inverse (whiskerRight α Cat.asSmallFunctor)
⊢ (map α).Final
-- Mathlib/Tactic/Module.lean
theorem eq_cons_cons [AddMonoid M] [SMul R M] {r₁ r₂ : R} (m : M) {l₁ l₂ : NF R M} (h1 : r₁ = r₂)
    (h2 : l₁.eval = l₂.eval) :
    ((r₁, m) ::ᵣ l₁).eval = ((r₂, m) ::ᵣ l₂).eval

Proof state:
R : Type u_2
M : Type u_3
inst✝¹ : AddMonoid M
inst✝ : SMul R M
r₁ r₂ : R
m : M
l₁ l₂ : NF R M
h1 : r₁ = r₂
h2 : l₁.eval = l₂.eval
⊢ ((r₁, m) ::ᵣ l₁).eval = ((r₂, m) ::ᵣ l₂).eval

Tactic:
simp only [NF.eval, NF.cons] at *

Result:
R : Type u_2
M : Type u_3
inst✝¹ : AddMonoid M
inst✝ : SMul R M
r₁ r₂ : R
m : M
l₁ l₂ : NF R M
h1 : r₁ = r₂
h2 : (map (fun x => x.1 • x.2) l₁).sum = (map (fun x => x.1 • x.2) l₂).sum
⊢ (map (fun x => x.1 • x.2) ((r₁, m) :: l₁)).sum = (map (fun x => x.1 • x.2) ((r₂, m) :: l₂)).sum

Proof state:
R : Type u_2
M : Type u_3
inst✝¹ : AddMonoid M
inst✝ : SMul R M
r₁ r₂ : R
m : M
l₁ l₂ : NF R M
h1 : r₁ = r₂
h2 : (map (fun x => x.1 • x.2) l₁).sum = (map (fun x => x.1 • x.2) l₂).sum
⊢ (map (fun x => x.1 • x.2) ((r₁, m) :: l₁)).sum = (map (fun x => x.1 • x.2) ((r₂, m) :: l₂)).sum

Tactic:
simp [h1, h2]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem mul_twoPow_eq_shiftLeft (x : BitVec w) (i : Nat) :
    x * (twoPow w i) = x <<< i

Proof state:
w : Nat
x : BitVec w
i : Nat
hi : ¬i < w
⊢ 2 ^ i % 2 ^ w = 0

Tactic:
rw [Nat.mod_eq_zero_of_dvd]

Result:
w : Nat
x : BitVec w
i : Nat
hi : ¬i < w
⊢ 2 ^ w ∣ 2 ^ i

Proof state:
w : Nat
x : BitVec w
i : Nat
hi : i < w
⊢ i < w

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
i : Nat
hi : ¬i < w
⊢ w ≤ i

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
i : Nat
hi : ¬i < w
⊢ 2 ^ w ∣ 2 ^ i

Tactic:
apply Nat.pow_dvd_pow 2 (by omega)

Result:
no goals

Proof state:
case neg
w : Nat
x : BitVec w
i : Nat
hi : ¬i < w
⊢ x.toNat * (2 ^ i % 2 ^ w) % 2 ^ w = x.toNat * 2 ^ i % 2 ^ w

Tactic:
have hpow : 2 ^ i % 2 ^ w = 0 := by
  rw [Nat.mod_eq_zero_of_dvd]
  apply Nat.pow_dvd_pow 2 (by omega)

Result:
case neg
w : Nat
x : BitVec w
i : Nat
hi : ¬i < w
hpow : 2 ^ i % 2 ^ w = 0
⊢ x.toNat * (2 ^ i % 2 ^ w) % 2 ^ w = x.toNat * 2 ^ i % 2 ^ w

Proof state:
case neg
w : Nat
x : BitVec w
i : Nat
hi : ¬i < w
hpow : 2 ^ i % 2 ^ w = 0
⊢ x.toNat * (2 ^ i % 2 ^ w) % 2 ^ w = x.toNat * 2 ^ i % 2 ^ w

Tactic:
simp [Nat.mul_mod, hpow]

Result:
no goals

Proof state:
case a
w : Nat
x : BitVec w
i : Nat
⊢ (x * twoPow w i).toNat = (x <<< i).toNat

Tactic:
simp only [toNat_mul, toNat_twoPow, toNat_shiftLeft, Nat.shiftLeft_eq]

Result:
case a
w : Nat
x : BitVec w
i : Nat
⊢ x.toNat * (2 ^ i % 2 ^ w) % 2 ^ w = x.toNat * 2 ^ i % 2 ^ w

Proof state:
case a
w : Nat
x : BitVec w
i : Nat
⊢ x.toNat * (2 ^ i % 2 ^ w) % 2 ^ w = x.toNat * 2 ^ i % 2 ^ w

Tactic:
by_cases hi : i < w

Result:
case pos
w : Nat
x : BitVec w
i : Nat
hi : i < w
⊢ x.toNat * (2 ^ i % 2 ^ w) % 2 ^ w = x.toNat * 2 ^ i % 2 ^ w

case neg
w : Nat
x : BitVec w
i : Nat
hi : ¬i < w
⊢ x.toNat * (2 ^ i % 2 ^ w) % 2 ^ w = x.toNat * 2 ^ i % 2 ^ w

Proof state:
w : Nat
x : BitVec w
i : Nat
⊢ x * twoPow w i = x <<< i

Tactic:
apply eq_of_toNat_eq

Result:
case a
w : Nat
x : BitVec w
i : Nat
⊢ (x * twoPow w i).toNat = (x <<< i).toNat

Proof state:
case pos
w : Nat
x : BitVec w
i : Nat
hi : i < w
hpow : 2 ^ i < 2 ^ w
⊢ x.toNat * (2 ^ i % 2 ^ w) % 2 ^ w = x.toNat * 2 ^ i % 2 ^ w

Tactic:
rw [Nat.mod_eq_of_lt hpow]

Result:
no goals

Proof state:
case pos
w : Nat
x : BitVec w
i : Nat
hi : i < w
⊢ x.toNat * (2 ^ i % 2 ^ w) % 2 ^ w = x.toNat * 2 ^ i % 2 ^ w

Tactic:
have hpow : 2^i < 2^w := Nat.pow_lt_pow_of_lt (by omega) (by omega)

Result:
case pos
w : Nat
x : BitVec w
i : Nat
hi : i < w
hpow : 2 ^ i < 2 ^ w
⊢ x.toNat * (2 ^ i % 2 ^ w) % 2 ^ w = x.toNat * 2 ^ i % 2 ^ w

Proof state:
w : Nat
x : BitVec w
i : Nat
hi : i < w
⊢ 1 < 2

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem Bool.and_eq_true (a b : Bool) : ((a && b) = true) = (a = true ∧ b = true)

Proof state:
a b : Bool
⊢ ((a && b) = true) = (a = true ∧ b = true)

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

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean
theorem hasEigenvalue_of_isRoot (h : (minpoly K f).IsRoot μ) : f.HasEigenvalue μ

Proof state:
case intro.intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : (minpoly K f).IsRoot μ
p : K[X]
hp : minpoly K f = (X - C μ) * p
con : LinearMap.ker (f - μ • 1) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - μ • 1
p_ne_0 : p ≠ 0
this : (aeval f) p = 0
h_deg : 1 + ↑p.natDegree ≤ ↑p.natDegree
⊢ False

Tactic:
norm_cast at h_deg

Result:
case intro.intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : (minpoly K f).IsRoot μ
p : K[X]
hp : minpoly K f = (X - C μ) * p
con : LinearMap.ker (f - μ • 1) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - μ • 1
p_ne_0 : p ≠ 0
this : (aeval f) p = 0
h_deg : 1 + p.natDegree ≤ p.natDegree
⊢ False

Proof state:
case intro.intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : (minpoly K f).IsRoot μ
p : K[X]
hp : minpoly K f = (X - C μ) * p
con : LinearMap.ker (f - μ • 1) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - μ • 1
p_ne_0 : p ≠ 0
this : (aeval f) p = 0
h_deg : (minpoly K f).degree ≤ p.degree
⊢ False

Tactic:
rw [hp, degree_mul, degree_X_sub_C, Polynomial.degree_eq_natDegree p_ne_0] at h_deg

Result:
case intro.intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : (minpoly K f).IsRoot μ
p : K[X]
hp : minpoly K f = (X - C μ) * p
con : LinearMap.ker (f - μ • 1) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - μ • 1
p_ne_0 : p ≠ 0
this : (aeval f) p = 0
h_deg : 1 + ↑p.natDegree ≤ ↑p.natDegree
⊢ False

Proof state:
case intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : (minpoly K f).IsRoot μ
p : K[X]
hp : minpoly K f = (X - C μ) * p
⊢ f.HasEigenvalue μ

Tactic:
rw [hasEigenvalue_iff, eigenspace_def]

Result:
case intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : (minpoly K f).IsRoot μ
p : K[X]
hp : minpoly K f = (X - C μ) * p
⊢ LinearMap.ker (f - μ • 1) ≠ ⊥

Proof state:
case intro.intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : (minpoly K f).IsRoot μ
p : K[X]
hp : minpoly K f = (X - C μ) * p
con : LinearMap.ker (f - μ • 1) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - μ • 1
p_ne_0 : p ≠ 0
this : (aeval f) p = 0
h_deg : 1 + p.natDegree ≤ p.natDegree
⊢ False

Tactic:
omega

Result:
no goals
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
theorem mem_skewAdjointSubmodule (f : Module.End R M) :
    f ∈ B.skewAdjointSubmodule ↔ B.IsSkewAdjoint f

Proof state:
R : Type u_1
M : Type u_5
M₂ : Type u_7
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
B : M →ₗ[R] M →ₗ[R] M₂
f : Module.End R M
⊢ f ∈ B.skewAdjointSubmodule ↔ (-B).IsAdjointPair B ⇑f ⇑f

Tactic:
exact Iff.rfl

Result:
no goals

Proof state:
R : Type u_1
M : Type u_5
M₂ : Type u_7
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
B : M →ₗ[R] M →ₗ[R] M₂
f : Module.End R M
⊢ f ∈ B.skewAdjointSubmodule ↔ B.IsSkewAdjoint ⇑f

Tactic:
rw [isSkewAdjoint_iff_neg_self_adjoint]

Result:
R : Type u_1
M : Type u_5
M₂ : Type u_7
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
B : M →ₗ[R] M →ₗ[R] M₂
f : Module.End R M
⊢ f ∈ B.skewAdjointSubmodule ↔ (-B).IsAdjointPair B ⇑f ⇑f
-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem principal_one_iff : Principal op 1 ↔ op 0 0 = 0

Proof state:
case refine_1
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
h : Principal op 1
⊢ op 0 0 = 0

Tactic:
rw [← lt_one_iff_zero]

Result:
case refine_1
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
h : Principal op 1
⊢ op 0 0 < 1

Proof state:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
⊢ Principal op 1 ↔ op 0 0 = 0

Tactic:
refine ⟨fun h => ?_, fun h a b ha hb => ?_⟩

Result:
case refine_1
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
h : Principal op 1
⊢ op 0 0 = 0

case refine_2
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
h : op 0 0 = 0
a b : Ordinal.{u_1}
ha : a < 1
hb : b < 1
⊢ op a b < 1

Proof state:
case refine_2
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
h : op 0 0 = 0
a b : Ordinal.{u_1}
ha : a < 1
hb : b < 1
⊢ op a b < 1

Tactic:
rwa [lt_one_iff_zero, ha, hb] at *

Result:
no goals

Proof state:
case refine_1
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
h : Principal op 1
⊢ op 0 0 < 1

Tactic:
exact h zero_lt_one zero_lt_one

Result:
no goals
-- Mathlib/Data/Finset/Range.lean
lemma range_nontrivial {n : ℕ} (hn : 1 < n) : (Finset.range n).Nontrivial

Proof state:
n : ℕ
hn : 1 < n
⊢ (range n).Nontrivial

Tactic:
rw [Finset.Nontrivial, Finset.coe_range]

Result:
n : ℕ
hn : 1 < n
⊢ (Set.Iio n).Nontrivial

Proof state:
n : ℕ
hn : 1 < n
⊢ (Set.Iio n).Nontrivial

Tactic:
exact ⟨0, Nat.zero_lt_one.trans hn, 1, hn, Nat.zero_ne_one⟩

Result:
no goals
-- Mathlib/Data/TypeVec.lean
theorem diag_sub_val {n} {α : TypeVec.{u} n} : subtypeVal (repeatEq α) ⊚ diagSub = prod.diag

Proof state:
case a.h
n : ℕ
α : TypeVec.{u} n
i : Fin2 n
x : α i
⊢ (subtypeVal α.repeatEq ⊚ diagSub) i x = prod.diag i x

Tactic:
induction i with
| fz => simp only [comp, subtypeVal, repeatEq.eq_2, diagSub, prod.diag]
| fs _ i_ih => apply @i_ih (drop α)

Result:
no goals

Proof state:
case a.h.fz
n n✝ : ℕ
α : TypeVec.{u} (n✝ + 1)
x : α Fin2.fz
⊢ (subtypeVal α.repeatEq ⊚ diagSub) Fin2.fz x = prod.diag Fin2.fz x

Tactic:
simp only [comp, subtypeVal, repeatEq.eq_2, diagSub, prod.diag]

Result:
no goals

Proof state:
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec.{u} n✝} (x : α a✝), (subtypeVal α.repeatEq ⊚ diagSub) a✝ x = prod.diag a✝ x
α : TypeVec.{u} (n✝ + 1)
x : α a✝.fs
⊢ (subtypeVal α.repeatEq ⊚ diagSub) a✝.fs x = prod.diag a✝.fs x

Tactic:
apply @i_ih (drop α)

Result:
no goals

Proof state:
n : ℕ
α : TypeVec.{u} n
⊢ subtypeVal α.repeatEq ⊚ diagSub = prod.diag

Tactic:
ext i x

Result:
case a.h
n : ℕ
α : TypeVec.{u} n
i : Fin2 n
x : α i
⊢ (subtypeVal α.repeatEq ⊚ diagSub) i x = prod.diag i x
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem continuousOn_sub_left (a : ℝ≥0∞) : ContinuousOn (a - ·) { x : ℝ≥0∞ | x ≠ ∞ }

Proof state:
a : ℝ≥0∞
⊢ MapsTo (fun x => (a, x)) {x | x ≠ ⊤} {p | p ≠ (⊤, ⊤)}

Tactic:
rintro _ h (_ | _)

Result:
case refl
h : ⊤ ∈ {x | x ≠ ⊤}
⊢ False

Proof state:
a : ℝ≥0∞
⊢ (fun x => a - x) = (fun p => p.1 - p.2) ∘ fun x => (a, x)

Tactic:
rfl

Result:
no goals

Proof state:
case refl
h : ⊤ ∈ {x | x ≠ ⊤}
⊢ False

Tactic:
exact h none_eq_top

Result:
no goals

Proof state:
a : ℝ≥0∞
⊢ ContinuousOn (fun x => a - x) {x | x ≠ ⊤}

Tactic:
rw [show (fun x => a - x) = (fun p : ℝ≥0∞ × ℝ≥0∞ => p.fst - p.snd) ∘ fun x => ⟨a, x⟩ by rfl]

Result:
a : ℝ≥0∞
⊢ ContinuousOn ((fun p => p.1 - p.2) ∘ fun x => (a, x)) {x | x ≠ ⊤}

Proof state:
a : ℝ≥0∞
⊢ ContinuousOn ((fun p => p.1 - p.2) ∘ fun x => (a, x)) {x | x ≠ ⊤}

Tactic:
apply continuousOn_sub.comp (by fun_prop)

Result:
a : ℝ≥0∞
⊢ MapsTo (fun x => (a, x)) {x | x ≠ ⊤} {p | p ≠ (⊤, ⊤)}

Proof state:
a : ℝ≥0∞
⊢ ContinuousOn (fun x => (a, x)) {x | x ≠ ⊤}

Tactic:
fun_prop

Result:
no goals
-- Mathlib/Topology/Basic.lean
lemma isOpen_iff_of_cover {f : α → Set X} (ho : ∀ i, IsOpen (f i)) (hU : (⋃ i, f i) = univ) :
    IsOpen s ↔ ∀ i, IsOpen (f i ∩ s)

Proof state:
X : Type u
α : Type u_1
s : Set X
inst✝ : TopologicalSpace X
f : α → Set X
ho : ∀ (i : α), IsOpen (f i)
hU : ⋃ i, f i = univ
h : ∀ (i : α), IsOpen (f i ∩ s)
⊢ IsOpen (⋃ i, f i ∩ s)

Tactic:
exact isOpen_iUnion fun i ↦ h i

Result:
no goals

Proof state:
X : Type u
α : Type u_1
s : Set X
inst✝ : TopologicalSpace X
f : α → Set X
ho : ∀ (i : α), IsOpen (f i)
hU : ⋃ i, f i = univ
⊢ IsOpen s ↔ ∀ (i : α), IsOpen (f i ∩ s)

Tactic:
refine ⟨fun h i ↦ (ho i).inter h, fun h ↦ ?_⟩

Result:
X : Type u
α : Type u_1
s : Set X
inst✝ : TopologicalSpace X
f : α → Set X
ho : ∀ (i : α), IsOpen (f i)
hU : ⋃ i, f i = univ
h : ∀ (i : α), IsOpen (f i ∩ s)
⊢ IsOpen s

Proof state:
X : Type u
α : Type u_1
s : Set X
inst✝ : TopologicalSpace X
f : α → Set X
ho : ∀ (i : α), IsOpen (f i)
hU : ⋃ i, f i = univ
h : ∀ (i : α), IsOpen (f i ∩ s)
⊢ IsOpen s

Tactic:
rw [← s.inter_univ, inter_comm, ← hU, iUnion_inter]

Result:
X : Type u
α : Type u_1
s : Set X
inst✝ : TopologicalSpace X
f : α → Set X
ho : ∀ (i : α), IsOpen (f i)
hU : ⋃ i, f i = univ
h : ∀ (i : α), IsOpen (f i ∩ s)
⊢ IsOpen (⋃ i, f i ∩ s)
-- Mathlib/RingTheory/PrincipalIdealDomain.lean
theorem IsBezout.span_gcd_eq_span_gcd (x y : R) :
    span {GCDMonoid.gcd x y} = span {IsBezout.gcd x y}

Proof state:
R : Type u
inst✝³ : CommRing R
inst✝² : IsBezout R
inst✝¹ : IsDomain R
inst✝ : GCDMonoid R
x y : R
⊢ Associated (GCDMonoid.gcd x y) (gcd x y)

Tactic:
exact associated_of_dvd_dvd
  (IsBezout.dvd_gcd (GCDMonoid.gcd_dvd_left _ _) <| GCDMonoid.gcd_dvd_right _ _)
  (GCDMonoid.dvd_gcd (IsBezout.gcd_dvd_left _ _) <| IsBezout.gcd_dvd_right _ _)

Result:
no goals

Proof state:
R : Type u
inst✝³ : CommRing R
inst✝² : IsBezout R
inst✝¹ : IsDomain R
inst✝ : GCDMonoid R
x y : R
⊢ Ideal.span {GCDMonoid.gcd x y} = Ideal.span {gcd x y}

Tactic:
rw [Ideal.span_singleton_eq_span_singleton]

Result:
R : Type u
inst✝³ : CommRing R
inst✝² : IsBezout R
inst✝¹ : IsDomain R
inst✝ : GCDMonoid R
x y : R
⊢ Associated (GCDMonoid.gcd x y) (gcd x y)
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem fromEdgeSet_univ : fromEdgeSet (Set.univ : Set (Sym2 V)) = ⊤

Proof state:
V : Type u
⊢ fromEdgeSet Set.univ = ⊤

Tactic:
ext v w

Result:
case Adj.h.h.a
V : Type u
v w : V
⊢ (fromEdgeSet Set.univ).Adj v w ↔ ⊤.Adj v w

Proof state:
case Adj.h.h.a
V : Type u
v w : V
⊢ (fromEdgeSet Set.univ).Adj v w ↔ ⊤.Adj v w

Tactic:
simp only [fromEdgeSet_adj, Set.mem_univ, true_and, top_adj]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RefVecOperator/Zip.lean
theorem go_get_aux {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefVec aig curr)
    (lhs rhs : RefVec aig len) (f : (aig : AIG α) → BinaryInput aig → Entrypoint α)
    [LawfulOperator α BinaryInput f] [chainable : LawfulZipOperator α f] :
    -- The hfoo here is a trick to make the dependent type gods happy
    ∀ (idx : Nat) (hidx : idx < curr) (hfoo),
      (go aig curr s hcurr lhs rhs f).vec.get idx (by omega)
        =
      (s.get idx hidx).cast hfoo

Proof state:
case isFalse
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
len : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
lhs rhs : aig.RefVec len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
idx : Nat
hidx : idx < curr
res : RefVecEntry α len
h✝ : ¬curr < len
hgo : { aig := aig, vec := ⋯ ▸ s } = res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.vec.get idx ⋯ = (s.get idx hidx).cast hfoo

Tactic:
rw [← hgo]

Result:
case isFalse
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
len : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
lhs rhs : aig.RefVec len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
idx : Nat
hidx : idx < curr
res : RefVecEntry α len
h✝ : ¬curr < len
hgo : { aig := aig, vec := ⋯ ▸ s } = res
⊢ ∀ (hfoo : aig.decls.size ≤ { aig := aig, vec := ⋯ ▸ s }.aig.decls.size),
    { aig := aig, vec := ⋯ ▸ s }.vec.get idx ⋯ = (s.get idx hidx).cast hfoo

Proof state:
case isFalse
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
aig : AIG α
curr : Nat
s : aig.RefVec curr
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
idx : Nat
hidx : idx < curr
hcurr : curr ≤ curr
lhs rhs : aig.RefVec curr
res : RefVecEntry α curr
h✝ : ¬curr < curr
hgo : { aig := aig, vec := ⋯ ▸ s } = res
⊢ (⋯ ▸ s).refs[idx] = s.refs[idx]

Tactic:
simp

Result:
no goals