harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Monadic.lean
theorem SatisfiesM_anyM_iff_exists [Monad m] [LawfulMonad m]
    (p : α → m Bool) (as : Array α) (start stop) (q : Fin as.size → Prop)
    (hp : ∀ i : Fin as.size, start ≤ i.1 → i.1 < stop → SatisfiesM (· = true ↔ q i) (p as[i])) :
    SatisfiesM
      (fun res => res = true ↔ ∃ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop ∧ q i)
      (anyM p as start stop)

Proof state:
case inr
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
start stop : Nat
q : Fin as.size → Prop
hp : ∀ (i : Fin as.size), start ≤ ↑i → ↑i < stop → SatisfiesM (fun x => x = true ↔ q i) (p as[i])
hstart : min stop as.size ≤ start
j : Fin as.size
h₁ : start ≤ ↑j
h₂ : ↑j < stop
⊢ ¬q j

Tactic:
cases Nat.not_lt.2 (Nat.le_trans hstart h₁) (Nat.lt_min.2 ⟨h₂, j.2⟩)

Result:
no goals

Proof state:
case inl.refine_1
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
start stop : Nat
q : Fin as.size → Prop
hp : ∀ (i : Fin as.size), start ≤ ↑i → ↑i < stop → SatisfiesM (fun x => x = true ↔ q i) (p as[i])
hstart : start ≤ min stop as.size
⊢ (fun j => start ≤ j ∧ ¬∃ i, start ≤ ↑i ∧ ↑i < j ∧ q i) start

Tactic:
exact ⟨Nat.le_refl _, fun ⟨i, h₁, h₂, _⟩ => (Nat.not_le_of_gt h₂ h₁).elim⟩

Result:
no goals

Proof state:
case inl.refine_2.h_1
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
start stop : Nat
q : Fin as.size → Prop
hp : ∀ (i : Fin as.size), start ≤ ↑i → ↑i < stop → SatisfiesM (fun x => x = true ↔ q i) (p as[i])
hstart : start ≤ min stop as.size
i : Fin as.size
h₂ : ↑i < stop
x✝ : (fun j => start ≤ j ∧ ¬∃ i, start ≤ ↑i ∧ ↑i < j ∧ q i) ↑i
h₁ : start ≤ ↑i
h₃ : ¬∃ i_1, start ≤ ↑i_1 ∧ ↑i_1 < ↑i ∧ q i_1
c✝ : Bool
hq : q i
⊢ ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q i

Tactic:
exact ⟨_, h₁, h₂, hq⟩

Result:
no goals

Proof state:
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
start stop : Nat
q : Fin as.size → Prop
hp : ∀ (i : Fin as.size), start ≤ ↑i → ↑i < stop → SatisfiesM (fun x => x = true ↔ q i) (p as[i])
hstart : start ≤ min stop as.size
x✝¹ : Bool
x✝ :
  bif x✝¹ then ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q i
  else start ≤ min stop as.size ∧ ¬∃ i, start ≤ ↑i ∧ ↑i < min stop as.size ∧ q i
h :
  bif true then ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q i
  else start ≤ min stop as.size ∧ ¬∃ i, start ≤ ↑i ∧ ↑i < min stop as.size ∧ q i
⊢ true = true ↔ ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q i

Tactic:
simp only [true_iff]

Result:
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : Array α
start stop : Nat
q : Fin as.size → Prop
hp : ∀ (i : Fin as.size), start ≤ ↑i → ↑i < stop → SatisfiesM (fun x => x = true ↔ q i) (p as[i])
hstart : start ≤ min stop as.size
x✝¹ : Bool
x✝ :
  bif x✝¹ then ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q i
  else start ≤ min stop as.size ∧ ¬∃ i, start ≤ ↑i ∧ ↑i < min stop as.size ∧ q i
h :
  bif true then ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q i
  else start ≤ min stop as.size ∧ ¬∃ i, start ≤ ↑i ∧ ↑i < min stop as.size ∧ q i
⊢ ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q i
-- Mathlib/RingTheory/Smooth/Basic.lean
theorem of_equiv [FormallySmooth R A] (e : A ≃ₐ[R] B) : FormallySmooth R B

Proof state:
case comp_surjective
R : Type u
inst✝⁷ : CommSemiring R
A B : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : FormallySmooth R A
e : A ≃ₐ[R] B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f : B →ₐ[R] C ⧸ I
⊢ ∃ a, (Ideal.Quotient.mkₐ R I).comp a = f

Tactic:
use (FormallySmooth.lift I ⟨2, hI⟩ (f.comp e : A →ₐ[R] C ⧸ I)).comp e.symm

Result:
case h
R : Type u
inst✝⁷ : CommSemiring R
A B : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : FormallySmooth R A
e : A ≃ₐ[R] B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f : B →ₐ[R] C ⧸ I
⊢ (Ideal.Quotient.mkₐ R I).comp ((lift I ⋯ (f.comp ↑e)).comp ↑e.symm) = f

Proof state:
case h
R : Type u
inst✝⁷ : CommSemiring R
A B : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : FormallySmooth R A
e : A ≃ₐ[R] B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f : B →ₐ[R] C ⧸ I
⊢ (Ideal.Quotient.mkₐ R I).comp ((lift I ⋯ (f.comp ↑e)).comp ↑e.symm) = f

Tactic:
rw [← AlgHom.comp_assoc, FormallySmooth.comp_lift, AlgHom.comp_assoc, AlgEquiv.comp_symm,
  AlgHom.comp_id]

Result:
no goals

Proof state:
case comp_surjective
R : Type u
inst✝⁵ : CommSemiring R
A B : Type u
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : FormallySmooth R A
e : A ≃ₐ[R] B
⊢ ∀ ⦃B_1 : Type u⦄ [inst : CommRing B_1] [inst_1 : Algebra R B_1] (I : Ideal B_1),
    I ^ 2 = ⊥ → Function.Surjective (Ideal.Quotient.mkₐ R I).comp

Tactic:
intro C _ _ I hI f

Result:
case comp_surjective
R : Type u
inst✝⁷ : CommSemiring R
A B : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : FormallySmooth R A
e : A ≃ₐ[R] B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f : B →ₐ[R] C ⧸ I
⊢ ∃ a, (Ideal.Quotient.mkₐ R I).comp a = f

Proof state:
R : Type u
inst✝⁵ : CommSemiring R
A B : Type u
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : FormallySmooth R A
e : A ≃ₐ[R] B
⊢ FormallySmooth R B

Tactic:
constructor

Result:
case comp_surjective
R : Type u
inst✝⁵ : CommSemiring R
A B : Type u
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : FormallySmooth R A
e : A ≃ₐ[R] B
⊢ ∀ ⦃B_1 : Type u⦄ [inst : CommRing B_1] [inst_1 : Algebra R B_1] (I : Ideal B_1),
    I ^ 2 = ⊥ → Function.Surjective (Ideal.Quotient.mkₐ R I).comp
-- Mathlib/CategoryTheory/ComposableArrows.lean
lemma mk₅_surjective (X : ComposableArrows C 5) :
    ∃ (X₀ X₁ X₂ X₃ X₄ X₅ : C) (f₀ : X₀ ⟶ X₁) (f₁ : X₁ ⟶ X₂) (f₂ : X₂ ⟶ X₃)
      (f₃ : X₃ ⟶ X₄) (f₄ : X₄ ⟶ X₅), X = mk₅ f₀ f₁ f₂ f₃ f₄ :=
  ⟨_, _, _, _, _, _, X.map' 0 1, X.map' 1 2, X.map' 2 3, X.map' 3 4, X.map' 4 5,
    ext₅ rfl rfl rfl rfl rfl rfl (by simp) (by simp) (by simp) (by simp) (by simp)⟩

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : ComposableArrows C 5
⊢ X.map' 2 3 ⋯ ⋯ =
    eqToHom ⋯ ≫
      (mk₅ (X.map' 0 1 ⋯ ⋯) (X.map' 1 2 ⋯ ⋯) (X.map' 2 3 ⋯ ⋯) (X.map' 3 4 ⋯ ⋯) (X.map' 4 5 ⋯ ⋯)).map' 2 3 ⋯ ⋯ ≫
        eqToHom ⋯

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : ComposableArrows C 5
⊢ X.map' 0 1 ⋯ ⋯ =
    eqToHom ⋯ ≫
      (mk₅ (X.map' 0 1 ⋯ ⋯) (X.map' 1 2 ⋯ ⋯) (X.map' 2 3 ⋯ ⋯) (X.map' 3 4 ⋯ ⋯) (X.map' 4 5 ⋯ ⋯)).map' 0 1 ⋯ ⋯ ≫
        eqToHom ⋯

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : ComposableArrows C 5
⊢ X.map' 1 2 ⋯ ⋯ =
    eqToHom ⋯ ≫
      (mk₅ (X.map' 0 1 ⋯ ⋯) (X.map' 1 2 ⋯ ⋯) (X.map' 2 3 ⋯ ⋯) (X.map' 3 4 ⋯ ⋯) (X.map' 4 5 ⋯ ⋯)).map' 1 2 ⋯ ⋯ ≫
        eqToHom ⋯

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : ComposableArrows C 5
⊢ X.map' 4 5 ⋯ ⋯ =
    eqToHom ⋯ ≫
      (mk₅ (X.map' 0 1 ⋯ ⋯) (X.map' 1 2 ⋯ ⋯) (X.map' 2 3 ⋯ ⋯) (X.map' 3 4 ⋯ ⋯) (X.map' 4 5 ⋯ ⋯)).map' 4 5 ⋯ ⋯ ≫
        eqToHom ⋯

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : ComposableArrows C 5
⊢ X.map' 3 4 ⋯ ⋯ =
    eqToHom ⋯ ≫
      (mk₅ (X.map' 0 1 ⋯ ⋯) (X.map' 1 2 ⋯ ⋯) (X.map' 2 3 ⋯ ⋯) (X.map' 3 4 ⋯ ⋯) (X.map' 4 5 ⋯ ⋯)).map' 3 4 ⋯ ⋯ ≫
        eqToHom ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
lemma coverEntropyInf_eq_coverEntropy (T : X → X) {F : Set X} (h : MapsTo T F F) :
    coverEntropyInf T F = coverEntropy T F

Proof state:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
h : MapsTo T F F
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ coverEntropyEntourage T F U ≤ coverEntropyInf T F

Tactic:
rcases comp_symm_mem_uniformity_sets U_uni with ⟨V, V_uni, V_symm, V_U⟩

Result:
case intro.intro.intro
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
h : MapsTo T F F
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SymmetricRel V
V_U : V ○ V ⊆ U
⊢ coverEntropyEntourage T F U ≤ coverEntropyInf T F

Proof state:
case intro.intro.intro
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
h : MapsTo T F F
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_symm : SymmetricRel V
V_U : V ○ V ⊆ U
⊢ coverEntropyEntourage T F U ≤ coverEntropyInf T F

Tactic:
exact (coverEntropyEntourage_antitone T F V_U).trans
  (le_iSup₂_of_le V V_uni (coverEntropyEntourage_le_coverEntropyInfEntourage h V_symm))

Result:
no goals

Proof state:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
h : MapsTo T F F
⊢ coverEntropyInf T F = coverEntropy T F

Tactic:
refine le_antisymm (coverEntropyInf_le_coverEntropy T F) (iSup₂_le fun U U_uni ↦ ?_)

Result:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
h : MapsTo T F F
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ coverEntropyEntourage T F U ≤ coverEntropyInf T F
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem finrank_span_finset_eq_card {s : Finset M} (hs : LinearIndepOn R id (s : Set M)) :
    finrank R (span R (s : Set M)) = s.card

Proof state:
case h.e'_3.h.e'_2.h
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
s : Finset M
hs : LinearIndepOn R id ↑s
a✝ : M
⊢ a✝ ∈ s ↔ a✝ ∈ (↑s).toFinset

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_3.h.e'_2
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
s : Finset M
hs : LinearIndepOn R id ↑s
⊢ s = (↑s).toFinset

Tactic:
ext

Result:
case h.e'_3.h.e'_2.h
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
s : Finset M
hs : LinearIndepOn R id ↑s
a✝ : M
⊢ a✝ ∈ s ↔ a✝ ∈ (↑s).toFinset

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
s : Finset M
hs : LinearIndepOn R id ↑s
⊢ finrank R ↥(span R ↑s) = s.card

Tactic:
convert finrank_span_set_eq_card (s := (s : Set M)) hs

Result:
case h.e'_3.h.e'_2
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
s : Finset M
hs : LinearIndepOn R id ↑s
⊢ s = (↑s).toFinset
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem roots_degree_eq_one (h : degree p = 1) : p.roots = {-((p.coeff 1)⁻¹ * p.coeff 0)}

Proof state:
R : Type u
inst✝ : Field R
p : R[X]
h : p.degree = 1
⊢ p.roots = {-((p.coeff 1)⁻¹ * p.coeff 0)}

Tactic:
rw [eq_X_add_C_of_degree_le_one (show degree p ≤ 1 by rw [h])]

Result:
R : Type u
inst✝ : Field R
p : R[X]
h : p.degree = 1
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).roots =
    {-(((C (p.coeff 1) * X + C (p.coeff 0)).coeff 1)⁻¹ * (C (p.coeff 1) * X + C (p.coeff 0)).coeff 0)}

Proof state:
R : Type u
inst✝ : Field R
p : R[X]
h : p.degree = 1
this : p.coeff 1 ≠ 0
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).roots =
    {-(((C (p.coeff 1) * X + C (p.coeff 0)).coeff 1)⁻¹ * (C (p.coeff 1) * X + C (p.coeff 0)).coeff 0)}

Tactic:
simp [roots_C_mul_X_add_C _ this]

Result:
no goals

Proof state:
R : Type u
inst✝ : Field R
p : R[X]
h : p.degree = 1
⊢ p.degree ≤ 1

Tactic:
rw [h]

Result:
no goals

Proof state:
R : Type u
inst✝ : Field R
p : R[X]
h : p.degree = 1
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).roots =
    {-(((C (p.coeff 1) * X + C (p.coeff 0)).coeff 1)⁻¹ * (C (p.coeff 1) * X + C (p.coeff 0)).coeff 0)}

Tactic:
have : p.coeff 1 ≠ 0 := coeff_ne_zero_of_eq_degree h

Result:
R : Type u
inst✝ : Field R
p : R[X]
h : p.degree = 1
this : p.coeff 1 ≠ 0
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).roots =
    {-(((C (p.coeff 1) * X + C (p.coeff 0)).coeff 1)⁻¹ * (C (p.coeff 1) * X + C (p.coeff 0)).coeff 0)}
-- Mathlib/LinearAlgebra/Dual.lean
theorem toDual_injective : Injective b.toDual := fun x y h ↦ b.ext_elem_iff.mpr fun i ↦ by
  simp_rw [← toDual_eq_repr]; exact DFunLike.congr_fun h _

Proof state:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
x y : M
h : b.toDual x = b.toDual y
i : ι
⊢ (b.repr x) i = (b.repr y) i

Tactic:
simp_rw [← toDual_eq_repr]

Result:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
x y : M
h : b.toDual x = b.toDual y
i : ι
⊢ (b.toDual x) (b i) = (b.toDual y) (b i)

Proof state:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
x y : M
h : b.toDual x = b.toDual y
i : ι
⊢ (b.toDual x) (b i) = (b.toDual y) (b i)

Tactic:
exact DFunLike.congr_fun h _

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Length.lean
theorem length_simple (i : B) : ℓ (s i) = 1

Proof state:
case h₂
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
length_lt_one : cs.length (cs.simple i) < 1
this✝ : cs.lengthParity (cs.simple i) = Multiplicative.ofAdd 0
this : Multiplicative.ofAdd 0 = Multiplicative.ofAdd 1
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
case h₂
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
length_lt_one : cs.length (cs.simple i) < 1
⊢ False

Tactic:
have : cs.lengthParity (s i) = Multiplicative.ofAdd 0 := by
  rw [lengthParity_eq_ofAdd_length, Nat.lt_one_iff.mp length_lt_one, Nat.cast_zero]

Result:
case h₂
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
length_lt_one : cs.length (cs.simple i) < 1
this : cs.lengthParity (cs.simple i) = Multiplicative.ofAdd 0
⊢ False

Proof state:
case h₂
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ 1 ≤ cs.length (cs.simple i)

Tactic:
by_contra! length_lt_one

Result:
case h₂
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
length_lt_one : cs.length (cs.simple i) < 1
⊢ False

Proof state:
case h₂
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
length_lt_one : cs.length (cs.simple i) < 1
this : cs.lengthParity (cs.simple i) = Multiplicative.ofAdd 0
⊢ False

Tactic:
have : Multiplicative.ofAdd (0 : ZMod 2) = Multiplicative.ofAdd 1 :=
  this.symm.trans (cs.lengthParity_simple i)

Result:
case h₂
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
length_lt_one : cs.length (cs.simple i) < 1
this✝ : cs.lengthParity (cs.simple i) = Multiplicative.ofAdd 0
this : Multiplicative.ofAdd 0 = Multiplicative.ofAdd 1
⊢ False

Proof state:
case h₁
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ cs.length (cs.simple i) ≤ 1

Tactic:
simpa using cs.length_wordProd_le [i]

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
length_lt_one : cs.length (cs.simple i) < 1
⊢ cs.lengthParity (cs.simple i) = Multiplicative.ofAdd 0

Tactic:
rw [lengthParity_eq_ofAdd_length, Nat.lt_one_iff.mp length_lt_one, Nat.cast_zero]

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ cs.length (cs.simple i) = 1

Tactic:
apply Nat.le_antisymm

Result:
case h₁
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ cs.length (cs.simple i) ≤ 1

case h₂
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ 1 ≤ cs.length (cs.simple i)
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem generateFrom_singleton (s : Set α) :
    generateFrom {s} = MeasurableSpace.comap (· ∈ s) ⊤

Proof state:
α : Type u_1
s : Set α
this : MeasurableSpace α := generateFrom {s}
⊢ generateFrom {s} = MeasurableSpace.comap (fun x => x ∈ s) ⊤

Tactic:
refine le_antisymm (generateFrom_le fun t ht => ⟨{True}, trivial, by simp [ht.symm]⟩) ?_

Result:
α : Type u_1
s : Set α
this : MeasurableSpace α := generateFrom {s}
⊢ MeasurableSpace.comap (fun x => x ∈ s) ⊤ ≤ generateFrom {s}

Proof state:
α : Type u_1
s : Set α
this : MeasurableSpace α := generateFrom {s}
⊢ MeasurableSpace.comap (fun x => x ∈ s) ⊤ ≤ generateFrom {s}

Tactic:
rintro _ ⟨u, -, rfl⟩

Result:
case intro.intro
α : Type u_1
s : Set α
this : MeasurableSpace α := generateFrom {s}
u : Set Prop
⊢ MeasurableSet ((fun x => x ∈ s) ⁻¹' u)

Proof state:
α : Type u_1
s : Set α
⊢ generateFrom {s} = MeasurableSpace.comap (fun x => x ∈ s) ⊤

Tactic:
letI : MeasurableSpace α := generateFrom {s}

Result:
α : Type u_1
s : Set α
this : MeasurableSpace α := generateFrom {s}
⊢ generateFrom {s} = MeasurableSpace.comap (fun x => x ∈ s) ⊤

Proof state:
α : Type u_1
s : Set α
⊢ generateFrom {s} = MeasurableSpace.comap (fun x => x ∈ s) ⊤

Tactic:
classical
letI : MeasurableSpace α := generateFrom {s}
refine le_antisymm (generateFrom_le fun t ht => ⟨{True}, trivial, by simp [ht.symm]⟩) ?_
rintro _ ⟨u, -, rfl⟩
exact (show MeasurableSet s from GenerateMeasurable.basic _ <| mem_singleton s).mem trivial

Result:
no goals

Proof state:
α : Type u_1
s : Set α
this : MeasurableSpace α := generateFrom {s}
t : Set α
ht : t ∈ {s}
⊢ (fun x => x ∈ s) ⁻¹' {True} = t

Tactic:
simp [ht.symm]

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
s : Set α
this : MeasurableSpace α := generateFrom {s}
u : Set Prop
⊢ MeasurableSet ((fun x => x ∈ s) ⁻¹' u)

Tactic:
exact (show MeasurableSet s from GenerateMeasurable.basic _ <| mem_singleton s).mem trivial

Result:
no goals
-- Mathlib/Order/Interval/Finset/Defs.lean
theorem map_subtype_embedding_Ioo (hp : ∀ ⦃a b x⦄, a ≤ x → x ≤ b → p a → p b → p x):
    (Ioo a b).map (Embedding.subtype p) = (Ioo a b : Finset α)

Proof state:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : x ∈ Ioo ↑a ↑b
⊢ p x

Tactic:
rw [mem_Ioo] at hx

Result:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : ↑a < x ∧ x < ↑b
⊢ p x

Proof state:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : ↑a < x ∧ x < ↑b
⊢ p x

Tactic:
exact hp hx.1.le hx.2.le a.prop b.prop

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Ioo a b) = Ioo ↑a ↑b

Tactic:
rw [subtype_Ioo_eq]

Result:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Ioo ↑a ↑b)) = Ioo ↑a ↑b

Proof state:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Ioo ↑a ↑b)) = Ioo ↑a ↑b

Tactic:
refine Finset.subtype_map_of_mem fun x hx => ?_

Result:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : x ∈ Ioo ↑a ↑b
⊢ p x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem extract_zipWith : (zipWith f l l').extract m n = zipWith f (l.extract m n) (l'.extract m n)

Proof state:
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
n✝ : Nat
l : Vector α✝² n✝
l' : Vector α✝¹ n✝
m n : Nat
⊢ (zipWith f l l').extract m n = zipWith f (l.extract m n) (l'.extract m n)

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
m n : Nat
l : Array α✝²
l' : Vector α✝¹ l.size
⊢ (zipWith f { toArray := l, size_toArray := ⋯ } l').extract m n =
    zipWith f ({ toArray := l, size_toArray := ⋯ }.extract m n) (l'.extract m n)

Proof state:
case mk
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
m n : Nat
l : Array α✝²
l' : Vector α✝¹ l.size
⊢ (zipWith f { toArray := l, size_toArray := ⋯ } l').extract m n =
    zipWith f ({ toArray := l, size_toArray := ⋯ }.extract m n) (l'.extract m n)

Tactic:
rcases l' with ⟨l', h⟩

Result:
case mk.mk
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
m n : Nat
l : Array α✝²
l' : Array α✝¹
h : l'.size = l.size
⊢ (zipWith f { toArray := l, size_toArray := ⋯ } { toArray := l', size_toArray := h }).extract m n =
    zipWith f ({ toArray := l, size_toArray := ⋯ }.extract m n) ({ toArray := l', size_toArray := h }.extract m n)

Proof state:
case mk.mk
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
m n : Nat
l : Array α✝²
l' : Array α✝¹
h : l'.size = l.size
⊢ (zipWith f { toArray := l, size_toArray := ⋯ } { toArray := l', size_toArray := h }).extract m n =
    zipWith f ({ toArray := l, size_toArray := ⋯ }.extract m n) ({ toArray := l', size_toArray := h }.extract m n)

Tactic:
simp [Array.extract_zipWith]

Result:
no goals
-- Mathlib/Data/Rel.lean
theorem image_id (s : Set α) : image (@Eq α) s = s

Proof state:
case h
α : Type u_1
s : Set α
x : α
⊢ x ∈ image Eq s ↔ x ∈ s

Tactic:
simp [mem_image]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
⊢ image Eq s = s

Tactic:
ext x

Result:
case h
α : Type u_1
s : Set α
x : α
⊢ x ∈ image Eq s ↔ x ∈ s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem mul_one (x : BitVec w) : x * 1#w = x

Proof state:
case zero
x : BitVec 0
⊢ x * 1#0 = x

Tactic:
apply Subsingleton.elim

Result:
no goals

Proof state:
case succ
n✝ : Nat
x : BitVec (n✝ + 1)
⊢ x * 1#(n✝ + 1) = x

Tactic:
apply eq_of_toNat_eq

Result:
case succ.a
n✝ : Nat
x : BitVec (n✝ + 1)
⊢ (x * 1#(n✝ + 1)).toNat = x.toNat

Proof state:
case succ.a
n✝ : Nat
x : BitVec (n✝ + 1)
⊢ (x * 1#(n✝ + 1)).toNat = x.toNat

Tactic:
simp [Nat.mod_eq_of_lt]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ x * 1#w = x

Tactic:
cases w

Result:
case zero
x : BitVec 0
⊢ x * 1#0 = x

case succ
n✝ : Nat
x : BitVec (n✝ + 1)
⊢ x * 1#(n✝ + 1) = x
-- Mathlib/Data/Finsupp/Single.lean
theorem single_of_embDomain_single (l : α →₀ M) (f : α ↪ β) (a : β) (b : M) (hb : b ≠ 0)
    (h : l.embDomain f = single a b) : ∃ x, l = single x b ∧ f x = a

Proof state:
case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
l : α →₀ M
f : α ↪ β
a : β
b : M
hb : b ≠ 0
h : embDomain f l = single a b
h_map_support : map f l.support = {a}
ha : a ∈ map f l.support
c : α
_hc₁ : c ∈ l.support
hc₂ : f c = a
d : α
h_cases : c = d
⊢ (single a b) (f d) = (single c b) d

Tactic:
simp only [Eq.symm h_cases, hc₂, single_eq_same]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Sheafification.lean
theorem sheafifyMap_id (P : Cᵒᵖ ⥤ D) : sheafifyMap J (𝟙 P) = 𝟙 (sheafify J P)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
inst✝ : HasWeakSheafify J D
P : Cᵒᵖ ⥤ D
⊢ sheafifyMap J (𝟙 P) = 𝟙 (sheafify J P)

Tactic:
simp [sheafifyMap, sheafify]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem any_eq_false {p : α → Bool} {as : Array α} :
    as.any p = false ↔ ∀ (i : Nat) (_ : i < as.size), ¬p as[i]

Proof state:
α : Type u_1
p : α → Bool
as : Array α
⊢ as.any p = false ↔ ∀ (i : Nat) (x : i < as.size), ¬p as[i] = true

Tactic:
rw [Bool.eq_false_iff, Ne, any_eq_true]

Result:
α : Type u_1
p : α → Bool
as : Array α
⊢ (¬∃ i x, p as[i] = true) ↔ ∀ (i : Nat) (x : i < as.size), ¬p as[i] = true

Proof state:
α : Type u_1
p : α → Bool
as : Array α
⊢ (¬∃ i x, p as[i] = true) ↔ ∀ (i : Nat) (x : i < as.size), ¬p as[i] = true

Tactic:
simp

Result:
no goals