harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Localization/HomEquiv.lean
@[simp]
lemma homMap_map (f : X ⟶ Y) :
    Φ.homMap L₁ L₂ (L₁.map f) = L₂.map (Φ.functor.map f)

Proof state:
C₁ : Type u_2
C₂ : Type u_3
D₁ : Type u_5
D₂ : Type u_6
inst✝⁵ : Category.{u_8, u_2} C₁
inst✝⁴ : Category.{u_10, u_3} C₂
inst✝³ : Category.{u_11, u_5} D₁
inst✝² : Category.{u_9, u_6} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝¹ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝ : L₂.IsLocalization W₂
X Y : C₁
f : X ⟶ Y
⊢ (Φ.functor ⋙ L₂).map f ≫
      (CatCommSq.iso Φ.functor L₁ L₂ (Φ.localizedFunctor L₁ L₂)).hom.app Y ≫
        (CatCommSq.iso Φ.functor L₁ L₂ (Φ.localizedFunctor L₁ L₂)).inv.app Y =
    L₂.map (Φ.functor.map f)

Tactic:
simp

Result:
no goals

Proof state:
C₁ : Type u_2
C₂ : Type u_3
D₁ : Type u_5
D₂ : Type u_6
inst✝⁵ : Category.{u_8, u_2} C₁
inst✝⁴ : Category.{u_10, u_3} C₂
inst✝³ : Category.{u_11, u_5} D₁
inst✝² : Category.{u_9, u_6} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝¹ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝ : L₂.IsLocalization W₂
X Y : C₁
f : X ⟶ Y
⊢ Φ.homMap L₁ L₂ (L₁.map f) = L₂.map (Φ.functor.map f)

Tactic:
dsimp [homMap]

Result:
C₁ : Type u_2
C₂ : Type u_3
D₁ : Type u_5
D₂ : Type u_6
inst✝⁵ : Category.{u_8, u_2} C₁
inst✝⁴ : Category.{u_10, u_3} C₂
inst✝³ : Category.{u_11, u_5} D₁
inst✝² : Category.{u_9, u_6} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝¹ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝ : L₂.IsLocalization W₂
X Y : C₁
f : X ⟶ Y
⊢ (CatCommSq.iso Φ.functor L₁ L₂ (Φ.localizedFunctor L₁ L₂)).hom.app X ≫
      (Φ.localizedFunctor L₁ L₂).map (L₁.map f) ≫ (CatCommSq.iso Φ.functor L₁ L₂ (Φ.localizedFunctor L₁ L₂)).inv.app Y =
    L₂.map (Φ.functor.map f)

Proof state:
C₁ : Type u_2
C₂ : Type u_3
D₁ : Type u_5
D₂ : Type u_6
inst✝⁵ : Category.{u_8, u_2} C₁
inst✝⁴ : Category.{u_10, u_3} C₂
inst✝³ : Category.{u_11, u_5} D₁
inst✝² : Category.{u_9, u_6} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝¹ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝ : L₂.IsLocalization W₂
X Y : C₁
f : X ⟶ Y
⊢ (CatCommSq.iso Φ.functor L₁ L₂ (Φ.localizedFunctor L₁ L₂)).hom.app X ≫
      (Φ.localizedFunctor L₁ L₂).map (L₁.map f) ≫ (CatCommSq.iso Φ.functor L₁ L₂ (Φ.localizedFunctor L₁ L₂)).inv.app Y =
    L₂.map (Φ.functor.map f)

Tactic:
erw [← NatTrans.naturality_assoc]

Result:
C₁ : Type u_2
C₂ : Type u_3
D₁ : Type u_5
D₂ : Type u_6
inst✝⁵ : Category.{u_8, u_2} C₁
inst✝⁴ : Category.{u_10, u_3} C₂
inst✝³ : Category.{u_11, u_5} D₁
inst✝² : Category.{u_9, u_6} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝¹ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝ : L₂.IsLocalization W₂
X Y : C₁
f : X ⟶ Y
⊢ (Φ.functor ⋙ L₂).map f ≫
      (CatCommSq.iso Φ.functor L₁ L₂ (Φ.localizedFunctor L₁ L₂)).hom.app Y ≫
        (CatCommSq.iso Φ.functor L₁ L₂ (Φ.localizedFunctor L₁ L₂)).inv.app Y =
    L₂.map (Φ.functor.map f)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean
theorem go_get (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w)
    (curr : Nat) (hcurr : curr ≤ w) (s : AIG.RefVec aig curr) :
    ∀ (idx : Nat) (hidx : idx < curr),
        (go input distance curr hcurr s).get idx (by omega)
          =
        s.get idx hidx

Proof state:
case isTrue.isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
idx : Nat
hidx : idx < curr
h✝¹ : curr < w
h✝ : distance + curr < w
⊢ (let s := s.push (input.get (distance + curr) ⋯);
        go input distance (curr + 1) ⋯ s).get
      idx ⋯ =
    s.get idx hidx

case isTrue.isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
idx : Nat
hidx : idx < curr
h✝¹ : curr < w
h✝ : ¬distance + curr < w
⊢ (let s := s.push (input.get (w - 1) ⋯);
        go input distance (curr + 1) ⋯ s).get
      idx ⋯ =
    s.get idx hidx

Tactic:
all_goals
  rw [go_get]
  rw [AIG.RefVec.get_push_ref_lt]

Result:
no goals

Proof state:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
distance curr : Nat
s : aig.RefVec curr
idx : Nat
hidx : idx < curr
input : aig.RefVec curr
hcurr : curr ≤ curr
h✝ : ¬curr < curr
⊢ (⋯ ▸ s).get idx ⋯ = s.get idx hidx

Tactic:
simp

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
idx : Nat
hidx : idx < curr
h✝ : ¬curr < w
⊢ curr = w

Tactic:
omega

Result:
no goals

Proof state:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
idx : Nat
hidx : idx < curr
h✝ : ¬curr < w
⊢ (⋯ ▸ s).get idx ⋯ = s.get idx hidx

Tactic:
have : curr = w := by omega

Result:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
idx : Nat
hidx : idx < curr
h✝ : ¬curr < w
this : curr = w
⊢ (⋯ ▸ s).get idx ⋯ = s.get idx hidx
-- Mathlib/RepresentationTheory/Basic.lean
theorem smul_one_tprod_asModule (r : MonoidAlgebra k G) (x : V) (y : W) :
    -- Porting note: required to since Lean 4 doesn't unfold asModule
    let y' : ρW.asModule := y
    let z : (1 ⊗ ρW).asModule := x ⊗ₜ y
    r • z = x ⊗ₜ (r • y')

Proof state:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρW : Representation k G W
r : MonoidAlgebra k G
x : V
y : W
⊢ let y' := y;
  let z := x ⊗ₜ[k] y;
  r • z = x ⊗ₜ[k] (r • y')

Tactic:
show asAlgebraHom (1 ⊗ ρW) _ _ = _ ⊗ₜ asAlgebraHom ρW _ _

Result:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρW : Representation k G W
r : MonoidAlgebra k G
x : V
y : W
⊢ ((1 ⊗ ρW).asAlgebraHom r) (x ⊗ₜ[k] y) = x ⊗ₜ[k] (ρW.asAlgebraHom r) y

Proof state:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρW : Representation k G W
r : MonoidAlgebra k G
x : V
y : W
⊢ ((1 ⊗ ρW).asAlgebraHom r) (x ⊗ₜ[k] y) = x ⊗ₜ[k] (ρW.asAlgebraHom r) y

Tactic:
simp only [asAlgebraHom_def, MonoidAlgebra.lift_apply, tprod_apply, MonoidHom.one_apply,
  LinearMap.finsupp_sum_apply, LinearMap.smul_apply, TensorProduct.map_tmul, LinearMap.one_apply]

Result:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρW : Representation k G W
r : MonoidAlgebra k G
x : V
y : W
⊢ (Finsupp.sum r fun i d => d • x ⊗ₜ[k] (ρW i) y) = x ⊗ₜ[k] Finsupp.sum r fun i d => d • (ρW i) y

Proof state:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρW : Representation k G W
r : MonoidAlgebra k G
x : V
y : W
⊢ (Finsupp.sum r fun i d => d • x ⊗ₜ[k] (ρW i) y) = x ⊗ₜ[k] Finsupp.sum r fun i d => d • (ρW i) y

Tactic:
simp only [Finsupp.sum, TensorProduct.tmul_sum, TensorProduct.tmul_smul]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem isOpen_set_pi {i : Set ι} {s : ∀ a, Set (π a)} (hi : i.Finite)
    (hs : ∀ a ∈ i, IsOpen (s a)) : IsOpen (pi i s)

Proof state:
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
i : Set ι
s : (a : ι) → Set (π a)
hi : i.Finite
hs : ∀ a ∈ i, IsOpen (s a)
⊢ IsOpen (i.pi s)

Tactic:
rw [pi_def]

Result:
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
i : Set ι
s : (a : ι) → Set (π a)
hi : i.Finite
hs : ∀ a ∈ i, IsOpen (s a)
⊢ IsOpen (⋂ a ∈ i, eval a ⁻¹' s a)

Proof state:
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
i : Set ι
s : (a : ι) → Set (π a)
hi : i.Finite
hs : ∀ a ∈ i, IsOpen (s a)
⊢ IsOpen (⋂ a ∈ i, eval a ⁻¹' s a)

Tactic:
exact hi.isOpen_biInter fun a ha => (hs _ ha).preimage (continuous_apply _)

Result:
no goals
-- Mathlib/Order/Sublattice.lean
@[simp] lemma mem_sInf {S : Set (Sublattice α)} : a ∈ sInf S ↔ ∀ L ∈ S, a ∈ L

Proof state:
α : Type u_2
inst✝ : Lattice α
a : α
S : Set (Sublattice α)
⊢ a ∈ ↑(sInf S) ↔ ∀ L ∈ S, a ∈ L

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
inst✝ : Lattice α
a : α
S : Set (Sublattice α)
⊢ a ∈ sInf S ↔ ∀ L ∈ S, a ∈ L

Tactic:
rw [← SetLike.mem_coe]

Result:
α : Type u_2
inst✝ : Lattice α
a : α
S : Set (Sublattice α)
⊢ a ∈ ↑(sInf S) ↔ ∀ L ∈ S, a ∈ L
-- Mathlib/Data/List/InsertIdx.lean
theorem insertIdx_eraseIdx {l : List α} {n : ℕ} (hn : n ≠ length l) (a : α) :
    insertIdx n a (l.eraseIdx n) = l.set n a

Proof state:
α : Type u
l : List α
n : ℕ
hn : n ≠ l.length
a : α
⊢ insertIdx n a (l.eraseIdx n) = l.set n a

Tactic:
induction n generalizing l <;> cases l <;> simp_all

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem IsBasis.hasBasis (h : IsBasis p s) : HasBasis h.filter p s :=
  ⟨fun t => by simp only [h.mem_filter_iff, exists_prop]⟩

Proof state:
α : Type u_1
ι : Sort u_4
p : ι → Prop
s : ι → Set α
h : IsBasis p s
t : Set α
⊢ t ∈ h.filter ↔ ∃ i, p i ∧ s i ⊆ t

Tactic:
simp only [h.mem_filter_iff, exists_prop]

Result:
no goals
-- Mathlib/Data/ENNReal/Basic.lean
theorem lt_iff_exists_rat_btwn :
    a < b ↔ ∃ q : ℚ, 0 ≤ q ∧ a < Real.toNNReal q ∧ (Real.toNNReal q : ℝ≥0∞) < b :=
  ⟨fun h => by
    rcases lt_iff_exists_coe.1 h with ⟨p, rfl, _⟩
    rcases exists_between h with ⟨c, pc, cb⟩
    rcases lt_iff_exists_coe.1 cb with ⟨r, rfl, _⟩
    rcases (NNReal.lt_iff_exists_rat_btwn _ _).1 (coe_lt_coe.1 pc) with ⟨q, hq0, pq, qr⟩
    exact ⟨q, hq0, coe_lt_coe.2 pq, lt_trans (coe_lt_coe.2 qr) cb⟩,
      fun ⟨_, _, qa, qb⟩ => lt_trans qa qb⟩

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
b : ℝ≥0∞
p : ℝ≥0
right✝¹ h : ↑p < b
r : ℝ≥0
right✝ : ↑r < b
pc : ↑p < ↑r
cb : ↑r < b
q : ℚ
hq0 : 0 ≤ q
pq : p < (↑q).toNNReal
qr : (↑q).toNNReal < r
⊢ ∃ q, 0 ≤ q ∧ ↑p < ↑(↑q).toNNReal ∧ ↑(↑q).toNNReal < b

Tactic:
exact ⟨q, hq0, coe_lt_coe.2 pq, lt_trans (coe_lt_coe.2 qr) cb⟩

Result:
no goals

Proof state:
a b : ℝ≥0∞
h : a < b
⊢ ∃ q, 0 ≤ q ∧ a < ↑(↑q).toNNReal ∧ ↑(↑q).toNNReal < b

Tactic:
rcases lt_iff_exists_coe.1 h with ⟨p, rfl, _⟩

Result:
case intro.intro
b : ℝ≥0∞
p : ℝ≥0
right✝ h : ↑p < b
⊢ ∃ q, 0 ≤ q ∧ ↑p < ↑(↑q).toNNReal ∧ ↑(↑q).toNNReal < b

Proof state:
case intro.intro.intro.intro.intro.intro
b : ℝ≥0∞
p : ℝ≥0
right✝¹ h : ↑p < b
r : ℝ≥0
right✝ : ↑r < b
pc : ↑p < ↑r
cb : ↑r < b
⊢ ∃ q, 0 ≤ q ∧ ↑p < ↑(↑q).toNNReal ∧ ↑(↑q).toNNReal < b

Tactic:
rcases (NNReal.lt_iff_exists_rat_btwn _ _).1 (coe_lt_coe.1 pc) with ⟨q, hq0, pq, qr⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
b : ℝ≥0∞
p : ℝ≥0
right✝¹ h : ↑p < b
r : ℝ≥0
right✝ : ↑r < b
pc : ↑p < ↑r
cb : ↑r < b
q : ℚ
hq0 : 0 ≤ q
pq : p < (↑q).toNNReal
qr : (↑q).toNNReal < r
⊢ ∃ q, 0 ≤ q ∧ ↑p < ↑(↑q).toNNReal ∧ ↑(↑q).toNNReal < b

Proof state:
case intro.intro
b : ℝ≥0∞
p : ℝ≥0
right✝ h : ↑p < b
⊢ ∃ q, 0 ≤ q ∧ ↑p < ↑(↑q).toNNReal ∧ ↑(↑q).toNNReal < b

Tactic:
rcases exists_between h with ⟨c, pc, cb⟩

Result:
case intro.intro.intro.intro
b : ℝ≥0∞
p : ℝ≥0
right✝ h : ↑p < b
c : ℝ≥0∞
pc : ↑p < c
cb : c < b
⊢ ∃ q, 0 ≤ q ∧ ↑p < ↑(↑q).toNNReal ∧ ↑(↑q).toNNReal < b

Proof state:
case intro.intro.intro.intro
b : ℝ≥0∞
p : ℝ≥0
right✝ h : ↑p < b
c : ℝ≥0∞
pc : ↑p < c
cb : c < b
⊢ ∃ q, 0 ≤ q ∧ ↑p < ↑(↑q).toNNReal ∧ ↑(↑q).toNNReal < b

Tactic:
rcases lt_iff_exists_coe.1 cb with ⟨r, rfl, _⟩

Result:
case intro.intro.intro.intro.intro.intro
b : ℝ≥0∞
p : ℝ≥0
right✝¹ h : ↑p < b
r : ℝ≥0
right✝ : ↑r < b
pc : ↑p < ↑r
cb : ↑r < b
⊢ ∃ q, 0 ≤ q ∧ ↑p < ↑(↑q).toNNReal ∧ ↑(↑q).toNNReal < b
-- Mathlib/RingTheory/NonUnitalSubring/Basic.lean
theorem mem_iSup_of_directed {ι} [hι : Nonempty ι] {S : ι → NonUnitalSubring R}
    (hS : Directed (· ≤ ·) S) {x : R} : (x ∈ ⨆ i, S i) ↔ ∃ i, x ∈ S i

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocRing R
ι : Sort u_1
hι : Nonempty ι
S : ι → NonUnitalSubring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
U : NonUnitalSubring R := NonUnitalSubring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubsemigroup) (⨆ i, (S i).toAddSubgroup) ⋯ ⋯
this : ⨆ i, S i ≤ U
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
simpa [U] using @this x

Result:
no goals

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocRing R
ι : Sort u_1
hι : Nonempty ι
S : ι → NonUnitalSubring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
U : NonUnitalSubring R := NonUnitalSubring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubsemigroup) (⨆ i, (S i).toAddSubgroup) ⋯ ⋯
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
suffices ⨆ i, S i ≤ U by simpa [U] using @this x

Result:
R : Type u
inst✝ : NonUnitalNonAssocRing R
ι : Sort u_1
hι : Nonempty ι
S : ι → NonUnitalSubring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
U : NonUnitalSubring R := NonUnitalSubring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubsemigroup) (⨆ i, (S i).toAddSubgroup) ⋯ ⋯
⊢ ⨆ i, S i ≤ U

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocRing R
ι : Sort u_1
hι : Nonempty ι
S : ι → NonUnitalSubring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
U : NonUnitalSubring R := NonUnitalSubring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubsemigroup) (⨆ i, (S i).toAddSubgroup) ⋯ ⋯
⊢ ⨆ i, S i ≤ U

Tactic:
exact iSup_le fun i x hx ↦ Set.mem_iUnion.2 ⟨i, hx⟩

Result:
no goals

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocRing R
ι : Sort u_1
hι : Nonempty ι
S : ι → NonUnitalSubring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
let U : NonUnitalSubring R :=
  NonUnitalSubring.mk' (⋃ i, (S i : Set R)) (⨆ i, (S i).toSubsemigroup) (⨆ i, (S i).toAddSubgroup)
    (Subsemigroup.coe_iSup_of_directed hS) (AddSubgroup.coe_iSup_of_directed hS)

Result:
R : Type u
inst✝ : NonUnitalNonAssocRing R
ι : Sort u_1
hι : Nonempty ι
S : ι → NonUnitalSubring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
U : NonUnitalSubring R := NonUnitalSubring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubsemigroup) (⨆ i, (S i).toAddSubgroup) ⋯ ⋯
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocRing R
ι : Sort u_1
hι : Nonempty ι
S : ι → NonUnitalSubring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
⊢ x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i

Tactic:
refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩

Result:
R : Type u
inst✝ : NonUnitalNonAssocRing R
ι : Sort u_1
hι : Nonempty ι
S : ι → NonUnitalSubring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i
-- Mathlib/Algebra/Homology/Embedding/CochainComplex.lean
lemma isStrictlyGE_iff (n : ℤ) :
    K.IsStrictlyGE n ↔ ∀ (i : ℤ) (_ : i < n), IsZero (K.X i)

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ i < n, IsZero (K.X i)
i : ℤ
hi : ∀ (i_1 : ℕ), (embeddingUpIntGE n).f i_1 ≠ i
⊢ IsZero (K.X i)

Tactic:
rw [not_mem_range_embeddingUpIntGE_iff] at hi

Result:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ i < n, IsZero (K.X i)
i : ℤ
hi : i < n
⊢ IsZero (K.X i)

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ K.IsStrictlyGE n → ∀ i < n, IsZero (K.X i)

Tactic:
intro _ i hi

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
a✝ : K.IsStrictlyGE n
i : ℤ
hi : i < n
⊢ IsZero (K.X i)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ K.IsStrictlyGE n ↔ ∀ i < n, IsZero (K.X i)

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ K.IsStrictlyGE n → ∀ i < n, IsZero (K.X i)

case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ (∀ i < n, IsZero (K.X i)) → K.IsStrictlyGE n

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ i < n, IsZero (K.X i)
i : ℤ
hi : i < n
⊢ IsZero (K.X i)

Tactic:
exact h i hi

Result:
no goals

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ (∀ i < n, IsZero (K.X i)) → K.IsStrictlyGE n

Tactic:
intro h

Result:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ i < n, IsZero (K.X i)
⊢ K.IsStrictlyGE n

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
a✝ : K.IsStrictlyGE n
i : ℤ
hi : i < n
⊢ IsZero (K.X i)

Tactic:
exact K.isZero_of_isStrictlyGE n i hi

Result:
no goals

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ i < n, IsZero (K.X i)
⊢ K.IsStrictlyGE n

Tactic:
refine IsStrictlySupported.mk (fun i hi ↦ ?_)

Result:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ i < n, IsZero (K.X i)
i : ℤ
hi : ∀ (i_1 : ℕ), (embeddingUpIntGE n).f i_1 ≠ i
⊢ IsZero (K.X i)
-- Mathlib/LinearAlgebra/Coevaluation.lean
theorem coevaluation_apply_one :
    (coevaluation K V) (1 : K) =
      let bV := Basis.ofVectorSpace K V
      ∑ i : Basis.ofVectorSpaceIndex K V, bV i ⊗ₜ[K] bV.coord i

Proof state:
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
⊢ (((Basis.singleton Unit K).constr K) fun x =>
        ∑ i : ↑(Basis.ofVectorSpaceIndex K V), (Basis.ofVectorSpace K V) i ⊗ₜ[K] (Basis.ofVectorSpace K V).coord i)
      1 =
    ∑ i : ↑(Basis.ofVectorSpaceIndex K V), (Basis.ofVectorSpace K V) i ⊗ₜ[K] (Basis.ofVectorSpace K V).coord i

Tactic:
rw [(Basis.singleton Unit K).constr_apply_fintype K]

Result:
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
⊢ ∑ i : Unit,
      (Basis.singleton Unit K).equivFun 1 i •
        ∑ i : ↑(Basis.ofVectorSpaceIndex K V), (Basis.ofVectorSpace K V) i ⊗ₜ[K] (Basis.ofVectorSpace K V).coord i =
    ∑ i : ↑(Basis.ofVectorSpaceIndex K V), (Basis.ofVectorSpace K V) i ⊗ₜ[K] (Basis.ofVectorSpace K V).coord i

Proof state:
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
⊢ (coevaluation K V) 1 =
    let bV := Basis.ofVectorSpace K V;
    ∑ i : ↑(Basis.ofVectorSpaceIndex K V), bV i ⊗ₜ[K] bV.coord i

Tactic:
simp only [coevaluation, id]

Result:
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
⊢ (((Basis.singleton Unit K).constr K) fun x =>
        ∑ i : ↑(Basis.ofVectorSpaceIndex K V), (Basis.ofVectorSpace K V) i ⊗ₜ[K] (Basis.ofVectorSpace K V).coord i)
      1 =
    ∑ i : ↑(Basis.ofVectorSpaceIndex K V), (Basis.ofVectorSpace K V) i ⊗ₜ[K] (Basis.ofVectorSpace K V).coord i

Proof state:
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
⊢ ∑ i : Unit,
      (Basis.singleton Unit K).equivFun 1 i •
        ∑ i : ↑(Basis.ofVectorSpaceIndex K V), (Basis.ofVectorSpace K V) i ⊗ₜ[K] (Basis.ofVectorSpace K V).coord i =
    ∑ i : ↑(Basis.ofVectorSpaceIndex K V), (Basis.ofVectorSpace K V) i ⊗ₜ[K] (Basis.ofVectorSpace K V).coord i

Tactic:
simp only [Fintype.univ_punit, Finset.sum_const, one_smul, Basis.singleton_repr,
  Basis.equivFun_apply, Basis.coe_ofVectorSpace, one_nsmul, Finset.card_singleton]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem RedRed.balance1 {l : RBNode α} {v : α} {r : RBNode α}
    (hl : l.RedRed p n) (hr : r.Balanced c n) : ∃ c, (balance1 l v r).Balanced c (n + 1)

Proof state:
case h_1
α : Type u_1
p : Prop
n : Nat
c : RBColor
v : α
r : RBNode α
hr : r.Balanced c n
x✝³ : RBNode α
x✝² : α
x✝¹ a✝¹ : RBNode α
x✝ : α
b✝ : RBNode α
y✝ : α
c✝ : RBNode α
hl : RedRed p (node red (node red a✝¹ x✝ b✝) y✝ c✝) n
c₂✝ : RBColor
a✝ : p
ha : a✝¹.Balanced black n
hb : b✝.Balanced black n
hc : c✝.Balanced c₂✝ n
⊢ ∃ c, (node red (node black a✝¹ x✝ b✝) y✝ (node black c✝ v r)).Balanced c (n + 1)

Tactic:
exact ⟨_, .red (.black ha hb) (.black hc hr)⟩

Result:
no goals

Proof state:
α : Type u_1
p : Prop
n : Nat
c : RBColor
l✝ : RBNode α
v : α
r : RBNode α
hl✝ : RedRed p l✝ n
hr : r.Balanced c n
x✝² : RBNode α
x✝¹ : α
x✝ l : RBNode α
c✝ : RBColor
hl : l.Balanced c✝ n
H1 : ∀ (a : RBNode α) (x : α) (b : RBNode α) (y : α) (c : RBNode α), l = node red (node red a x b) y c → False
H2 : ∀ (a : RBNode α) (x : α) (b : RBNode α) (y : α) (c : RBNode α), l = node red a x (node red b y c) → False
⊢ ∃ c, (node black l v r).Balanced c (n + 1)

Tactic:
exact ⟨_, .black hl hr⟩

Result:
no goals

Proof state:
α : Type u_1
p : Prop
n : Nat
c : RBColor
l : RBNode α
v : α
r : RBNode α
hl : RedRed p l n
hr : r.Balanced c n
⊢ ∃ c, (l.balance1 v r).Balanced c (n + 1)

Tactic:
unfold balance1

Result:
α : Type u_1
p : Prop
n : Nat
c : RBColor
l : RBNode α
v : α
r : RBNode α
hl : RedRed p l n
hr : r.Balanced c n
⊢ ∃ c,
    (match l, v, r with
        | node red (node red a x b) y c, z, d => node red (node black a x b) y (node black c z d)
        | node red a x (node red b y c), z, d => node red (node black a x b) y (node black c z d)
        | a, x, b => node black a x b).Balanced
      c (n + 1)
-- Mathlib/Combinatorics/Schnirelmann.lean
lemma schnirelmannDensity_congr {B : Set ℕ} [DecidablePred (· ∈ B)] (h : A = B) :
    schnirelmannDensity A = schnirelmannDensity B :=
  schnirelmannDensity_congr' (by aesop)

Proof state:
A : Set ℕ
inst✝¹ : DecidablePred fun x => x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x => x ∈ B
h : A = B
⊢ ∀ n > 0, n ∈ A ↔ n ∈ B

Tactic:
aesop

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem Ioi_pred_eq_insert_of_not_isMin (ha : ¬IsMin a) : Ioi (pred a) = insert a (Ioi a)

Proof state:
case h
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
x : α
⊢ x ∈ Ioi (pred a) ↔ x ∈ insert a (Ioi a)

Tactic:
simp only [insert, mem_setOf, @eq_comm _ x a, mem_Ioi, Set.insert]

Result:
case h
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
x : α
⊢ pred a < x ↔ a = x ∨ a < x

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
⊢ Ioi (pred a) = insert a (Ioi a)

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
x : α
⊢ x ∈ Ioi (pred a) ↔ x ∈ insert a (Ioi a)

Proof state:
case h
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
x : α
⊢ pred a < x ↔ a = x ∨ a < x

Tactic:
exact pred_lt_iff_eq_or_lt_of_not_isMin ha

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem sdiff_le_sdiff_iff_le (hx : x ≤ z) (hy : y ≤ z) : z \ x ≤ z \ y ↔ y ≤ x

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hx : x ≤ z
hy : y ≤ z
h : z \ x ≤ z \ y
⊢ y ≤ x

Tactic:
rw [← sdiff_sdiff_eq_self hx, ← sdiff_sdiff_eq_self hy]

Result:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hx : x ≤ z
hy : y ≤ z
h : z \ x ≤ z \ y
⊢ z \ (z \ y) ≤ z \ (z \ x)

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hx : x ≤ z
hy : y ≤ z
h : z \ x ≤ z \ y
⊢ z \ (z \ y) ≤ z \ (z \ x)

Tactic:
exact sdiff_le_sdiff_left h

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hx : x ≤ z
hy : y ≤ z
⊢ z \ x ≤ z \ y ↔ y ≤ x

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

Result:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hx : x ≤ z
hy : y ≤ z
h : z \ x ≤ z \ y
⊢ y ≤ x