harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Monoidal/Bimod.lean
theorem whiskerLeft_π_actLeft :
    (R.X ◁ coequalizer.π _ _) ≫ actLeft P Q =
      (α_ _ _ _).inv ≫ (P.actLeft ▷ Q.X) ≫ coequalizer.π _ _

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon_ C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
⊢ R.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ actLeft P Q =
    (α_ R.X P.X Q.X).inv ≫ P.actLeft ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

Tactic:
erw [map_π_preserves_coequalizer_inv_colimMap (tensorLeft _)]

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon_ C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
⊢ ((α_ R.X P.X Q.X).inv ≫ P.actLeft ▷ Q.X) ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) =
    (α_ R.X P.X Q.X).inv ≫ P.actLeft ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon_ C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
⊢ ((α_ R.X P.X Q.X).inv ≫ P.actLeft ▷ Q.X) ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) =
    (α_ R.X P.X Q.X).inv ≫ P.actLeft ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

Tactic:
simp only [Category.assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem init_eq_of_concat_eq {a b : α} {l₁ l₂ : List α} : concat l₁ a = concat l₂ b → l₁ = l₂

Proof state:
α : Type u_1
a b : α
l₁ l₂ : List α
h : l₁ ++ [a] = l₂ ++ [b]
⊢ l₁ = l₂

Tactic:
apply append_inj_left' h (by simp)

Result:
no goals

Proof state:
α : Type u_1
a b : α
l₁ l₂ : List α
⊢ l₁ ++ [a] = l₂ ++ [b] → l₁ = l₂

Tactic:
intro h

Result:
α : Type u_1
a b : α
l₁ l₂ : List α
h : l₁ ++ [a] = l₂ ++ [b]
⊢ l₁ = l₂

Proof state:
α : Type u_1
a b : α
l₁ l₂ : List α
⊢ l₁.concat a = l₂.concat b → l₁ = l₂

Tactic:
simp only [concat_eq_append]

Result:
α : Type u_1
a b : α
l₁ l₂ : List α
⊢ l₁ ++ [a] = l₂ ++ [b] → l₁ = l₂

Proof state:
α : Type u_1
a b : α
l₁ l₂ : List α
h : l₁ ++ [a] = l₂ ++ [b]
⊢ [a].length = [b].length

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
lemma rpow_add_natCast (hx : x ≠ 0) (y : ℝ) (n : ℕ) : x ^ (y + n) = x ^ y * x ^ n

Proof state:
case a
x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ ↑(x ^ (y + ↑n)) = ↑(x ^ y * x ^ n)

Tactic:
exact Real.rpow_add_natCast (mod_cast hx) _ _

Result:
no goals

Proof state:
x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ x ^ (y + ↑n) = x ^ y * x ^ n

Tactic:
ext

Result:
case a
x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ ↑(x ^ (y + ↑n)) = ↑(x ^ y * x ^ n)
-- Mathlib/Topology/MetricSpace/HausdorffDimension.lean
theorem iSup_limsup_dimH (s : Set X) : ⨆ x, limsup dimH (𝓝[s] x).smallSets = dimH s

Proof state:
case refine_1
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
x : X
⊢ limsup dimH (𝓝[s] x).smallSets ≤ dimH s

Tactic:
refine limsup_le_of_le isCobounded_le_of_bot ?_

Result:
case refine_1
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
x : X
⊢ ∀ᶠ (n : Set X) in (𝓝[s] x).smallSets, dimH n ≤ dimH s

Proof state:
case refine_1
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
x : X
⊢ ∀ᶠ (n : Set X) in (𝓝[s] x).smallSets, dimH n ≤ dimH s

Tactic:
exact eventually_smallSets.2 ⟨s, self_mem_nhdsWithin, fun t => dimH_mono⟩

Result:
no goals

Proof state:
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
⊢ ⨆ x, limsup dimH (𝓝[s] x).smallSets = dimH s

Tactic:
refine le_antisymm (iSup_le fun x => ?_) ?_

Result:
case refine_1
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
x : X
⊢ limsup dimH (𝓝[s] x).smallSets ≤ dimH s

case refine_2
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
⊢ dimH s ≤ ⨆ x, limsup dimH (𝓝[s] x).smallSets

Proof state:
case refine_2
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
⊢ dimH s ≤ ⨆ x, limsup dimH (𝓝[s] x).smallSets

Tactic:
rw [← bsupr_limsup_dimH]

Result:
case refine_2
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
⊢ ⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets ≤ ⨆ x, limsup dimH (𝓝[s] x).smallSets

Proof state:
case refine_2
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
⊢ ⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets ≤ ⨆ x, limsup dimH (𝓝[s] x).smallSets

Tactic:
exact iSup₂_le_iSup _ _

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
theorem eigenspace_restrict_le_eigenspace (f : End R M) {p : Submodule R M} (hfp : ∀ x ∈ p, f x ∈ p)
    (μ : R) : (eigenspace (f.restrict hfp) μ).map p.subtype ≤ f.eigenspace μ

Proof state:
case intro.intro
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hfp : ∀ x ∈ p, f x ∈ p
μ : R
x : ↥p
hx : x ∈ ↑(eigenspace (LinearMap.restrict f hfp) μ)
⊢ p.subtype x ∈ f.eigenspace μ

Tactic:
simp only [SetLike.mem_coe, mem_eigenspace_iff, LinearMap.restrict_apply] at hx ⊢

Result:
case intro.intro
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hfp : ∀ x ∈ p, f x ∈ p
μ : R
x : ↥p
hx : ⟨f ↑x, ⋯⟩ = μ • x
⊢ f (p.subtype x) = μ • p.subtype x

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hfp : ∀ x ∈ p, f x ∈ p
μ : R
⊢ Submodule.map p.subtype (eigenspace (LinearMap.restrict f hfp) μ) ≤ f.eigenspace μ

Tactic:
rintro a ⟨x, hx, rfl⟩

Result:
case intro.intro
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hfp : ∀ x ∈ p, f x ∈ p
μ : R
x : ↥p
hx : x ∈ ↑(eigenspace (LinearMap.restrict f hfp) μ)
⊢ p.subtype x ∈ f.eigenspace μ

Proof state:
case intro.intro
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hfp : ∀ x ∈ p, f x ∈ p
μ : R
x : ↥p
hx : ⟨f ↑x, ⋯⟩ = μ • x
⊢ f (p.subtype x) = μ • p.subtype x

Tactic:
exact congr_arg Subtype.val hx

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem edgeSet_sdiff_sdiff_isDiag (G : SimpleGraph V) (s : Set (Sym2 V)) :
    G.edgeSet \ (s \ { e | e.IsDiag }) = G.edgeSet \ s

Proof state:
case h
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
e : Sym2 V
⊢ e ∈ G.edgeSet → (e ∈ s → e.IsDiag ↔ e ∉ s)

Tactic:
intro h

Result:
case h
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
e : Sym2 V
h : e ∈ G.edgeSet
⊢ e ∈ s → e.IsDiag ↔ e ∉ s

Proof state:
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
⊢ G.edgeSet \ (s \ {e | e.IsDiag}) = G.edgeSet \ s

Tactic:
ext e

Result:
case h
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
e : Sym2 V
⊢ e ∈ G.edgeSet \ (s \ {e | e.IsDiag}) ↔ e ∈ G.edgeSet \ s

Proof state:
case h
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
e : Sym2 V
h : e ∈ G.edgeSet
⊢ e ∈ s → e.IsDiag ↔ e ∉ s

Tactic:
simp only [G.not_isDiag_of_mem_edgeSet h, imp_false]

Result:
no goals

Proof state:
case h
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
e : Sym2 V
⊢ e ∈ G.edgeSet \ (s \ {e | e.IsDiag}) ↔ e ∈ G.edgeSet \ s

Tactic:
simp only [Set.mem_diff, Set.mem_setOf_eq, not_and, not_not, and_congr_right_iff]

Result:
case h
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
e : Sym2 V
⊢ e ∈ G.edgeSet → (e ∈ s → e.IsDiag ↔ e ∉ s)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem zip_map (f : α → γ) (g : β → δ) (l₁ : Vector α n) (l₂ : Vector β n) :
    zip (l₁.map f) (l₂.map g) = (zip l₁ l₂).map (Prod.map f g)

Proof state:
case mk.mk
α : Type u_1
γ : Type u_2
β : Type u_3
δ : Type u_4
f : α → γ
g : β → δ
l₁ : Array α
l₂ : Array β
h : l₂.size = l₁.size
⊢ (map f { toArray := l₁, size_toArray := ⋯ }).zip (map g { toArray := l₂, size_toArray := h }) =
    map (Prod.map f g) ({ toArray := l₁, size_toArray := ⋯ }.zip { toArray := l₂, size_toArray := h })

Tactic:
simp [Array.zip_map, h]

Result:
no goals

Proof state:
case mk
α : Type u_1
γ : Type u_2
β : Type u_3
δ : Type u_4
f : α → γ
g : β → δ
l₁ : Array α
l₂ : Vector β l₁.size
⊢ (map f { toArray := l₁, size_toArray := ⋯ }).zip (map g l₂) =
    map (Prod.map f g) ({ toArray := l₁, size_toArray := ⋯ }.zip l₂)

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

Result:
case mk.mk
α : Type u_1
γ : Type u_2
β : Type u_3
δ : Type u_4
f : α → γ
g : β → δ
l₁ : Array α
l₂ : Array β
h : l₂.size = l₁.size
⊢ (map f { toArray := l₁, size_toArray := ⋯ }).zip (map g { toArray := l₂, size_toArray := h }) =
    map (Prod.map f g) ({ toArray := l₁, size_toArray := ⋯ }.zip { toArray := l₂, size_toArray := h })

Proof state:
α : Type u_1
γ : Type u_2
β : Type u_3
δ : Type u_4
n : Nat
f : α → γ
g : β → δ
l₁ : Vector α n
l₂ : Vector β n
⊢ (map f l₁).zip (map g l₂) = map (Prod.map f g) (l₁.zip l₂)

Tactic:
rcases l₁ with ⟨l₁, rfl⟩

Result:
case mk
α : Type u_1
γ : Type u_2
β : Type u_3
δ : Type u_4
f : α → γ
g : β → δ
l₁ : Array α
l₂ : Vector β l₁.size
⊢ (map f { toArray := l₁, size_toArray := ⋯ }).zip (map g l₂) =
    map (Prod.map f g) ({ toArray := l₁, size_toArray := ⋯ }.zip l₂)
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem snd_invOf (x : tsze R M) [Invertible x] [Invertible x.fst] :
    (⅟x).snd = -(⅟x.fst •> x.snd <• ⅟x.fst)

Proof state:
R : Type u
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Semiring R
inst✝⁴ : Module Rᵐᵒᵖ M
inst✝³ : Module R M
inst✝² : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
inst✝¹ : Invertible x
inst✝ : Invertible x.fst
⊢ (⅟x).snd = -(⅟x.fst •> x.snd <• ⅟x.fst)

Tactic:
letI := invertibleOfInvertibleFst x

Result:
R : Type u
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Semiring R
inst✝⁴ : Module Rᵐᵒᵖ M
inst✝³ : Module R M
inst✝² : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
inst✝¹ : Invertible x
inst✝ : Invertible x.fst
this : Invertible x := x.invertibleOfInvertibleFst
⊢ (⅟x).snd = -(⅟x.fst •> x.snd <• ⅟x.fst)

Proof state:
case convert_2
R : Type u
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Semiring R
inst✝⁴ : Module Rᵐᵒᵖ M
inst✝³ : Module R M
inst✝² : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
inst✝¹ : Invertible x
inst✝ : Invertible x.fst
this : Invertible x := x.invertibleOfInvertibleFst
⊢ ⅟x = ⅟x

Tactic:
convert rfl

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Semiring R
inst✝⁴ : Module Rᵐᵒᵖ M
inst✝³ : Module R M
inst✝² : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
inst✝¹ : Invertible x
inst✝ : Invertible x.fst
this : Invertible x := x.invertibleOfInvertibleFst
⊢ (⅟x).snd = -(⅟x.fst •> x.snd <• ⅟x.fst)

Tactic:
convert congr_arg (TrivSqZeroExt.snd (R := R) (M := M)) (_ : _ = ⅟ x)

Result:
case convert_2
R : Type u
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Semiring R
inst✝⁴ : Module Rᵐᵒᵖ M
inst✝³ : Module R M
inst✝² : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
inst✝¹ : Invertible x
inst✝ : Invertible x.fst
this : Invertible x := x.invertibleOfInvertibleFst
⊢ ⅟x = ⅟x
-- Mathlib/Data/List/Sigma.lean
theorem nodup_zipIdx_map_snd (l : List α) : (l.zipIdx.map Prod.snd).Nodup

Proof state:
α : Type u
l : List α
⊢ (map Prod.snd l.zipIdx).Nodup

Tactic:
simp [List.nodup_range']

Result:
no goals
-- Mathlib/GroupTheory/Complement.lean
theorem isComplement_univ_left : IsComplement univ S ↔ ∃ g : G, S = {g}

Proof state:
case refine_3.intro
G : Type u_1
inst✝ : Group G
g : G
⊢ IsComplement univ {g}

Tactic:
exact isComplement_univ_singleton

Result:
no goals

Proof state:
case refine_2
G : Type u_1
inst✝ : Group G
S : Set G
h : IsComplement univ S
a : G
ha : a ∈ S
b : G
hb : b ∈ S
⊢ a = b

Tactic:
have : (⟨⟨_, mem_top a⁻¹⟩, ⟨a, ha⟩⟩ : (⊤ : Set G) × S) = ⟨⟨_, mem_top b⁻¹⟩, ⟨b, hb⟩⟩ :=
  h.1 ((inv_mul_cancel a).trans (inv_mul_cancel b).symm)

Result:
case refine_2
G : Type u_1
inst✝ : Group G
S : Set G
h : IsComplement univ S
a : G
ha : a ∈ S
b : G
hb : b ∈ S
this : (⟨a⁻¹, ⋯⟩, ⟨a, ha⟩) = (⟨b⁻¹, ⋯⟩, ⟨b, hb⟩)
⊢ a = b

Proof state:
case refine_1
G : Type u_1
inst✝ : Group G
S : Set G
h : IsComplement univ S
⊢ S.Nonempty

Tactic:
obtain ⟨a, _⟩ := h.2 1

Result:
case refine_1.intro
G : Type u_1
inst✝ : Group G
S : Set G
h : IsComplement univ S
a : ↑univ × ↑S
h✝ : (fun x => ↑x.1 * ↑x.2) a = 1
⊢ S.Nonempty

Proof state:
case refine_3
G : Type u_1
inst✝ : Group G
S : Set G
⊢ (∃ g, S = {g}) → IsComplement univ S

Tactic:
rintro ⟨g, rfl⟩

Result:
case refine_3.intro
G : Type u_1
inst✝ : Group G
g : G
⊢ IsComplement univ {g}

Proof state:
G : Type u_1
inst✝ : Group G
S : Set G
⊢ IsComplement univ S ↔ ∃ g, S = {g}

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

Result:
case refine_1
G : Type u_1
inst✝ : Group G
S : Set G
h : IsComplement univ S
⊢ S.Nonempty

case refine_2
G : Type u_1
inst✝ : Group G
S : Set G
h : IsComplement univ S
a : G
ha : a ∈ S
b : G
hb : b ∈ S
⊢ a = b

case refine_3
G : Type u_1
inst✝ : Group G
S : Set G
⊢ (∃ g, S = {g}) → IsComplement univ S

Proof state:
case refine_2
G : Type u_1
inst✝ : Group G
S : Set G
h : IsComplement univ S
a : G
ha : a ∈ S
b : G
hb : b ∈ S
this : (⟨a⁻¹, ⋯⟩, ⟨a, ha⟩) = (⟨b⁻¹, ⋯⟩, ⟨b, hb⟩)
⊢ a = b

Tactic:
exact Subtype.ext_iff.mp (Prod.ext_iff.mp this).2

Result:
no goals

Proof state:
case refine_1.intro
G : Type u_1
inst✝ : Group G
S : Set G
h : IsComplement univ S
a : ↑univ × ↑S
h✝ : (fun x => ↑x.1 * ↑x.2) a = 1
⊢ S.Nonempty

Tactic:
exact ⟨a.2.1, a.2.2⟩

Result:
no goals
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem isTotallyDisconnected_iff :
    S.IsTotallyDisconnected ↔ ∀ c d, (S.arrows c d).Nonempty → c = d

Proof state:
case mpr.mk.mk.mk
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
h : ∀ (c d : C), (S.arrows c d).Nonempty → c = d
c : C
hc : c ∈ S.objs
d : C
hd : d ∈ S.objs
f : ↑⟨c, hc⟩ ⟶ ↑⟨d, hd⟩
fS : f ∈ S.arrows ↑⟨c, hc⟩ ↑⟨d, hd⟩
⊢ ⟨c, hc⟩ = ⟨d, hd⟩

Tactic:
simp only [Subtype.mk_eq_mk]

Result:
case mpr.mk.mk.mk
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
h : ∀ (c d : C), (S.arrows c d).Nonempty → c = d
c : C
hc : c ∈ S.objs
d : C
hd : d ∈ S.objs
f : ↑⟨c, hc⟩ ⟶ ↑⟨d, hd⟩
fS : f ∈ S.arrows ↑⟨c, hc⟩ ↑⟨d, hd⟩
⊢ c = d

Proof state:
case mpr.mk.mk.mk
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
h : ∀ (c d : C), (S.arrows c d).Nonempty → c = d
c : C
hc : c ∈ S.objs
d : C
hd : d ∈ S.objs
f : ↑⟨c, hc⟩ ⟶ ↑⟨d, hd⟩
fS : f ∈ S.arrows ↑⟨c, hc⟩ ↑⟨d, hd⟩
⊢ c = d

Tactic:
exact h c d ⟨f, fS⟩

Result:
no goals

Proof state:
case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ (∀ (c d : C), (S.arrows c d).Nonempty → c = d) → S.IsTotallyDisconnected

Tactic:
rintro h ⟨c, hc⟩ ⟨d, hd⟩ ⟨f, fS⟩

Result:
case mpr.mk.mk.mk
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
h : ∀ (c d : C), (S.arrows c d).Nonempty → c = d
c : C
hc : c ∈ S.objs
d : C
hd : d ∈ S.objs
f : ↑⟨c, hc⟩ ⟶ ↑⟨d, hd⟩
fS : f ∈ S.arrows ↑⟨c, hc⟩ ↑⟨d, hd⟩
⊢ ⟨c, hc⟩ = ⟨d, hd⟩

Proof state:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ S.IsTotallyDisconnected → ∀ (c d : C), (S.arrows c d).Nonempty → c = d

Tactic:
rintro h c d ⟨f, fS⟩

Result:
case mp.intro
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
h : S.IsTotallyDisconnected
c d : C
f : c ⟶ d
fS : f ∈ S.arrows c d
⊢ c = d

Proof state:
case mp.intro
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
h : S.IsTotallyDisconnected
c d : C
f : c ⟶ d
fS : f ∈ S.arrows c d
⊢ c = d

Tactic:
exact congr_arg Subtype.val <| h ⟨c, mem_objs_of_src S fS⟩ ⟨d, mem_objs_of_tgt S fS⟩ ⟨f, fS⟩

Result:
no goals

Proof state:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ S.IsTotallyDisconnected ↔ ∀ (c d : C), (S.arrows c d).Nonempty → c = d

Tactic:
constructor

Result:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ S.IsTotallyDisconnected → ∀ (c d : C), (S.arrows c d).Nonempty → c = d

case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ (∀ (c d : C), (S.arrows c d).Nonempty → c = d) → S.IsTotallyDisconnected
-- Mathlib/Order/Cover.lean
theorem mk_covBy_mk_iff : (a₁, b₁) ⋖ (a₂, b₂) ↔ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂

Proof state:
case refine_2.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ : β
h : a₁ ⋖ a₂
⊢ (a₁, b₁) ⋖ (a₂, b₁)

Tactic:
exact mk_covBy_mk_iff_left.2 h

Result:
no goals

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
⊢ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂ → (a₁, b₁) ⋖ (a₂, b₂)

Tactic:
rintro (⟨h, rfl⟩ | ⟨h, rfl⟩)

Result:
case refine_2.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ : β
h : a₁ ⋖ a₂
⊢ (a₁, b₁) ⋖ (a₂, b₁)

case refine_2.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ : α
b₁ b₂ : β
h : b₁ ⋖ b₂
⊢ (a₁, b₁) ⋖ (a₁, b₂)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
⊢ (a₁, b₁) ⋖ (a₂, b₂) ↔ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂

Tactic:
refine ⟨fun h => ?_, ?_⟩

Result:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
h : (a₁, b₁) ⋖ (a₂, b₂)
⊢ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂

case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
⊢ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂ → (a₁, b₁) ⋖ (a₂, b₂)

Proof state:
case refine_2.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ : α
b₁ b₂ : β
h : b₁ ⋖ b₂
⊢ (a₁, b₁) ⋖ (a₁, b₂)

Tactic:
exact mk_covBy_mk_iff_right.2 h

Result:
no goals

Proof state:
case refine_1.inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ : β
h : (a₁, b₁) ⋖ (a₂, b₁)
⊢ a₁ ⋖ a₂ ∧ b₁ = b₁ ∨ b₁ ⋖ b₁ ∧ a₁ = a₂

Tactic:
exact Or.inl ⟨mk_covBy_mk_iff_left.1 h, rfl⟩

Result:
no goals

Proof state:
case refine_1.inl
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ : α
b₁ b₂ : β
h : (a₁, b₁) ⋖ (a₁, b₂)
⊢ a₁ ⋖ a₁ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₁

Tactic:
exact Or.inr ⟨mk_covBy_mk_iff_right.1 h, rfl⟩

Result:
no goals

Proof state:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
h : (a₁, b₁) ⋖ (a₂, b₂)
⊢ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂

Tactic:
obtain rfl | rfl : a₁ = a₂ ∨ b₁ = b₂ := fst_eq_or_snd_eq_of_wcovBy h.wcovBy

Result:
case refine_1.inl
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ : α
b₁ b₂ : β
h : (a₁, b₁) ⋖ (a₁, b₂)
⊢ a₁ ⋖ a₁ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₁

case refine_1.inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ : β
h : (a₁, b₁) ⋖ (a₂, b₁)
⊢ a₁ ⋖ a₂ ∧ b₁ = b₁ ∨ b₁ ⋖ b₁ ∧ a₁ = a₂
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem zero_of_epi_comp {X Y Z : C} (f : X ⟶ Y) {g : Y ⟶ Z} [Epi f] (h : f ≫ g = 0) : g = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Epi f
h : f ≫ g = 0
⊢ g = 0

Tactic:
rw [← comp_zero, cancel_epi] at h

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Epi f
h✝ : f ≫ g = 0
h : g = 0
⊢ g = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Epi f
h✝ : f ≫ g = 0
h : g = 0
⊢ g = 0

Tactic:
exact h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CNF.lean
theorem atomToCNF_eval :
    (atomToCNF output a).eval assign
      =
    (assign output == assign a)

Proof state:
α✝ : Type u_1
output a : α✝
assign : α✝ → Bool
⊢ CNF.eval assign (atomToCNF output a) = (assign output == assign a)

Tactic:
simp only [atomToCNF, CNF.eval_cons, CNF.Clause.eval_cons, beq_true, beq_false,
  CNF.Clause.eval_nil, Bool.or_false, CNF.eval_nil, Bool.and_true]

Result:
α✝ : Type u_1
output a : α✝
assign : α✝ → Bool
⊢ ((assign output || !assign a) && (!assign output || assign a)) = (assign output == assign a)

Proof state:
α✝ : Type u_1
output a : α✝
assign : α✝ → Bool
⊢ ((assign output || !assign a) && (!assign output || assign a)) = (assign output == assign a)

Tactic:
cases assign output <;> cases assign a <;> decide

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
/-- Binary entropy is strictly increasing in interval [0, 1/2]. -/
lemma binEntropy_strictMonoOn : StrictMonoOn binEntropy (Icc 0 2⁻¹)

Proof state:
⊢ Icc 0 2⁻¹ = Icc 0 (1 - 1 / 2)

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ 2 ≤ 2

Tactic:
rfl

Result:
no goals

Proof state:
⊢ StrictMonoOn (qaryEntropy 2) (Icc 0 (1 - 1 / 2))

Tactic:
exact qaryEntropy_strictMonoOn (by rfl)

Result:
no goals

Proof state:
⊢ StrictMonoOn binEntropy (Icc 0 2⁻¹)

Tactic:
rw [show Icc (0 : ℝ) 2⁻¹ = Icc 0 (1 - 1/2) by norm_num, ← qaryEntropy_two]

Result:
⊢ StrictMonoOn (qaryEntropy 2) (Icc 0 (1 - 1 / 2))
-- Mathlib/Data/List/Sublists.lean
theorem nodup_sublists' {l : List α} : Nodup (sublists' l) ↔ Nodup l

Proof state:
α : Type u
l : List α
⊢ l.sublists'.Nodup ↔ l.Nodup

Tactic:
rw [sublists'_eq_sublists, nodup_map_iff reverse_injective, nodup_sublists, nodup_reverse]

Result:
no goals
-- Mathlib/ModelTheory/Satisfiability.lean
theorem exists_elementaryEmbedding_card_eq (M : Type w') [L.Structure M] [iM : Infinite M]
    (κ : Cardinal.{w}) (h1 : ℵ₀ ≤ κ) (h2 : lift.{w} L.card ≤ Cardinal.lift.{max u v} κ) :
    ∃ N : Bundled L.Structure, (Nonempty (N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] N)) ∧ #N = κ

Proof state:
case inr
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h : lift.{w', w} κ > lift.{w, w'} #M
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ #↑N = κ

Tactic:
obtain ⟨N, hN1, hN2⟩ := exists_elementaryEmbedding_card_eq_of_ge L M κ h2 (le_of_lt h)

Result:
case inr.intro.intro
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h : lift.{w', w} κ > lift.{w, w'} #M
N : Bundled L.Structure
hN1 : Nonempty (M ↪ₑ[L] ↑N)
hN2 : #↑N = κ
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ #↑N = κ

Proof state:
case inr.intro.intro
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h : lift.{w', w} κ > lift.{w, w'} #M
N : Bundled L.Structure
hN1 : Nonempty (M ↪ₑ[L] ↑N)
hN2 : #↑N = κ
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ #↑N = κ

Tactic:
exact ⟨N, Or.inr hN1, hN2⟩

Result:
no goals

Proof state:
case inl
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h : lift.{w', w} κ ≤ lift.{w, w'} #M
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ #↑N = κ

Tactic:
obtain ⟨N, hN1, hN2⟩ := exists_elementaryEmbedding_card_eq_of_le L M κ h1 h2 h

Result:
case inl.intro.intro
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h : lift.{w', w} κ ≤ lift.{w, w'} #M
N : Bundled L.Structure
hN1 : Nonempty (↑N ↪ₑ[L] M)
hN2 : #↑N = κ
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ #↑N = κ

Proof state:
case inl.intro.intro
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h : lift.{w', w} κ ≤ lift.{w, w'} #M
N : Bundled L.Structure
hN1 : Nonempty (↑N ↪ₑ[L] M)
hN2 : #↑N = κ
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ #↑N = κ

Tactic:
exact ⟨N, Or.inl hN1, hN2⟩

Result:
no goals

Proof state:
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ #↑N = κ

Tactic:
cases le_or_gt (lift.{w'} κ) (Cardinal.lift.{w} #M) with
| inl h =>
  obtain ⟨N, hN1, hN2⟩ := exists_elementaryEmbedding_card_eq_of_le L M κ h1 h2 h
  exact ⟨N, Or.inl hN1, hN2⟩
| inr h =>
  obtain ⟨N, hN1, hN2⟩ := exists_elementaryEmbedding_card_eq_of_ge L M κ h2 (le_of_lt h)
  exact ⟨N, Or.inr hN1, hN2⟩

Result:
no goals