harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem sum_centroidWeightsIndicator_eq_one_of_card_eq_add_one [CharZero k] [Fintype ι] {n : ℕ}
    (h : #s = n + 1) : ∑ i, s.centroidWeightsIndicator k i = 1

Proof state:
k : Type u_1
inst✝² : DivisionRing k
ι : Type u_4
s : Finset ι
inst✝¹ : CharZero k
inst✝ : Fintype ι
n : ℕ
h : #s = n + 1
⊢ ∑ i ∈ s, centroidWeights k s i = 1

Tactic:
exact s.sum_centroidWeights_eq_one_of_card_eq_add_one k h

Result:
no goals

Proof state:
k : Type u_1
inst✝² : DivisionRing k
ι : Type u_4
s : Finset ι
inst✝¹ : CharZero k
inst✝ : Fintype ι
n : ℕ
h : #s = n + 1
⊢ ∑ i : ι, centroidWeightsIndicator k s i = 1

Tactic:
rw [sum_centroidWeightsIndicator]

Result:
k : Type u_1
inst✝² : DivisionRing k
ι : Type u_4
s : Finset ι
inst✝¹ : CharZero k
inst✝ : Fintype ι
n : ℕ
h : #s = n + 1
⊢ ∑ i ∈ s, centroidWeights k s i = 1
-- Mathlib/Topology/ContinuousOn.lean
theorem ContinuousOn.union_isClosed {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    {s t : Set X} (hs : IsClosed s) (ht : IsClosed t) {f : X → Y} (hfs : ContinuousOn f s)
    (hft : ContinuousOn f t) : ContinuousOn f (s ∪ t)

Proof state:
case refine_1
X : Type u_5
Y : Type u_6
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s t : Set X
hs : IsClosed s
ht : IsClosed t
f : X → Y
hfs : ContinuousOn f s
hft : ContinuousOn f t
x : X
hx : x ∈ s ∪ t
⊢ ContinuousWithinAt f s x

Tactic:
refine if hx : x ∈ s then hfs x hx else continuousWithinAt_of_not_mem_closure ?_

Result:
case refine_1
X : Type u_5
Y : Type u_6
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s t : Set X
hs : IsClosed s
ht : IsClosed t
f : X → Y
hfs : ContinuousOn f s
hft : ContinuousOn f t
x : X
hx✝ : x ∈ s ∪ t
hx : x ∉ s
⊢ x ∉ closure s

Proof state:
X : Type u_5
Y : Type u_6
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s t : Set X
hs : IsClosed s
ht : IsClosed t
f : X → Y
hfs : ContinuousOn f s
hft : ContinuousOn f t
⊢ ContinuousOn f (s ∪ t)

Tactic:
refine fun x hx ↦ .union ?_ ?_

Result:
case refine_1
X : Type u_5
Y : Type u_6
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s t : Set X
hs : IsClosed s
ht : IsClosed t
f : X → Y
hfs : ContinuousOn f s
hft : ContinuousOn f t
x : X
hx : x ∈ s ∪ t
⊢ ContinuousWithinAt f s x

case refine_2
X : Type u_5
Y : Type u_6
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s t : Set X
hs : IsClosed s
ht : IsClosed t
f : X → Y
hfs : ContinuousOn f s
hft : ContinuousOn f t
x : X
hx : x ∈ s ∪ t
⊢ ContinuousWithinAt f t x

Proof state:
case refine_1
X : Type u_5
Y : Type u_6
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s t : Set X
hs : IsClosed s
ht : IsClosed t
f : X → Y
hfs : ContinuousOn f s
hft : ContinuousOn f t
x : X
hx✝ : x ∈ s ∪ t
hx : x ∉ s
⊢ x ∉ closure s

Tactic:
rwa [hs.closure_eq]

Result:
no goals

Proof state:
case refine_2
X : Type u_5
Y : Type u_6
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s t : Set X
hs : IsClosed s
ht : IsClosed t
f : X → Y
hfs : ContinuousOn f s
hft : ContinuousOn f t
x : X
hx✝ : x ∈ s ∪ t
hx : x ∉ t
⊢ x ∉ closure t

Tactic:
rwa [ht.closure_eq]

Result:
no goals

Proof state:
case refine_2
X : Type u_5
Y : Type u_6
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s t : Set X
hs : IsClosed s
ht : IsClosed t
f : X → Y
hfs : ContinuousOn f s
hft : ContinuousOn f t
x : X
hx : x ∈ s ∪ t
⊢ ContinuousWithinAt f t x

Tactic:
refine if hx : x ∈ t then hft x hx else continuousWithinAt_of_not_mem_closure ?_

Result:
case refine_2
X : Type u_5
Y : Type u_6
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s t : Set X
hs : IsClosed s
ht : IsClosed t
f : X → Y
hfs : ContinuousOn f s
hft : ContinuousOn f t
x : X
hx✝ : x ∈ s ∪ t
hx : x ∉ t
⊢ x ∉ closure t
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem or_self_right : (a ∨ b) ∨ b ↔ a ∨ b

Proof state:
a b : Prop
⊢ (a ∨ b) ∨ b ↔ a ∨ b

Tactic:
rw [ propext or_assoc, or_self]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Icc_eq_empty_iff : Icc a b = ∅ ↔ ¬a ≤ b

Proof state:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Icc a b = ∅ ↔ ¬a ≤ b

Tactic:
rw [← coe_eq_empty, coe_Icc, Set.Icc_eq_empty_iff]

Result:
no goals
-- Mathlib/Data/Setoid/Basic.lean
theorem mapOfSurjective_eq_map (h : ker f ≤ r) (hf : Surjective f) :
    map r f = mapOfSurjective r f h hf

Proof state:
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
h : ker f ≤ r
hf : Surjective f
⊢ r.map f = r.mapOfSurjective f h hf

Tactic:
rw [← eqvGen_of_setoid (mapOfSurjective r f h hf)]

Result:
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
h : ker f ≤ r
hf : Surjective f
⊢ r.map f = Relation.EqvGen.setoid ⇑(r.mapOfSurjective f h hf)

Proof state:
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
h : ker f ≤ r
hf : Surjective f
⊢ r.map f = Relation.EqvGen.setoid ⇑(r.mapOfSurjective f h hf)

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem sbtw_const_vadd_iff {x y z : P} (v : V) :
    Sbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z) ↔ Sbtw R x y z

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
v : V
⊢ Sbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z) ↔ Sbtw R x y z

Tactic:
rw [Sbtw, Sbtw, wbtw_const_vadd_iff, (AddAction.injective v).ne_iff,
  (AddAction.injective v).ne_iff]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem comap_incl_eq_bot : N₂.comap N.incl = ⊥ ↔ N ⊓ N₂ = ⊥

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N₂ : LieSubmodule R L M
⊢ Submodule.comap (↑N).subtype ↑N₂ = ⊥ ↔ ↑N ⊓ ↑N₂ = ⊥

Tactic:
rw [← Submodule.disjoint_iff_comap_eq_bot, disjoint_iff]

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N₂ : LieSubmodule R L M
⊢ comap N.incl N₂ = ⊥ ↔ N ⊓ N₂ = ⊥

Tactic:
simp only [← toSubmodule_inj, toSubmodule_comap, incl_coe, bot_toSubmodule,
  inf_toSubmodule]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N₂ : LieSubmodule R L M
⊢ Submodule.comap (↑N).subtype ↑N₂ = ⊥ ↔ ↑N ⊓ ↑N₂ = ⊥
-- Mathlib/Data/Multiset/AddSub.lean
theorem le_cons_erase (s : Multiset α) (a : α) : s ≤ a ::ₘ s.erase a :=
  if h : a ∈ s then le_of_eq (cons_erase h).symm
  else by rw [erase_of_not_mem h]; apply le_cons_self

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∉ s
⊢ s ≤ a ::ₘ s

Tactic:
apply le_cons_self

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∉ s
⊢ s ≤ a ::ₘ s.erase a

Tactic:
rw [erase_of_not_mem h]

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∉ s
⊢ s ≤ a ::ₘ s
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem S_eval_two (n : ℤ) : (S R n).eval 2 = n + 1

Proof state:
case one
R : Type u_1
inst✝ : CommRing R
⊢ 2 = 1 + 1

Tactic:
norm_num

Result:
no goals

Proof state:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 2 (S R (-↑n)) = ↑(-↑n) + 1
ih2 : eval 2 (S R (-↑n + 1)) = ↑(-↑n + 1) + 1
⊢ 2 * (-↑n + 1) - (-↑n + 1 + 1) = -↑n

Tactic:
ring

Result:
no goals

Proof state:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 2 (S R (↑n + 1)) = ↑(↑n + 1) + 1
ih2 : eval 2 (S R ↑n) = ↑↑n + 1
⊢ 2 * (↑n + 1 + 1) - (↑n + 1) = ↑n + 2 + 1

Tactic:
ring

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝ : CommRing R
⊢ eval 2 (S R 0) = ↑0 + 1

Tactic:
simp

Result:
no goals

Proof state:
case one
R : Type u_1
inst✝ : CommRing R
⊢ eval 2 (S R 1) = ↑1 + 1

Tactic:
simp

Result:
case one
R : Type u_1
inst✝ : CommRing R
⊢ 2 = 1 + 1

Proof state:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 2 (S R (↑n + 1)) = ↑(↑n + 1) + 1
ih2 : eval 2 (S R ↑n) = ↑↑n + 1
⊢ eval 2 (S R (↑n + 2)) = ↑(↑n + 2) + 1

Tactic:
simp only [S_add_two, eval_sub, eval_mul, eval_ofNat, eval_X, mul_one, ih1,
  Int.cast_add, Int.cast_natCast, Int.cast_one, ih2, Int.cast_ofNat]

Result:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 2 (S R (↑n + 1)) = ↑(↑n + 1) + 1
ih2 : eval 2 (S R ↑n) = ↑↑n + 1
⊢ 2 * (↑n + 1 + 1) - (↑n + 1) = ↑n + 2 + 1

Proof state:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 2 (S R (-↑n)) = ↑(-↑n) + 1
ih2 : eval 2 (S R (-↑n + 1)) = ↑(-↑n + 1) + 1
⊢ eval 2 (S R (-↑n - 1)) = ↑(-↑n - 1) + 1

Tactic:
simp only [S_sub_one, eval_sub, eval_mul, eval_ofNat, eval_X, mul_one,
  ih1, Int.cast_neg, Int.cast_natCast, ih2, Int.cast_add, Int.cast_one, Int.cast_sub,
  sub_add_cancel]

Result:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval 2 (S R (-↑n)) = ↑(-↑n) + 1
ih2 : eval 2 (S R (-↑n + 1)) = ↑(-↑n + 1) + 1
⊢ 2 * (-↑n + 1) - (-↑n + 1 + 1) = -↑n

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ eval 2 (S R n) = ↑n + 1

Tactic:
induction n using Polynomial.Chebyshev.induct with
| zero => simp
| one => simp; norm_num
| add_two n ih1 ih2 =>
  simp only [S_add_two, eval_sub, eval_mul, eval_ofNat, eval_X, mul_one, ih1,
    Int.cast_add, Int.cast_natCast, Int.cast_one, ih2, Int.cast_ofNat]
  ring
| neg_add_one n ih1 ih2 =>
  simp only [S_sub_one, eval_sub, eval_mul, eval_ofNat, eval_X, mul_one,
    ih1, Int.cast_neg, Int.cast_natCast, ih2, Int.cast_add, Int.cast_one, Int.cast_sub,
    sub_add_cancel]
  ring

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_pow (f : R → R) (n : ℕ) (a : A)
    (hf : ContinuousOn f (spectrum R a)

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f : R → R
n : ℕ
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ (cfcHom ha) { toFun := (spectrum R a).restrict fun x => f x ^ n, continuous_toFun := ⋯ } =
    (cfcHom ha) ({ toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ } ^ n)

Tactic:
congr

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f : R → R
n : ℕ
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ cfc (fun x => f x ^ n) a = cfc f a ^ n

Tactic:
rw [cfc_apply f a, ← map_pow, cfc_apply _ a]

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f : R → R
n : ℕ
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ (cfcHom ha) { toFun := (spectrum R a).restrict fun x => f x ^ n, continuous_toFun := ⋯ } =
    (cfcHom ha) ({ toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ } ^ n)
-- Mathlib/Algebra/Polynomial/Roots.lean
@[simp]
lemma roots_neg (p : R[X]) : (-p).roots = p.roots

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ (-p).roots = p.roots

Tactic:
rw [← neg_one_smul R p, roots_smul_nonzero p (neg_ne_zero.mpr one_ne_zero)]

Result:
no goals
-- Mathlib/Algebra/Ring/Subsemiring/Basic.lean
theorem mem_iInf {ι : Sort*} {S : ι → Subsemiring R} {x : R} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i

Proof state:
R : Type u
inst✝ : NonAssocSemiring R
ι : Sort u_1
S : ι → Subsemiring R
x : R
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

Tactic:
simp only [iInf, mem_sInf, Set.forall_mem_range]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma inv_map_Δ' : (W.map φ).Δ'⁻¹ = Units.map φ W.Δ'⁻¹

Proof state:
R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ (W.map φ).Δ'⁻¹ = (Units.map ↑φ) W.Δ'⁻¹

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/WithDensity.lean
theorem withDensityᵥ_smul_eq_withDensityᵥ_withDensity {f : α → ℝ≥0} {g : α → E}
    (hf : AEMeasurable f μ) (hfg : Integrable (f • g) μ) :
    μ.withDensityᵥ (f • g) = (μ.withDensity (fun x ↦ f x)).withDensityᵥ g

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
g : α → E
hf : AEMeasurable f μ
hfg : Integrable (f • g) μ
s : Set α
hs : MeasurableSet s
⊢ ∫ (x : α) in s, (f • g) x ∂μ = ∫ (x : α) in s, f x • g x ∂μ

Tactic:
simp only [Pi.smul_apply']

Result:
no goals

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
g : α → E
hf : AEMeasurable f μ
hfg : Integrable (f • g) μ
s : Set α
hs : MeasurableSet s
⊢ ↑(μ.withDensityᵥ (f • g)) s = ↑((μ.withDensity fun x => ↑(f x)).withDensityᵥ g) s

Tactic:
rw [withDensityᵥ_apply hfg hs,
  withDensityᵥ_apply ((integrable_withDensity_iff_integrable_smul₀ hf).mpr hfg) hs,
  setIntegral_withDensity_eq_setIntegral_smul₀ hf.restrict _ hs]

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
g : α → E
hf : AEMeasurable f μ
hfg : Integrable (f • g) μ
s : Set α
hs : MeasurableSet s
⊢ ∫ (x : α) in s, (f • g) x ∂μ = ∫ (x : α) in s, f x • g x ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
g : α → E
hf : AEMeasurable f μ
hfg : Integrable (f • g) μ
⊢ μ.withDensityᵥ (f • g) = (μ.withDensity fun x => ↑(f x)).withDensityᵥ g

Tactic:
ext s hs

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
g : α → E
hf : AEMeasurable f μ
hfg : Integrable (f • g) μ
s : Set α
hs : MeasurableSet s
⊢ ↑(μ.withDensityᵥ (f • g)) s = ↑((μ.withDensity fun x => ↑(f x)).withDensityᵥ g) s
-- Mathlib/RingTheory/Valuation/AlgebraInstances.lean
theorem isIntegral_of_mem_ringOfIntegers' {x : (integralClosure v.valuationSubring L)} :
    IsIntegral v.valuationSubring (x : integralClosure v.valuationSubring L)

Proof state:
K : Type u_1
inst✝² : Field K
v : Valuation K ℤₘ₀
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
x : ↥(integralClosure (↥v.valuationSubring) L)
⊢ IsIntegral (↥v.valuationSubring) x

Tactic:
apply isIntegral_of_mem_ringOfIntegers

Result:
no goals
-- Mathlib/LinearAlgebra/Trace.lean
theorem trace_conj (g : M →ₗ[R] M) (f : (M →ₗ[R] M)ˣ) :
    trace R M (↑f * g * ↑f⁻¹) = trace R M g

Proof state:
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
g : M →ₗ[R] M
f : (M →ₗ[R] M)ˣ
⊢ (trace R M) (↑f * g * ↑f⁻¹) = (trace R M) g

Tactic:
rw [trace_mul_comm]

Result:
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
g : M →ₗ[R] M
f : (M →ₗ[R] M)ˣ
⊢ (trace R M) (↑f⁻¹ * (↑f * g)) = (trace R M) g

Proof state:
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
g : M →ₗ[R] M
f : (M →ₗ[R] M)ˣ
⊢ (trace R M) (↑f⁻¹ * (↑f * g)) = (trace R M) g

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
theorem trace_adjMatrix [AddCommMonoid α] [One α] : Matrix.trace (G.adjMatrix α) = 0

Proof state:
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : AddCommMonoid α
inst✝ : One α
⊢ (adjMatrix α G).trace = 0

Tactic:
simp [Matrix.trace]

Result:
no goals
-- Mathlib/RingTheory/LaurentSeries.lean
theorem hasseDeriv_comp_coeff (k l : ℕ) (f : LaurentSeries V) (n : ℤ) :
    (hasseDeriv R k (hasseDeriv R l f)).coeff n =
      ((Nat.choose (k + l) k) • hasseDeriv R (k + l) f).coeff n

Proof state:
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k l : ℕ
f : V⸨X⸩
n : ℤ
⊢ ((hasseDeriv R k) ((hasseDeriv R l) f)).coeff n = ((k + l).choose k • ((hasseDeriv R (k + l)) f).coeff) n

Tactic:
simp only [hasseDeriv_coeff, Pi.smul_apply, Nat.cast_add]

Result:
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k l : ℕ
f : V⸨X⸩
n : ℤ
⊢ Ring.choose (n + ↑k) k • Ring.choose (n + ↑k + ↑l) l • f.coeff (n + ↑k + ↑l) =
    (k + l).choose k • Ring.choose (n + (↑k + ↑l)) (k + l) • f.coeff (n + (↑k + ↑l))

Proof state:
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k l : ℕ
f : V⸨X⸩
n : ℤ
⊢ Ring.choose (n + ↑k) k • Ring.choose (n + ↑k + ↑l) l • f.coeff (n + ↑k + ↑l) =
    (k + l).choose k • Ring.choose (n + (↑k + ↑l)) (k + l) • f.coeff (n + (↑k + ↑l))

Tactic:
rw [smul_smul, mul_comm, ← Ring.choose_add_smul_choose (n + k), add_assoc, Nat.choose_symm_add,
  smul_assoc]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k l : ℕ
f : V⸨X⸩
n : ℤ
⊢ ((hasseDeriv R k) ((hasseDeriv R l) f)).coeff n = ((k + l).choose k • (hasseDeriv R (k + l)) f).coeff n

Tactic:
rw [coeff_nsmul]

Result:
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k l : ℕ
f : V⸨X⸩
n : ℤ
⊢ ((hasseDeriv R k) ((hasseDeriv R l) f)).coeff n = ((k + l).choose k • ((hasseDeriv R (k + l)) f).coeff) n
-- Mathlib/Topology/Algebra/InfiniteSum/Order.lean
theorem tprod_ne_one_iff (hf : Multipliable f) : ∏' i, f i ≠ 1 ↔ ∃ x, f x ≠ 1

Proof state:
ι : Type u_1
α : Type u_3
inst✝³ : OrderedCommMonoid α
inst✝² : CanonicallyOrderedMul α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
hf : Multipliable f
⊢ ∏' (i : ι), f i ≠ 1 ↔ ∃ x, f x ≠ 1

Tactic:
rw [Ne, tprod_eq_one_iff hf, not_forall]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Int.lean
theorem norm_coe_units (e : ℤˣ) : ‖(e : ℤ)‖ = 1

Proof state:
e : ℤˣ
⊢ ‖↑e‖ = 1

Tactic:
rw [← coe_nnnorm, nnnorm_coe_units, NNReal.coe_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/UInt/Basic.lean
theorem usize_size_le : USize.size ≤ 18446744073709551616

Proof state:
⊢ USize.size ≤ 18446744073709551616

Tactic:
cases usize_size_eq <;> next h => rw [h]; decide

Result:
no goals

Proof state:
h : USize.size = 18446744073709551616
⊢ 18446744073709551616 ≤ 18446744073709551616

Tactic:
decide

Result:
no goals

Proof state:
h : USize.size = 18446744073709551616
⊢ USize.size ≤ 18446744073709551616

Tactic:
rw [h]

Result:
h : USize.size = 18446744073709551616
⊢ 18446744073709551616 ≤ 18446744073709551616
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapFinIdx_eq_ofFn {as : Array α} {f : (i : Nat) → α → (h : i < as.size) → β} :
    as.mapFinIdx f = Array.ofFn fun i : Fin as.size => f i as[i] i.2

Proof state:
α : Type u_1
β : Type u_2
as : Array α
f : (i : Nat) → α → i < as.size → β
⊢ as.mapFinIdx f = ofFn fun i => f (↑i) as[i] ⋯

Tactic:
cases as

Result:
case mk
α : Type u_1
β : Type u_2
toList✝ : List α
f : (i : Nat) → α → i < { toList := toList✝ }.size → β
⊢ { toList := toList✝ }.mapFinIdx f = ofFn fun i => f ↑i { toList := toList✝ }[i] ⋯

Proof state:
case mk
α : Type u_1
β : Type u_2
toList✝ : List α
f : (i : Nat) → α → i < { toList := toList✝ }.size → β
⊢ { toList := toList✝ }.mapFinIdx f = ofFn fun i => f ↑i { toList := toList✝ }[i] ⋯

Tactic:
simp [List.mapFinIdx_eq_ofFn]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma zpow_right_strictMono₀ (ha : 1 < a) : StrictMono fun n : ℤ ↦ a ^ n

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulStrictMono G₀
ha : 1 < a
⊢ StrictMono fun n => a ^ n

Tactic:
refine strictMono_int_of_lt_succ fun n ↦ ?_

Result:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulStrictMono G₀
ha : 1 < a
n : ℤ
⊢ a ^ n < a ^ (n + 1)

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulStrictMono G₀
ha : 1 < a
n : ℤ
⊢ a ^ n < a ^ (n + 1)

Tactic:
rw [zpow_add_one₀ (zero_lt_one.trans ha).ne']

Result:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulStrictMono G₀
ha : 1 < a
n : ℤ
⊢ a ^ n < a ^ n * a

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulStrictMono G₀
ha : 1 < a
n : ℤ
⊢ a ^ n < a ^ n * a

Tactic:
exact lt_mul_of_one_lt_right (zpow_pos (zero_lt_one.trans ha) _) ha

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Invariant.lean
@[simp]
protected lemma isCompl_mk_iff {p q : Submodule R M}
    (hp : p ∈ f.invtSubmodule) (hq : q ∈ f.invtSubmodule) :
    IsCompl (α := f.invtSubmodule) ⟨p, hp⟩ ⟨q, hq⟩ ↔ IsCompl p q

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : p ∈ f.invtSubmodule
hq : q ∈ f.invtSubmodule
⊢ IsCompl ⟨p, hp⟩ ⟨q, hq⟩ ↔ IsCompl p q

Tactic:
simp [isCompl_iff]

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean
theorem fst_iso_of_right_embedding_range_subset {X Y S : TopCat} (f : X ⟶ S) {g : Y ⟶ S}
    (hg : IsEmbedding g) (H : Set.range f ⊆ Set.range g) :
    IsIso (pullback.fst f g)

Proof state:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
hg : IsEmbedding ⇑(ConcreteCategory.hom g)
H : Set.range ⇑(ConcreteCategory.hom f) ⊆ Set.range ⇑(ConcreteCategory.hom g)
x : ↑X
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (pullback.fst f g))

Tactic:
rw [pullback_fst_range]

Result:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
hg : IsEmbedding ⇑(ConcreteCategory.hom g)
H : Set.range ⇑(ConcreteCategory.hom f) ⊆ Set.range ⇑(ConcreteCategory.hom g)
x : ↑X
⊢ x ∈ {x | ∃ y, (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) y}

Proof state:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
hg : IsEmbedding ⇑(ConcreteCategory.hom g)
H : Set.range ⇑(ConcreteCategory.hom f) ⊆ Set.range ⇑(ConcreteCategory.hom g)
⊢ IsIso (pullback.fst f g)

Tactic:
let esto : (pullback f g : TopCat) ≃ₜ X :=
  (Homeomorph.ofIsEmbedding _ (fst_isEmbedding_of_right f hg)).trans
    { toFun := Subtype.val
      invFun := fun x =>
        ⟨x, by
          rw [pullback_fst_range]
          exact ⟨_, (H (Set.mem_range_self x)).choose_spec.symm⟩⟩
      left_inv := fun ⟨_, _⟩ => rfl
      right_inv := fun x => rfl }

Result:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
hg : IsEmbedding ⇑(ConcreteCategory.hom g)
H : Set.range ⇑(ConcreteCategory.hom f) ⊆ Set.range ⇑(ConcreteCategory.hom g)
esto : ↑(pullback f g) ≃ₜ ↑X :=
  (Homeomorph.ofIsEmbedding ⇑(ConcreteCategory.hom (pullback.fst f g)) ⋯).trans
    { toFun := Subtype.val, invFun := fun x => ⟨x, ⋯⟩, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯,
      continuous_invFun := ⋯ }
⊢ IsIso (pullback.fst f g)

Proof state:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
hg : IsEmbedding ⇑(ConcreteCategory.hom g)
H : Set.range ⇑(ConcreteCategory.hom f) ⊆ Set.range ⇑(ConcreteCategory.hom g)
esto : ↑(pullback f g) ≃ₜ ↑X :=
  (Homeomorph.ofIsEmbedding ⇑(ConcreteCategory.hom (pullback.fst f g)) ⋯).trans
    { toFun := Subtype.val, invFun := fun x => ⟨x, ⋯⟩, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯,
      continuous_invFun := ⋯ }
⊢ IsIso (pullback.fst f g)

Tactic:
convert (isoOfHomeo esto).isIso_hom

Result:
no goals

Proof state:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
hg : IsEmbedding ⇑(ConcreteCategory.hom g)
H : Set.range ⇑(ConcreteCategory.hom f) ⊆ Set.range ⇑(ConcreteCategory.hom g)
x : ↑X
⊢ x ∈ {x | ∃ y, (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) y}

Tactic:
exact ⟨_, (H (Set.mem_range_self x)).choose_spec.symm⟩

Result:
no goals