harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Real/Pointwise.lean
theorem Real.iInf_mul_of_nonpos (ha : r ≤ 0) (f : ι → ℝ) : (⨅ i, f i) * r = ⨆ i, f i * r

Proof state:
ι : Sort u_1
r : ℝ
ha : r ≤ 0
f : ι → ℝ
⊢ (⨅ i, f i) * r = ⨆ i, f i * r

Tactic:
simp only [Real.mul_iInf_of_nonpos ha, mul_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/lake/Lake/Util/Name.lean
theorem quickCmpAux_iff_eq : ∀ {n n'}, quickCmpAux n n' = .eq ↔ n = n'
| .anonymous, n => by cases n <;> simp [quickCmpAux]
| n, .anonymous => by cases n <;> simp [quickCmpAux]
| .num .., .str .. => by simp [quickCmpAux]
| .str .., .num .. => by simp [quickCmpAux]
| .num p₁ n₁, .num p₂ n₂ => by
  simp only [quickCmpAux]; split <;>
  simp_all [quickCmpAux_iff_eq, show ∀ p, (p → False) ↔ ¬ p from fun _ => .rfl]
| .str p₁ s₁, .str p₂ s₂ => by
  simp only [quickCmpAux]; split <;>
  simp_all [quickCmpAux_iff_eq, show ∀ p, (p → False) ↔ ¬ p from fun _ => .rfl]

Proof state:
p₁ : Name
s₁ : String
p₂ : Name
s₂ : String
⊢ (p₁.str s₁).quickCmpAux (p₂.str s₂) = Ordering.eq ↔ p₁.str s₁ = p₂.str s₂

Tactic:
simp only [quickCmpAux]

Result:
p₁ : Name
s₁ : String
p₂ : Name
s₂ : String
⊢ (match compare s₁ s₂ with
      | Ordering.eq => p₁.quickCmpAux p₂
      | ord => ord) =
      Ordering.eq ↔
    p₁.str s₁ = p₂.str s₂

Proof state:
p₁ : Name
n₁ : Nat
p₂ : Name
n₂ : Nat
⊢ (match compare n₁ n₂ with
      | Ordering.eq => p₁.quickCmpAux p₂
      | ord => ord) =
      Ordering.eq ↔
    p₁.num n₁ = p₂.num n₂

Tactic:
split <;>
simp_all [quickCmpAux_iff_eq, show ∀ p, (p → False) ↔ ¬ p from fun _ => .rfl]

Result:
no goals

Proof state:
p₁ : Name
n₁ : Nat
p₂ : Name
n₂ : Nat
⊢ (p₁.num n₁).quickCmpAux (p₂.num n₂) = Ordering.eq ↔ p₁.num n₁ = p₂.num n₂

Tactic:
simp only [quickCmpAux]

Result:
p₁ : Name
n₁ : Nat
p₂ : Name
n₂ : Nat
⊢ (match compare n₁ n₂ with
      | Ordering.eq => p₁.quickCmpAux p₂
      | ord => ord) =
      Ordering.eq ↔
    p₁.num n₁ = p₂.num n₂

Proof state:
p₁ : Name
s₁ : String
p₂ : Name
s₂ : String
⊢ (match compare s₁ s₂ with
      | Ordering.eq => p₁.quickCmpAux p₂
      | ord => ord) =
      Ordering.eq ↔
    p₁.str s₁ = p₂.str s₂

Tactic:
split <;>
simp_all [quickCmpAux_iff_eq, show ∀ p, (p → False) ↔ ¬ p from fun _ => .rfl]

Result:
no goals

Proof state:
pre✝¹ : Name
i✝ : Nat
pre✝ : Name
str✝ : String
⊢ (pre✝¹.num i✝).quickCmpAux (pre✝.str str✝) = Ordering.eq ↔ pre✝¹.num i✝ = pre✝.str str✝

Tactic:
simp [quickCmpAux]

Result:
no goals

Proof state:
pre✝¹ : Name
str✝ : String
pre✝ : Name
i✝ : Nat
⊢ (pre✝¹.str str✝).quickCmpAux (pre✝.num i✝) = Ordering.eq ↔ pre✝¹.str str✝ = pre✝.num i✝

Tactic:
simp [quickCmpAux]

Result:
no goals

Proof state:
n : Name
⊢ anonymous.quickCmpAux n = Ordering.eq ↔ anonymous = n

Tactic:
cases n <;> simp [quickCmpAux]

Result:
no goals

Proof state:
n : Name
⊢ n.quickCmpAux anonymous = Ordering.eq ↔ n = anonymous

Tactic:
cases n <;> simp [quickCmpAux]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Schur.lean
theorem finrank_hom_simple_simple (X Y : C) [∀ X Y : C, FiniteDimensional 𝕜 (X ⟶ Y)] [Simple X]
    [Simple Y] : finrank 𝕜 (X ⟶ Y) = if Nonempty (X ≅ Y) then 1 else 0

Proof state:
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : ∀ (X Y : C), FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ finrank 𝕜 (X ⟶ Y) = if Nonempty (X ≅ Y) then 1 else 0

Tactic:
split_ifs with h

Result:
case pos
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : ∀ (X Y : C), FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nonempty (X ≅ Y)
⊢ finrank 𝕜 (X ⟶ Y) = 1

case neg
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : ∀ (X Y : C), FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
h : ¬Nonempty (X ≅ Y)
⊢ finrank 𝕜 (X ⟶ Y) = 0

Proof state:
case neg
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : ∀ (X Y : C), FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
h : ¬Nonempty (X ≅ Y)
⊢ finrank 𝕜 (X ⟶ Y) = 0

Tactic:
exact (finrank_hom_simple_simple_eq_zero_iff 𝕜 X Y).2 (not_nonempty_iff.mp h)

Result:
no goals

Proof state:
case pos
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : ∀ (X Y : C), FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nonempty (X ≅ Y)
⊢ finrank 𝕜 (X ⟶ Y) = 1

Tactic:
exact (finrank_hom_simple_simple_eq_one_iff 𝕜 X Y).2 h

Result:
no goals
-- Mathlib/Data/Finset/Sum.lean
@[simp] lemma toRight_map_sumComm : (u.map (Equiv.sumComm _ _).toEmbedding).toRight = u.toLeft

Proof state:
case h
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
x : α
⊢ x ∈ (map (Equiv.sumComm α β).toEmbedding u).toRight ↔ x ∈ u.toLeft

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
⊢ (map (Equiv.sumComm α β).toEmbedding u).toRight = u.toLeft

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
x : α
⊢ x ∈ (map (Equiv.sumComm α β).toEmbedding u).toRight ↔ x ∈ u.toLeft
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocMod_neg' (a b : α) : toIocMod hp (-a) b = p - toIcoMod hp a (-b)

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp (-a) b = p - toIcoMod hp a (-b)

Tactic:
simpa only [neg_neg] using toIocMod_neg hp (-a) (-b)

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean
/-- If `Q` contains identities and respects isomorphisms (i.e. is satisfied by isomorphisms),
and `P` is affine locally defined by `affineAnd Q`, then `P` contains identities. -/
lemma HasAffineProperty.affineAnd_containsIdentities {P : MorphismProperty Scheme.{u}}
    (hA : HasAffineProperty P (affineAnd Q)) (hQi : RingHom.RespectsIso Q)
    (hQ : RingHom.ContainsIdentities Q) :
    P.ContainsIdentities where
  id_mem X

Proof state:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
hQ : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] => Q
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ IsAffineOpen (𝟙 X ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app (𝟙 X) U))

Tactic:
exact ⟨hU, hQ _⟩

Result:
no goals

Proof state:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
hQ : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] => Q
X : Scheme
⊢ ∀ (U : X.Opens), IsAffineOpen U → IsAffineOpen (𝟙 X ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app (𝟙 X) U))

Tactic:
intro U hU

Result:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
hQ : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] => Q
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ IsAffineOpen (𝟙 X ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app (𝟙 X) U))

Proof state:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
hQ : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] => Q
X : Scheme
⊢ P (𝟙 X)

Tactic:
rw [eq_targetAffineLocally P, targetAffineLocally_affineAnd_iff hQi]

Result:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q
hQ : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] => Q
X : Scheme
⊢ ∀ (U : X.Opens), IsAffineOpen U → IsAffineOpen (𝟙 X ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app (𝟙 X) U))
-- Mathlib/GroupTheory/CommutingProbability.lean
theorem commProb_le_one : commProb M ≤ 1

Proof state:
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
⊢ commProb M ≤ 1

Tactic:
refine div_le_one_of_le₀ ?_ (sq_nonneg (Nat.card M : ℚ))

Result:
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
⊢ ↑(Nat.card { p // Commute p.1 p.2 }) ≤ ↑(Nat.card M) ^ 2

Proof state:
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
⊢ Nat.card { p // Commute p.1 p.2 } ≤ Nat.card (M × M)

Tactic:
apply Finite.card_subtype_le

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
⊢ ↑(Nat.card { p // Commute p.1 p.2 }) ≤ ↑(Nat.card M) ^ 2

Tactic:
rw [← Nat.cast_pow, Nat.cast_le, sq, ← Nat.card_prod]

Result:
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
⊢ Nat.card { p // Commute p.1 p.2 } ≤ Nat.card (M × M)
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem ContinuousLinearEquiv.contDiffAt_comp_iff (e : G ≃L[𝕜] E) :
    ContDiffAt 𝕜 n (f ∘ e) (e.symm x) ↔ ContDiffAt 𝕜 n f x

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
x : E
n : WithTop ℕ∞
e : G ≃L[𝕜] E
⊢ ContDiffWithinAt 𝕜 n (f ∘ ⇑e) (?m.445397 ⁻¹' univ) (e.symm x) ↔ ContDiffWithinAt 𝕜 n f univ x

𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
x : E
n : WithTop ℕ∞
e : G ≃L[𝕜] E
⊢ Type ?u.445393

𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
x : E
n : WithTop ℕ∞
e : G ≃L[𝕜] E
⊢ G → ?m.445396

Tactic:
exact e.contDiffWithinAt_comp_iff

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
x : E
n : WithTop ℕ∞
e : G ≃L[𝕜] E
⊢ ContDiffAt 𝕜 n (f ∘ ⇑e) (e.symm x) ↔ ContDiffAt 𝕜 n f x

Tactic:
rw [← contDiffWithinAt_univ, ← contDiffWithinAt_univ, ← preimage_univ]

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
x : E
n : WithTop ℕ∞
e : G ≃L[𝕜] E
⊢ ContDiffWithinAt 𝕜 n (f ∘ ⇑e) (?m.445397 ⁻¹' univ) (e.symm x) ↔ ContDiffWithinAt 𝕜 n f univ x

𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
x : E
n : WithTop ℕ∞
e : G ≃L[𝕜] E
⊢ Type ?u.445393

𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
x : E
n : WithTop ℕ∞
e : G ≃L[𝕜] E
⊢ G → ?m.445396
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean
theorem biprod.isoCoprod_inv {X Y : C} [HasBinaryBiproduct X Y] :
    (biprod.isoCoprod X Y).inv = coprod.desc biprod.inl biprod.inr

Proof state:
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (isoCoprod X Y).inv = coprod.desc inl inr

Tactic:
ext <;> simp [biprod.isoCoprod]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem coeff_monomial_mul (p : R[X]) (n d : ℕ) (r : R) :
    coeff (monomial n r * p) (d + n) = r * coeff p d

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
r : R
⊢ ((monomial n) r * p).coeff (d + n) = r * p.coeff d

Tactic:
rw [← C_mul_X_pow_eq_monomial, mul_assoc, coeff_C_mul, X_pow_mul, coeff_mul_X_pow]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Bivariate.lean
lemma map_mapRingHom_eval_map_eval (r : R) :
    ((p.map <| mapRingHom f).eval <| q.map f).eval (f r) = f ((p.eval q).eval r)

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X][Y]
q : R[X]
r : R
⊢ eval (f r) (eval (map f q) (map (mapRingHom f) p)) = f (eval r (eval q p))

Tactic:
rw [map_mapRingHom_eval_map, eval_map, eval₂_hom]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem centroid_univ (s : Finset P) : univ.centroid k ((↑) : s → P) = s.centroid k id

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Finset P
⊢ centroid k univ Subtype.val = centroid k s id

Tactic:
rw [centroid, centroid, ← s.attach_affineCombination_coe]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Finset P
⊢ (affineCombination k univ Subtype.val) (centroidWeights k univ) =
    (affineCombination k s.attach Subtype.val) (centroidWeights k s ∘ Subtype.val)

Proof state:
case h.e_6.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Finset P
⊢ centroidWeights k univ = centroidWeights k s ∘ Subtype.val

Tactic:
ext

Result:
case h.e_6.h.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Finset P
x✝ : { x // x ∈ s }
⊢ centroidWeights k univ x✝ = (centroidWeights k s ∘ Subtype.val) x✝

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Finset P
⊢ (affineCombination k univ Subtype.val) (centroidWeights k univ) =
    (affineCombination k s.attach Subtype.val) (centroidWeights k s ∘ Subtype.val)

Tactic:
congr

Result:
case h.e_6.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Finset P
⊢ centroidWeights k univ = centroidWeights k s ∘ Subtype.val

Proof state:
case h.e_6.h.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Finset P
x✝ : { x // x ∈ s }
⊢ centroidWeights k univ x✝ = (centroidWeights k s ∘ Subtype.val) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Units/Regulator.lean
theorem regulator_eq_det (w' : InfinitePlace K) (e : {w // w ≠ w'} ≃ Fin (rank K)) :
    regulator K =
      |(Matrix.of fun i w : {w // w ≠ w'} ↦ (mult w.val : ℝ) *
        Real.log (w.val (fundSystem K (e i) : K))).det|

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
⊢ Fintype.card { w // w ≠ w₀ } = Fintype.card (Fin (rank K))

Tactic:
rw [Fintype.card_subtype_compl, Fintype.card_ofSubsingleton, Fintype.card_fin, rank]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
e' : { w // w ≠ w₀ } ≃ Fin (rank K) := Fintype.equivOfCardEq ⋯
⊢ |(Matrix.of fun i w =>
          ↑(↑w).mult *
            Real.log (↑w ((algebraMap (𝓞 K) K) ↑(Additive.toMul (Additive.ofMul (fundSystem K (e' i))))))).det| =
    |(Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(fundSystem K (e i))))).det|

Tactic:
exact abs_det_eq_abs_det K (fun i ↦ fundSystem K i) e' e

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
⊢ regulator K = |(Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(fundSystem K (e i))))).det|

Tactic:
let e' : {w : InfinitePlace K // w ≠ w₀} ≃ Fin (rank K) := Fintype.equivOfCardEq (by
  rw [Fintype.card_subtype_compl, Fintype.card_ofSubsingleton, Fintype.card_fin, rank])

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
e' : { w // w ≠ w₀ } ≃ Fin (rank K) := Fintype.equivOfCardEq ⋯
⊢ regulator K = |(Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(fundSystem K (e i))))).det|

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
e' : { w // w ≠ w₀ } ≃ Fin (rank K) := Fintype.equivOfCardEq ⋯
⊢ regulator K = |(Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(fundSystem K (e i))))).det|

Tactic:
simp_rw [regulator_eq_det' K e', logEmbedding, AddMonoidHom.coe_mk, ZeroHom.coe_mk]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
e' : { w // w ≠ w₀ } ≃ Fin (rank K) := Fintype.equivOfCardEq ⋯
⊢ |(Matrix.of fun i w =>
          ↑(↑w).mult *
            Real.log (↑w ((algebraMap (𝓞 K) K) ↑(Additive.toMul (Additive.ofMul (fundSystem K (e' i))))))).det| =
    |(Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(fundSystem K (e i))))).det|
-- Mathlib/Data/Real/GoldenRatio.lean
theorem fibRec_charPoly_eq {β : Type*} [CommRing β] :
    fibRec.charPoly = X ^ 2 - (X + (1 : β[X]))

Proof state:
β : Type u_2
inst✝ : CommRing β
⊢ fibRec.charPoly = X ^ 2 - (X + 1)

Tactic:
rw [fibRec, LinearRecurrence.charPoly]

Result:
β : Type u_2
inst✝ : CommRing β
⊢ (monomial { order := 2, coeffs := ![1, 1] }.order) 1 -
      ∑ i : Fin { order := 2, coeffs := ![1, 1] }.order, (monomial ↑i) ({ order := 2, coeffs := ![1, 1] }.coeffs i) =
    X ^ 2 - (X + 1)

Proof state:
β : Type u_2
inst✝ : CommRing β
⊢ (monomial { order := 2, coeffs := ![1, 1] }.order) 1 -
      ∑ i : Fin { order := 2, coeffs := ![1, 1] }.order, (monomial ↑i) ({ order := 2, coeffs := ![1, 1] }.coeffs i) =
    X ^ 2 - (X + 1)

Tactic:
simp [Finset.sum_fin_eq_sum_range, Finset.sum_range_succ', ← smul_X_eq_monomial]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Basic.lean
theorem not_isField : ¬IsField (𝓞 K)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h_inj : Injective ⇑(algebraMap ℤ (𝓞 K))
⊢ ¬IsField (𝓞 K)

Tactic:
intro hf

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h_inj : Injective ⇑(algebraMap ℤ (𝓞 K))
hf : IsField (𝓞 K)
⊢ False

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ¬IsField (𝓞 K)

Tactic:
have h_inj : Function.Injective (algebraMap ℤ (𝓞 K)) := RingHom.injective_int (algebraMap ℤ (𝓞 K))

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h_inj : Injective ⇑(algebraMap ℤ (𝓞 K))
⊢ ¬IsField (𝓞 K)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h_inj : Injective ⇑(algebraMap ℤ (𝓞 K))
hf : IsField (𝓞 K)
⊢ False

Tactic:
exact Int.not_isField
  (((IsIntegralClosure.isIntegral_algebra ℤ K).isField_iff_isField h_inj).mpr hf)

Result:
no goals
-- Mathlib/GroupTheory/FreeAbelianGroup.lean
theorem of_ne_zero (x : α) : of x ≠ 0

Proof state:
α : Type u
x : α
h : of x = 0
f : FreeAbelianGroup α →+ ℤ := lift 1
hfx : f (of x) = 1
⊢ f (of x) = 0

Tactic:
rw [h, map_zero]

Result:
no goals

Proof state:
α : Type u
x : α
h : of x = 0
f : FreeAbelianGroup α →+ ℤ := lift 1
hfx : f (of x) = 1
hf0 : f (of x) = 0
⊢ False

Tactic:
exact one_ne_zero <| hfx.symm.trans hf0

Result:
no goals

Proof state:
α : Type u
x : α
h : of x = 0
f : FreeAbelianGroup α →+ ℤ := lift 1
⊢ False

Tactic:
have hfx : f (of x) = 1 := lift.of _ _

Result:
α : Type u
x : α
h : of x = 0
f : FreeAbelianGroup α →+ ℤ := lift 1
hfx : f (of x) = 1
⊢ False

Proof state:
α : Type u
x : α
⊢ of x ≠ 0

Tactic:
intro h

Result:
α : Type u
x : α
h : of x = 0
⊢ False

Proof state:
α : Type u
x : α
h : of x = 0
⊢ False

Tactic:
let f : FreeAbelianGroup α →+ ℤ := lift 1

Result:
α : Type u
x : α
h : of x = 0
f : FreeAbelianGroup α →+ ℤ := lift 1
⊢ False

Proof state:
α : Type u
x : α
h : of x = 0
f : FreeAbelianGroup α →+ ℤ := lift 1
hfx : f (of x) = 1
⊢ False

Tactic:
have hf0 : f (of x) = 0 := by rw [h, map_zero]

Result:
α : Type u
x : α
h : of x = 0
f : FreeAbelianGroup α →+ ℤ := lift 1
hfx : f (of x) = 1
hf0 : f (of x) = 0
⊢ False
-- Mathlib/Order/Birkhoff.lean
@[simp] lemma birkhoffFinset_inf (a b : α) :
    birkhoffFinset (a ⊓ b) = birkhoffFinset a ∩ birkhoffFinset b

Proof state:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : DecidableEq α
a b : α
⊢ birkhoffFinset (a ⊓ b) = birkhoffFinset a ∩ birkhoffFinset b

Tactic:
dsimp [OrderEmbedding.birkhoffFinset]

Result:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : DecidableEq α
a b : α
⊢ Fintype.finsetOrderIsoSet.symm.toOrderEmbedding (birkhoffSet (a ⊓ b)) =
    Fintype.finsetOrderIsoSet.symm.toOrderEmbedding (birkhoffSet a) ∩
      Fintype.finsetOrderIsoSet.symm.toOrderEmbedding (birkhoffSet b)

Proof state:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : DecidableEq α
a b : α
⊢ birkhoffFinset (a ⊓ b) = birkhoffFinset a ∩ birkhoffFinset b

Tactic:
classical
dsimp [OrderEmbedding.birkhoffFinset]
rw [birkhoffSet_inf, OrderIso.coe_toOrderEmbedding]
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : DecidableEq α
a b : α
⊢ Fintype.finsetOrderIsoSet.symm (birkhoffSet a ∩ birkhoffSet b) =
    Fintype.finsetOrderIsoSet.symm (birkhoffSet a) ∩ Fintype.finsetOrderIsoSet.symm (birkhoffSet b)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : DecidableEq α
a b : α
⊢ Fintype.finsetOrderIsoSet.symm.toOrderEmbedding (birkhoffSet (a ⊓ b)) =
    Fintype.finsetOrderIsoSet.symm.toOrderEmbedding (birkhoffSet a) ∩
      Fintype.finsetOrderIsoSet.symm.toOrderEmbedding (birkhoffSet b)

Tactic:
rw [birkhoffSet_inf, OrderIso.coe_toOrderEmbedding]

Result:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : DecidableEq α
a b : α
⊢ Fintype.finsetOrderIsoSet.symm (birkhoffSet a ∩ birkhoffSet b) =
    Fintype.finsetOrderIsoSet.symm (birkhoffSet a) ∩ Fintype.finsetOrderIsoSet.symm (birkhoffSet b)