harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/Preserves/Basic.lean
/-- Transfer preservation of limits along a natural isomorphism in the diagram. -/
lemma preservesLimit_of_iso_diagram {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂)
    [PreservesLimit K₁ F] : PreservesLimit K₂ F where
  preserves {c} t := ⟨by
    apply IsLimit.postcomposeInvEquiv (isoWhiskerRight h F :) _ _
    have := (IsLimit.postcomposeInvEquiv h c).symm t
    apply IsLimit.ofIsoLimit (isLimitOfPreserves F this)
    exact Cones.ext (Iso.refl _)⟩

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesLimit K₁ F
c : Cone K₂
t : IsLimit c
this : IsLimit ((Cones.postcompose h.inv).obj c)
⊢ F.mapCone ((Cones.postcompose h.inv).obj c) ≅ (Cones.postcompose (isoWhiskerRight h F).inv).obj (F.mapCone c)

Tactic:
exact Cones.ext (Iso.refl _)

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesLimit K₁ F
c : Cone K₂
t : IsLimit c
this : IsLimit ((Cones.postcompose h.inv).obj c)
⊢ IsLimit ((Cones.postcompose (isoWhiskerRight h F).inv).obj (F.mapCone c))

Tactic:
apply IsLimit.ofIsoLimit (isLimitOfPreserves F this)

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesLimit K₁ F
c : Cone K₂
t : IsLimit c
this : IsLimit ((Cones.postcompose h.inv).obj c)
⊢ F.mapCone ((Cones.postcompose h.inv).obj c) ≅ (Cones.postcompose (isoWhiskerRight h F).inv).obj (F.mapCone c)

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesLimit K₁ F
c : Cone K₂
t : IsLimit c
⊢ IsLimit (F.mapCone c)

Tactic:
apply IsLimit.postcomposeInvEquiv (isoWhiskerRight h F :) _ _

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesLimit K₁ F
c : Cone K₂
t : IsLimit c
⊢ IsLimit ((Cones.postcompose (isoWhiskerRight h F).inv).obj (F.mapCone c))

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesLimit K₁ F
c : Cone K₂
t : IsLimit c
⊢ IsLimit ((Cones.postcompose (isoWhiskerRight h F).inv).obj (F.mapCone c))

Tactic:
have := (IsLimit.postcomposeInvEquiv h c).symm t

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesLimit K₁ F
c : Cone K₂
t : IsLimit c
this : IsLimit ((Cones.postcompose h.inv).obj c)
⊢ IsLimit ((Cones.postcompose (isoWhiskerRight h F).inv).obj (F.mapCone c))
-- Mathlib/Data/Complex/Exponential.lean
theorem exp_conj : exp (conj x) = conj (exp x)

Proof state:
x : ℂ
x✝ : ℕ
⊢ ↑(exp' ((starRingEnd ℂ) x)) x✝ = ↑(cauSeqConj (exp' x)) x✝

Tactic:
dsimp [exp', Function.comp_def, cauSeqConj]

Result:
x : ℂ
x✝ : ℕ
⊢ ∑ m ∈ range x✝, (starRingEnd ℂ) x ^ m / ↑m.factorial = (starRingEnd ℂ) (∑ m ∈ range x✝, x ^ m / ↑m.factorial)

Proof state:
x : ℂ
⊢ (exp' ((starRingEnd ℂ) x)).lim = (starRingEnd ℂ) (exp' x).lim

Tactic:
rw [← lim_conj]

Result:
x : ℂ
⊢ (exp' ((starRingEnd ℂ) x)).lim = (cauSeqConj (exp' x)).lim

Proof state:
x : ℂ
x✝ : ℕ
⊢ ∑ m ∈ range x✝, (starRingEnd ℂ) x ^ m / ↑m.factorial = ∑ x_1 ∈ range x✝, (starRingEnd ℂ) (x ^ x_1 / ↑x_1.factorial)

Tactic:
refine sum_congr rfl fun n _ => ?_

Result:
x : ℂ
x✝¹ n : ℕ
x✝ : n ∈ range x✝¹
⊢ (starRingEnd ℂ) x ^ n / ↑n.factorial = (starRingEnd ℂ) (x ^ n / ↑n.factorial)

Proof state:
x : ℂ
⊢ cexp ((starRingEnd ℂ) x) = (starRingEnd ℂ) (cexp x)

Tactic:
dsimp [exp]

Result:
x : ℂ
⊢ (exp' ((starRingEnd ℂ) x)).lim = (starRingEnd ℂ) (exp' x).lim

Proof state:
x : ℂ
⊢ (exp' ((starRingEnd ℂ) x)).lim = (cauSeqConj (exp' x)).lim

Tactic:
refine congr_arg CauSeq.lim (CauSeq.ext fun _ => ?_)

Result:
x : ℂ
x✝ : ℕ
⊢ ↑(exp' ((starRingEnd ℂ) x)) x✝ = ↑(cauSeqConj (exp' x)) x✝

Proof state:
x : ℂ
x✝¹ n : ℕ
x✝ : n ∈ range x✝¹
⊢ (starRingEnd ℂ) x ^ n / ↑n.factorial = (starRingEnd ℂ) (x ^ n / ↑n.factorial)

Tactic:
rw [map_div₀, map_pow, ← ofReal_natCast, conj_ofReal]

Result:
no goals

Proof state:
x : ℂ
x✝ : ℕ
⊢ ∑ m ∈ range x✝, (starRingEnd ℂ) x ^ m / ↑m.factorial = (starRingEnd ℂ) (∑ m ∈ range x✝, x ^ m / ↑m.factorial)

Tactic:
rw [map_sum (starRingEnd _)]

Result:
x : ℂ
x✝ : ℕ
⊢ ∑ m ∈ range x✝, (starRingEnd ℂ) x ^ m / ↑m.factorial = ∑ x_1 ∈ range x✝, (starRingEnd ℂ) (x ^ x_1 / ↑x_1.factorial)
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem log_zero_right (b : Ordinal) : log b 0 = 0

Proof state:
b : Ordinal.{u_1}
⊢ log b 0 = 0

Tactic:
obtain hb | hb := lt_or_le 1 b

Result:
case inl
b : Ordinal.{u_1}
hb : 1 < b
⊢ log b 0 = 0

case inr
b : Ordinal.{u_1}
hb : b ≤ 1
⊢ log b 0 = 0

Proof state:
case inr
b : Ordinal.{u_1}
hb : b ≤ 1
⊢ log b 0 = 0

Tactic:
rw [log_of_left_le_one hb]

Result:
no goals

Proof state:
case inl.h
b : Ordinal.{u_1}
hb : 1 < b
⊢ 1 ∈ {o | 0 < b ^ o}

Tactic:
rw [mem_setOf, opow_one]

Result:
case inl.h
b : Ordinal.{u_1}
hb : 1 < b
⊢ 0 < b

Proof state:
case inl
b : Ordinal.{u_1}
hb : 1 < b
⊢ log b 0 = 0

Tactic:
rw [log_def hb, ← Ordinal.le_zero, pred_le, succ_zero]

Result:
case inl
b : Ordinal.{u_1}
hb : 1 < b
⊢ sInf {o | 0 < b ^ o} ≤ 1

Proof state:
case inl
b : Ordinal.{u_1}
hb : 1 < b
⊢ sInf {o | 0 < b ^ o} ≤ 1

Tactic:
apply csInf_le'

Result:
case inl.h
b : Ordinal.{u_1}
hb : 1 < b
⊢ 1 ∈ {o | 0 < b ^ o}

Proof state:
case inl.h
b : Ordinal.{u_1}
hb : 1 < b
⊢ 0 < b

Tactic:
exact bot_lt_of_lt hb

Result:
no goals
-- Mathlib/Algebra/Polynomial/Identities.lean
theorem poly_binom_aux3 (f : R[X]) (x y : R) :
    f.eval (x + y) =
      ((f.sum fun e a => a * x ^ e) + f.sum fun e a => a * e * x ^ (e - 1) * y) +
        f.sum fun e a => a * (polyBinomAux1 x y e a).val * y ^ 2

Proof state:
R : Type u
inst✝ : CommRing R
f : R[X]
x y : R
⊢ eval (x + y) f =
    ((f.sum fun e a => a * x ^ e) + f.sum fun e a => a * ↑e * x ^ (e - 1) * y) +
      f.sum fun e a => a * ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2

Tactic:
rw [poly_binom_aux2]

Result:
R : Type u
inst✝ : CommRing R
f : R[X]
x y : R
⊢ (f.sum fun e a => a * (x ^ e + ↑e * x ^ (e - 1) * y + ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2)) =
    ((f.sum fun e a => a * x ^ e) + f.sum fun e a => a * ↑e * x ^ (e - 1) * y) +
      f.sum fun e a => a * ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2

Proof state:
R : Type u
inst✝ : CommRing R
f : R[X]
x y : R
⊢ (f.sum fun e a => a * (x ^ e + ↑e * x ^ (e - 1) * y + ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2)) =
    ((f.sum fun e a => a * x ^ e) + f.sum fun e a => a * ↑e * x ^ (e - 1) * y) +
      f.sum fun e a => a * ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2

Tactic:
simp [left_distrib, sum_add, mul_assoc]

Result:
no goals
-- Mathlib/Data/Real/Archimedean.lean
theorem le_sSup_iff (h : BddAbove s) (h' : s.Nonempty) :
    a ≤ sSup s ↔ ∀ ε, ε < 0 → ∃ x ∈ s, a + ε < x

Proof state:
case refine_2
s : Set ℝ
a : ℝ
h : BddAbove s
h' : s.Nonempty
H : ∀ ε < 0, ∃ x ∈ s, a + ε < x
ε : ℝ
ε_pos : 0 < ε
⊢ a < sSup s + ε

Tactic:
rcases H _ (neg_lt_zero.mpr ε_pos) with ⟨x, x_in, hx⟩

Result:
case refine_2.intro.intro
s : Set ℝ
a : ℝ
h : BddAbove s
h' : s.Nonempty
H : ∀ ε < 0, ∃ x ∈ s, a + ε < x
ε : ℝ
ε_pos : 0 < ε
x : ℝ
x_in : x ∈ s
hx : a + -ε < x
⊢ a < sSup s + ε

Proof state:
case refine_2.intro.intro
s : Set ℝ
a : ℝ
h : BddAbove s
h' : s.Nonempty
H : ∀ ε < 0, ∃ x ∈ s, a + ε < x
ε : ℝ
ε_pos : 0 < ε
x : ℝ
x_in : x ∈ s
hx : a + -ε < x
⊢ a < sSup s + ε

Tactic:
exact sub_lt_iff_lt_add.mp (lt_csSup_of_lt h x_in hx)

Result:
no goals

Proof state:
s : Set ℝ
a : ℝ
h : BddAbove s
h' : s.Nonempty
⊢ a ≤ sSup s ↔ ∀ ε < 0, ∃ x ∈ s, a + ε < x

Tactic:
rw [le_iff_forall_pos_lt_add]

Result:
s : Set ℝ
a : ℝ
h : BddAbove s
h' : s.Nonempty
⊢ (∀ (ε : ℝ), 0 < ε → a < sSup s + ε) ↔ ∀ ε < 0, ∃ x ∈ s, a + ε < x

Proof state:
s : Set ℝ
a : ℝ
h : BddAbove s
h' : s.Nonempty
⊢ (∀ (ε : ℝ), 0 < ε → a < sSup s + ε) ↔ ∀ ε < 0, ∃ x ∈ s, a + ε < x

Tactic:
refine ⟨fun H ε ε_neg => ?_, fun H ε ε_pos => ?_⟩

Result:
case refine_1
s : Set ℝ
a : ℝ
h : BddAbove s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → a < sSup s + ε
ε : ℝ
ε_neg : ε < 0
⊢ ∃ x ∈ s, a + ε < x

case refine_2
s : Set ℝ
a : ℝ
h : BddAbove s
h' : s.Nonempty
H : ∀ ε < 0, ∃ x ∈ s, a + ε < x
ε : ℝ
ε_pos : 0 < ε
⊢ a < sSup s + ε

Proof state:
case refine_1
s : Set ℝ
a : ℝ
h : BddAbove s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → a < sSup s + ε
ε : ℝ
ε_neg : ε < 0
⊢ ∃ x ∈ s, a + ε < x

Tactic:
exact exists_lt_of_lt_csSup h' (lt_sub_iff_add_lt.mp (H _ (neg_pos.mpr ε_neg)))

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem one_div_spanSingleton (x : K) : 1 / spanSingleton R₁⁰ x = spanSingleton R₁⁰ x⁻¹

Proof state:
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
x : K
⊢ 1 / spanSingleton R₁⁰ x = spanSingleton R₁⁰ x⁻¹

Tactic:
exact if h : x = 0 then by simp [h] else (eq_one_div_of_mul_eq_one_right _ _ (by simp [h])).symm

Result:
no goals

Proof state:
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
x : K
⊢ 1 / spanSingleton R₁⁰ x = spanSingleton R₁⁰ x⁻¹

Tactic:
classical
exact if h : x = 0 then by simp [h] else (eq_one_div_of_mul_eq_one_right _ _ (by simp [h])).symm

Result:
no goals

Proof state:
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
x : K
h : x = 0
⊢ 1 / spanSingleton R₁⁰ x = spanSingleton R₁⁰ x⁻¹

Tactic:
simp [h]

Result:
no goals

Proof state:
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
x : K
h : ¬x = 0
⊢ spanSingleton R₁⁰ x * spanSingleton R₁⁰ x⁻¹ = 1

Tactic:
simp [h]

Result:
no goals
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem aequiv_root (h : IsAdjoinRoot S f) (h' : IsAdjoinRoot T f) :
    h.aequiv h' h.root = h'.root

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R[X]
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
h : IsAdjoinRoot S f
h' : IsAdjoinRoot T f
⊢ (h.aequiv h') h.root = h'.root

Tactic:
rw [aequiv, AlgEquiv.coe_mk, Equiv.coe_fn_mk, liftHom_root]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Defs.lean
theorem contravariant_le_iff_contravariant_lt_and_eq [PartialOrder N] :
    Contravariant M N μ (· ≤ ·) ↔ Contravariant M N μ (· < ·) ∧ Contravariant M N μ (· = ·)

Proof state:
case refine_2
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Contravariant M N μ fun x1 x2 => x1 ≤ x2
a : M
b c : N
bc : (fun x1 x2 => x1 = x2) (μ a b) (μ a c)
⊢ (fun x1 x2 => x1 = x2) b c

Tactic:
exact (h a bc.le).antisymm (h a bc.ge)

Result:
no goals

Proof state:
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Contravariant M N μ fun x1 x2 => x1 ≤ x2
a : M
b : N
bc : μ a b < μ a b
⊢ False

Tactic:
exact lt_irrefl _ bc

Result:
no goals

Proof state:
case refine_1
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Contravariant M N μ fun x1 x2 => x1 ≤ x2
a : M
b c : N
bc : (fun x1 x2 => x1 < x2) (μ a b) (μ a c)
⊢ (fun x1 x2 => x1 < x2) b c

Tactic:
exact (h a bc.le).lt_of_ne (by rintro rfl; exact lt_irrefl _ bc)

Result:
no goals

Proof state:
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Contravariant M N μ fun x1 x2 => x1 ≤ x2
a : M
b c : N
bc : (fun x1 x2 => x1 < x2) (μ a b) (μ a c)
⊢ b ≠ c

Tactic:
rintro rfl

Result:
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Contravariant M N μ fun x1 x2 => x1 ≤ x2
a : M
b : N
bc : μ a b < μ a b
⊢ False

Proof state:
case refine_3
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : (Contravariant M N μ fun x1 x2 => x1 < x2) ∧ Contravariant M N μ fun x1 x2 => x1 = x2
a : M
b c : N
bc : (fun x1 x2 => x1 ≤ x2) (μ a b) (μ a c)
⊢ (fun x1 x2 => x1 ≤ x2) b c

Tactic:
exact bc.lt_or_eq.elim (fun bc ↦ (h.1 a bc).le) (fun bc ↦ (h.2 a bc).le)

Result:
no goals

Proof state:
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
⊢ (Contravariant M N μ fun x1 x2 => x1 ≤ x2) ↔
    (Contravariant M N μ fun x1 x2 => x1 < x2) ∧ Contravariant M N μ fun x1 x2 => x1 = x2

Tactic:
refine ⟨fun h ↦ ⟨fun a b c bc ↦ ?_, fun a b c bc ↦ ?_⟩, fun h ↦ fun a b c bc ↦ ?_⟩

Result:
case refine_1
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Contravariant M N μ fun x1 x2 => x1 ≤ x2
a : M
b c : N
bc : (fun x1 x2 => x1 < x2) (μ a b) (μ a c)
⊢ (fun x1 x2 => x1 < x2) b c

case refine_2
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Contravariant M N μ fun x1 x2 => x1 ≤ x2
a : M
b c : N
bc : (fun x1 x2 => x1 = x2) (μ a b) (μ a c)
⊢ (fun x1 x2 => x1 = x2) b c

case refine_3
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : (Contravariant M N μ fun x1 x2 => x1 < x2) ∧ Contravariant M N μ fun x1 x2 => x1 = x2
a : M
b c : N
bc : (fun x1 x2 => x1 ≤ x2) (μ a b) (μ a c)
⊢ (fun x1 x2 => x1 ≤ x2) b c
-- Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean
theorem d_comp_ε : (groupCohomology.resolution k G).d 1 0 ≫ ε k G = 0

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
x : ↑((resolution k G).X 1).V
⊢ (forget₂ToModuleCatHomotopyEquiv k G).hom.f 1 ≫
      ((ChainComplex.single₀ (ModuleCat k)).obj ((forget₂ (Rep k G) (ModuleCat k)).obj (Rep.trivial k G k))).d 1 0 =
    0

Tactic:
exact comp_zero

Result:
no goals

Proof state:
case h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
x : ↑((resolution k G).X 1).V
this : (forget₂ToModuleCat k G).d 1 0 ≫ (forget₂ (Rep k G) (ModuleCat k)).map (ε k G) = 0
⊢ (ModuleCat.Hom.hom ((resolution k G).d 1 0 ≫ ε k G).hom) x = (ModuleCat.Hom.hom (Action.Hom.hom 0)) x

Tactic:
exact LinearMap.ext_iff.1 (ModuleCat.hom_ext_iff.mp this) _

Result:
no goals

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
x : ↑((resolution k G).X 1).V
⊢ (forget₂ToModuleCat k G).d 1 0 ≫ (forget₂ (Rep k G) (ModuleCat k)).map (ε k G) = 0

Tactic:
rw [← forget₂ToModuleCatHomotopyEquiv_f_0_eq,
  ← (forget₂ToModuleCatHomotopyEquiv k G).1.2 1 0 rfl]

Result:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
x : ↑((resolution k G).X 1).V
⊢ (forget₂ToModuleCatHomotopyEquiv k G).hom.f 1 ≫
      ((ChainComplex.single₀ (ModuleCat k)).obj ((forget₂ (Rep k G) (ModuleCat k)).obj (Rep.trivial k G k))).d 1 0 =
    0

Proof state:
case h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ ((resolution k G).d 1 0 ≫ ε k G).hom = Action.Hom.hom 0

Tactic:
refine ModuleCat.hom_ext <| LinearMap.ext fun x => ?_

Result:
case h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
x : ↑((resolution k G).X 1).V
⊢ (ModuleCat.Hom.hom ((resolution k G).d 1 0 ≫ ε k G).hom) x = (ModuleCat.Hom.hom (Action.Hom.hom 0)) x

Proof state:
case h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
x : ↑((resolution k G).X 1).V
⊢ (ModuleCat.Hom.hom ((resolution k G).d 1 0 ≫ ε k G).hom) x = (ModuleCat.Hom.hom (Action.Hom.hom 0)) x

Tactic:
have : (forget₂ToModuleCat k G).d 1 0
    ≫ (forget₂ (Rep k G) (ModuleCat.{u} k)).map (ε k G) = 0 := by
  rw [← forget₂ToModuleCatHomotopyEquiv_f_0_eq,
    ← (forget₂ToModuleCatHomotopyEquiv k G).1.2 1 0 rfl]
  exact comp_zero

Result:
case h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
x : ↑((resolution k G).X 1).V
this : (forget₂ToModuleCat k G).d 1 0 ≫ (forget₂ (Rep k G) (ModuleCat k)).map (ε k G) = 0
⊢ (ModuleCat.Hom.hom ((resolution k G).d 1 0 ≫ ε k G).hom) x = (ModuleCat.Hom.hom (Action.Hom.hom 0)) x

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ (resolution k G).d 1 0 ≫ ε k G = 0

Tactic:
ext : 1

Result:
case h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ ((resolution k G).d 1 0 ≫ ε k G).hom = Action.Hom.hom 0
-- Mathlib/Probability/UniformOn.lean
theorem uniformOn_disjoint_union (hs : s.Finite) (ht : t.Finite) (hst : Disjoint s t) :
    uniformOn s u * uniformOn (s ∪ t) s + uniformOn t u * uniformOn (s ∪ t) t =
      uniformOn (s ∪ t) u

Proof state:
case inr.inl
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s u : Set Ω
hs : s.Finite
hs' : s.Nonempty
ht : ∅.Finite
hst : Disjoint s ∅
⊢ (uniformOn s) u * (uniformOn (s ∪ ∅)) s + (uniformOn ∅) u * (uniformOn (s ∪ ∅)) ∅ = (uniformOn (s ∪ ∅)) u

Tactic:
simp [uniformOn_self hs hs']

Result:
no goals
-- Mathlib/Topology/LocallyConstant/Basic.lean
theorem ofIsClopen_fiber_one {X : Type*} [TopologicalSpace X] {U : Set X} [∀ x, Decidable (x ∈ U)]
    (hU : IsClopen U) : ofIsClopen hU ⁻¹' ({1} : Set (Fin 2)) = Uᶜ

Proof state:
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ ⇑(ofIsClopen hU) ⁻¹' {1} = Uᶜ

Tactic:
ext

Result:
case h
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x✝ : X
⊢ x✝ ∈ ⇑(ofIsClopen hU) ⁻¹' {1} ↔ x✝ ∈ Uᶜ

Proof state:
case h
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x✝ : X
⊢ x✝ ∈ ⇑(ofIsClopen hU) ⁻¹' {1} ↔ x✝ ∈ Uᶜ

Tactic:
simp only [ofIsClopen, mem_singleton_iff, coe_mk, Fin.zero_eq_one_iff, mem_preimage,
  ite_eq_right_iff, mem_compl_iff, Nat.succ_succ_ne_one]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem disjoint_inv_right_iff : Disjoint f g⁻¹ ↔ Disjoint f g

Proof state:
α : Type u_1
f g : Perm α
⊢ f.Disjoint g⁻¹ ↔ f.Disjoint g

Tactic:
rw [disjoint_comm, disjoint_inv_left_iff, disjoint_comm]

Result:
no goals
-- Mathlib/ModelTheory/DirectLimit.lean
theorem lift_unique (F : DirectLimit G f ↪[L] P) (x) :
    F x =
      lift L ι G f (fun i => F.comp <| of L ι G f i)
        (fun i j hij x => by rw [F.comp_apply, F.comp_apply, of_f]) x :=
  DirectLimit.inductionOn x fun i x => by rw [lift_of]; rfl

Proof state:
L : Language
ι : Type v
inst✝⁵ : Preorder ι
G : ι → Type w
inst✝⁴ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝³ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝² : DirectedSystem G fun i j h => ⇑(f i j h)
inst✝¹ : Nonempty ι
P : Type u₁
inst✝ : L.Structure P
g : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
F : DirectLimit G f ↪[L] P
x✝ : DirectLimit G f
i j : ι
hij : i ≤ j
x : G i
⊢ ((fun i => F.comp (of L ι G f i)) j) ((f i j hij) x) = ((fun i => F.comp (of L ι G f i)) i) x

Tactic:
rw [F.comp_apply, F.comp_apply, of_f]

Result:
no goals

Proof state:
L : Language
ι : Type v
inst✝⁵ : Preorder ι
G : ι → Type w
inst✝⁴ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝³ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝² : DirectedSystem G fun i j h => ⇑(f i j h)
inst✝¹ : Nonempty ι
P : Type u₁
inst✝ : L.Structure P
F : DirectLimit G f ↪[L] P
x✝ : DirectLimit G f
i : ι
x : G i
⊢ F ((of L ι G f i) x) = (lift L ι G f (fun i => F.comp (of L ι G f i)) ⋯) ((of L ι G f i) x)

Tactic:
rw [lift_of]

Result:
L : Language
ι : Type v
inst✝⁵ : Preorder ι
G : ι → Type w
inst✝⁴ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝³ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝² : DirectedSystem G fun i j h => ⇑(f i j h)
inst✝¹ : Nonempty ι
P : Type u₁
inst✝ : L.Structure P
F : DirectLimit G f ↪[L] P
x✝ : DirectLimit G f
i : ι
x : G i
⊢ F ((of L ι G f i) x) = (F.comp (of L ι G f i)) x

Proof state:
L : Language
ι : Type v
inst✝⁵ : Preorder ι
G : ι → Type w
inst✝⁴ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝³ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝² : DirectedSystem G fun i j h => ⇑(f i j h)
inst✝¹ : Nonempty ι
P : Type u₁
inst✝ : L.Structure P
F : DirectLimit G f ↪[L] P
x✝ : DirectLimit G f
i : ι
x : G i
⊢ F ((of L ι G f i) x) = (F.comp (of L ι G f i)) x

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maximal.lean
theorem bot_isMaximal : IsMaximal (⊥ : Ideal K) :=
  ⟨⟨fun h => absurd ((eq_top_iff_one (⊤ : Ideal K)).mp rfl) (by rw [← h]; simp), fun I hI =>
      or_iff_not_imp_left.mp (eq_bot_or_top I) (ne_of_gt hI)⟩⟩

Proof state:
K : Type u
inst✝ : DivisionSemiring K
h : ⊥ = ⊤
⊢ 1 ∉ ⊤

Tactic:
rw [← h]

Result:
K : Type u
inst✝ : DivisionSemiring K
h : ⊥ = ⊤
⊢ 1 ∉ ⊥

Proof state:
K : Type u
inst✝ : DivisionSemiring K
h : ⊥ = ⊤
⊢ 1 ∉ ⊥

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Ring/Rat.lean
@[simp] lemma den_mul_eq_num (q : ℚ) : q.den * q = q.num

Proof state:
q : ℚ
⊢ ↑q.den * q = ↑q.num

Tactic:
rw [mul_comm, mul_den_eq_num]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem mem_idealRange_iff (h : IsIdealMorphism f) {y : L'} :
    y ∈ idealRange f ↔ ∃ x : L, f x = y

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
h : LieIdeal.toLieSubalgebra R L' f.idealRange = f.range
y : L'
⊢ y ∈ f.idealRange ↔ ∃ x, f x = y

Tactic:
rw [← LieSubmodule.mem_coe, ← LieIdeal.coe_toLieSubalgebra, h, f.range_coe, Set.mem_range]

Result:
no goals

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
h : f.IsIdealMorphism
y : L'
⊢ y ∈ f.idealRange ↔ ∃ x, f x = y

Tactic:
rw [f.isIdealMorphism_def] at h

Result:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
h : LieIdeal.toLieSubalgebra R L' f.idealRange = f.range
y : L'
⊢ y ∈ f.idealRange ↔ ∃ x, f x = y
-- Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean
theorem monotone_degree :
    Monotone (fun (x : DegLex (α →₀ ℕ)) ↦ (ofDegLex x).degree)

Proof state:
case inl
α : Type u_1
inst✝ : LinearOrder α
x y : DegLex (α →₀ ℕ)
h : (ofDegLex x).degree < (ofDegLex y).degree
⊢ (fun x => (ofDegLex x).degree) x ≤ (fun x => (ofDegLex x).degree) y

Tactic:
apply le_of_lt h

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrder α
x y : DegLex (α →₀ ℕ)
h : (ofDegLex x).degree = (ofDegLex y).degree ∧ toLex (ofDegLex x) ≤ toLex (ofDegLex y)
⊢ (fun x => (ofDegLex x).degree) x ≤ (fun x => (ofDegLex x).degree) y

Tactic:
apply le_of_eq h.1

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
⊢ Monotone fun x => (ofDegLex x).degree

Tactic:
intro x y

Result:
α : Type u_1
inst✝ : LinearOrder α
x y : DegLex (α →₀ ℕ)
⊢ x ≤ y → (fun x => (ofDegLex x).degree) x ≤ (fun x => (ofDegLex x).degree) y

Proof state:
α : Type u_1
inst✝ : LinearOrder α
x y : DegLex (α →₀ ℕ)
⊢ x ≤ y → (fun x => (ofDegLex x).degree) x ≤ (fun x => (ofDegLex x).degree) y

Tactic:
rw [le_iff]

Result:
α : Type u_1
inst✝ : LinearOrder α
x y : DegLex (α →₀ ℕ)
⊢ (ofDegLex x).degree < (ofDegLex y).degree ∨
      (ofDegLex x).degree = (ofDegLex y).degree ∧ toLex (ofDegLex x) ≤ toLex (ofDegLex y) →
    (fun x => (ofDegLex x).degree) x ≤ (fun x => (ofDegLex x).degree) y

Proof state:
α : Type u_1
inst✝ : LinearOrder α
x y : DegLex (α →₀ ℕ)
⊢ (ofDegLex x).degree < (ofDegLex y).degree ∨
      (ofDegLex x).degree = (ofDegLex y).degree ∧ toLex (ofDegLex x) ≤ toLex (ofDegLex y) →
    (fun x => (ofDegLex x).degree) x ≤ (fun x => (ofDegLex x).degree) y

Tactic:
rintro (h | h)

Result:
case inl
α : Type u_1
inst✝ : LinearOrder α
x y : DegLex (α →₀ ℕ)
h : (ofDegLex x).degree < (ofDegLex y).degree
⊢ (fun x => (ofDegLex x).degree) x ≤ (fun x => (ofDegLex x).degree) y

case inr
α : Type u_1
inst✝ : LinearOrder α
x y : DegLex (α →₀ ℕ)
h : (ofDegLex x).degree = (ofDegLex y).degree ∧ toLex (ofDegLex x) ≤ toLex (ofDegLex y)
⊢ (fun x => (ofDegLex x).degree) x ≤ (fun x => (ofDegLex x).degree) y