harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Fin/Basic.lean
/-- Sending `Fin (n+1)` to `Fin n` by subtracting one from anything above `p`
then back to `Fin (n+1)` with a gap around `p` is the identity away from `p`. -/
@[simp]
lemma succAbove_predAbove {p : Fin n} {i : Fin (n + 1)} (h : i ≠ castSucc p) :
    p.castSucc.succAbove (p.predAbove i) = i

Proof state:
case inl
n : ℕ
p : Fin n
i : Fin (n + 1)
h✝ : i ≠ p.castSucc
h : i < p.castSucc
⊢ p.castSucc.succAbove (p.predAbove i) = i

Tactic:
rw [predAbove_of_le_castSucc _ _ (Fin.le_of_lt h), succAbove_castPred_of_lt _ _ h]

Result:
no goals

Proof state:
case inr
n : ℕ
p : Fin n
i : Fin (n + 1)
h✝ : i ≠ p.castSucc
h : p.castSucc < i
⊢ p.castSucc.succAbove (p.predAbove i) = i

Tactic:
rw [predAbove_of_castSucc_lt _ _ h, succAbove_pred_of_lt _ _ h]

Result:
no goals

Proof state:
n : ℕ
p : Fin n
i : Fin (n + 1)
h : i ≠ p.castSucc
⊢ p.castSucc.succAbove (p.predAbove i) = i

Tactic:
obtain h | h := Fin.lt_or_lt_of_ne h

Result:
case inl
n : ℕ
p : Fin n
i : Fin (n + 1)
h✝ : i ≠ p.castSucc
h : i < p.castSucc
⊢ p.castSucc.succAbove (p.predAbove i) = i

case inr
n : ℕ
p : Fin n
i : Fin (n + 1)
h✝ : i ≠ p.castSucc
h : p.castSucc < i
⊢ p.castSucc.succAbove (p.predAbove i) = i
-- Mathlib/RingTheory/HahnSeries/Basic.lean
theorem embDomain_injective {f : Γ ↪o Γ'} :
    Function.Injective (embDomain f : HahnSeries Γ R → HahnSeries Γ' R) := fun x y xy => by
  ext g
  rw [HahnSeries.ext_iff, funext_iff] at xy
  have xyg := xy (f g)
  rwa [embDomain_coeff, embDomain_coeff] at xyg

Proof state:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : HahnSeries Γ R
xy : embDomain f x = embDomain f y
⊢ x = y

Tactic:
ext g

Result:
case coeff.h
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : HahnSeries Γ R
xy : embDomain f x = embDomain f y
g : Γ
⊢ x.coeff g = y.coeff g

Proof state:
case coeff.h
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : HahnSeries Γ R
xy : embDomain f x = embDomain f y
g : Γ
⊢ x.coeff g = y.coeff g

Tactic:
rw [HahnSeries.ext_iff, funext_iff] at xy

Result:
case coeff.h
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : HahnSeries Γ R
xy : ∀ (x_1 : Γ'), (embDomain f x).coeff x_1 = (embDomain f y).coeff x_1
g : Γ
⊢ x.coeff g = y.coeff g

Proof state:
case coeff.h
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : HahnSeries Γ R
xy : ∀ (x_1 : Γ'), (embDomain f x).coeff x_1 = (embDomain f y).coeff x_1
g : Γ
xyg : (embDomain f x).coeff (f g) = (embDomain f y).coeff (f g)
⊢ x.coeff g = y.coeff g

Tactic:
rwa [embDomain_coeff, embDomain_coeff] at xyg

Result:
no goals

Proof state:
case coeff.h
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : HahnSeries Γ R
xy : ∀ (x_1 : Γ'), (embDomain f x).coeff x_1 = (embDomain f y).coeff x_1
g : Γ
⊢ x.coeff g = y.coeff g

Tactic:
have xyg := xy (f g)

Result:
case coeff.h
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : HahnSeries Γ R
xy : ∀ (x_1 : Γ'), (embDomain f x).coeff x_1 = (embDomain f y).coeff x_1
g : Γ
xyg : (embDomain f x).coeff (f g) = (embDomain f y).coeff (f g)
⊢ x.coeff g = y.coeff g
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem mul_X_pow_comp {k : ℕ} : (p * X ^ k).comp r = p.comp r * r ^ k

Proof state:
case succ
R : Type u
inst✝ : Semiring R
p r : R[X]
k : ℕ
ih : (p * X ^ k).comp r = p.comp r * r ^ k
⊢ (p * X ^ (k + 1)).comp r = p.comp r * r ^ (k + 1)

Tactic:
simp [ih, pow_succ, ← mul_assoc, mul_X_comp]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p r : R[X]
k : ℕ
⊢ (p * X ^ k).comp r = p.comp r * r ^ k

Tactic:
induction k with
| zero => simp
| succ k ih => simp [ih, pow_succ, ← mul_assoc, mul_X_comp]

Result:
no goals

Proof state:
case zero
R : Type u
inst✝ : Semiring R
p r : R[X]
⊢ (p * X ^ 0).comp r = p.comp r * r ^ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem Codisjoint.himp_eq_right (h : Codisjoint a b) : b ⇨ a = a

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
⊢ b ⇨ a = ⊤ ⇨ a

Tactic:
rw [← h.eq_top, sup_himp_self_left]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
⊢ b ⇨ a = a

Tactic:
conv_rhs => rw [← @top_himp _ _ a]

Result:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
⊢ b ⇨ a = ⊤ ⇨ a
-- Mathlib/Data/List/Indexes.lean
theorem foldlIdx_eq_foldlIdxSpec (f : ℕ → α → β → α) (a bs start) :
    foldlIdx f a bs start = foldlIdxSpec f a bs start

Proof state:
α : Type u
β : Type v
f : ℕ → α → β → α
a : α
bs : List β
start : ℕ
⊢ foldlIdx f a bs start = foldlIdxSpec f a bs start

Tactic:
induction bs generalizing start a

Result:
case nil
α : Type u
β : Type v
f : ℕ → α → β → α
a : α
start : ℕ
⊢ foldlIdx f a [] start = foldlIdxSpec f a [] start

case cons
α : Type u
β : Type v
f : ℕ → α → β → α
head✝ : β
tail✝ : List β
tail_ih✝ : ∀ (a : α) (start : ℕ), foldlIdx f a tail✝ start = foldlIdxSpec f a tail✝ start
a : α
start : ℕ
⊢ foldlIdx f a (head✝ :: tail✝) start = foldlIdxSpec f a (head✝ :: tail✝) start

Proof state:
case nil
α : Type u
β : Type v
f : ℕ → α → β → α
a : α
start : ℕ
⊢ foldlIdx f a [] start = foldlIdxSpec f a [] start

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u
β : Type v
f : ℕ → α → β → α
head✝ : β
tail✝ : List β
tail_ih✝ : ∀ (a : α) (start : ℕ), foldlIdx f a tail✝ start = foldlIdxSpec f a tail✝ start
a : α
start : ℕ
⊢ foldlIdx f a (head✝ :: tail✝) start = foldlIdxSpec f a (head✝ :: tail✝) start

Tactic:
simp [foldlIdxSpec, *]

Result:
no goals
-- Mathlib/Order/SupClosed.lean
lemma InfClosed.preimage [FunLike F β α] [InfHomClass F β α] (hs : InfClosed s) (f : F) :
    InfClosed (f ⁻¹' s) :=
  fun a ha b hb ↦ by simpa [map_inf] using hs ha hb

Proof state:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : SemilatticeInf α
inst✝² : SemilatticeInf β
s : Set α
inst✝¹ : FunLike F β α
inst✝ : InfHomClass F β α
hs : InfClosed s
f : F
a : β
ha : a ∈ ⇑f ⁻¹' s
b : β
hb : b ∈ ⇑f ⁻¹' s
⊢ a ⊓ b ∈ ⇑f ⁻¹' s

Tactic:
simpa [map_inf] using hs ha hb

Result:
no goals
-- Mathlib/Topology/Semicontinuous.lean
theorem lowerSemicontinuousOn_univ_iff : LowerSemicontinuousOn f univ ↔ LowerSemicontinuous f

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type u_2
inst✝ : Preorder β
f : α → β
⊢ LowerSemicontinuousOn f univ ↔ LowerSemicontinuous f

Tactic:
simp [LowerSemicontinuousOn, LowerSemicontinuous, lowerSemicontinuousWithinAt_univ_iff]

Result:
no goals
-- Mathlib/Data/Part.lean
theorem some_append_some [Append α] (a b : α) : some a ++ some b = some (a ++ b)

Proof state:
α : Type u_1
inst✝ : Append α
a b : α
⊢ some a ++ some b = some (a ++ b)

Tactic:
simp [append_def]

Result:
no goals
-- Mathlib/Analysis/MeanInequalitiesPow.lean
theorem rpow_add_le_mul_rpow_add_rpow (z₁ z₂ : ℝ≥0∞) {p : ℝ} (hp : 1 ≤ p) :
    (z₁ + z₂) ^ p ≤ (2 : ℝ≥0∞) ^ (p - 1) * (z₁ ^ p + z₂ ^ p)

Proof state:
case h.e'_4
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
⊢ 2⁻¹ * 2 ^ p * (z₁ ^ p + z₂ ^ p) = 2⁻¹ * (2 ^ p * z₁ ^ p) + 2⁻¹ * (2 ^ p * z₂ ^ p)

Tactic:
ring

Result:
no goals

Proof state:
case h.e'_3
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
⊢ (z₁ + z₂) ^ p = (1 / 2 * (2 * z₁) + 1 / 2 * (2 * z₂)) ^ p

Tactic:
simp [← mul_assoc, ENNReal.inv_mul_cancel two_ne_zero ofNat_ne_top]

Result:
no goals

Proof state:
case h.e'_4
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
⊢ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p) = 1 / 2 * (2 * z₁) ^ p + 1 / 2 * (2 * z₂) ^ p

Tactic:
simp only [mul_rpow_of_nonneg _ _ (zero_le_one.trans hp), rpow_sub _ _ two_ne_zero ofNat_ne_top,
  ENNReal.div_eq_inv_mul, rpow_one, mul_one]

Result:
case h.e'_4
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
⊢ 2⁻¹ * 2 ^ p * (z₁ ^ p + z₂ ^ p) = 2⁻¹ * (2 ^ p * z₁ ^ p) + 2⁻¹ * (2 ^ p * z₂ ^ p)

Proof state:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
⊢ (z₁ + z₂) ^ p ≤ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p)

Tactic:
convert rpow_arith_mean_le_arith_mean2_rpow (1 / 2) (1 / 2) (2 * z₁) (2 * z₂)
    (ENNReal.add_halves 1) hp using 1

Result:
case h.e'_3
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
⊢ (z₁ + z₂) ^ p = (1 / 2 * (2 * z₁) + 1 / 2 * (2 * z₂)) ^ p

case h.e'_4
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
⊢ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p) = 1 / 2 * (2 * z₁) ^ p + 1 / 2 * (2 * z₂) ^ p
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isLittleO_const_left_of_ne {c : E''} (hc : c ≠ 0) :
    (fun _x => c) =o[l] g ↔ Tendsto (fun x => ‖g x‖) l atTop

Proof state:
α : Type u_1
F : Type u_4
E'' : Type u_9
inst✝¹ : Norm F
inst✝ : NormedAddCommGroup E''
g : α → F
l : Filter α
c : E''
hc : c ≠ 0
⊢ (fun _x => c) =o[l] g ↔ (fun _x => 1) =o[l] g

Tactic:
exact ⟨(isBigO_const_const (1 : ℝ) hc l).trans_isLittleO,
  (isBigO_const_one ℝ c l).trans_isLittleO⟩

Result:
no goals

Proof state:
α : Type u_1
F : Type u_4
E'' : Type u_9
inst✝¹ : Norm F
inst✝ : NormedAddCommGroup E''
g : α → F
l : Filter α
c : E''
hc : c ≠ 0
⊢ (fun _x => c) =o[l] g ↔ Tendsto (fun x => ‖g x‖) l atTop

Tactic:
simp only [← isLittleO_one_left_iff ℝ]

Result:
α : Type u_1
F : Type u_4
E'' : Type u_9
inst✝¹ : Norm F
inst✝ : NormedAddCommGroup E''
g : α → F
l : Filter α
c : E''
hc : c ≠ 0
⊢ (fun _x => c) =o[l] g ↔ (fun _x => 1) =o[l] g
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem kernelSubobject_zero {A B : C} : kernelSubobject (0 : A ⟶ B) = ⊤ :=
  (isIso_iff_mk_eq_top _).mp (by infer_instance)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
A B : C
⊢ IsIso (kernel.ι 0)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem galoisConnection_map_comap (hφ : Function.Injective φ.obj) :
    GaloisConnection (map φ hφ) (comap φ)

Proof state:
case mpr.im
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
T : Subgroupoid D
h : ∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d
c d : D
c✝ d✝ : C
a : c✝ ⟶ d✝
gφS : a ∈ S.arrows c✝ d✝
⊢ φ.map a ∈ T.arrows (φ.obj c✝) (φ.obj d✝)

Tactic:
exact h gφS

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
T : Subgroupoid D
⊢ map φ hφ S ≤ T ↔ S ≤ comap φ T

Tactic:
simp_rw [le_iff]

Result:
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
T : Subgroupoid D
⊢ (∀ {c d : D}, (map φ hφ S).arrows c d ⊆ T.arrows c d) ↔ ∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d

Proof state:
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
T : Subgroupoid D
⊢ (∀ {c d : D}, (map φ hφ S).arrows c d ⊆ T.arrows c d) ↔ ∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d

Tactic:
constructor

Result:
case mp
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
T : Subgroupoid D
⊢ (∀ {c d : D}, (map φ hφ S).arrows c d ⊆ T.arrows c d) → ∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d

case mpr
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
T : Subgroupoid D
⊢ (∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d) → ∀ {c d : D}, (map φ hφ S).arrows c d ⊆ T.arrows c d

Proof state:
case mpr
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
T : Subgroupoid D
⊢ (∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d) → ∀ {c d : D}, (map φ hφ S).arrows c d ⊆ T.arrows c d

Tactic:
rintro h _ _ g ⟨a, gφS⟩

Result:
case mpr.im
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
T : Subgroupoid D
h : ∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d
c d : D
c✝ d✝ : C
a : c✝ ⟶ d✝
gφS : a ∈ S.arrows c✝ d✝
⊢ φ.map a ∈ T.arrows (φ.obj c✝) (φ.obj d✝)

Proof state:
case mp
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
T : Subgroupoid D
⊢ (∀ {c d : D}, (map φ hφ S).arrows c d ⊆ T.arrows c d) → ∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d

Tactic:
exact fun h c d f fS => h (Map.Arrows.im f fS)

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
⊢ GaloisConnection (map φ hφ) (comap φ)

Tactic:
rintro S T

Result:
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
T : Subgroupoid D
⊢ map φ hφ S ≤ T ↔ S ≤ comap φ T
-- Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
theorem ι_range_disjoint_one :
    Disjoint (LinearMap.range (ι R : M →ₗ[R] TensorAlgebra R M))
      (1 : Submodule R (TensorAlgebra R M))

Proof state:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ∀ x ∈ LinearMap.range (ι R), x ∈ LinearMap.range (Algebra.linearMap R (TensorAlgebra R M)) → x = 0

Tactic:
rintro _ ⟨x, hx⟩ ⟨r, rfl⟩

Result:
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
hx : (ι R) x = (Algebra.linearMap R (TensorAlgebra R M)) r
⊢ (Algebra.linearMap R (TensorAlgebra R M)) r = 0

Proof state:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ Disjoint (LinearMap.range (ι R)) 1

Tactic:
rw [Submodule.disjoint_def, Submodule.one_eq_range]

Result:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ∀ x ∈ LinearMap.range (ι R), x ∈ LinearMap.range (Algebra.linearMap R (TensorAlgebra R M)) → x = 0

Proof state:
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
hx : x = 0 ∧ r = 0
⊢ (Algebra.linearMap R (TensorAlgebra R M)) r = 0

Tactic:
rw [hx.2, map_zero]

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
hx : (ι R) x = (Algebra.linearMap R (TensorAlgebra R M)) r
⊢ (Algebra.linearMap R (TensorAlgebra R M)) r = 0

Tactic:
rw [Algebra.linearMap_apply, ι_eq_algebraMap_iff] at hx

Result:
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
hx : x = 0 ∧ r = 0
⊢ (Algebra.linearMap R (TensorAlgebra R M)) r = 0
-- Mathlib/Algebra/Group/Center.lean
@[to_additive (attr := simp) addCentralizer_addCentralizer_addCentralizer]
lemma centralizer_centralizer_centralizer (S : Set M) :
    S.centralizer.centralizer.centralizer = S.centralizer

Proof state:
M : Type u_1
inst✝ : Mul M
S : Set M
x : M
hx : x ∈ S.centralizer.centralizer.centralizer
⊢ x ∈ S.centralizer

Tactic:
rw [Set.mem_centralizer_iff]

Result:
M : Type u_1
inst✝ : Mul M
S : Set M
x : M
hx : x ∈ S.centralizer.centralizer.centralizer
⊢ ∀ m ∈ S, m * x = x * m

Proof state:
M : Type u_1
inst✝ : Mul M
S : Set M
⊢ S.centralizer.centralizer.centralizer ⊆ S.centralizer

Tactic:
intro x hx

Result:
M : Type u_1
inst✝ : Mul M
S : Set M
x : M
hx : x ∈ S.centralizer.centralizer.centralizer
⊢ x ∈ S.centralizer

Proof state:
M : Type u_1
inst✝ : Mul M
S : Set M
x : M
hx : ∀ m ∈ S.centralizer.centralizer, m * x = x * m
y : M
hy : y ∈ S
⊢ y * x = x * y

Tactic:
exact hx y <| Set.subset_centralizer_centralizer hy

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Mul M
S : Set M
x : M
hx : x ∈ S.centralizer.centralizer.centralizer
y : M
hy : y ∈ S
⊢ y * x = x * y

Tactic:
rw [Set.mem_centralizer_iff] at hx

Result:
M : Type u_1
inst✝ : Mul M
S : Set M
x : M
hx : ∀ m ∈ S.centralizer.centralizer, m * x = x * m
y : M
hy : y ∈ S
⊢ y * x = x * y

Proof state:
M : Type u_1
inst✝ : Mul M
S : Set M
⊢ S.centralizer.centralizer.centralizer = S.centralizer

Tactic:
refine Set.Subset.antisymm ?_ Set.subset_centralizer_centralizer

Result:
M : Type u_1
inst✝ : Mul M
S : Set M
⊢ S.centralizer.centralizer.centralizer ⊆ S.centralizer

Proof state:
M : Type u_1
inst✝ : Mul M
S : Set M
x : M
hx : x ∈ S.centralizer.centralizer.centralizer
⊢ ∀ m ∈ S, m * x = x * m

Tactic:
intro y hy

Result:
M : Type u_1
inst✝ : Mul M
S : Set M
x : M
hx : x ∈ S.centralizer.centralizer.centralizer
y : M
hy : y ∈ S
⊢ y * x = x * y
-- Mathlib/LinearAlgebra/Matrix/Basis.lean
theorem toMatrix_unitsSMul [DecidableEq ι] (e : Basis ι R₂ M₂) (w : ι → R₂ˣ) :
    e.toMatrix (e.unitsSMul w) = diagonal ((↑) ∘ w)

Proof state:
case neg
ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
inst✝ : DecidableEq ι
e : Basis ι R₂ M₂
w : ι → R₂ˣ
i j : ι
h : ¬i = j
⊢ e.toMatrix (⇑(e.unitsSMul w)) i j = Matrix.diagonal (Units.val ∘ w) i j

Tactic:
simp [h, toMatrix_apply, unitsSMul_apply, Units.smul_def, Ne.symm h]

Result:
no goals

Proof state:
case pos
ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
inst✝ : DecidableEq ι
e : Basis ι R₂ M₂
w : ι → R₂ˣ
i j : ι
h : i = j
⊢ e.toMatrix (⇑(e.unitsSMul w)) i j = Matrix.diagonal (Units.val ∘ w) i j

Tactic:
simp [h, toMatrix_apply, unitsSMul_apply, Units.smul_def]

Result:
no goals

Proof state:
case a
ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
inst✝ : DecidableEq ι
e : Basis ι R₂ M₂
w : ι → R₂ˣ
i j : ι
⊢ e.toMatrix (⇑(e.unitsSMul w)) i j = Matrix.diagonal (Units.val ∘ w) i j

Tactic:
by_cases h : i = j

Result:
case pos
ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
inst✝ : DecidableEq ι
e : Basis ι R₂ M₂
w : ι → R₂ˣ
i j : ι
h : i = j
⊢ e.toMatrix (⇑(e.unitsSMul w)) i j = Matrix.diagonal (Units.val ∘ w) i j

case neg
ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
inst✝ : DecidableEq ι
e : Basis ι R₂ M₂
w : ι → R₂ˣ
i j : ι
h : ¬i = j
⊢ e.toMatrix (⇑(e.unitsSMul w)) i j = Matrix.diagonal (Units.val ∘ w) i j

Proof state:
ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
inst✝ : DecidableEq ι
e : Basis ι R₂ M₂
w : ι → R₂ˣ
⊢ e.toMatrix ⇑(e.unitsSMul w) = Matrix.diagonal (Units.val ∘ w)

Tactic:
ext i j

Result:
case a
ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
inst✝ : DecidableEq ι
e : Basis ι R₂ M₂
w : ι → R₂ˣ
i j : ι
⊢ e.toMatrix (⇑(e.unitsSMul w)) i j = Matrix.diagonal (Units.val ∘ w) i j
-- Mathlib/NumberTheory/Cyclotomic/Basic.lean
theorem neZero' [IsCyclotomicExtension {n} A B] [IsDomain B] : NeZero ((n : ℕ) : A)

Proof state:
n : ℕ+
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsCyclotomicExtension {n} A B
inst✝ : IsDomain B
this : NeZero ↑↑n
⊢ NeZero ↑↑n

Tactic:
exact NeZero.nat_of_neZero (algebraMap A B)

Result:
no goals

Proof state:
n : ℕ+
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsCyclotomicExtension {n} A B
inst✝ : IsDomain B
⊢ NeZero ↑↑n

Tactic:
haveI := IsCyclotomicExtension.neZero n A B

Result:
n : ℕ+
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsCyclotomicExtension {n} A B
inst✝ : IsDomain B
this : NeZero ↑↑n
⊢ NeZero ↑↑n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem zip_unzip (l : Array (α × β)) : zip (unzip l).1 (unzip l).2 = l

Proof state:
case mk
α : Type u_1
β : Type u_2
toList✝ : List (α × β)
⊢ { toList := toList✝ }.unzip.fst.zip { toList := toList✝ }.unzip.snd = { toList := toList✝ }

Tactic:
simp only [List.unzip_toArray, Prod.map_fst, Prod.map_snd, List.zip_toArray, List.zip_unzip]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Array (α × β)
⊢ l.unzip.fst.zip l.unzip.snd = l

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
toList✝ : List (α × β)
⊢ { toList := toList✝ }.unzip.fst.zip { toList := toList✝ }.unzip.snd = { toList := toList✝ }
-- Mathlib/Algebra/Module/LocalizedModule/Submodule.lean
@[simp]
lemma localized'_span (s : Set M) : (span R s).localized' S p f = span S (f '' s)

Proof state:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
s : Set M
⊢ localized' S p f (span R s) = span S (⇑f '' s)

Tactic:
rw [localized'_eq_span, ← map_coe, map_span, span_span_of_tower]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
theorem IsBlock.image {H Y : Type*} [Group H] [MulAction H Y]
    {φ : G →* H} (j : X →ₑ[φ] Y)
    (hφ : Function.Surjective φ) (hj : Function.Injective j)
    (hB : IsBlock G B) :
    IsBlock H (j '' B)

Proof state:
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
B : Set X
H : Type u_3
Y : Type u_4
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : G →* H
j : X →ₑ[⇑φ] Y
hφ : Function.Surjective ⇑φ
hj : Function.Injective ⇑j
hB : IsBlock G B
⊢ IsBlock H (⇑j '' B)

Tactic:
simp only [IsBlock, hφ.forall, ← image_smul_setₛₗ]

Result:
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
B : Set X
H : Type u_3
Y : Type u_4
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : G →* H
j : X →ₑ[⇑φ] Y
hφ : Function.Surjective ⇑φ
hj : Function.Injective ⇑j
hB : IsBlock G B
⊢ ∀ (x x_1 : G), ⇑j '' (x • B) ≠ ⇑j '' (x_1 • B) → Disjoint (⇑j '' (x • B)) (⇑j '' (x_1 • B))

Proof state:
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
B : Set X
H : Type u_3
Y : Type u_4
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : G →* H
j : X →ₑ[⇑φ] Y
hφ : Function.Surjective ⇑φ
hj : Function.Injective ⇑j
hB : IsBlock G B
⊢ ∀ (x x_1 : G), ⇑j '' (x • B) ≠ ⇑j '' (x_1 • B) → Disjoint (⇑j '' (x • B)) (⇑j '' (x_1 • B))

Tactic:
exact fun g₁ g₂ hg ↦ disjoint_image_of_injective hj <| hB <| ne_of_apply_ne _ hg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_setWidth'' (x : BitVec w) : (x.setWidth (k + 1)).msb = x.getLsbD k

Proof state:
w k : Nat
x : BitVec w
⊢ (setWidth (k + 1) x).msb = x.getLsbD k

Tactic:
simp [BitVec.msb, getMsbD]

Result:
no goals