harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Sites/Adjunction.lean
@[simp]
lemma adjunction_unit_app_val [HasWeakSheafify J D] [HasSheafCompose J F] (adj : G ⊣ F)
    (X : Sheaf J E) : ((adjunction J adj).unit.app X).val =
      (adj.whiskerRight Cᵒᵖ).unit.app _ ≫ whiskerRight (toSheafify J (X.val ⋙ G)) F

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{u_2, u_1} E
F : D ⥤ E
G : E ⥤ D
inst✝¹ : HasWeakSheafify J D
inst✝ : J.HasSheafCompose F
adj : G ⊣ F
X : Sheaf J E
⊢ ((adjunction J adj).unit.app X).val =
    (Adjunction.whiskerRight Cᵒᵖ adj).unit.app X.val ≫ whiskerRight (toSheafify J (X.val ⋙ G)) F

Tactic:
change (sheafToPresheaf _ _).map ((adjunction J adj).unit.app X) = _

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{u_2, u_1} E
F : D ⥤ E
G : E ⥤ D
inst✝¹ : HasWeakSheafify J D
inst✝ : J.HasSheafCompose F
adj : G ⊣ F
X : Sheaf J E
⊢ (sheafToPresheaf J E).map ((adjunction J adj).unit.app X) =
    (Adjunction.whiskerRight Cᵒᵖ adj).unit.app X.val ≫ whiskerRight (toSheafify J (X.val ⋙ G)) F

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{u_2, u_1} E
F : D ⥤ E
G : E ⥤ D
inst✝¹ : HasWeakSheafify J D
inst✝ : J.HasSheafCompose F
adj : G ⊣ F
X : Sheaf J E
⊢ (Adjunction.whiskerRight Cᵒᵖ adj).unit.app ((sheafToPresheaf J E).obj X) ≫
      whiskerRight (toSheafify J ((sheafToPresheaf J E).obj X ⋙ G)) F =
    (Adjunction.whiskerRight Cᵒᵖ adj).unit.app X.val ≫ whiskerRight (toSheafify J (X.val ⋙ G)) F

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{u_2, u_1} E
F : D ⥤ E
G : E ⥤ D
inst✝¹ : HasWeakSheafify J D
inst✝ : J.HasSheafCompose F
adj : G ⊣ F
X : Sheaf J E
⊢ (sheafToPresheaf J E).map ((adjunction J adj).unit.app X) =
    (Adjunction.whiskerRight Cᵒᵖ adj).unit.app X.val ≫ whiskerRight (toSheafify J (X.val ⋙ G)) F

Tactic:
simp only [Functor.id_obj, Functor.comp_obj, whiskeringRight_obj_obj, adjunction,
  Adjunction.map_restrictFullyFaithful_unit_app, Adjunction.comp_unit_app,
  sheafificationAdjunction_unit_app, whiskeringRight_obj_map, Iso.refl_hom, NatTrans.id_app,
  Functor.comp_map, Functor.map_id, whiskerRight_id', Category.comp_id]

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{u_2, u_1} E
F : D ⥤ E
G : E ⥤ D
inst✝¹ : HasWeakSheafify J D
inst✝ : J.HasSheafCompose F
adj : G ⊣ F
X : Sheaf J E
⊢ (Adjunction.whiskerRight Cᵒᵖ adj).unit.app ((sheafToPresheaf J E).obj X) ≫
      whiskerRight (toSheafify J ((sheafToPresheaf J E).obj X ⋙ G)) F =
    (Adjunction.whiskerRight Cᵒᵖ adj).unit.app X.val ≫ whiskerRight (toSheafify J (X.val ⋙ G)) F
-- Mathlib/MeasureTheory/OuterMeasure/Operations.lean
theorem top_apply {s : Set α} (h : s.Nonempty) : (⊤ : OuterMeasure α) s = ∞ :=
  let ⟨a, as⟩ := h
  top_unique <| le_trans (by simp [smul_dirac_apply, as]) (le_iSup₂ (∞ • dirac a) trivial)

Proof state:
α : Type u_1
s : Set α
h : s.Nonempty
a : α
as : a ∈ s
⊢ ⊤ ≤ (⊤ • dirac a) s

Tactic:
simp [smul_dirac_apply, as]

Result:
no goals
-- Mathlib/Data/Complex/BigOperators.lean
@[simp]
lemma im_expect (f : α → ℂ) : (𝔼 i ∈ s, f i).im = 𝔼 i ∈ s, (f i).im :=
  map_expect (LinearMap.mk imAddGroupHom.toAddHom (by simp)) f s

Proof state:
α : Type u_1
s : Finset α
f : α → ℂ
⊢ ∀ (m : ℚ≥0) (x : ℂ), (↑imAddGroupHom).toFun (m • x) = (RingHom.id ℚ≥0) m • (↑imAddGroupHom).toFun x

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[reassoc (attr := simp)]
lemma inl_v_snd_v (p q : ℤ) (hpq : p + (-1) = q) :
    (inl φ).v p q hpq ≫ (snd φ).v q q (add_zero q) = 0

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
p q : ℤ
hpq : p + -1 = q
⊢ (inl φ).v p q hpq ≫ (snd φ).v q q ⋯ = 0

Tactic:
simp [inl, snd]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm_exponent_top {f : α → ε} : eLpNorm f ∞ μ = eLpNormEssSup f μ

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
f : α → ε
⊢ eLpNorm f ⊤ μ = eLpNormEssSup f μ

Tactic:
simp [eLpNorm]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem coe_eq_one_iff : (φ : MvPowerSeries σ R) = 1 ↔ φ = 1

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
φ : MvPolynomial σ R
⊢ ↑φ = 1 ↔ φ = 1

Tactic:
rw [← coe_one, coe_inj]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm_one_eq_lintegral_enorm {f : α → ε} : eLpNorm f 1 μ = ∫⁻ x, ‖f x‖ₑ ∂μ

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
f : α → ε
⊢ eLpNorm f 1 μ = ∫⁻ (x : α), ‖f x‖ₑ ∂μ

Tactic:
simp_rw [eLpNorm_eq_lintegral_rpow_enorm one_ne_zero ENNReal.coe_ne_top, ENNReal.one_toReal,
  one_div_one, ENNReal.rpow_one]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Field.lean
theorem Tendsto.atTop_div_const (hr : 0 < r) (hf : Tendsto f l atTop) :
    Tendsto (fun x => f x / r) l atTop

Proof state:
α : Type u_1
β : Type u_2
inst✝ : LinearOrderedSemifield α
l : Filter β
f : β → α
r : α
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto (fun x => f x / r) l atTop

Tactic:
simpa only [div_eq_mul_inv] using hf.atTop_mul_const (inv_pos.2 hr)

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Norm.lean
theorem absNorm_eq' {I : FractionalIdeal R⁰ K} (a : R⁰) (I₀ : Ideal R)
    (h : a • (I : Submodule R K) = Submodule.map (Algebra.linearMap R K) I₀) :
    absNorm I = (Ideal.absNorm I₀ : ℚ) / |Algebra.norm ℤ (a : R)|

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Module.Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • ↑I = Submodule.map (Algebra.linearMap R K) I₀
⊢ absNorm I = ↑(Ideal.absNorm I₀) / ↑|(Algebra.norm ℤ) ↑a|

Tactic:
rw [absNorm, ← absNorm_div_norm_eq_absNorm_div_norm a I₀ h, MonoidWithZeroHom.coe_mk,
  ZeroHom.coe_mk]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem norm_compContinuous_le [TopologicalSpace γ] (f : α →ᵇ β) (g : C(γ, α)) :
    ‖f.compContinuous g‖ ≤ ‖f‖ :=
  ((lipschitz_compContinuous g).dist_le_mul f 0).trans <| by
    rw [NNReal.coe_one, one_mul, dist_zero_right]

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : TopologicalSpace γ
f : α →ᵇ β
g : C(γ, α)
⊢ ↑1 * dist f 0 ≤ ‖f‖

Tactic:
rw [NNReal.coe_one, one_mul, dist_zero_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} {fallback : β}
    (hab : a == b) : getD m a fallback = getD m b fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
a b : α
fallback : β
hab : (a == b) = true
⊢ getD m a fallback = getD m b fallback

Tactic:
simp_to_raw using Raw₀.Const.getD_congr

Result:
no goals
-- Mathlib/Data/NNRat/Defs.lean
theorem coe_sub (h : q ≤ p) : ((p - q : ℚ≥0) : ℚ) = p - q :=
  max_eq_left <| le_sub_comm.2 <| by rwa [sub_zero]

Proof state:
p q : ℚ≥0
h : q ≤ p
⊢ ↑q ≤ ↑p - 0

Tactic:
rwa [sub_zero]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
lemma intCast_cast_mul (x y : ZMod n) : (cast (x * y) : ℤ) = cast x * cast y % n

Proof state:
n : ℕ
x y : ZMod n
⊢ (x * y).cast = x.cast * y.cast % ↑n

Tactic:
rw [← ZMod.coe_intCast, Int.cast_mul, ZMod.intCast_zmod_cast, ZMod.intCast_zmod_cast]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
theorem comp_right_hasFDerivAt_iff {f : F → G} {x : E} {f' : F →L[𝕜] G} :
    HasFDerivAt (f ∘ iso) (f'.comp (iso : E →L[𝕜] F)) x ↔ HasFDerivAt f f' (iso x)

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
x : E
f' : F →L[𝕜] G
⊢ HasFDerivAt (f ∘ ⇑iso) (f'.comp ↑iso) x ↔ HasFDerivAt f f' (iso x)

Tactic:
simp only [← hasFDerivWithinAt_univ, ← comp_right_hasFDerivWithinAt_iff, preimage_univ]

Result:
no goals
-- Mathlib/Algebra/Group/Defs.lean
@[to_additive mul_nsmul']
lemma pow_mul' (a : M) (m n : ℕ) : a ^ (m * n) = (a ^ n) ^ m

Proof state:
M : Type u_2
inst✝ : Monoid M
a : M
m n : ℕ
⊢ a ^ (m * n) = (a ^ n) ^ m

Tactic:
rw [Nat.mul_comm, pow_mul]

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Lipschitz.lean
theorem lipschitzOnWith_iff_restrict : LipschitzOnWith K f s ↔ LipschitzWith K (s.restrict f)

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
⊢ LipschitzOnWith K f s ↔ LipschitzWith K (s.restrict f)

Tactic:
simp [LipschitzOnWith, LipschitzWith]

Result:
no goals
-- Mathlib/Algebra/Homology/TotalComplex.lean
@[reassoc]
lemma mapMap_D₂ (i₁₂ i₁₂' : I₁₂) :
    GradedObject.mapMap (toGradedObjectMap φ) _ i₁₂ ≫ L.D₂ c₁₂ i₁₂ i₁₂' =
      K.D₂ c₁₂ i₁₂ i₁₂' ≫ GradedObject.mapMap (toGradedObjectMap φ) _ i₁₂'

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
c₁₂ : ComplexShape I₁₂
inst✝³ : TotalComplexShape c₁ c₂ c₁₂
inst✝² : DecidableEq I₁₂
inst✝¹ : K.HasTotal c₁₂
inst✝ : L.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
⊢ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫ L.D₂ c₁₂ i₁₂ i₁₂' =
    K.D₂ c₁₂ i₁₂ i₁₂' ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂'

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Fold.lean
theorem foldr_loop_succ (f : Fin n → α → α) (x) (h : i < n) :
    foldr.loop n f (i+1) h x = foldr.loop n f i (Nat.le_of_lt h) (f ⟨i, h⟩ x)

Proof state:
n : Nat
α : Sort u_1
i : Nat
f : Fin n → α → α
x : α
h : i < n
⊢ foldr.loop n f (i + 1) h x = foldr.loop n f i ⋯ (f ⟨i, h⟩ x)

Tactic:
rw [foldr.loop]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Prod.lean
lemma prod_sum {ι ι' : Type*} [Countable ι'] (m : ι → Measure α) (m' : ι' → Measure β)
    [∀ n, SFinite (m' n)] :
    (Measure.sum m).prod (Measure.sum m') =
      Measure.sum (fun (p : ι × ι') ↦ (m p.1).prod (m' p.2))

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
ι : Type u_4
ι' : Type u_5
inst✝¹ : Countable ι'
m : ι → Measure α
m' : ι' → Measure β
inst✝ : ∀ (n : ι'), SFinite (m' n)
⊢ (sum m).prod (sum m') = sum fun p => (m p.1).prod (m' p.2)

Tactic:
simp_rw [prod_sum_left, prod_sum_right, sum_sum]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/WellKnown.lean
theorem invOneSubPow_zero : invOneSubPow S 0 = 1

Proof state:
S : Type u_1
inst✝ : CommRing S
⊢ invOneSubPow S 0 = 1

Tactic:
delta invOneSubPow

Result:
S : Type u_1
inst✝ : CommRing S
⊢ (match 0 with
    | 0 => 1
    | d.succ => { val := mk fun n => ↑((d + n).choose d), inv := (1 - X) ^ (d + 1), val_inv := ⋯, inv_val := ⋯ }) =
    1

Proof state:
S : Type u_1
inst✝ : CommRing S
⊢ (match 0 with
    | 0 => 1
    | d.succ => { val := mk fun n => ↑((d + n).choose d), inv := (1 - X) ^ (d + 1), val_inv := ⋯, inv_val := ⋯ }) =
    1

Tactic:
simp only [Units.val_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLastD_map (f : α → β) (l : List α) (a : α) : getLastD (map f l) (f a) = f (getLastD l a)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : List α
a : α
⊢ (map f l).getLastD (f a) = f (l.getLastD a)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Bitwise.lean
lemma bit_mod_two_eq_one_iff (a x) :
    bit a x % 2 = 1 ↔ a

Proof state:
a : Bool
x : ℕ
⊢ bit a x % 2 = 1 ↔ a = true

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
@[simp]
lemma snd_reverse (p : G.Walk u v) : p.reverse.snd = p.penultimate

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.snd = p.penultimate

Tactic:
simpa using getVert_reverse p 1

Result:
no goals
-- Mathlib/Order/Interval/Set/OrderIso.lean
theorem preimage_Ioo (e : α ≃o β) (a b : β) : e ⁻¹' Ioo a b = Ioo (e.symm a) (e.symm b)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : β
⊢ ⇑e ⁻¹' Ioo a b = Ioo (e.symm a) (e.symm b)

Tactic:
simp [← Ioi_inter_Iio]

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Basic.lean
theorem inter_comm (s₁ s₂ : Finset α) : s₁ ∩ s₂ = s₂ ∩ s₁ :=
  ext fun _ => by simp only [mem_inter, and_comm]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
x✝ : α
⊢ x✝ ∈ s₁ ∩ s₂ ↔ x✝ ∈ s₂ ∩ s₁

Tactic:
simp only [mem_inter, and_comm]

Result:
no goals
-- Mathlib/GroupTheory/Commutator/Basic.lean
theorem commutator_eq_bot_iff_le_centralizer : ⁅H₁, H₂⁆ = ⊥ ↔ H₁ ≤ centralizer H₂

Proof state:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
p : G
_hp : p ∈ H₁
q : G
hq : q ∈ H₂
⊢ ⁅p, q⁆ ∈ ⊥ ↔ q * p = p * q

Tactic:
rw [mem_bot, commutatorElement_eq_one_iff_mul_comm, eq_comm]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
⊢ ⁅H₁, H₂⁆ = ⊥ ↔ H₁ ≤ centralizer ↑H₂

Tactic:
rw [eq_bot_iff, commutator_le]

Result:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
⊢ (∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅g₁, g₂⁆ ∈ ⊥) ↔ H₁ ≤ centralizer ↑H₂

Proof state:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
⊢ (∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅g₁, g₂⁆ ∈ ⊥) ↔ H₁ ≤ centralizer ↑H₂

Tactic:
refine forall_congr' fun p =>
  forall_congr' fun _hp => forall_congr' fun q => forall_congr' fun hq => ?_

Result:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
p : G
_hp : p ∈ H₁
q : G
hq : q ∈ H₂
⊢ ⁅p, q⁆ ∈ ⊥ ↔ q * p = p * q
-- Mathlib/Data/Option/NAry.lean
theorem map₂_map_left_anticomm {f : α' → β → γ} {g : α → α'} {f' : β → α → δ} {g' : δ → γ}
    (h_left_anticomm : ∀ a b, f (g a) b = g' (f' b a)) :
    map₂ f (a.map g) b = (map₂ f' b a).map g'

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
α' : Type u_5
f : α' → β → γ
g : α → α'
f' : β → α → δ
g' : δ → γ
h_left_anticomm : ∀ (a : α) (b : β), f (g a) b = g' (f' b a)
⊢ map₂ f (Option.map g a) b = Option.map g' (map₂ f' b a)

Tactic:
cases a <;> cases b <;> simp [h_left_anticomm]

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean
theorem _root_.Algebra.adjoin.powerBasis'_gen (hx : IsIntegral R x) :
    (adjoin.powerBasis' hx).gen = ⟨x, SetLike.mem_coe.1 <| subset_adjoin <| mem_singleton x⟩

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
⊢ (adjoin.powerBasis' hx).gen = ⟨x, ⋯⟩

Tactic:
rw [Algebra.adjoin.powerBasis', PowerBasis.map_gen, AdjoinRoot.powerBasis'_gen, equivAdjoin,
  AlgEquiv.ofBijective_apply, Minpoly.toAdjoin, liftHom_root]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Abs.lean
lemma abs_unit_intCast (a : ℤˣ) : |((a : ℤ) : α)| = 1

Proof state:
α : Type u_1
inst✝ : LinearOrderedCommRing α
a : ℤˣ
⊢ |↑↑a| = 1

Tactic:
cases Int.units_eq_one_or a <;> simp_all

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem hasFDerivAt_ring_inverse (x : Rˣ) :
    HasFDerivAt Ring.inverse (-mulLeftRight 𝕜 R ↑x⁻¹ ↑x⁻¹) x :=
  have : (fun t : R => Ring.inverse (↑x + t) - ↑x⁻¹ + ↑x⁻¹ * t * ↑x⁻¹) =o[𝓝 0] id :=
    (inverse_add_norm_diff_second_order x).trans_isLittleO (isLittleO_norm_pow_id one_lt_two)
  by simpa [hasFDerivAt_iff_isLittleO_nhds_zero] using this

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
R : Type u_5
inst✝² : NormedRing R
inst✝¹ : HasSummableGeomSeries R
inst✝ : NormedAlgebra 𝕜 R
x : Rˣ
this : (fun t => Ring.inverse (↑x + t) - ↑x⁻¹ + ↑x⁻¹ * t * ↑x⁻¹) =o[𝓝 0] _root_.id
⊢ HasFDerivAt Ring.inverse (-((mulLeftRight 𝕜 R) ↑x⁻¹) ↑x⁻¹) ↑x

Tactic:
simpa [hasFDerivAt_iff_isLittleO_nhds_zero] using this

Result:
no goals
-- Mathlib/Data/Set/Function.lean
lemma SurjOn.comp_right {s : Set β} {t : Set γ} (hf : Surjective f) (hg : SurjOn g s t) :
    SurjOn (g ∘ f) (f ⁻¹' s) t

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
s : Set β
t : Set γ
hf : Surjective f
hg : SurjOn g s t
⊢ SurjOn (g ∘ f) (f ⁻¹' s) t

Tactic:
rwa [SurjOn, image_comp g f, image_preimage_eq _ hf]

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem star_eq_neg {c₁ : R} {a : ℍ[R,c₁,0,c₃]} : star a = -a ↔ a.re = 0

Proof state:
R : Type u_3
c₃ : R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
c₁ : R
a : ℍ[R,c₁,c₃]
⊢ star a = -a ↔ a.re = 0

Tactic:
simp [QuaternionAlgebra.ext_iff, eq_neg_iff_add_eq_zero]

Result:
no goals
-- Mathlib/Dynamics/Newton.lean
theorem isFixedPt_newtonMap_of_isUnit_iff (h : IsUnit <| aeval x (derivative P)) :
    IsFixedPt P.newtonMap x ↔ aeval x P = 0

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsUnit ((aeval x) (derivative P))
⊢ IsFixedPt P.newtonMap x ↔ (aeval x) P = 0

Tactic:
rw [IsFixedPt, newtonMap_apply, sub_eq_self, Ring.inverse_mul_eq_iff_eq_mul _ _ _ h, mul_zero]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem map_one_of_isOneCocycle {f : G → A} (hf : IsOneCocycle f) :
    f 1 = 0

Proof state:
G : Type u_1
A : Type u_2
inst✝² : Monoid G
inst✝¹ : AddCommGroup A
inst✝ : MulAction G A
f : G → A
hf : IsOneCocycle f
⊢ f 1 = 0

Tactic:
simpa only [mul_one, one_smul, self_eq_add_right] using hf 1 1

Result:
no goals
-- Mathlib/GroupTheory/Perm/List.lean
theorem formPerm_apply_lt_get (xs : List α) (h : Nodup xs) (n : ℕ) (hn : n + 1 < xs.length) :
    formPerm xs (xs.get (Fin.mk n ((Nat.lt_succ_self n).trans hn))) =
      xs.get (Fin.mk (n + 1) hn)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
xs : List α
h : xs.Nodup
n : ℕ
hn : n + 1 < xs.length
⊢ xs.formPerm (xs.get ⟨n, ⋯⟩) = xs.get ⟨n + 1, hn⟩

Tactic:
simp_all [formPerm_apply_lt_getElem]

Result:
no goals
-- Mathlib/Topology/FiberBundle/Trivialization.lean
theorem mk_symm (e : Pretrivialization F (π F E)) {b : B} (hb : b ∈ e.baseSet) (y : F) :
    TotalSpace.mk b (e.symm b y) = e.toPartialEquiv.symm (b, y)

Proof state:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → Zero (E x)
e : Pretrivialization F TotalSpace.proj
b : B
hb : b ∈ e.baseSet
y : F
⊢ { proj := b, snd := e.symm b y } = ↑e.symm (b, y)

Tactic:
simp only [e.symm_apply hb, TotalSpace.mk_cast (e.proj_symm_apply' hb), TotalSpace.eta]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Coloring.lean
theorem Coloring.card_colorClasses_le [Fintype α] [Fintype C.colorClasses] :
    Fintype.card C.colorClasses ≤ Fintype.card α

Proof state:
V : Type u
G : SimpleGraph V
α : Type u_1
C : G.Coloring α
inst✝¹ : Fintype α
inst✝ : Fintype ↑C.colorClasses
⊢ card ↑(Setoid.ker ⇑C).classes ≤ card α

Tactic:
convert Setoid.card_classes_ker_le C

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
α : Type u_1
C : G.Coloring α
inst✝¹ : Fintype α
inst✝ : Fintype ↑C.colorClasses
⊢ card ↑C.colorClasses ≤ card α

Tactic:
simp only [colorClasses]

Result:
V : Type u
G : SimpleGraph V
α : Type u_1
C : G.Coloring α
inst✝¹ : Fintype α
inst✝ : Fintype ↑C.colorClasses
⊢ card ↑(Setoid.ker ⇑C).classes ≤ card α
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem descFactorial_one (n : ℕ) : n.descFactorial 1 = n

Proof state:
n : ℕ
⊢ n.descFactorial 1 = n

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/ERealExp.lean
@[simp] lemma exp_zero : exp 0 = 1

Proof state:
⊢ exp 0 = 1

Tactic:
simp [exp]

Result:
no goals
-- Mathlib/Order/WithBot.lean
@[simp]
lemma WithBot.toDual_le_toDual_iff {x y : WithBot α} : x.toDual ≤ y.toDual ↔ y ≤ x

Proof state:
α : Type u_1
inst✝ : LE α
x y : WithBot α
⊢ WithBot.toDual x ≤ WithBot.toDual y ↔ y ≤ x

Tactic:
cases x <;> cases y <;> simp

Result:
no goals
-- Mathlib/Algebra/Field/Basic.lean
theorem Commute.inv_sub_inv (hab : Commute a b) (ha : a ≠ 0) (hb : b ≠ 0) :
    a⁻¹ - b⁻¹ = (b - a) / (a * b)

Proof state:
K : Type u_1
inst✝ : DivisionRing K
a b : K
hab : Commute a b
ha : a ≠ 0
hb : b ≠ 0
⊢ a⁻¹ - b⁻¹ = (b - a) / (a * b)

Tactic:
simp only [inv_eq_one_div, (Commute.one_right a).div_sub_div hab ha hb, one_mul, mul_one]

Result:
no goals
-- Mathlib/Analysis/Convex/Integral.lean
theorem ConcaveOn.set_average_mem_hypograph (hg : ConcaveOn ℝ s g) (hgc : ContinuousOn g s)
    (hsc : IsClosed s) (h0 : μ t ≠ 0) (ht : μ t ≠ ∞) (hfs : ∀ᵐ x ∂μ.restrict t, f x ∈ s)
    (hfi : IntegrableOn f t μ) (hgi : IntegrableOn (g ∘ f) t μ) :
    (⨍ x in t, f x ∂μ, ⨍ x in t, g (f x) ∂μ) ∈ {p : E × ℝ | p.1 ∈ s ∧ p.2 ≤ g p.1}

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
s : Set E
t : Set α
f : α → E
g : E → ℝ
hg : ConcaveOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed s
h0 : μ t ≠ 0
ht : μ t ≠ ⊤
hfs : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ s
hfi : IntegrableOn f t μ
hgi : IntegrableOn (g ∘ f) t μ
⊢ (⨍ (x : α) in t, f x ∂μ, ⨍ (x : α) in t, g (f x) ∂μ) ∈ {p | p.1 ∈ s ∧ p.2 ≤ g p.1}

Tactic:
simpa only [mem_setOf_eq, Pi.neg_apply, average_neg, neg_le_neg_iff] using
  hg.neg.set_average_mem_epigraph hgc.neg hsc h0 ht hfs hfi hgi.neg

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem not_mem_support_iff : n ∉ p.support ↔ p.coeff n = 0

Proof state:
R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
⊢ n ∉ p.support ↔ p.coeff n = 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem attach_map {o : Option α} (f : α → β) :
    (o.map f).attach = o.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem f h⟩)

Proof state:
α : Type u_1
β : Type u_2
o : Option α
f : α → β
⊢ (Option.map f o).attach =
    Option.map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨f x, ⋯⟩)
      o.attach

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/RingTheory/LocalRing/Module.lean
theorem map_mkQ_eq_top {N : Submodule R M} [Module.Finite R M] :
    N.map (Submodule.mkQ (𝔪 • ⊤)) = ⊤ ↔ N = ⊤

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
N : Submodule R M
inst✝ : Module.Finite R M
⊢ Submodule.map (𝔪 • ⊤).mkQ N = ⊤ ↔ N = ⊤

Tactic:
rw [← map_mkQ_eq (N₁ := N) le_top Module.Finite.fg_top, Submodule.map_top, Submodule.range_mkQ]

Result:
no goals
-- Mathlib/Order/Interval/Finset/SuccPred.lean
lemma Iio_succ_eq_Iic (b : α) : Iio (succ b) = Iic b := coe_injective <| by simp

Proof state:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrderBot α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
b : α
⊢ ↑(Iio (succ b)) = ↑(Iic b)

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem card_support_swap_mul {f : Perm α} {x : α} (hx : f x ≠ x) :
    #(swap x (f x) * f).support < #f.support :=
  Finset.card_lt_card
    ⟨fun _ hz => (mem_support_swap_mul_imp_mem_support_ne hz).left, fun h =>
      absurd (h (mem_support.2 hx)) (mt mem_support.1 (by simp))⟩

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
hx : f x ≠ x
h : f.support ⊆ (swap x (f x) * f).support
⊢ ¬(swap x (f x) * f) x ≠ x

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem IsPath.dropUntil {u v w : V} {p : G.Walk v w} (hc : p.IsPath)
    (h : u ∈ p.support) : (p.dropUntil u h).IsPath :=
  IsPath.of_append_right (p := p.takeUntil u h) (q := p.dropUntil u h)
    (by rwa [← take_spec _ h] at hc)

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
hc : p.IsPath
h : u ∈ p.support
⊢ ((p.takeUntil u h).append (p.dropUntil u h)).IsPath

Tactic:
rwa [← take_spec _ h] at hc

Result:
no goals