harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mk_mem_zipIdx_iff_le_and_getElem?_sub {k i : Nat} {x : α} {l : Array α} :
    (x, i) ∈ zipIdx l k ↔ k ≤ i ∧ l[i - k]? = some x

Proof state:
α : Type u_1
k i : Nat
x : α
l : Array α
⊢ (x, i) ∈ l.zipIdx k ↔ k ≤ i ∧ l[i - k]? = some x

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
k i : Nat
x : α
l : List α
⊢ (x, i) ∈ { toList := l }.zipIdx k ↔ k ≤ i ∧ { toList := l }[i - k]? = some x

Proof state:
case mk
α : Type u_1
k i : Nat
x : α
l : List α
⊢ (x, i) ∈ { toList := l }.zipIdx k ↔ k ≤ i ∧ { toList := l }[i - k]? = some x

Tactic:
simp [List.mk_mem_zipIdx_iff_le_and_getElem?_sub]

Result:
no goals
-- Mathlib/SetTheory/Game/Domineering.lean
theorem card_of_mem_left {b : Board} {m : ℤ × ℤ} (h : m ∈ left b) : 2 ≤ Finset.card b

Proof state:
b : Board
m : ℤ × ℤ
h : m ∈ left b
w₁ : m ∈ b
w₂ : (m.1, m.2 - 1) ∈ Finset.erase b m
i₁ : (Finset.erase b m).card < Finset.card b
i₂ : 0 < (Finset.erase b m).card
⊢ 2 ≤ Finset.card b

Tactic:
exact Nat.lt_of_le_of_lt i₂ i₁

Result:
no goals

Proof state:
b : Board
m : ℤ × ℤ
h : m ∈ left b
⊢ 2 ≤ Finset.card b

Tactic:
have w₁ : m ∈ b := (Finset.mem_inter.1 h).1

Result:
b : Board
m : ℤ × ℤ
h : m ∈ left b
w₁ : m ∈ b
⊢ 2 ≤ Finset.card b

Proof state:
b : Board
m : ℤ × ℤ
h : m ∈ left b
w₁ : m ∈ b
w₂ : (m.1, m.2 - 1) ∈ Finset.erase b m
⊢ 2 ≤ Finset.card b

Tactic:
have i₁ := Finset.card_erase_lt_of_mem w₁

Result:
b : Board
m : ℤ × ℤ
h : m ∈ left b
w₁ : m ∈ b
w₂ : (m.1, m.2 - 1) ∈ Finset.erase b m
i₁ : (Finset.erase b m).card < Finset.card b
⊢ 2 ≤ Finset.card b

Proof state:
b : Board
m : ℤ × ℤ
h : m ∈ left b
w₁ : m ∈ b
w₂ : (m.1, m.2 - 1) ∈ Finset.erase b m
i₁ : (Finset.erase b m).card < Finset.card b
⊢ 2 ≤ Finset.card b

Tactic:
have i₂ := Nat.lt_of_le_of_lt (Nat.zero_le _) (Finset.card_erase_lt_of_mem w₂)

Result:
b : Board
m : ℤ × ℤ
h : m ∈ left b
w₁ : m ∈ b
w₂ : (m.1, m.2 - 1) ∈ Finset.erase b m
i₁ : (Finset.erase b m).card < Finset.card b
i₂ : 0 < (Finset.erase b m).card
⊢ 2 ≤ Finset.card b

Proof state:
b : Board
m : ℤ × ℤ
h : m ∈ left b
w₁ : m ∈ b
⊢ 2 ≤ Finset.card b

Tactic:
have w₂ : (m.1, m.2 - 1) ∈ b.erase m := snd_pred_mem_erase_of_mem_left h

Result:
b : Board
m : ℤ × ℤ
h : m ∈ left b
w₁ : m ∈ b
w₂ : (m.1, m.2 - 1) ∈ Finset.erase b m
⊢ 2 ≤ Finset.card b
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem getVert_append {u v w : V} (p : G.Walk u v) (q : G.Walk v w) (i : ℕ) :
    (p.append q).getVert i = if i < p.length then p.getVert i else q.getVert (i - p.length)

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
i : ℕ
⊢ (p.append q).getVert i = if i < p.length then p.getVert i else q.getVert (i - p.length)

Tactic:
induction p generalizing i with
| nil => simp
| cons h p ih => cases i <;> simp [getVert, ih, Nat.succ_lt_succ_iff]

Result:
no goals

Proof state:
case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
q : G.Walk u✝ w
i : ℕ
⊢ (nil.append q).getVert i = if i < nil.length then nil.getVert i else q.getVert (i - nil.length)

Tactic:
simp

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih :
  ∀ (q : G.Walk w✝ w) (i : ℕ), (p.append q).getVert i = if i < p.length then p.getVert i else q.getVert (i - p.length)
q : G.Walk w✝ w
i : ℕ
⊢ ((cons h p).append q).getVert i =
    if i < (cons h p).length then (cons h p).getVert i else q.getVert (i - (cons h p).length)

Tactic:
cases i <;> simp [getVert, ih, Nat.succ_lt_succ_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem span_nat_eq (s : AddSubmonoid M) : (span ℕ (s : Set M)).toAddSubmonoid = s

Proof state:
M : Type u_4
inst✝ : AddCommMonoid M
s : AddSubmonoid M
⊢ (span ℕ ↑s).toAddSubmonoid = s

Tactic:
rw [span_nat_eq_addSubmonoid_closure, s.closure_eq]

Result:
no goals
-- Mathlib/Analysis/Convex/Star.lean
theorem StarConvex.mem (hs : StarConvex 𝕜 x s) (h : s.Nonempty) : x ∈ s

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
y : E
hy : y ∈ s
⊢ x ∈ s

Tactic:
convert hs hy zero_le_one le_rfl (add_zero 1)

Result:
case h.e'_5
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
y : E
hy : y ∈ s
⊢ x = 1 • x + 0 • y

Proof state:
case h.e'_5
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
y : E
hy : y ∈ s
⊢ x = 1 • x + 0 • y

Tactic:
rw [one_smul, zero_smul, add_zero]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
h : s.Nonempty
⊢ x ∈ s

Tactic:
obtain ⟨y, hy⟩ := h

Result:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
y : E
hy : y ∈ s
⊢ x ∈ s
-- Mathlib/LinearAlgebra/Determinant.lean
theorem detAux_def'' {ι' : Type*} [Fintype ι'] [DecidableEq ι'] (tb : Trunc <| Basis ι A M)
    (b' : Basis ι' A M) (f : M →ₗ[A] M) :
    LinearMap.detAux tb f = Matrix.det (LinearMap.toMatrix b' b' f)

Proof state:
case h
M : Type u_2
inst✝⁶ : AddCommGroup M
ι : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
ι' : Type u_7
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
b' : Basis ι' A M
f : M →ₗ[A] M
b : Basis ι A M
⊢ (detAux (Trunc.mk b)) f = ((toMatrix b' b') f).det

Tactic:
rw [detAux_def', det_toMatrix_eq_det_toMatrix b b']

Result:
no goals

Proof state:
M : Type u_2
inst✝⁶ : AddCommGroup M
ι : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
ι' : Type u_7
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
tb : Trunc (Basis ι A M)
b' : Basis ι' A M
f : M →ₗ[A] M
⊢ (detAux tb) f = ((toMatrix b' b') f).det

Tactic:
induction tb using Trunc.induction_on with
| h b => rw [detAux_def', det_toMatrix_eq_det_toMatrix b b']

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem affineCombination_apply_const (w : ι → k) (p : P) (h : ∑ i ∈ s, w i = 1) :
    s.affineCombination k (fun _ => p) w = p

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : P
h : ∑ i ∈ s, w i = 1
⊢ (affineCombination k s fun x => p) w = p

Tactic:
rw [affineCombination_apply, s.weightedVSubOfPoint_apply_const, h, one_smul, vsub_vadd]

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
@[simp]
lemma map_neg_divisorsAntidiag :
    z.divisorsAntidiag.map (Equiv.neg _).toEmbedding = z.divisorsAntidiag

Proof state:
case h
z : ℤ
a✝ : ℤ × ℤ
⊢ a✝ ∈ map (Equiv.toEmbedding (Equiv.neg (ℤ × ℤ))) z.divisorsAntidiag ↔ a✝ ∈ z.divisorsAntidiag

Tactic:
simp [mem_divisorsAntidiag, mul_comm]

Result:
no goals

Proof state:
z : ℤ
⊢ map (Equiv.toEmbedding (Equiv.neg (ℤ × ℤ))) z.divisorsAntidiag = z.divisorsAntidiag

Tactic:
ext

Result:
case h
z : ℤ
a✝ : ℤ × ℤ
⊢ a✝ ∈ map (Equiv.toEmbedding (Equiv.neg (ℤ × ℤ))) z.divisorsAntidiag ↔ a✝ ∈ z.divisorsAntidiag
-- Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
lemma addVal_eq_zero_iff {x : R} :
    addVal R x = 0 ↔ IsUnit x

Proof state:
case inr.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hϖ : Irreducible ϖ
n : ℕ
u : Rˣ
hx : ↑u * ϖ ^ n ≠ 0
⊢ (addVal R) (↑u * ϖ ^ n) = 0 ↔ IsUnit (↑u * ϖ ^ n)

Tactic:
simp [isUnit_pow_iff_of_not_isUnit hϖ.not_unit, hϖ]

Result:
no goals

Proof state:
case inr.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hϖ : Irreducible ϖ
⊢ (addVal R) x = 0 ↔ IsUnit x

Tactic:
obtain ⟨n, u, rfl⟩ := eq_unit_mul_pow_irreducible hx hϖ

Result:
case inr.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
hϖ : Irreducible ϖ
n : ℕ
u : Rˣ
hx : ↑u * ϖ ^ n ≠ 0
⊢ (addVal R) (↑u * ϖ ^ n) = 0 ↔ IsUnit (↑u * ϖ ^ n)

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
⊢ (addVal R) x = 0 ↔ IsUnit x

Tactic:
rcases eq_or_ne x 0 with rfl|hx

Result:
case inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
⊢ (addVal R) 0 = 0 ↔ IsUnit 0

case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
hx : x ≠ 0
⊢ (addVal R) x = 0 ↔ IsUnit x

Proof state:
case inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
⊢ (addVal R) 0 = 0 ↔ IsUnit 0

Tactic:
simp

Result:
no goals

Proof state:
case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
hx : x ≠ 0
⊢ (addVal R) x = 0 ↔ IsUnit x

Tactic:
obtain ⟨ϖ, hϖ⟩ := exists_irreducible R

Result:
case inr.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
x : R
hx : x ≠ 0
ϖ : R
hϖ : Irreducible ϖ
⊢ (addVal R) x = 0 ↔ IsUnit x
-- Mathlib/GroupTheory/QuotientGroup/Defs.lean
theorem map_map {I : Type*} [Group I] (M : Subgroup H) (O : Subgroup I) [M.Normal] [O.Normal]
    (f : G →* H) (g : H →* I) (hf : N ≤ Subgroup.comap f M) (hg : M ≤ Subgroup.comap g O)
    (hgf : N ≤ Subgroup.comap (g.comp f) O :=
      hf.trans ((Subgroup.comap_mono hg).trans_eq (Subgroup.comap_comap _ _ _)))
    (x : G ⧸ N) : map M O g hg (map N M f hf x) = map N O (g.comp f) hgf x

Proof state:
G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst✝³ : Group H
I : Type u_1
inst✝² : Group I
M : Subgroup H
O : Subgroup I
inst✝¹ : M.Normal
inst✝ : O.Normal
f : G →* H
g : H →* I
hf : N ≤ Subgroup.comap f M
hg : M ≤ Subgroup.comap g O
hgf : optParam (N ≤ Subgroup.comap (g.comp f) O) ⋯
x✝ : G ⧸ N
x : G
⊢ (map M O g hg) ((map N M f hf) ↑x) = (map N O (g.comp f) hgf) ↑x

Tactic:
simp only [map_mk, MonoidHom.comp_apply]

Result:
no goals

Proof state:
G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst✝³ : Group H
I : Type u_1
inst✝² : Group I
M : Subgroup H
O : Subgroup I
inst✝¹ : M.Normal
inst✝ : O.Normal
f : G →* H
g : H →* I
hf : N ≤ Subgroup.comap f M
hg : M ≤ Subgroup.comap g O
hgf : optParam (N ≤ Subgroup.comap (g.comp f) O) ⋯
x : G ⧸ N
⊢ (map M O g hg) ((map N M f hf) x) = (map N O (g.comp f) hgf) x

Tactic:
refine induction_on x fun x => ?_

Result:
G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst✝³ : Group H
I : Type u_1
inst✝² : Group I
M : Subgroup H
O : Subgroup I
inst✝¹ : M.Normal
inst✝ : O.Normal
f : G →* H
g : H →* I
hf : N ≤ Subgroup.comap f M
hg : M ≤ Subgroup.comap g O
hgf : optParam (N ≤ Subgroup.comap (g.comp f) O) ⋯
x✝ : G ⧸ N
x : G
⊢ (map M O g hg) ((map N M f hf) ↑x) = (map N O (g.comp f) hgf) ↑x
-- Mathlib/RingTheory/FinitePresentation.lean
theorem equiv [FinitePresentation R A] (e : A ≃ₐ[R] B) : FinitePresentation R B

Proof state:
case h.right
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ RingHom.ker ((↑e).comp f).toRingHom = RingHom.ker f.toRingHom

Tactic:
have hco : (AlgHom.comp (e : A →ₐ[R] B) f).toRingHom = RingHom.comp (e.toRingEquiv : A ≃+* B)
  f.toRingHom := by
  have h : (AlgHom.comp (e : A →ₐ[R] B) f).toRingHom =
    e.toAlgHom.toRingHom.comp f.toRingHom := rfl
  have h1 : ↑e.toRingEquiv = e.toAlgHom.toRingHom := rfl
  rw [h, h1]

Result:
case h.right
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
hco : ((↑e).comp f).toRingHom = (↑e.toRingEquiv).comp f.toRingHom
⊢ RingHom.ker ((↑e).comp f).toRingHom = RingHom.ker f.toRingHom

Proof state:
case h.left
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ Surjective ⇑((↑e).comp f)

Tactic:
rw [AlgHom.coe_comp]

Result:
case h.left
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ Surjective (⇑↑e ∘ ⇑f)

Proof state:
case h.right
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
hco : ((↑e).comp f).toRingHom = (↑e.toRingEquiv).comp f.toRingHom
⊢ RingHom.ker ((↑e).comp f).toRingHom = RingHom.ker f.toRingHom

Tactic:
rw [RingHom.ker_eq_comap_bot, hco, ← Ideal.comap_comap, ← RingHom.ker_eq_comap_bot,
  RingHom.ker_coe_equiv (AlgEquiv.toRingEquiv e), RingHom.ker_eq_comap_bot]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem iUnion_filter_not (π : Prepartition I) (p : Box ι → Prop) :
    (π.filter fun J => ¬p J).iUnion = π.iUnion \ (π.filter p).iUnion

Proof state:
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
⊢ (π.filter fun J => ¬p J).iUnion = π.iUnion \ (π.filter p).iUnion

Tactic:
simp only [Prepartition.iUnion]

Result:
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
⊢ ⋃ J ∈ π.filter fun J => ¬p J, ↑J = (⋃ J ∈ π, ↑J) \ ⋃ J ∈ π.filter p, ↑J

Proof state:
case h.e'_2
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
⊢ ↑π.boxes ∪ ↑(π.filter p).boxes = ↑π.boxes

Tactic:
rw [Set.union_eq_left, filter_boxes, coe_filter]

Result:
case h.e'_2
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
⊢ {x | x ∈ π.boxes ∧ p x} ⊆ ↑π.boxes

Proof state:
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
⊢ (↑π.boxes ∪ ↑(π.filter p).boxes).PairwiseDisjoint Box.toSet

Tactic:
rw [Set.PairwiseDisjoint]

Result:
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
⊢ (↑π.boxes ∪ ↑(π.filter p).boxes).Pairwise (Disjoint on Box.toSet)

Proof state:
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
⊢ ⋃ J ∈ π.filter fun J => ¬p J, ↑J = (⋃ J ∈ π, ↑J) \ ⋃ J ∈ π.filter p, ↑J

Tactic:
convert
  (@Set.biUnion_diff_biUnion_eq (ι → ℝ) (Box ι) π.boxes (π.filter p).boxes (↑) _).symm using 4

Result:
case h.e'_2.h.e'_3.h.pq.a.a
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
x✝ : Box ι
⊢ (x✝ ∈ π.filter fun J => ¬p J) ↔ x✝ ∈ ↑π.boxes \ ↑(π.filter p).boxes

ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
⊢ (↑π.boxes ∪ ↑(π.filter p).boxes).PairwiseDisjoint Box.toSet

Proof state:
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
⊢ (↑π.boxes ∪ ↑(π.filter p).boxes).Pairwise (Disjoint on Box.toSet)

Tactic:
convert π.pairwiseDisjoint

Result:
case h.e'_2
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
⊢ ↑π.boxes ∪ ↑(π.filter p).boxes = ↑π.boxes

Proof state:
case h.e'_2.h.e'_3.h.pq.a.a
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
x✝ : Box ι
⊢ (x✝ ∈ π.filter fun J => ¬p J) ↔ x✝ ∈ ↑π.boxes \ ↑(π.filter p).boxes

Tactic:
simp +contextual

Result:
no goals

Proof state:
case h.e'_2
ι : Type u_1
I : Box ι
π : Prepartition I
p : Box ι → Prop
⊢ {x | x ∈ π.boxes ∧ p x} ⊆ ↑π.boxes

Tactic:
exact fun _ ⟨h, _⟩ => h

Result:
no goals
-- Mathlib/Order/GameAdd.lean
theorem gameAdd_iff {rα rβ} {x y : α × β} :
    GameAdd rα rβ x y ↔ rα x.1 y.1 ∧ x.2 = y.2 ∨ rβ x.2 y.2 ∧ x.1 = y.1

Proof state:
case mp
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x y : α × β
⊢ GameAdd rα rβ x y → rα x.1 y.1 ∧ x.2 = y.2 ∨ rβ x.2 y.2 ∧ x.1 = y.1

Tactic:
rintro (@⟨a₁, a₂, b, h⟩ | @⟨a, b₁, b₂, h⟩)

Result:
case mp.fst
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a₁ a₂ : α
b : β
h : rα a₁ a₂
⊢ rα (a₁, b).1 (a₂, b).1 ∧ (a₁, b).2 = (a₂, b).2 ∨ rβ (a₁, b).2 (a₂, b).2 ∧ (a₁, b).1 = (a₂, b).1

case mp.snd
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a : α
b₁ b₂ : β
h : rβ b₁ b₂
⊢ rα (a, b₁).1 (a, b₂).1 ∧ (a, b₁).2 = (a, b₂).2 ∨ rβ (a, b₁).2 (a, b₂).2 ∧ (a, b₁).1 = (a, b₂).1

Proof state:
case mpr.mk.mk.inl.intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a₁ : α
b₁ : β
a₂ : α
h : rα (a₁, b₁).1 (a₂, b₁).1
⊢ GameAdd rα rβ (a₁, b₁) (a₂, b₁)

case mpr.mk.mk.inr.intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a₁ : α
b₁ b₂ : β
h : rβ (a₁, b₁).2 (a₁, b₂).2
⊢ GameAdd rα rβ (a₁, b₁) (a₁, b₂)

Tactic:
exacts [GameAdd.fst h, GameAdd.snd h]

Result:
no goals

Proof state:
case mp.fst
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a₁ a₂ : α
b : β
h : rα a₁ a₂
⊢ rα (a₁, b).1 (a₂, b).1 ∧ (a₁, b).2 = (a₂, b).2 ∨ rβ (a₁, b).2 (a₂, b).2 ∧ (a₁, b).1 = (a₂, b).1

case mp.snd
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a : α
b₁ b₂ : β
h : rβ b₁ b₂
⊢ rα (a, b₁).1 (a, b₂).1 ∧ (a, b₁).2 = (a, b₂).2 ∨ rβ (a, b₁).2 (a, b₂).2 ∧ (a, b₁).1 = (a, b₂).1

Tactic:
exacts [Or.inl ⟨h, rfl⟩, Or.inr ⟨h, rfl⟩]

Result:
no goals

Proof state:
case mpr
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x y : α × β
⊢ rα x.1 y.1 ∧ x.2 = y.2 ∨ rβ x.2 y.2 ∧ x.1 = y.1 → GameAdd rα rβ x y

Tactic:
revert x y

Result:
case mpr
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
⊢ ∀ {x y : α × β}, rα x.1 y.1 ∧ x.2 = y.2 ∨ rβ x.2 y.2 ∧ x.1 = y.1 → GameAdd rα rβ x y

Proof state:
case mpr
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
⊢ ∀ {x y : α × β}, rα x.1 y.1 ∧ x.2 = y.2 ∨ rβ x.2 y.2 ∧ x.1 = y.1 → GameAdd rα rβ x y

Tactic:
rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ (⟨h, rfl : b₁ = b₂⟩ | ⟨h, rfl : a₁ = a₂⟩)

Result:
case mpr.mk.mk.inl.intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a₁ : α
b₁ : β
a₂ : α
h : rα (a₁, b₁).1 (a₂, b₁).1
⊢ GameAdd rα rβ (a₁, b₁) (a₂, b₁)

case mpr.mk.mk.inr.intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a₁ : α
b₁ b₂ : β
h : rβ (a₁, b₁).2 (a₁, b₂).2
⊢ GameAdd rα rβ (a₁, b₁) (a₁, b₂)

Proof state:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x y : α × β
⊢ GameAdd rα rβ x y ↔ rα x.1 y.1 ∧ x.2 = y.2 ∨ rβ x.2 y.2 ∧ x.1 = y.1

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x y : α × β
⊢ GameAdd rα rβ x y → rα x.1 y.1 ∧ x.2 = y.2 ∨ rβ x.2 y.2 ∧ x.1 = y.1

case mpr
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x y : α × β
⊢ rα x.1 y.1 ∧ x.2 = y.2 ∨ rβ x.2 y.2 ∧ x.1 = y.1 → GameAdd rα rβ x y
-- Mathlib/Algebra/Ring/Ext.lean
theorem toNonAssocSemiring_injective :
    Function.Injective (@toNonAssocSemiring R)

Proof state:
R : Type u
⊢ Function.Injective (@toNonAssocSemiring R)

Tactic:
intro _ _ h

Result:
R : Type u
a₁✝ a₂✝ : NonAssocRing R
h : toNonAssocSemiring = toNonAssocSemiring
⊢ a₁✝ = a₂✝

Proof state:
R : Type u
a₁✝ a₂✝ : NonAssocRing R
h : toNonAssocSemiring = toNonAssocSemiring
⊢ a₁✝ = a₂✝

Tactic:
ext x y

Result:
case h_add.h.h
R : Type u
a₁✝ a₂✝ : NonAssocRing R
h : toNonAssocSemiring = toNonAssocSemiring
x y : R
⊢ x + y = x + y

case h_mul.h.h
R : Type u
a₁✝ a₂✝ : NonAssocRing R
h : toNonAssocSemiring = toNonAssocSemiring
x y : R
⊢ x * y = x * y
-- Mathlib/Order/Interval/Set/SuccPred.lean
lemma Icc_succ_left_eq_Ioc_of_not_isMax (ha : ¬ IsMax a) (b : α) : Icc (succ a) b = Ioc a b

Proof state:
case h
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a : α
ha : ¬IsMax a
b x : α
⊢ x ∈ Icc (succ a) b ↔ x ∈ Ioc a b

Tactic:
rw [mem_Icc, mem_Ioc, succ_le_iff_of_not_isMax ha]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a : α
ha : ¬IsMax a
b : α
⊢ Icc (succ a) b = Ioc a b

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a : α
ha : ¬IsMax a
b x : α
⊢ x ∈ Icc (succ a) b ↔ x ∈ Ioc a b
-- Mathlib/Order/Atoms.lean
theorem le_iff_atom_le_imp {α} [BooleanAlgebra α] [IsAtomic α] {x y : α} :
    x ≤ y ↔ ∀ a, IsAtom a → a ≤ x → a ≤ y

Proof state:
α : Type u_4
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
h : ∀ (a : α), IsAtom a → a ≤ x → a ≤ y
⊢ x ≤ y

Tactic:
have : x ⊓ yᶜ = ⊥ := of_not_not fun hbot =>
  have ⟨a, ha, hle⟩ := (eq_bot_or_exists_atom_le _).resolve_left hbot
  have ⟨hx, hy'⟩ := le_inf_iff.1 hle
  have hy := h a ha hx
  have : a ≤ y ⊓ yᶜ := le_inf_iff.2 ⟨hy, hy'⟩
  ha.1 (by simpa using this)

Result:
α : Type u_4
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
h : ∀ (a : α), IsAtom a → a ≤ x → a ≤ y
this : x ⊓ yᶜ = ⊥
⊢ x ≤ y

Proof state:
α : Type u_4
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
h : ∀ (a : α), IsAtom a → a ≤ x → a ≤ y
hbot : ¬x ⊓ yᶜ = ⊥
a : α
ha : IsAtom a
hle : a ≤ x ⊓ yᶜ
hx : a ≤ x
hy' : a ≤ yᶜ
hy : a ≤ y
this : a ≤ y ⊓ yᶜ
⊢ a = ⊥

Tactic:
simpa using this

Result:
no goals

Proof state:
α : Type u_4
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
h : ∀ (a : α), IsAtom a → a ≤ x → a ≤ y
this : x ⊓ yᶜ = ⊥
⊢ x ≤ y

Tactic:
exact (eq_compl_iff_isCompl.1 (by simp)).inf_right_eq_bot_iff.1 this

Result:
no goals

Proof state:
α : Type u_4
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
h : ∀ (a : α), IsAtom a → a ≤ x → a ≤ y
this : x ⊓ yᶜ = ⊥
⊢ y = yᶜᶜ

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem mk'_self' (y : S) : f.mk' (y : M) y = 1 :=
  show _ * _ = _ by rw [mul_inv_left, mul_one]

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
y : ↥S
⊢ f.toMap ↑y * ↑((IsUnit.liftRight (f.toMap.restrict S) ⋯) y)⁻¹ = 1

Tactic:
rw [mul_inv_left, mul_one]

Result:
no goals
-- Mathlib/Probability/Process/Stopping.lean
theorem stoppedValue_sub_eq_sum [AddCommGroup β] (hle : τ ≤ π) :
    stoppedValue u π - stoppedValue u τ = fun ω =>
      (∑ i ∈ Finset.Ico (τ ω) (π ω), (u (i + 1) - u i)) ω

Proof state:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ
inst✝ : AddCommGroup β
hle : τ ≤ π
⊢ stoppedValue u π - stoppedValue u τ = fun ω => (∑ i ∈ Finset.Ico (τ ω) (π ω), (u (i + 1) - u i)) ω

Tactic:
ext ω

Result:
case h
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ
inst✝ : AddCommGroup β
hle : τ ≤ π
ω : Ω
⊢ (stoppedValue u π - stoppedValue u τ) ω = (∑ i ∈ Finset.Ico (τ ω) (π ω), (u (i + 1) - u i)) ω

Proof state:
case h
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ
inst✝ : AddCommGroup β
hle : τ ≤ π
ω : Ω
⊢ (stoppedValue u π - stoppedValue u τ) ω = (∑ i ∈ Finset.Ico (τ ω) (π ω), (u (i + 1) - u i)) ω

Tactic:
rw [Finset.sum_Ico_eq_sub _ (hle ω), Finset.sum_range_sub, Finset.sum_range_sub]

Result:
case h
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ
inst✝ : AddCommGroup β
hle : τ ≤ π
ω : Ω
⊢ (stoppedValue u π - stoppedValue u τ) ω = (u (π ω) - u 0 - (u (τ ω) - u 0)) ω

Proof state:
case h
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ π : Ω → ℕ
inst✝ : AddCommGroup β
hle : τ ≤ π
ω : Ω
⊢ (stoppedValue u π - stoppedValue u τ) ω = (u (π ω) - u 0 - (u (τ ω) - u 0)) ω

Tactic:
simp [stoppedValue]

Result:
no goals