harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Module/SnakeLemma.lean
lemma SnakeLemma.eq_of_eq (x : K₃)
    (y₁) (hy₁ : f₂ y₁ = ι₃ x) (z₁) (hz₁ : g₁ z₁ = i₂ y₁)
    (y₂) (hy₂ : f₂ y₂ = ι₃ x) (z₂) (hz₂ : g₁ z₂ = i₂ y₂) : π₁ z₁ = π₁ z₂

Proof state:
R : Type u_3
inst✝¹⁴ : CommRing R
M₁ : Type ?u.35643
M₂ : Type u_2
M₃ : Type u_1
N₁ : Type u_6
N₂ : Type u_5
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R M₁
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₃
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_4
C₁ : Type u_7
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₃ : K₃ →ₗ[R] M₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
x : K₃
y₁ : M₂
hy₁ : f₂ y₁ = ι₃ x
z₁ : N₁
hz₁ : g₁ z₁ = i₂ y₁
y₂ : M₂
hy₂ : f₂ y₂ = ι₃ x
z₂ : N₁
hz₂ : g₁ z₂ = i₂ y₂
⊢ π₁ z₁ = π₁ z₂

Tactic:
have := sub_eq_zero.mpr (hy₁.trans hy₂.symm)

Result:
R : Type u_3
inst✝¹⁴ : CommRing R
M₁ : Type ?u.35643
M₂ : Type u_2
M₃ : Type u_1
N₁ : Type u_6
N₂ : Type u_5
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R M₁
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₃
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_4
C₁ : Type u_7
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₃ : K₃ →ₗ[R] M₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
x : K₃
y₁ : M₂
hy₁ : f₂ y₁ = ι₃ x
z₁ : N₁
hz₁ : g₁ z₁ = i₂ y₁
y₂ : M₂
hy₂ : f₂ y₂ = ι₃ x
z₂ : N₁
hz₂ : g₁ z₂ = i₂ y₂
this : f₂ y₁ - f₂ y₂ = 0
⊢ π₁ z₁ = π₁ z₂

Proof state:
case intro
R : Type u_3
inst✝¹⁴ : CommRing R
M₁ : Type ?u.35643
M₂ : Type u_2
M₃ : Type u_1
N₁ : Type u_6
N₂ : Type u_5
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R M₁
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₃
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_4
C₁ : Type u_7
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₃ : K₃ →ₗ[R] M₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
x : K₃
y₁ : M₂
hy₁ : f₂ y₁ = ι₃ x
z₁ : N₁
y₂ : M₂
hy₂ : f₂ y₂ = ι₃ x
z₂ : N₁
hz₂ : g₁ z₂ = i₂ y₂
d : M₁
hz₁ : z₁ - z₂ = i₁ d
hd : f₁ d = y₁ - y₂
⊢ i₁ d ∈ Set.range ⇑i₁

Tactic:
exact ⟨_, rfl⟩

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem All.lowerBound?_lb {t : RBNode α} (hp : t.All p) (H : ∀ {x}, lb = some x → p x) :
    t.lowerBound? cut lb = some x → p x

Proof state:
α : Type u_1
p : α → Prop
lb : Option α
cut : α → Ordering
x : α
t : RBNode α
hp : All p t
H : ∀ {x : α}, lb = some x → p x
⊢ lowerBound? cut t lb = some x → p x

Tactic:
rw [← reverse_reverse t, lowerBound?_reverse]

Result:
α : Type u_1
p : α → Prop
lb : Option α
cut : α → Ordering
x : α
t : RBNode α
hp : All p t
H : ∀ {x : α}, lb = some x → p x
⊢ RBNode.upperBound? (fun x => (cut x).swap) t.reverse lb = some x → p x

Proof state:
α : Type u_1
p : α → Prop
lb : Option α
cut : α → Ordering
x : α
t : RBNode α
hp : All p t
H : ∀ {x : α}, lb = some x → p x
⊢ RBNode.upperBound? (fun x => (cut x).swap) t.reverse lb = some x → p x

Tactic:
exact All.upperBound?_ub (All.reverse.2 hp) H

Result:
no goals
-- Mathlib/CategoryTheory/Limits/EpiMono.lean
lemma mono_iff_fst_eq_snd (hc : IsLimit c) : Mono f ↔ c.fst = c.snd

Proof state:
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
⊢ c.fst = c.snd → Mono f

Tactic:
intro hf

Result:
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
hf : c.fst = c.snd
⊢ Mono f

Proof state:
case mpr.right_cancellation
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
hf : c.fst = c.snd
Z : C
g g' : Z ⟶ X
h : g ≫ f = g' ≫ f
⊢ g = g'

Tactic:
obtain ⟨φ, rfl, rfl⟩ := PullbackCone.IsLimit.lift' hc g g' h

Result:
case mpr.right_cancellation.mk.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
hf : c.fst = c.snd
Z : C
φ : Z ⟶ c.pt
h : (φ ≫ c.fst) ≫ f = (φ ≫ c.snd) ≫ f
⊢ φ ≫ c.fst = φ ≫ c.snd

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
⊢ Mono f ↔ c.fst = c.snd

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
⊢ Mono f → c.fst = c.snd

case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
⊢ c.fst = c.snd → Mono f

Proof state:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
⊢ Mono f → c.fst = c.snd

Tactic:
intro hf

Result:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
hf : Mono f
⊢ c.fst = c.snd

Proof state:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
hf : Mono f
⊢ c.fst = c.snd

Tactic:
simpa only [← cancel_mono f] using c.condition

Result:
no goals

Proof state:
case mpr.right_cancellation.mk.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
hf : c.fst = c.snd
Z : C
φ : Z ⟶ c.pt
h : (φ ≫ c.fst) ≫ f = (φ ≫ c.snd) ≫ f
⊢ φ ≫ c.fst = φ ≫ c.snd

Tactic:
rw [hf]

Result:
no goals

Proof state:
case mpr.right_cancellation
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
hf : c.fst = c.snd
⊢ ∀ {Z : C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h

Tactic:
intro Z g g' h

Result:
case mpr.right_cancellation
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
hf : c.fst = c.snd
Z : C
g g' : Z ⟶ X
h : g ≫ f = g' ≫ f
⊢ g = g'

Proof state:
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
hf : c.fst = c.snd
⊢ Mono f

Tactic:
constructor

Result:
case mpr.right_cancellation
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
hf : c.fst = c.snd
⊢ ∀ {Z : C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h
-- Mathlib/AlgebraicTopology/DoldKan/Projections.lean
theorem comp_P_eq_self_iff {Y : C} {n q : ℕ} {φ : Y ⟶ X _⦋n + 1⦌} :
    φ ≫ (P q).f (n + 1) = φ ↔ HigherFacesVanish q φ

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
⊢ φ ≫ (P q).f (n + 1) = φ → HigherFacesVanish q φ

Tactic:
intro hφ

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
hφ : φ ≫ (P q).f (n + 1) = φ
⊢ HigherFacesVanish q φ

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
⊢ HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ

Tactic:
exact HigherFacesVanish.comp_P_eq_self

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
⊢ φ ≫ (P q).f (n + 1) = φ ↔ HigherFacesVanish q φ

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
⊢ φ ≫ (P q).f (n + 1) = φ → HigherFacesVanish q φ

case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
⊢ HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
hφ : φ ≫ (P q).f (n + 1) = φ
⊢ HigherFacesVanish q φ

Tactic:
rw [← hφ]

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
hφ : φ ≫ (P q).f (n + 1) = φ
⊢ HigherFacesVanish q (φ ≫ (P q).f (n + 1))

Proof state:
case mp.v
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
hφ : φ ≫ (P q).f (n + 1) = φ
⊢ HigherFacesVanish q ((P q).f (n + 1))

Tactic:
apply HigherFacesVanish.of_P

Result:
no goals

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
hφ : φ ≫ (P q).f (n + 1) = φ
⊢ HigherFacesVanish q (φ ≫ (P q).f (n + 1))

Tactic:
apply HigherFacesVanish.of_comp

Result:
case mp.v
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
hφ : φ ≫ (P q).f (n + 1) = φ
⊢ HigherFacesVanish q ((P q).f (n + 1))
-- Mathlib/Topology/EMetricSpace/Defs.lean
theorem edist_congr_right {x y z : α} (h : edist x y = 0) : edist x z = edist y z

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist x z = edist y z

Tactic:
apply le_antisymm

Result:
case a
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist x z ≤ edist y z

case a
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist y z ≤ edist x z

Proof state:
case a
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist y x = 0
⊢ edist y z ≤ edist y x + edist x z

Tactic:
apply edist_triangle

Result:
no goals

Proof state:
case a
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist x z ≤ edist y z

Tactic:
rw [← zero_add (edist y z), ← h]

Result:
case a
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist x z ≤ edist x y + edist y z

Proof state:
case a
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist y x = 0
⊢ edist y z ≤ edist x z

Tactic:
rw [← zero_add (edist x z), ← h]

Result:
case a
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist y x = 0
⊢ edist y z ≤ edist y x + edist x z

Proof state:
case a
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist x z ≤ edist x y + edist y z

Tactic:
apply edist_triangle

Result:
no goals

Proof state:
case a
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist y z ≤ edist x z

Tactic:
rw [edist_comm] at h

Result:
case a
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist y x = 0
⊢ edist y z ≤ edist x z
-- Mathlib/Topology/ContinuousMap/Polynomial.lean
lemma toContinuousMapOn_X_eq_restrict_id (s : Set R) :
    X.toContinuousMapOn s = restrict s (.id R)

Proof state:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
⊢ X.toContinuousMapOn s = restrict s (ContinuousMap.id R)

Tactic:
ext

Result:
case h
R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
a✝ : ↑s
⊢ (X.toContinuousMapOn s) a✝ = (restrict s (ContinuousMap.id R)) a✝

Proof state:
case h
R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
s : Set R
a✝ : ↑s
⊢ (X.toContinuousMapOn s) a✝ = (restrict s (ContinuousMap.id R)) a✝

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/CoprodI.lean
theorem _root_.FreeGroup.injective_lift_of_ping_pong : Function.Injective (FreeGroup.lift a)

Proof state:
case refine_2
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hgt : n < 0
h1n : n ≤ -1
⊢ ∀ n ≤ -1, a i ^ n • (X i)ᶜ ⊆ Y i → a i ^ (n - 1) • (X i)ᶜ ⊆ Y i

Tactic:
intro n _ hi

Result:
case refine_2
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n✝ : ℤ
hnne0 : n✝ ≠ 0
hgt : n✝ < 0
h1n : n✝ ≤ -1
n : ℤ
a✝ : n ≤ -1
hi : a i ^ n • (X i)ᶜ ⊆ Y i
⊢ a i ^ (n - 1) • (X i)ᶜ ⊆ Y i

Proof state:
case hpp.inl
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hlt : n > 0
⊢ a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i

Tactic:
have h1n : 1 ≤ n := hlt

Result:
case hpp.inl
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i => FreeGroup Unit
f : (i : ι) → H i →* G := fun i => FreeGroup.lift fun x => a i
X' : ι → Set α := fun i => X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hlt : n > 0
h1n : 1 ≤ n
⊢ a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem measurableSet_regionBetween (hf : Measurable f) (hg : Measurable g) (hs : MeasurableSet s) :
    MeasurableSet (regionBetween f g s)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet (regionBetween f g s)

Tactic:
dsimp only [regionBetween, Ioo, mem_setOf_eq, setOf_and]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet ({a | a.1 ∈ s} ∩ {a | a.2 ∈ {a_1 | f a.1 < a_1} ∩ {a_1 | a_1 < g a.1}})

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet ({a | a.1 ∈ s} ∩ {a | a.2 ∈ {a_1 | f a.1 < a_1} ∩ {a_1 | a_1 < g a.1}})

Tactic:
refine
  MeasurableSet.inter ?_
    ((measurableSet_lt (hf.comp measurable_fst) measurable_snd).inter
      (measurableSet_lt measurable_snd (hg.comp measurable_fst)))

Result:
α : Type u_1
inst✝ : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet {a | a.1 ∈ s}

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet {a | a.1 ∈ s}

Tactic:
exact measurable_fst hs

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Compression/UV.lean
theorem sup_sdiff_injOn [GeneralizedBooleanAlgebra α] (u v : α) :
    { x | Disjoint u x ∧ v ≤ x }.InjOn fun x => (x ⊔ u) \ v

Proof state:
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
u v a : α
ha : a ∈ {x | Disjoint u x ∧ v ≤ x}
b : α
hb : b ∈ {x | Disjoint u x ∧ v ≤ x}
hab : (a ⊔ u) \ v = (b ⊔ u) \ v
⊢ ((a ⊔ u) \ v) \ u ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v

Tactic:
rw [hab]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
u v a : α
ha : a ∈ {x | Disjoint u x ∧ v ≤ x}
b : α
hb : b ∈ {x | Disjoint u x ∧ v ≤ x}
hab : (fun x => (x ⊔ u) \ v) a = (fun x => (x ⊔ u) \ v) b
⊢ ((a ⊔ u) \ v) \ u ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v

Tactic:
dsimp at hab

Result:
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
u v a : α
ha : a ∈ {x | Disjoint u x ∧ v ≤ x}
b : α
hb : b ∈ {x | Disjoint u x ∧ v ≤ x}
hab : (a ⊔ u) \ v = (b ⊔ u) \ v
⊢ ((a ⊔ u) \ v) \ u ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v

Proof state:
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
u v a : α
ha : a ∈ {x | Disjoint u x ∧ v ≤ x}
b : α
hb : b ∈ {x | Disjoint u x ∧ v ≤ x}
hab : (fun x => (x ⊔ u) \ v) a = (fun x => (x ⊔ u) \ v) b
h : ((a ⊔ u) \ v) \ u ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v
⊢ a = b

Tactic:
rwa [sdiff_sdiff_comm, ha.1.symm.sup_sdiff_cancel_right, sdiff_sdiff_comm,
  hb.1.symm.sup_sdiff_cancel_right, sdiff_sup_cancel ha.2, sdiff_sup_cancel hb.2] at h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
u v : α
⊢ Set.InjOn (fun x => (x ⊔ u) \ v) {x | Disjoint u x ∧ v ≤ x}

Tactic:
rintro a ha b hb hab

Result:
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
u v a : α
ha : a ∈ {x | Disjoint u x ∧ v ≤ x}
b : α
hb : b ∈ {x | Disjoint u x ∧ v ≤ x}
hab : (fun x => (x ⊔ u) \ v) a = (fun x => (x ⊔ u) \ v) b
⊢ a = b

Proof state:
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
u v a : α
ha : a ∈ {x | Disjoint u x ∧ v ≤ x}
b : α
hb : b ∈ {x | Disjoint u x ∧ v ≤ x}
hab : (fun x => (x ⊔ u) \ v) a = (fun x => (x ⊔ u) \ v) b
⊢ a = b

Tactic:
have h : ((a ⊔ u) \ v) \ u ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v := by
  dsimp at hab
  rw [hab]

Result:
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
u v a : α
ha : a ∈ {x | Disjoint u x ∧ v ≤ x}
b : α
hb : b ∈ {x | Disjoint u x ∧ v ≤ x}
hab : (fun x => (x ⊔ u) \ v) a = (fun x => (x ⊔ u) \ v) b
h : ((a ⊔ u) \ v) \ u ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v
⊢ a = b
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem zipIdx_eq_append_iff {l : List α} {k : Nat} :
    zipIdx l k = l₁ ++ l₂ ↔
      ∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = zipIdx l₁' k ∧ l₂ = zipIdx l₂' (k + l₁'.length)

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
k : Nat
w x : List α
y z : List Nat
h : w.length = y.length
h' : ∃ k_1, k_1 ≤ (w ++ x).length ∧ y = range' k k_1 ∧ z = range' (k + k_1) ((w ++ x).length - k_1)
⊢ ∃ l₁' l₂', w ++ x = l₁' ++ l₂' ∧ w.zip y = l₁'.zipIdx k ∧ x.zip z = l₂'.zipIdx (k + l₁'.length)

Tactic:
obtain ⟨k, -, rfl, rfl⟩ := h'

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
k✝ : Nat
w x : List α
k : Nat
h : w.length = (range' k✝ k).length
⊢ ∃ l₁' l₂',
    w ++ x = l₁' ++ l₂' ∧
      w.zip (range' k✝ k) = l₁'.zipIdx k✝ ∧ x.zip (range' (k✝ + k) ((w ++ x).length - k)) = l₂'.zipIdx (k✝ + l₁'.length)

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
k : Nat
w x : List α
⊢ x.zip (range' (k + w.length) (w.length + x.length - w.length)) = x.zip (range' (k + w.length) x.length)

Tactic:
congr

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.e_a.e_len
α : Type u_1
k : Nat
w x : List α
⊢ w.length + x.length - w.length = x.length
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_Iio_add_Ici (h_left : IntegrableOn f (Iio b) μ)
    (h_right : IntegrableOn f (Ici b) μ) :
    (∫ x in Iio b, f x ∂μ) + (∫ x in Ici b, f x ∂μ) = ∫ (x : ℝ), f x ∂μ

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℝ → E
μ : Measure ℝ
h_left : IntegrableOn f (Iio b) μ
h_right : IntegrableOn f (Ici b) μ
⊢ ∫ (x : ℝ) in Iio b, f x ∂μ + ∫ (x : ℝ) in Ici b, f x ∂μ = ∫ (x : ℝ), f x ∂μ

Tactic:
convert (setIntegral_union (Iio_disjoint_Ici <| Eq.le rfl) measurableSet_Ici h_left h_right).symm

Result:
case h.e'_3.h.e'_6
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℝ → E
μ : Measure ℝ
h_left : IntegrableOn f (Iio b) μ
h_right : IntegrableOn f (Ici b) μ
⊢ μ = μ.restrict (Iio b ∪ Ici b)

Proof state:
case h.e'_3.h.e'_6
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℝ → E
μ : Measure ℝ
h_left : IntegrableOn f (Iio b) μ
h_right : IntegrableOn f (Ici b) μ
⊢ μ = μ.restrict (Iio b ∪ Ici b)

Tactic:
rw [Iio_union_Ici, Measure.restrict_univ]

Result:
no goals
-- Mathlib/Computability/PartrecCode.lean
theorem eval_part : Partrec₂ eval :=
  (Partrec.rfindOpt
    (evaln_prim.to_comp.comp ((Computable.snd.pair (fst.comp fst)).pair (snd.comp fst))).to₂).of_eq
    fun a => by simp [eval_eq_rfindOpt]

Proof state:
a : Code × ℕ
⊢ (rfindOpt fun b =>
      evaln (((a, b).2, (a, b).1.1), (a, b).1.2).1.1 (((a, b).2, (a, b).1.1), (a, b).1.2).1.2
        (((a, b).2, (a, b).1.1), (a, b).1.2).2) =
    a.1.eval a.2

Tactic:
simp [eval_eq_rfindOpt]

Result:
no goals
-- Mathlib/Topology/MetricSpace/IsometricSMul.lean
theorem edist_inv [PseudoEMetricSpace G] [IsometricSMul G G] [IsometricSMul Gᵐᵒᵖ G]
    (x y : G) : edist x⁻¹ y = edist x y⁻¹

Proof state:
G : Type v
inst✝³ : Group G
inst✝² : PseudoEMetricSpace G
inst✝¹ : IsometricSMul G G
inst✝ : IsometricSMul Gᵐᵒᵖ G
x y : G
⊢ edist x⁻¹ y = edist x y⁻¹

Tactic:
rw [← edist_inv_inv, inv_inv]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem pmap_eq_pmapImpl : @pmap = @pmapImpl

Proof state:
⊢ @pmap = @Array.pmapImpl

Tactic:
funext α β p f L h'

Result:
case h.h.h.h.h.h
α : Type u_2
β : Type u_1
p : α → Prop
f : (a : α) → p a → β
L : Array α
h' : ∀ (a : α), a ∈ L → p a
⊢ pmap f L h' = Array.pmapImpl f L h'

Proof state:
case h.h.h.h.h.h.mk
α : Type u_2
β : Type u_1
p : α → Prop
f : (a : α) → p a → β
toList✝ : List α
h' : ∀ (a : α), a ∈ { toList := toList✝ } → p a
⊢ List.pmap f toList✝ ⋯ = List.pmap (fun a h => f a ⋯) toList✝ ⋯

Tactic:
apply List.pmap_congr_left

Result:
case h.h.h.h.h.h.mk.h
α : Type u_2
β : Type u_1
p : α → Prop
f : (a : α) → p a → β
toList✝ : List α
h' : ∀ (a : α), a ∈ { toList := toList✝ } → p a
⊢ ∀ (a : α), a ∈ toList✝ → ∀ (h₁ : p a) (h₂ : a ∈ toList✝ ∧ p a), f a h₁ = f a ⋯

Proof state:
case h.h.h.h.h.h
α : Type u_2
β : Type u_1
p : α → Prop
f : (a : α) → p a → β
L : Array α
h' : ∀ (a : α), a ∈ L → p a
⊢ pmap f L h' = Array.pmapImpl f L h'

Tactic:
cases L

Result:
case h.h.h.h.h.h.mk
α : Type u_2
β : Type u_1
p : α → Prop
f : (a : α) → p a → β
toList✝ : List α
h' : ∀ (a : α), a ∈ { toList := toList✝ } → p a
⊢ pmap f { toList := toList✝ } h' = Array.pmapImpl f { toList := toList✝ } h'

Proof state:
case h.h.h.h.h.h.mk
α : Type u_2
β : Type u_1
p : α → Prop
f : (a : α) → p a → β
toList✝ : List α
h' : ∀ (a : α), a ∈ { toList := toList✝ } → p a
⊢ pmap f { toList := toList✝ } h' = Array.pmapImpl f { toList := toList✝ } h'

Tactic:
simp only [pmap, pmapImpl, List.attachWith_toArray, List.map_toArray, mk.injEq, List.map_attachWith]

Result:
case h.h.h.h.h.h.mk
α : Type u_2
β : Type u_1
p : α → Prop
f : (a : α) → p a → β
toList✝ : List α
h' : ∀ (a : α), a ∈ { toList := toList✝ } → p a
⊢ List.pmap f toList✝ ⋯ = List.pmap (fun a h => f a ⋯) toList✝ ⋯

Proof state:
case h.h.h.h.h.h.mk.h
α : Type u_2
β : Type u_1
p : α → Prop
f : (a : α) → p a → β
toList✝ : List α
h' : ∀ (a : α), a ∈ { toList := toList✝ } → p a
⊢ ∀ (a : α), a ∈ toList✝ → ∀ (h₁ : p a) (h₂ : a ∈ toList✝ ∧ p a), f a h₁ = f a ⋯

Tactic:
intro a m h₁ h₂

Result:
case h.h.h.h.h.h.mk.h
α : Type u_2
β : Type u_1
p : α → Prop
f : (a : α) → p a → β
toList✝ : List α
h' : ∀ (a : α), a ∈ { toList := toList✝ } → p a
a : α
m : a ∈ toList✝
h₁ : p a
h₂ : a ∈ toList✝ ∧ p a
⊢ f a h₁ = f a ⋯

Proof state:
case h.h.h.h.h.h.mk.h
α : Type u_2
β : Type u_1
p : α → Prop
f : (a : α) → p a → β
toList✝ : List α
h' : ∀ (a : α), a ∈ { toList := toList✝ } → p a
a : α
m : a ∈ toList✝
h₁ : p a
h₂ : a ∈ toList✝ ∧ p a
⊢ f a h₁ = f a ⋯

Tactic:
congr

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_zero_length (x : BitVec 0) : x.toNat = 0

Proof state:
x : BitVec 0
⊢ x.toNat = 0

Tactic:
simp [of_length_zero]

Result:
no goals