harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem mem_span_insert' {x y} {s : Set M} :
    x ∈ span R (insert y s) ↔ ∃ a : R, x + a • y ∈ span R s

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
y : M
s : Set M
a : R
z : M
hz : z ∈ span R s
⊢ a • y + z + -a • y ∈ span R s

Tactic:
simp [hz, add_assoc]

Result:
no goals

Proof state:
case mpr.intro
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
s : Set M
a : R
h : x + a • y ∈ span R s
⊢ ∃ a, ∃ z ∈ span R s, x = a • y + z

Tactic:
exact ⟨-a, _, h, by simp [add_comm, add_left_comm]⟩

Result:
no goals

Proof state:
case mpr
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
s : Set M
⊢ (∃ a, x + a • y ∈ span R s) → ∃ a, ∃ z ∈ span R s, x = a • y + z

Tactic:
rintro ⟨a, h⟩

Result:
case mpr.intro
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
s : Set M
a : R
h : x + a • y ∈ span R s
⊢ ∃ a, ∃ z ∈ span R s, x = a • y + z

Proof state:
case mp
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
s : Set M
⊢ (∃ a, ∃ z ∈ span R s, x = a • y + z) → ∃ a, x + a • y ∈ span R s

Tactic:
rintro ⟨a, z, hz, rfl⟩

Result:
case mp.intro.intro.intro
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
y : M
s : Set M
a : R
z : M
hz : z ∈ span R s
⊢ ∃ a_1, a • y + z + a_1 • y ∈ span R s

Proof state:
case mp.intro.intro.intro
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
y : M
s : Set M
a : R
z : M
hz : z ∈ span R s
⊢ ∃ a_1, a • y + z + a_1 • y ∈ span R s

Tactic:
exact ⟨-a, by simp [hz, add_assoc]⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
s : Set M
⊢ x ∈ span R (insert y s) ↔ ∃ a, x + a • y ∈ span R s

Tactic:
rw [mem_span_insert]

Result:
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
s : Set M
⊢ (∃ a, ∃ z ∈ span R s, x = a • y + z) ↔ ∃ a, x + a • y ∈ span R s

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
s : Set M
⊢ (∃ a, ∃ z ∈ span R s, x = a • y + z) ↔ ∃ a, x + a • y ∈ span R s

Tactic:
constructor

Result:
case mp
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
s : Set M
⊢ (∃ a, ∃ z ∈ span R s, x = a • y + z) → ∃ a, x + a • y ∈ span R s

case mpr
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
s : Set M
⊢ (∃ a, x + a • y ∈ span R s) → ∃ a, ∃ z ∈ span R s, x = a • y + z

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
s : Set M
a : R
h : x + a • y ∈ span R s
⊢ x = -a • y + (x + a • y)

Tactic:
simp [add_comm, add_left_comm]

Result:
no goals
-- Mathlib/RingTheory/RingHomProperties.lean
theorem RespectsIso.cancel_left_isIso (hP : RespectsIso @P) {R S T : CommRingCat} (f : R ⟶ S)
    (g : S ⟶ T) [IsIso f] : P (g.hom.comp f.hom) ↔ P g.hom :=
  ⟨fun H => by
    convert hP.2 (f ≫ g).hom (asIso f).symm.commRingCatIsoToRingEquiv H
    simp [← CommRingCat.hom_comp], hP.2 g.hom (asIso f).commRingCatIsoToRingEquiv⟩

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
inst✝ : IsIso f
H : P ((CommRingCat.Hom.hom g).comp (CommRingCat.Hom.hom f))
⊢ P (CommRingCat.Hom.hom g)

Tactic:
convert hP.2 (f ≫ g).hom (asIso f).symm.commRingCatIsoToRingEquiv H

Result:
case h.e'_5
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
inst✝ : IsIso f
H : P ((CommRingCat.Hom.hom g).comp (CommRingCat.Hom.hom f))
⊢ CommRingCat.Hom.hom g = (CommRingCat.Hom.hom (f ≫ g)).comp (asIso f).symm.commRingCatIsoToRingEquiv.toRingHom

Proof state:
case h.e'_5
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
inst✝ : IsIso f
H : P ((CommRingCat.Hom.hom g).comp (CommRingCat.Hom.hom f))
⊢ CommRingCat.Hom.hom g = (CommRingCat.Hom.hom (f ≫ g)).comp (asIso f).symm.commRingCatIsoToRingEquiv.toRingHom

Tactic:
simp [← CommRingCat.hom_comp]

Result:
no goals
-- Mathlib/CategoryTheory/EpiMono.lean
theorem isIso_of_epi_of_isSplitMono {X Y : C} (f : X ⟶ Y) [IsSplitMono f] [Epi f] : IsIso f :=
  ⟨⟨retraction f, ⟨by simp, by simp [← cancel_epi f]⟩⟩⟩

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝¹ : IsSplitMono f
inst✝ : Epi f
⊢ retraction f ≫ f = 𝟙 Y

Tactic:
simp [← cancel_epi f]

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝¹ : IsSplitMono f
inst✝ : Epi f
⊢ f ≫ retraction f = 𝟙 X

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
theorem of_sections
    (h : ∀ x, ∃ g : Y → X, ContinuousAt g (f x) ∧ g (f x) = x ∧ RightInverse g f) : IsOpenMap f :=
  of_nhds_le fun x =>
    let ⟨g, hgc, hgx, hgf⟩ := h x
    calc
      𝓝 (f x) = map f (map g (𝓝 (f x)))

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (x : X), ∃ g, ContinuousAt g (f x) ∧ g (f x) = x ∧ RightInverse g f
x : X
g : Y → X
hgc : ContinuousAt g (f x)
hgx : g (f x) = x
hgf : RightInverse g f
⊢ map f (𝓝 (g (f x))) = map f (𝓝 x)

Tactic:
rw [hgx]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (x : X), ∃ g, ContinuousAt g (f x) ∧ g (f x) = x ∧ RightInverse g f
x : X
g : Y → X
hgc : ContinuousAt g (f x)
hgx : g (f x) = x
hgf : RightInverse g f
⊢ 𝓝 (f x) = map f (map g (𝓝 (f x)))

Tactic:
rw [map_map, hgf.comp_eq_id, map_id]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Finrank.lean
theorem finrank_lt_of_rank_lt {n : ℕ} (h : Module.rank R M < ↑n) : finrank R M < n

Proof state:
case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M < ↑n
⊢ ↑n < ℵ₀

Tactic:
exact nat_lt_aleph0 n

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M < ↑n
⊢ finrank R M < n

Tactic:
rwa [← Cardinal.toNat_lt_iff_lt_of_lt_aleph0, toNat_natCast] at h

Result:
case hc
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M < ↑n
⊢ Module.rank R M < ℵ₀

case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M < ↑n
⊢ ↑n < ℵ₀

Proof state:
case hc
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M < ↑n
⊢ Module.rank R M < ℵ₀

Tactic:
exact h.trans (nat_lt_aleph0 n)

Result:
no goals
-- Mathlib/RingTheory/Coalgebra/Basic.lean
theorem comul_comp_fst :
    comul ∘ₗ .fst R A B = TensorProduct.map (.fst R A B) (.fst R A B) ∘ₗ comul

Proof state:
case hl
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ (comul ∘ₗ LinearMap.fst R A B) ∘ₗ inl R A B =
    (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B

Tactic:
rw [comp_assoc, fst_comp_inl, comp_id, comp_assoc, comul_comp_inl, ← comp_assoc,
  ← TensorProduct.map_comp, fst_comp_inl, TensorProduct.map_id, id_comp]

Result:
no goals

Proof state:
case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ (comul ∘ₗ LinearMap.fst R A B) ∘ₗ inr R A B =
    (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inr R A B

Tactic:
rw [comp_assoc, fst_comp_inr, comp_zero, comp_assoc, comul_comp_inr, ← comp_assoc,
  ← TensorProduct.map_comp, fst_comp_inr, TensorProduct.map_zero_left, zero_comp]

Result:
no goals

Proof state:
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ comul ∘ₗ LinearMap.fst R A B = TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul

Tactic:
ext : 1

Result:
case hl
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ (comul ∘ₗ LinearMap.fst R A B) ∘ₗ inl R A B =
    (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B

case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ (comul ∘ₗ LinearMap.fst R A B) ∘ₗ inr R A B =
    (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inr R A B
-- Mathlib/FieldTheory/PurelyInseparable/PerfectClosure.lean
theorem mem_perfectClosure_iff_natSepDegree_eq_one {x : E} :
    x ∈ perfectClosure F E ↔ (minpoly F x).natSepDegree = 1

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
⊢ x ∈ perfectClosure F E ↔ (minpoly F x).natSepDegree = 1

Tactic:
rw [mem_perfectClosure_iff, minpoly.natSepDegree_eq_one_iff_pow_mem (ringExpChar F)]

Result:
no goals
-- Mathlib/GroupTheory/OreLocalization/Basic.lean
theorem one_div_smul {r : X} {s t : S} : ((1 : R) /ₒ t) • (r /ₒ s) = r /ₒ (s * t)

Proof state:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r : X
s t : ↥S
⊢ ↑s * 1 = 1 * ↑s

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r : X
s t : ↥S
⊢ (1 /ₒ t) • (r /ₒ s) = r /ₒ (s * t)

Tactic:
simp [oreDiv_smul_char 1 r t s 1 s (by simp)]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Sieves.lean
lemma mem_functorPushforward_iff_of_full_of_faithful [F.Full] [F.Faithful]
    {X Y : C} (R : Sieve X) (f : Y ⟶ X) :
    (R.arrows.functorPushforward F) (F.map f) ↔ R f

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : C
R : Sieve X
f : Y ⟶ X
⊢ Presieve.functorPushforward F R.arrows (F.map f) ↔ R.arrows f

Tactic:
rw [Sieve.mem_functorPushforward_iff_of_full]

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : C
R : Sieve X
f : Y ⟶ X
⊢ (∃ g, F.map g = F.map f ∧ R.arrows g) ↔ R.arrows f

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : C
R : Sieve X
f : Y ⟶ X
⊢ (∃ g, F.map g = F.map f ∧ R.arrows g) ↔ R.arrows f

Tactic:
refine ⟨fun ⟨g, hcomp, hg⟩ ↦ ?_, fun hf ↦ ⟨f, rfl, hf⟩⟩

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : C
R : Sieve X
f : Y ⟶ X
x✝ : ∃ g, F.map g = F.map f ∧ R.arrows g
g : Y ⟶ X
hcomp : F.map g = F.map f
hg : R.arrows g
⊢ R.arrows f

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : C
R : Sieve X
f : Y ⟶ X
x✝ : ∃ g, F.map g = F.map f ∧ R.arrows g
g : Y ⟶ X
hcomp : F.map g = F.map f
hg : R.arrows g
⊢ R.arrows f

Tactic:
rwa [← F.map_injective hcomp]

Result:
no goals
-- Mathlib/Probability/Martingale/Basic.lean
theorem smul_nonpos {f : ι → Ω → F} {c : ℝ} (hc : c ≤ 0) (hf : Submartingale f ℱ μ) :
    Supermartingale (c • f) ℱ μ

Proof state:
Ω : Type u_1
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst✝³ : NormedLatticeAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : OrderedSMul ℝ F
f : ι → Ω → F
c : ℝ
hc : c ≤ 0
hf : Submartingale f ℱ μ
⊢ - -c • f = -(-c • f)

Tactic:
ext (i x)

Result:
case h.h
Ω : Type u_1
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst✝³ : NormedLatticeAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : OrderedSMul ℝ F
f : ι → Ω → F
c : ℝ
hc : c ≤ 0
hf : Submartingale f ℱ μ
i : ι
x : Ω
⊢ (- -c • f) i x = (-(-c • f)) i x

Proof state:
Ω : Type u_1
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst✝³ : NormedLatticeAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : OrderedSMul ℝ F
f : ι → Ω → F
c : ℝ
hc : c ≤ 0
hf : Submartingale f ℱ μ
⊢ Supermartingale (c • f) ℱ μ

Tactic:
rw [← neg_neg c, (by ext (i x); simp : - -c • f = -(-c • f))]

Result:
Ω : Type u_1
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst✝³ : NormedLatticeAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : OrderedSMul ℝ F
f : ι → Ω → F
c : ℝ
hc : c ≤ 0
hf : Submartingale f ℱ μ
⊢ Supermartingale (-(-c • f)) ℱ μ

Proof state:
case h.h
Ω : Type u_1
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst✝³ : NormedLatticeAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : OrderedSMul ℝ F
f : ι → Ω → F
c : ℝ
hc : c ≤ 0
hf : Submartingale f ℱ μ
i : ι
x : Ω
⊢ (- -c • f) i x = (-(-c • f)) i x

Tactic:
simp

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst✝³ : NormedLatticeAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : OrderedSMul ℝ F
f : ι → Ω → F
c : ℝ
hc : c ≤ 0
hf : Submartingale f ℱ μ
⊢ Supermartingale (-(-c • f)) ℱ μ

Tactic:
exact (hf.smul_nonneg <| neg_nonneg.2 hc).neg

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_one_left_eq_zero : logb 1 = 0

Proof state:
⊢ logb 1 = 0

Tactic:
ext

Result:
case h
x✝ : ℝ
⊢ logb 1 x✝ = 0 x✝

Proof state:
case h
x✝ : ℝ
⊢ logb 1 x✝ = 0 x✝

Tactic:
rw [logb_one_left, Pi.zero_apply]

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/TransfiniteIteration.lean
lemma arrowMk_iterationFunctor_map (i₁ i₂ : J) (h₁₂ : i₁ ≤ i₂)
    {j : J} (iter : Φ.Iteration j) (hj : i₂ ≤ j) :
    Arrow.mk ((Φ.iterationFunctor J).map (homOfLE h₁₂)) =
      Arrow.mk (iter.F.map (homOfLE h₁₂ : ⟨i₁, h₁₂.trans hj⟩ ⟶ ⟨i₂, hj⟩))

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
j : J
iter : Φ.Iteration j
hj : i₂ ≤ j
⊢ arrowMap (Φ.iter i₂).F i₁ i₂ ⋯ ⋯ = Arrow.mk (iter.F.map (homOfLE h₁₂))

Tactic:
exact Arrow.ext (Iteration.congr_obj _ _ _ _ _)
  (Iteration.congr_obj _ _ _ _ _) (Iteration.congr_map _ _ _ _ _)

Result:
no goals

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
j : J
iter : Φ.Iteration j
hj : i₂ ≤ j
⊢ Arrow.mk ((Φ.iter i₁).mapObj (Φ.iter i₂) ⋯ ⋯ ⋯ ⋯) = Arrow.mk (iter.F.map (homOfLE h₁₂))

Tactic:
rw [Iteration.arrow_mk_mapObj]

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
j : J
iter : Φ.Iteration j
hj : i₂ ≤ j
⊢ arrowMap (Φ.iter i₂).F i₁ i₂ ⋯ ⋯ = Arrow.mk (iter.F.map (homOfLE h₁₂))

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
j : J
iter : Φ.Iteration j
hj : i₂ ≤ j
⊢ Arrow.mk ((Φ.iterationFunctor J).map (homOfLE h₁₂)) = Arrow.mk (iter.F.map (homOfLE h₁₂))

Tactic:
dsimp [iterationFunctor]

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
j : J
iter : Φ.Iteration j
hj : i₂ ≤ j
⊢ Arrow.mk ((Φ.iter i₁).mapObj (Φ.iter i₂) ⋯ ⋯ ⋯ ⋯) = Arrow.mk (iter.F.map (homOfLE h₁₂))
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
@[simp]
lemma homologyMap_sub : homologyMap (φ - ψ) i = homologyMap φ i - homologyMap ψ i

Proof state:
C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
φ ψ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ ShortComplex.homologyMap ((shortComplexFunctor C c i).map (φ - ψ)) =
    ShortComplex.homologyMap ((shortComplexFunctor C c i).map φ) -
      ShortComplex.homologyMap ((shortComplexFunctor C c i).map ψ)

Tactic:
rw [← ShortComplex.homologyMap_sub]

Result:
C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
φ ψ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ ShortComplex.homologyMap ((shortComplexFunctor C c i).map (φ - ψ)) =
    ShortComplex.homologyMap ((shortComplexFunctor C c i).map φ - (shortComplexFunctor C c i).map ψ)

Proof state:
C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
φ ψ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ ShortComplex.homologyMap ((shortComplexFunctor C c i).map (φ - ψ)) =
    ShortComplex.homologyMap ((shortComplexFunctor C c i).map φ - (shortComplexFunctor C c i).map ψ)

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
φ ψ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ homologyMap (φ - ψ) i = homologyMap φ i - homologyMap ψ i

Tactic:
dsimp [homologyMap]

Result:
C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
φ ψ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ ShortComplex.homologyMap ((shortComplexFunctor C c i).map (φ - ψ)) =
    ShortComplex.homologyMap ((shortComplexFunctor C c i).map φ) -
      ShortComplex.homologyMap ((shortComplexFunctor C c i).map ψ)
-- Mathlib/Topology/UniformSpace/CompleteSeparated.lean
theorem IsComplete.isClosed [UniformSpace α] [T0Space α] {s : Set α} (h : IsComplete s) :
    IsClosed s :=
  isClosed_iff_clusterPt.2 fun a ha => by
    let f := 𝓝[s] a
    have : Cauchy f := cauchy_nhds.mono' ha inf_le_left
    rcases h f this inf_le_right with ⟨y, ys, fy⟩
    rwa [(tendsto_nhds_unique' ha inf_le_left fy : a = y)]

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : T0Space α
s : Set α
h : IsComplete s
a : α
ha : ClusterPt a (𝓟 s)
f : Filter α := 𝓝[s] a
this : Cauchy f
y : α
ys : y ∈ s
fy : f ≤ 𝓝 y
⊢ a ∈ s

Tactic:
rwa [(tendsto_nhds_unique' ha inf_le_left fy : a = y)]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : T0Space α
s : Set α
h : IsComplete s
a : α
ha : ClusterPt a (𝓟 s)
f : Filter α := 𝓝[s] a
this : Cauchy f
⊢ a ∈ s

Tactic:
rcases h f this inf_le_right with ⟨y, ys, fy⟩

Result:
case intro.intro
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : T0Space α
s : Set α
h : IsComplete s
a : α
ha : ClusterPt a (𝓟 s)
f : Filter α := 𝓝[s] a
this : Cauchy f
y : α
ys : y ∈ s
fy : f ≤ 𝓝 y
⊢ a ∈ s

Proof state:
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : T0Space α
s : Set α
h : IsComplete s
a : α
ha : ClusterPt a (𝓟 s)
⊢ a ∈ s

Tactic:
let f := 𝓝[s] a

Result:
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : T0Space α
s : Set α
h : IsComplete s
a : α
ha : ClusterPt a (𝓟 s)
f : Filter α := 𝓝[s] a
⊢ a ∈ s

Proof state:
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : T0Space α
s : Set α
h : IsComplete s
a : α
ha : ClusterPt a (𝓟 s)
f : Filter α := 𝓝[s] a
⊢ a ∈ s

Tactic:
have : Cauchy f := cauchy_nhds.mono' ha inf_le_left

Result:
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : T0Space α
s : Set α
h : IsComplete s
a : α
ha : ClusterPt a (𝓟 s)
f : Filter α := 𝓝[s] a
this : Cauchy f
⊢ a ∈ s
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem extend_function_of_lt {α β : Type*} {s : Set α} (f : s ↪ β) (hs : #s < #α)
    (h : Nonempty (α ≃ β)) : ∃ g : α ≃ β, ∀ x : s, g x = f x

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
⊢ ∃ g, ∀ (x : ↑s), g ↑x = f x

Tactic:
cases fintypeOrInfinite α

Result:
case inl
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
val✝ : Fintype α
⊢ ∃ g, ∀ (x : ↑s), g ↑x = f x

case inr
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
val✝ : Infinite α
⊢ ∃ g, ∀ (x : ↑s), g ↑x = f x

Proof state:
case inr.intro.h2
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : lift.{u_2, u_1} #α = lift.{u_1, u_2} #β
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ #↑(range ⇑f) < #β

Tactic:
rwa [← lift_lt, mk_range_eq_of_injective f.injective, ← h, lift_lt]

Result:
no goals

Proof state:
case inr
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
val✝ : Infinite α
⊢ ∃ g, ∀ (x : ↑s), g ↑x = f x

Tactic:
apply extend_function f

Result:
case inr
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
val✝ : Infinite α
⊢ Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)

Proof state:
case inr.intro
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
val✝ : Infinite α
g : α ≃ β
⊢ Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)

Tactic:
haveI := Infinite.of_injective _ g.injective

Result:
case inr.intro
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)

Proof state:
case inl
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
val✝ : Fintype α
⊢ ∃ g, ∀ (x : ↑s), g ↑x = f x

Tactic:
exact extend_function_finite f h

Result:
no goals

Proof state:
case inr.intro
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : lift.{u_2, u_1} #α = lift.{u_1, u_2} #β
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ lift.{u_2, u_1} #↑sᶜ = lift.{u_1, u_2} #↑(range ⇑f)ᶜ

Tactic:
rwa [mk_compl_of_infinite s hs, mk_compl_of_infinite]

Result:
case inr.intro.h2
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : lift.{u_2, u_1} #α = lift.{u_1, u_2} #β
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ #↑(range ⇑f) < #β

Proof state:
case inr.intro
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)

Tactic:
rw [← lift_mk_eq'] at h ⊢

Result:
case inr.intro
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : lift.{u_2, u_1} #α = lift.{u_1, u_2} #β
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ lift.{u_2, u_1} #↑sᶜ = lift.{u_1, u_2} #↑(range ⇑f)ᶜ

Proof state:
case inr
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
val✝ : Infinite α
⊢ Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)

Tactic:
obtain ⟨g⟩ := id h

Result:
case inr.intro
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
val✝ : Infinite α
g : α ≃ β
⊢ Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)