harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Logic/Relation.lean
theorem Equivalence.eqvGen_iff (h : Equivalence r) : EqvGen r a b ↔ r a b :=
  Iff.intro
    (by
      intro h
      induction h with
      | rel => assumption
      | refl => exact h.1 _
      | symm => apply h.symm; assumption
      | trans _ _ _ _ _ hab hbc => exact h.trans hab hbc)
    (EqvGen.rel a b)

Proof state:
case symm
α : Type u_1
r : α → α → Prop
a b : α
h : Equivalence r
x✝ y✝ : α
a✝ : EqvGen r x✝ y✝
a_ih✝ : r x✝ y✝
⊢ r x✝ y✝

Tactic:
assumption

Result:
no goals

Proof state:
case trans
α : Type u_1
r : α → α → Prop
a b : α
h : Equivalence r
x✝ y✝ z✝ : α
a✝¹ : EqvGen r x✝ y✝
a✝ : EqvGen r y✝ z✝
hab : r x✝ y✝
hbc : r y✝ z✝
⊢ r x✝ z✝

Tactic:
exact h.trans hab hbc

Result:
no goals

Proof state:
case symm
α : Type u_1
r : α → α → Prop
a b : α
h : Equivalence r
x✝ y✝ : α
a✝ : EqvGen r x✝ y✝
a_ih✝ : r x✝ y✝
⊢ r y✝ x✝

Tactic:
apply h.symm

Result:
case symm
α : Type u_1
r : α → α → Prop
a b : α
h : Equivalence r
x✝ y✝ : α
a✝ : EqvGen r x✝ y✝
a_ih✝ : r x✝ y✝
⊢ r x✝ y✝

Proof state:
α : Type u_1
r : α → α → Prop
a b : α
h : Equivalence r
⊢ EqvGen r a b → r a b

Tactic:
intro h

Result:
α : Type u_1
r : α → α → Prop
a b : α
h✝ : Equivalence r
h : EqvGen r a b
⊢ r a b

Proof state:
case refl
α : Type u_1
r : α → α → Prop
a b : α
h : Equivalence r
x✝ : α
⊢ r x✝ x✝

Tactic:
exact h.1 _

Result:
no goals

Proof state:
case rel
α : Type u_1
r : α → α → Prop
a b : α
h : Equivalence r
x✝ y✝ : α
a✝ : r x✝ y✝
⊢ r x✝ y✝

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
a b : α
h✝ : Equivalence r
h : EqvGen r a b
⊢ r a b

Tactic:
induction h with
| rel => assumption
| refl => exact h.1 _
| symm => apply h.symm; assumption
| trans _ _ _ _ _ hab hbc => exact h.trans hab hbc

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.lean
theorem preservesZeroMorphisms_of_map_zero_object (i : F.obj 0 ≅ 0) : PreservesZeroMorphisms F where
  map_zero X Y :=
    calc
      F.map (0 : X ⟶ Y) = F.map (0 : X ⟶ 0) ≫ F.map 0

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroObject C
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroMorphisms D
F : C ⥤ D
i : F.obj 0 ≅ 0
X Y : C
⊢ F.map 0 ≫ (i.hom ≫ i.inv) ≫ F.map 0 = 0

Tactic:
simp only [zero_of_to_zero i.hom, zero_comp, comp_zero]

Result:
no goals

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroObject C
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroMorphisms D
F : C ⥤ D
i : F.obj 0 ≅ 0
X Y : C
⊢ F.map 0 = F.map 0 ≫ F.map 0

Tactic:
rw [← Functor.map_comp, comp_zero]

Result:
no goals

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroObject C
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroMorphisms D
F : C ⥤ D
i : F.obj 0 ≅ 0
X Y : C
⊢ F.map 0 ≫ F.map 0 = F.map 0 ≫ (i.hom ≫ i.inv) ≫ F.map 0

Tactic:
rw [Iso.hom_inv_id, Category.id_comp]

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Pi.lean
/-- Given a family of endomorphisms `i ↦ f i`, a family of candidate eigenvalues `i ↦ μ i`, and a
submodule `p` which is invariant wrt every `f i`, the intersection of `p` with the simultaneous
maximal generalised eigenspace (taken over all `i`), is the same as the simultaneous maximal
generalised eigenspace of the `f i` restricted to `p`. -/
lemma _root_.Submodule.inf_iInf_maxGenEigenspace_of_forall_mapsTo {μ : ι → R}
    (p : Submodule R M) (hfp : ∀ i, MapsTo (f i) p p) :
    p ⊓ ⨅ i, (f i).maxGenEigenspace (μ i) =
      (⨅ i, maxGenEigenspace ((f i).restrict (hfp i)) (μ i)).map p.subtype

Proof state:
case inl
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → End R M
μ : ι → R
p : Submodule R M
hfp : ∀ (i : ι), MapsTo ⇑(f i) ↑p ↑p
h✝ : IsEmpty ι
⊢ p ⊓ ⨅ i, (f i).maxGenEigenspace (μ i) =
    Submodule.map p.subtype (⨅ i, maxGenEigenspace (LinearMap.restrict (f i) ⋯) (μ i))

Tactic:
simp [iInf_of_isEmpty]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → End R M
μ : ι → R
p : Submodule R M
hfp : ∀ (i : ι), MapsTo ⇑(f i) ↑p ↑p
⊢ p ⊓ ⨅ i, (f i).maxGenEigenspace (μ i) =
    Submodule.map p.subtype (⨅ i, maxGenEigenspace (LinearMap.restrict (f i) ⋯) (μ i))

Tactic:
cases isEmpty_or_nonempty ι

Result:
case inl
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → End R M
μ : ι → R
p : Submodule R M
hfp : ∀ (i : ι), MapsTo ⇑(f i) ↑p ↑p
h✝ : IsEmpty ι
⊢ p ⊓ ⨅ i, (f i).maxGenEigenspace (μ i) =
    Submodule.map p.subtype (⨅ i, maxGenEigenspace (LinearMap.restrict (f i) ⋯) (μ i))

case inr
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → End R M
μ : ι → R
p : Submodule R M
hfp : ∀ (i : ι), MapsTo ⇑(f i) ↑p ↑p
h✝ : Nonempty ι
⊢ p ⊓ ⨅ i, (f i).maxGenEigenspace (μ i) =
    Submodule.map p.subtype (⨅ i, maxGenEigenspace (LinearMap.restrict (f i) ⋯) (μ i))

Proof state:
case inr
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → End R M
μ : ι → R
p : Submodule R M
hfp : ∀ (i : ι), MapsTo ⇑(f i) ↑p ↑p
h✝ : Nonempty ι
⊢ p ⊓ ⨅ i, (f i).maxGenEigenspace (μ i) =
    Submodule.map p.subtype (⨅ i, maxGenEigenspace (LinearMap.restrict (f i) ⋯) (μ i))

Tactic:
simp_rw [inf_iInf, p.inf_genEigenspace _ (hfp _), Submodule.map_iInf _ p.injective_subtype]

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
theorem continuousOn_lift₂ {f : X → Y → Z} {hf : ∀ a b c d, (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d}
    {s : Set (SeparationQuotient X × SeparationQuotient Y)} :
    ContinuousOn (uncurry <| lift₂ f hf) s ↔ ContinuousOn (uncurry f) (Prod.map mk mk ⁻¹' s)

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y → Z
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
s : Set (SeparationQuotient X × SeparationQuotient Y)
⊢ (∀ (a : X) (b : Y), (mk a, mk b) ∈ s → ContinuousWithinAt (uncurry f) (Prod.map mk mk ⁻¹' s) (a, b)) ↔
    ∀ (a : X) (b : Y), (a, b) ∈ Prod.map mk mk ⁻¹' s → ContinuousWithinAt (uncurry f) (Prod.map mk mk ⁻¹' s) (a, b)

Tactic:
rfl

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y → Z
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
s : Set (SeparationQuotient X × SeparationQuotient Y)
⊢ ContinuousOn (uncurry (lift₂ f hf)) s ↔ ContinuousOn (uncurry f) (Prod.map mk mk ⁻¹' s)

Tactic:
simp_rw [ContinuousOn, (surjective_mk.prodMap surjective_mk).forall, Prod.forall, Prod.map,
  continuousWithinAt_lift₂]

Result:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y → Z
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
s : Set (SeparationQuotient X × SeparationQuotient Y)
⊢ (∀ (a : X) (b : Y), (mk a, mk b) ∈ s → ContinuousWithinAt (uncurry f) (Prod.map mk mk ⁻¹' s) (a, b)) ↔
    ∀ (a : X) (b : Y), (a, b) ∈ Prod.map mk mk ⁻¹' s → ContinuousWithinAt (uncurry f) (Prod.map mk mk ⁻¹' s) (a, b)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem lt_of_add_lt_add_left {n : Nat} : n + k < n + m → k < m

Proof state:
k m n : Nat
⊢ n + k < n + m → k < m

Tactic:
rw [Nat.add_comm n, Nat.add_comm n]

Result:
k m n : Nat
⊢ k + n < m + n → k < m

Proof state:
k m n : Nat
⊢ k + n < m + n → k < m

Tactic:
exact Nat.lt_of_add_lt_add_right

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Pasting.lean
theorem inl_inl_pushoutLeftPushoutInrIso_hom :
    (pushout.inl f g) ≫ (pushout.inl (pushout.inr f g) g') ≫
      (pushoutLeftPushoutInrIso f g g').hom = (pushout.inl f (g ≫ g'))

Proof state:
C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
g' : Z ⟶ W
inst✝¹ : HasPushout f g
inst✝ : HasPushout (pushout.inr f g) g'
⊢ (pushout.inl f g ≫ pushout.inl (pushout.inr f g) g') ≫ (pushoutLeftPushoutInrIso f g g').hom = pushout.inl f (g ≫ g')

Tactic:
apply IsColimit.comp_coconePointUniqueUpToIso_hom (pasteHorizIsPushout _ _ _) _ WalkingSpan.left

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
g' : Z ⟶ W
inst✝¹ : HasPushout f g
inst✝ : HasPushout (pushout.inr f g) g'
⊢ pushout.inl f g ≫ pushout.inl (pushout.inr f g) g' ≫ (pushoutLeftPushoutInrIso f g g').hom = pushout.inl f (g ≫ g')

Tactic:
rw [← Category.assoc]

Result:
C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
g' : Z ⟶ W
inst✝¹ : HasPushout f g
inst✝ : HasPushout (pushout.inr f g) g'
⊢ (pushout.inl f g ≫ pushout.inl (pushout.inr f g) g') ≫ (pushoutLeftPushoutInrIso f g g').hom = pushout.inl f (g ≫ g')
-- Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean
lemma symm_Λ₀_eq (s : ℂ) :
    P.symm.Λ₀ s = P.symm.Λ s + (1 / s) • P.g₀ + (P.ε⁻¹ / (P.k - s)) • P.f₀

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
⊢ P.symm.Λ₀ s = P.symm.Λ s + (1 / s) • P.g₀ + (P.ε⁻¹ / (↑P.k - s)) • P.f₀

Tactic:
rw [P.symm.Λ₀_eq]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
⊢ P.symm.Λ s + (1 / s) • P.symm.f₀ + (P.symm.ε / (↑P.symm.k - s)) • P.symm.g₀ =
    P.symm.Λ s + (1 / s) • P.g₀ + (P.ε⁻¹ / (↑P.k - s)) • P.f₀

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
⊢ P.symm.Λ s + (1 / s) • P.symm.f₀ + (P.symm.ε / (↑P.symm.k - s)) • P.symm.g₀ =
    P.symm.Λ s + (1 / s) • P.g₀ + (P.ε⁻¹ / (↑P.k - s)) • P.f₀

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
theorem mkPiRing_eq_zero_iff [Fintype ι] (z : M₂) : MultilinearMap.mkPiRing R ι z = 0 ↔ z = 0

Proof state:
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
z : M₂
⊢ MultilinearMap.mkPiRing R ι z = 0 ↔ z = 0

Tactic:
rw [← mkPiRing_zero, mkPiRing_eq_iff]

Result:
no goals
-- Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
lemma commute_of_mem_adjoin_singleton_of_commute {a b c : A}
    (hc : c ∈ adjoin R {b}) (h : Commute a b) :
    Commute a c :=
  commute_of_mem_adjoin_of_forall_mem_commute hc <| by simpa

Proof state:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b c : A
hc : c ∈ adjoin R {b}
h : Commute a b
⊢ ∀ b_1 ∈ {b}, Commute a b_1

Tactic:
simpa

Result:
no goals
-- Mathlib/RingTheory/Support.lean
lemma Module.mem_support_iff_of_finite [Module.Finite R M] :
    p ∈ Module.support R M ↔ Module.annihilator R M ≤ p.asIdeal

Proof state:
case mk.intro.refine_1.intro
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p : PrimeSpectrum R
inst✝ : Module.Finite R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
H : ∀ m ∈ ↑s, ∃ x, x • m = 0 ∧ x ∉ p.asIdeal
x : { a // a ∈ ↑s } → R
hx : ∀ (x_1 : { a // a ∈ ↑s }), x x_1 • ↑x_1 = 0
hx' : ∀ (x_1 : { a // a ∈ ↑s }), x x_1 ∉ p.asIdeal
m : ↑↑s
k : R
hk : ∏ i ∈ s.attach, x i = x m * k
⊢ s.attach.prod x • ↑m = 0

Tactic:
rw [hk, mul_comm, mul_smul, hx, smul_zero]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem mem_ofZNum' : ∀ {m : Num} {n : ZNum}, m ∈ ofZNum' n ↔ n = toZNum m
  | 0, 0 => ⟨fun _ => rfl, fun _ => rfl⟩
  | pos _, 0 => ⟨nofun, nofun⟩
  | m, ZNum.pos p =>
    Option.some_inj.trans <| by cases m <;> constructor <;> intro h <;> try cases h <;> rfl
  | m, ZNum.neg p => ⟨nofun, fun h => by cases m <;> cases h⟩

Proof state:
m : Num
p : PosNum
h : ZNum.neg p = m.toZNum
⊢ m ∈ ofZNum' (ZNum.neg p)

Tactic:
cases m <;> cases h

Result:
no goals

Proof state:
m : Num
p : PosNum
⊢ pos p = m ↔ ZNum.pos p = m.toZNum

Tactic:
cases m <;> constructor <;> intro h <;> try cases h <;> rfl

Result:
no goals

Proof state:
case pos.mpr
p a✝ : PosNum
h : ZNum.pos p = (pos a✝).toZNum
⊢ pos p = pos a✝

Tactic:
cases h <;> rfl

Result:
no goals
-- Mathlib/Topology/Compactness/Lindelof.lean
theorem isLindelof_open_iff_eq_countable_iUnion_of_isTopologicalBasis (b : ι → Set X)
    (hb : IsTopologicalBasis (Set.range b)) (hb' : ∀ i, IsLindelof (b i)) (U : Set X) :
    IsLindelof U ∧ IsOpen U ↔ ∃ s : Set ι, s.Countable ∧ U = ⋃ i ∈ s, b i

Proof state:
case mp.intro.intro.intro.intro.intro.refine_2
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : Y → ι
h₁ : IsLindelof (⋃ i, (b ∘ f') i)
h₂ : IsOpen (⋃ i, (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ ⋃ i, (b ∘ f') i ⊆ ⋃ i ∈ t, (b ∘ f') i
⊢ ⋃ i ∈ f' '' t, b i ≤ ⋃ i, (b ∘ f') i

Tactic:
apply Set.iUnion₂_subset

Result:
case mp.intro.intro.intro.intro.intro.refine_2.h
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : Y → ι
h₁ : IsLindelof (⋃ i, (b ∘ f') i)
h₂ : IsOpen (⋃ i, (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ ⋃ i, (b ∘ f') i ⊆ ⋃ i ∈ t, (b ∘ f') i
⊢ ∀ i ∈ f' '' t, b i ⊆ ⋃ i, (b ∘ f') i
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
lemma isIso_ι (hg : S.g = 0) : IsIso h.ι

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
hg : S.g = 0
φ : h.Q ⟶ (KernelFork.ofι h.ι ⋯).pt
hφ : φ ≫ h.ι = 𝟙 h.Q
⊢ h.ι ≫ φ = 𝟙 h.H

Tactic:
rw [← cancel_mono h.ι, assoc, hφ, comp_id, id_comp]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
hg : S.g = 0
φ : h.Q ⟶ (KernelFork.ofι h.ι ⋯).pt
hφ : φ ≫ h.ι = 𝟙 h.Q
⊢ IsIso h.ι

Tactic:
exact ⟨φ, by rw [← cancel_mono h.ι, assoc, hφ, comp_id, id_comp], hφ⟩

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
hg : S.g = 0
φ : h.Q ⟶ (KernelFork.ofι h.ι ⋯).pt
hφ : φ ≫ Fork.ι (KernelFork.ofι h.ι ⋯) = 𝟙 h.Q
⊢ IsIso h.ι

Tactic:
dsimp at hφ

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
hg : S.g = 0
φ : h.Q ⟶ (KernelFork.ofι h.ι ⋯).pt
hφ : φ ≫ h.ι = 𝟙 h.Q
⊢ IsIso h.ι

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
hg : S.g = 0
⊢ 𝟙 h.Q ≫ h.g' = 0

Tactic:
rw [← cancel_epi h.p, id_comp, p_g', comp_zero, hg]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
hg : S.g = 0
⊢ IsIso h.ι

Tactic:
have ⟨φ, hφ⟩ := KernelFork.IsLimit.lift' h.hι' (𝟙 _)
  (by rw [← cancel_epi h.p, id_comp, p_g', comp_zero, hg])

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
hg : S.g = 0
φ : h.Q ⟶ (KernelFork.ofι h.ι ⋯).pt
hφ : φ ≫ Fork.ι (KernelFork.ofι h.ι ⋯) = 𝟙 h.Q
⊢ IsIso h.ι
-- Mathlib/Algebra/Order/Floor.lean
theorem ceil_natCast (n : ℕ) : ⌈(n : α)⌉ = n :=
  eq_of_forall_ge_iff fun a => by rw [ceil_le, ← cast_natCast, cast_le]

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
n : ℕ
a : ℤ
⊢ ⌈↑n⌉ ≤ a ↔ ↑n ≤ a

Tactic:
rw [ceil_le, ← cast_natCast, cast_le]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Presheaf.lean
@[simp]
lemma compYonedaIsoYonedaCompLan_inv_app_app_apply_eq_id (X : C) :
    ((compYonedaIsoYonedaCompLan F).inv.app X).app (Opposite.op (F.obj X))
      ((F.op.lanUnit.app (yoneda.obj X)).app _ (𝟙 X)) = 𝟙 _ :=
  (congr_fun (Functor.descOfIsLeftKanExtension_fac_app _
    (F.op.lanUnit.app (yoneda.obj X)) _ (yonedaMap F X) (Opposite.op X)) (𝟙 _)).trans (by simp)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P
X : C
⊢ (yonedaMap F X).app (Opposite.op X) (𝟙 (Opposite.unop (Opposite.op X))) = 𝟙 (Opposite.unop (Opposite.op (F.obj X)))

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Projective.lean
lemma isProbabilityMeasure [∀ i, IsProbabilityMeasure (P i)] (hμ : IsProjectiveLimit μ P) :
    IsProbabilityMeasure μ

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
μ : Measure ((i : ι) → α i)
inst✝ : ∀ (i : Finset ι), IsProbabilityMeasure (P i)
hμ : IsProjectiveLimit μ P
⊢ IsProbabilityMeasure μ

Tactic:
constructor

Result:
case measure_univ
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
μ : Measure ((i : ι) → α i)
inst✝ : ∀ (i : Finset ι), IsProbabilityMeasure (P i)
hμ : IsProjectiveLimit μ P
⊢ μ univ = 1

Proof state:
case measure_univ
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
μ : Measure ((i : ι) → α i)
inst✝ : ∀ (i : Finset ι), IsProbabilityMeasure (P i)
hμ : IsProjectiveLimit μ P
⊢ (P ∅) univ = 1

Tactic:
exact measure_univ

Result:
no goals

Proof state:
case measure_univ
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
μ : Measure ((i : ι) → α i)
inst✝ : ∀ (i : Finset ι), IsProbabilityMeasure (P i)
hμ : IsProjectiveLimit μ P
⊢ μ univ = 1

Tactic:
rw [hμ.measure_univ_eq (∅ : Finset ι)]

Result:
case measure_univ
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
μ : Measure ((i : ι) → α i)
inst✝ : ∀ (i : Finset ι), IsProbabilityMeasure (P i)
hμ : IsProjectiveLimit μ P
⊢ (P ∅) univ = 1
-- Mathlib/NumberTheory/LegendreSymbol/QuadraticReciprocity.lean
theorem exists_sq_eq_prime_iff_of_mod_four_eq_three (hp3 : p % 4 = 3) (hq3 : q % 4 = 3)
    (hpq : p ≠ q) : IsSquare (q : ZMod p) ↔ ¬IsSquare (p : ZMod q)

Proof state:
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp3 : p % 4 = 3
hq3 : q % 4 = 3
hpq : p ≠ q
⊢ IsSquare ↑q ↔ ¬IsSquare ↑p

Tactic:
rw [← eq_one_iff' p (prime_ne_zero p q hpq), ← eq_neg_one_iff' q,
  quadratic_reciprocity_three_mod_four hp3 hq3, neg_inj]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem angle_sub_eq_arccos_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) :
    angle x (x - y) = Real.arccos (‖x‖ / ‖x - y‖)

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
⊢ angle x (x - y) = Real.arccos (‖x‖ / ‖x - y‖)

Tactic:
rw [sub_eq_add_neg, angle_add_eq_arccos_of_inner_eq_zero h]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ angle x (x - y) = Real.arccos (‖x‖ / ‖x - y‖)

Tactic:
rw [← neg_eq_zero, ← inner_neg_right] at h

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
⊢ angle x (x - y) = Real.arccos (‖x‖ / ‖x - y‖)
-- Mathlib/LinearAlgebra/Matrix/IsDiag.lean
theorem IsDiag.smul [Monoid R] [AddMonoid α] [DistribMulAction R α] (k : R) {A : Matrix n n α}
    (ha : A.IsDiag) : (k • A).IsDiag

Proof state:
α : Type u_1
R : Type u_3
n : Type u_4
inst✝² : Monoid R
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction R α
k : R
A : Matrix n n α
ha : A.IsDiag
i j : n
h : i ≠ j
⊢ (k • A) i j = 0

Tactic:
simp [ha h]

Result:
no goals

Proof state:
α : Type u_1
R : Type u_3
n : Type u_4
inst✝² : Monoid R
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction R α
k : R
A : Matrix n n α
ha : A.IsDiag
⊢ (k • A).IsDiag

Tactic:
intro i j h

Result:
α : Type u_1
R : Type u_3
n : Type u_4
inst✝² : Monoid R
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction R α
k : R
A : Matrix n n α
ha : A.IsDiag
i j : n
h : i ≠ j
⊢ (k • A) i j = 0
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem lt_pred {a b} : a < pred b ↔ succ a < b

Proof state:
a b : Ordinal.{u_4}
h : ∃ a, b = succ a
c : Ordinal.{u_4}
e : b = succ c
⊢ a < b.pred ↔ succ a < b

Tactic:
rw [e, pred_succ, succ_lt_succ_iff]

Result:
no goals

Proof state:
a b : Ordinal.{u_4}
h : ∃ a, b = succ a
⊢ a < b.pred ↔ succ a < b

Tactic:
let ⟨c, e⟩ := h

Result:
a b : Ordinal.{u_4}
h : ∃ a, b = succ a
c : Ordinal.{u_4}
e : b = succ c
⊢ a < b.pred ↔ succ a < b

Proof state:
a b : Ordinal.{u_4}
⊢ a < b.pred ↔ succ a < b

Tactic:
exact if h : ∃ a, b = succ a then by
  let ⟨c, e⟩ := h
  rw [e, pred_succ, succ_lt_succ_iff]
else by simp only [pred, dif_neg h, succ_lt_of_not_succ h]

Result:
no goals

Proof state:
a b : Ordinal.{u_4}
h : ¬∃ a, b = succ a
⊢ a < b.pred ↔ succ a < b

Tactic:
simp only [pred, dif_neg h, succ_lt_of_not_succ h]

Result:
no goals

Proof state:
a b : Ordinal.{u_4}
⊢ a < b.pred ↔ succ a < b

Tactic:
classical
exact if h : ∃ a, b = succ a then by
  let ⟨c, e⟩ := h
  rw [e, pred_succ, succ_lt_succ_iff]
else by simp only [pred, dif_neg h, succ_lt_of_not_succ h]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem aleph0_lt_mk_iff : ℵ₀ < #α ↔ Uncountable α

Proof state:
α : Type u
⊢ ℵ₀ < #α ↔ Uncountable α

Tactic:
rw [← not_le, ← not_countable_iff, not_iff_not, mk_le_aleph0_iff]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem lift_type_le {α : Type u} {β : Type v} {r s} [IsWellOrder α r] [IsWellOrder β s] :
    lift.{max v w} (type r) ≤ lift.{max u w} (type s) ↔ Nonempty (r ≼i s)

Proof state:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s) ↔ Nonempty (r ≼i s)

Tactic:
constructor <;> refine fun ⟨f⟩ ↦ ⟨?_⟩

Result:
case mp
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝ : lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s)
f : ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r ≼i ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r
⊢ r ≼i s

case mpr
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝ : Nonempty (r ≼i s)
f : r ≼i s
⊢ ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r ≼i ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r

Proof state:
case mp
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝ : lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s)
f : ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r ≼i ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r
⊢ r ≼i s

Tactic:
exact (RelIso.preimage Equiv.ulift r).symm.toInitialSeg.trans
  (f.trans (RelIso.preimage Equiv.ulift s).toInitialSeg)

Result:
no goals

Proof state:
case mpr
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝ : Nonempty (r ≼i s)
f : r ≼i s
⊢ ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r ≼i ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r

Tactic:
exact (RelIso.preimage Equiv.ulift r).toInitialSeg.trans
  (f.trans (RelIso.preimage Equiv.ulift s).symm.toInitialSeg)

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem mk'_eq_of_eq' {a₁ b₁ : M} {a₂ b₂ : S} (H : b₁ * ↑a₂ = a₁ * ↑b₂) :
    f.mk' a₁ a₂ = f.mk' b₁ b₂ :=
  f.mk'_eq_of_eq <| by simpa only [mul_comm] using H

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
a₁ b₁ : M
a₂ b₂ : ↥S
H : b₁ * ↑a₂ = a₁ * ↑b₂
⊢ ↑a₂ * b₁ = ↑b₂ * a₁

Tactic:
simpa only [mul_comm] using H

Result:
no goals