harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Lie/Weights/Basic.lean
theorem zero_genWeightSpace_eq_top_of_nilpotent' [IsNilpotent L M] :
    genWeightSpace M (0 : L → R) = ⊤

Proof state:
case h
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : IsNilpotent L M
m✝ : M
⊢ m✝ ∈ genWeightSpace M 0 ↔ m✝ ∈ ⊤

Tactic:
simp [genWeightSpace, genWeightSpaceOf]

Result:
no goals

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : IsNilpotent L M
⊢ genWeightSpace M 0 = ⊤

Tactic:
ext

Result:
case h
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : IsNilpotent L M
m✝ : M
⊢ m✝ ∈ genWeightSpace M 0 ↔ m✝ ∈ ⊤
-- Mathlib/Data/Complex/Basic.lean
theorem I_mul (z : ℂ) : I * z = ⟨-z.im, z.re⟩ :=
  Complex.ext_iff.2 <| by simp

Proof state:
z : ℂ
⊢ (I * z).re = { re := -z.im, im := z.re }.re ∧ (I * z).im = { re := -z.im, im := z.re }.im

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Lie/Sl2.lean
lemma symm (ht : IsSl2Triple h e f) : IsSl2Triple (-h) f e where
  h_ne_zero

Proof state:
L : Type u_2
inst✝ : LieRing L
h e f : L
ht : IsSl2Triple h e f
⊢ ⁅f, e⁆ = -h

Tactic:
rw [← neg_eq_iff_eq_neg, lie_skew, ht.lie_e_f]

Result:
no goals

Proof state:
L : Type u_2
inst✝ : LieRing L
h e f : L
ht : IsSl2Triple h e f
⊢ -h ≠ 0

Tactic:
simpa using ht.h_ne_zero

Result:
no goals

Proof state:
L : Type u_2
inst✝ : LieRing L
h e f : L
ht : IsSl2Triple h e f
⊢ ⁅-h, f⁆ = 2 • f

Tactic:
rw [neg_lie, neg_eq_iff_eq_neg, ht.lie_h_f_nsmul]

Result:
no goals

Proof state:
L : Type u_2
inst✝ : LieRing L
h e f : L
ht : IsSl2Triple h e f
⊢ ⁅-h, e⁆ = -(2 • e)

Tactic:
rw [neg_lie, neg_inj, ht.lie_h_e_nsmul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem flatten_reverse (L : Array (Array α)) :
    L.reverse.flatten = (L.map reverse).flatten.reverse

Proof state:
case of
α : Type u_1
xss✝ : List (List α)
⊢ (List.map List.toArray xss✝).toArray.reverse.flatten =
    (map reverse (List.map List.toArray xss✝).toArray).flatten.reverse

Tactic:
simp [flatten_toArray, List.flatten_reverse, Function.comp_def]

Result:
no goals

Proof state:
α : Type u_1
L : Array (Array α)
⊢ L.reverse.flatten = (map reverse L).flatten.reverse

Tactic:
cases L using array₂_induction

Result:
case of
α : Type u_1
xss✝ : List (List α)
⊢ (List.map List.toArray xss✝).toArray.reverse.flatten =
    (map reverse (List.map List.toArray xss✝).toArray).flatten.reverse
-- Mathlib/Algebra/Order/Interval/Finset/SuccPred.lean
lemma Ici_add_one_eq_Ioi_of_not_isMax (ha : ¬ IsMax a) : Ici (a + 1) = Ioi a

Proof state:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrderTop α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a : α
ha : ¬IsMax a
⊢ Ici (a + 1) = Ioi a

Tactic:
simpa [succ_eq_add_one] using Ici_succ_eq_Ioi_of_not_isMax ha

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem ofList_cons (a : α) (l : List α) : ofList (a::l) = cons a (ofList l)

Proof state:
α : Type u
a : α
l : List α
⊢ ↑(a :: l) = cons a ↑l

Tactic:
ext1 (_ | n) <;> rfl

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
@[to_additive]
lemma IsOfFinOrder.natCard_powers_le_orderOf (ha : IsOfFinOrder a) :
    Nat.card (powers a : Set G) ≤ orderOf a

Proof state:
G : Type u_1
inst✝ : Monoid G
a : G
ha : IsOfFinOrder a
⊢ Nat.card ↑↑(powers a) ≤ orderOf a

Tactic:
simpa [ha.powers_eq_image_range_orderOf, Finset.card_range, Nat.Iio_eq_range]
  using Finset.card_image_le (s := Finset.range (orderOf a))

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Monoid G
a : G
ha : IsOfFinOrder a
⊢ Nat.card ↑↑(powers a) ≤ orderOf a

Tactic:
classical
simpa [ha.powers_eq_image_range_orderOf, Finset.card_range, Nat.Iio_eq_range]
  using Finset.card_image_le (s := Finset.range (orderOf a))

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean
lemma L₀_g_δ : S.L₀.g ≫ S.δ = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.L₀.g ≫ S.δ = 0

Tactic:
erw [← L₀X₂ToP_comp_pullback_snd, assoc, S.L₀'_exact.g_desc,
  L₀X₂ToP_comp_φ₁_assoc, zero_comp]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem castSucc_lt_succ (i : Fin n) : i.castSucc < i.succ :=
  lt_def.2 <| by simp only [coe_castSucc, val_succ, Nat.lt_succ_self]

Proof state:
n : Nat
i : Fin n
⊢ ↑i.castSucc < ↑i.succ

Tactic:
simp only [coe_castSucc, val_succ, Nat.lt_succ_self]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean
@[simp]
lemma toNNReal_algebraMap (r : ℝ≥0) :
    (algebraMap ℝ C(X, ℝ) r).toNNReal = algebraMap ℝ≥0 C(X, ℝ≥0) r

Proof state:
case h.a
X : Type u_1
inst✝ : TopologicalSpace X
r : ℝ≥0
a✝ : X
⊢ ↑(((algebraMap ℝ C(X, ℝ)) ↑r).toNNReal a✝) = ↑(((algebraMap ℝ≥0 C(X, ℝ≥0)) r) a✝)

Tactic:
simp

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
r : ℝ≥0
⊢ ((algebraMap ℝ C(X, ℝ)) ↑r).toNNReal = (algebraMap ℝ≥0 C(X, ℝ≥0)) r

Tactic:
ext

Result:
case h.a
X : Type u_1
inst✝ : TopologicalSpace X
r : ℝ≥0
a✝ : X
⊢ ↑(((algebraMap ℝ C(X, ℝ)) ↑r).toNNReal a✝) = ↑(((algebraMap ℝ≥0 C(X, ℝ≥0)) r) a✝)
-- Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean
theorem directSum_isInternal_of_commute (hA : A.IsSymmetric) (hB : B.IsSymmetric)
    (hAB : Commute A B) :
    DirectSum.IsInternal (fun (i : 𝕜 × 𝕜) ↦ (eigenspace A i.2 ⊓ eigenspace B i.1))

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
A B : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hA : A.IsSymmetric
hB : B.IsSymmetric
hAB : Commute A B
⊢ ⨆ j, ⨆ i, eigenspace A (i, j).2 ⊓ eigenspace B (i, j).1 = ⊤

Tactic:
exact iSup_iSup_eigenspace_inf_eigenspace_eq_top_of_commute hA hB hAB

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
A B : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hA : A.IsSymmetric
hB : B.IsSymmetric
hAB : Commute A B
⊢ (⨆ i, eigenspace A i.2 ⊓ eigenspace B i.1)ᗮ = ⊥

Tactic:
rw [Submodule.orthogonal_eq_bot_iff, iSup_prod, iSup_comm]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
A B : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hA : A.IsSymmetric
hB : B.IsSymmetric
hAB : Commute A B
⊢ ⨆ j, ⨆ i, eigenspace A (i, j).2 ⊓ eigenspace B (i, j).1 = ⊤

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
A B : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hA : A.IsSymmetric
hB : B.IsSymmetric
hAB : Commute A B
⊢ DirectSum.IsInternal fun i => eigenspace A i.2 ⊓ eigenspace B i.1

Tactic:
apply (orthogonalFamily_eigenspace_inf_eigenspace hA hB).isInternal_iff.mpr

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
A B : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hA : A.IsSymmetric
hB : B.IsSymmetric
hAB : Commute A B
⊢ (⨆ i, eigenspace A i.2 ⊓ eigenspace B i.1)ᗮ = ⊥
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma CFC.eq_zero_of_quasispectrum_eq_zero (h_spec : σₙ R a ⊆ {0}) (ha : p a

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
a : A
h_spec : σₙ R a ⊆ {0}
ha : autoParam (p a) _auto✝
⊢ a = 0

Tactic:
simpa [cfcₙ_id R a] using cfcₙ_congr (a := a) (f := id) (g := fun _ : R ↦ 0) fun x ↦ by simp_all

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
a : A
h_spec : σₙ R a ⊆ {0}
ha : autoParam (p a) _auto✝
x : R
⊢ x ∈ σₙ R a → id x = (fun x => 0) x

Tactic:
simp_all

Result:
no goals
-- Mathlib/MeasureTheory/Group/Prod.lean
theorem quasiMeasurePreserving_div_left_of_right_invariant [IsMulRightInvariant μ] (g : G) :
    QuasiMeasurePreserving (fun h : G => g / h) μ μ

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
g : G
⊢ QuasiMeasurePreserving (fun h => g / h) μ.inv.inv μ.inv.inv

Tactic:
exact
  (quasiMeasurePreserving_div_left μ.inv g).mono (inv_absolutelyContinuous μ.inv)
    (absolutelyContinuous_inv μ.inv)

Result:
no goals

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
g : G
⊢ QuasiMeasurePreserving (fun h => g / h) μ μ

Tactic:
rw [← μ.inv_inv]

Result:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
g : G
⊢ QuasiMeasurePreserving (fun h => g / h) μ.inv.inv μ.inv.inv
-- Mathlib/Algebra/Group/Indicator.lean
theorem mulIndicator_comp_of_one {g : M → N} (hg : g 1 = 1) :
    mulIndicator s (g ∘ f) = g ∘ mulIndicator s f

Proof state:
α : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : One M
inst✝ : One N
s : Set α
f : α → M
g : M → N
hg : g 1 = 1
⊢ s.mulIndicator (g ∘ f) = g ∘ s.mulIndicator f

Tactic:
funext

Result:
case h
α : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : One M
inst✝ : One N
s : Set α
f : α → M
g : M → N
hg : g 1 = 1
x✝ : α
⊢ s.mulIndicator (g ∘ f) x✝ = (g ∘ s.mulIndicator f) x✝

Proof state:
case h
α : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : One M
inst✝ : One N
s : Set α
f : α → M
g : M → N
hg : g 1 = 1
x✝ : α
⊢ s.mulIndicator (g ∘ f) x✝ = (g ∘ s.mulIndicator f) x✝

Tactic:
simp only [mulIndicator]

Result:
case h
α : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : One M
inst✝ : One N
s : Set α
f : α → M
g : M → N
hg : g 1 = 1
x✝ : α
⊢ (if x✝ ∈ s then (g ∘ f) x✝ else 1) = (g ∘ s.mulIndicator f) x✝

Proof state:
case h
α : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : One M
inst✝ : One N
s : Set α
f : α → M
g : M → N
hg : g 1 = 1
x✝ : α
⊢ (if x✝ ∈ s then (g ∘ f) x✝ else 1) = (g ∘ s.mulIndicator f) x✝

Tactic:
split_ifs <;> simp [*]

Result:
no goals
-- Mathlib/LinearAlgebra/StdBasis.lean
theorem basis_apply [DecidableEq η] (s : ∀ j, Basis (ιs j) R (Ms j)) (ji) :
    Pi.basis s ji = Pi.single ji.1 (s ji.1 ji.2) :=
  Basis.apply_eq_iff.mpr (by simp)

Proof state:
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
ji : (j : η) × ιs j
⊢ (Pi.basis s).repr (single ji.fst ((s ji.fst) ji.snd)) = Finsupp.single ji 1

Tactic:
simp

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem commute_sub_nat (n : ℕ) : Function.Commute f (· - n)

Proof state:
f : CircleDeg1Lift
n : ℕ
⊢ Function.Commute ⇑f fun x => x - ↑n

Tactic:
simpa only [sub_eq_add_neg] using
  (f.commute_add_nat n).inverses_right (Equiv.addRight _).right_inv (Equiv.addRight _).left_inv

Result:
no goals
-- Mathlib/GroupTheory/HNNExtension.lean
theorem prod_cons (g : G) (u : ℤˣ) (w : NormalWord d) (h1 : w.head ∈ d.set u)
    (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?,
      w.head ∈ toSubgroup A B u → u = u') :
    (cons g u w h1 h2).prod φ = of g * (t ^ (u : ℤ) * w.prod φ)

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : G
u : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
⊢ ReducedWord.prod φ (cons g u w h1 h2).toReducedWord = of g * (t ^ ↑u * ReducedWord.prod φ w.toReducedWord)

Tactic:
simp [ReducedWord.prod, cons, smul_def, mul_assoc]

Result:
no goals
-- Mathlib/FieldTheory/LinearDisjoint.lean
theorem of_isField' {A : Type v} [Field A] {B : Type w} [Field B]
    [Algebra F A] [Algebra F B] (H : IsField (A ⊗[F] B))
    {K : Type*} [Field K] [Algebra F K] (fa : A →ₐ[F] K) (fb : B →ₐ[F] K) :
    fa.fieldRange.LinearDisjoint fb.fieldRange

Proof state:
case H
F : Type u
inst✝⁶ : Field F
A : Type v
inst✝⁵ : Field A
B : Type w
inst✝⁴ : Field B
inst✝³ : Algebra F A
inst✝² : Algebra F B
H : IsField (A ⊗[F] B)
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra F K
fa : A →ₐ[F] K
fb : B →ₐ[F] K
⊢ IsField (↥fa.fieldRange.toSubalgebra ⊗[F] ↥fb.fieldRange.toSubalgebra)

Tactic:
exact Algebra.TensorProduct.congr (AlgEquiv.ofInjective fa fa.injective)
  (AlgEquiv.ofInjective fb fb.injective) |>.symm.toMulEquiv.isField _ H

Result:
no goals

Proof state:
F : Type u
inst✝⁶ : Field F
A : Type v
inst✝⁵ : Field A
B : Type w
inst✝⁴ : Field B
inst✝³ : Algebra F A
inst✝² : Algebra F B
H : IsField (A ⊗[F] B)
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra F K
fa : A →ₐ[F] K
fb : B →ₐ[F] K
⊢ fa.fieldRange.LinearDisjoint ↥fb.fieldRange

Tactic:
rw [linearDisjoint_iff']

Result:
F : Type u
inst✝⁶ : Field F
A : Type v
inst✝⁵ : Field A
B : Type w
inst✝⁴ : Field B
inst✝³ : Algebra F A
inst✝² : Algebra F B
H : IsField (A ⊗[F] B)
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra F K
fa : A →ₐ[F] K
fb : B →ₐ[F] K
⊢ fa.fieldRange.LinearDisjoint fb.fieldRange.toSubalgebra

Proof state:
F : Type u
inst✝⁶ : Field F
A : Type v
inst✝⁵ : Field A
B : Type w
inst✝⁴ : Field B
inst✝³ : Algebra F A
inst✝² : Algebra F B
H : IsField (A ⊗[F] B)
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra F K
fa : A →ₐ[F] K
fb : B →ₐ[F] K
⊢ fa.fieldRange.LinearDisjoint fb.fieldRange.toSubalgebra

Tactic:
apply Subalgebra.LinearDisjoint.of_isField

Result:
case H
F : Type u
inst✝⁶ : Field F
A : Type v
inst✝⁵ : Field A
B : Type w
inst✝⁴ : Field B
inst✝³ : Algebra F A
inst✝² : Algebra F B
H : IsField (A ⊗[F] B)
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra F K
fa : A →ₐ[F] K
fb : B →ₐ[F] K
⊢ IsField (↥fa.fieldRange.toSubalgebra ⊗[F] ↥fb.fieldRange.toSubalgebra)
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem card_nthRootsFinset {ζ : R} {n : ℕ} (h : IsPrimitiveRoot ζ n) :
    #(nthRootsFinset n R) = n

Proof state:
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ #(nthRootsFinset n R) = n

Tactic:
rw [nthRootsFinset, ← Multiset.toFinset_eq (nthRoots_one_nodup h), card_mk, h.card_nthRoots_one]

Result:
no goals

Proof state:
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ #(nthRootsFinset n R) = n

Tactic:
classical
rw [nthRootsFinset, ← Multiset.toFinset_eq (nthRoots_one_nodup h), card_mk, h.card_nthRoots_one]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Metric.lean
lemma dist_ne_zero_iff_ne_and_reachable : G.dist u v ≠ 0 ↔ u ≠ v ∧ G.Reachable u v

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ ¬(u = v ∨ ¬G.Reachable u v) ↔ u ≠ v ∧ G.Reachable u v

Tactic:
push_neg

Result:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ u ≠ v ∧ G.Reachable u v ↔ u ≠ v ∧ G.Reachable u v

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ u ≠ v ∧ G.Reachable u v ↔ u ≠ v ∧ G.Reachable u v

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.dist u v ≠ 0 ↔ u ≠ v ∧ G.Reachable u v

Tactic:
rw [ne_eq, dist_eq_zero_iff_eq_or_not_reachable.not]

Result:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ ¬(u = v ∨ ¬G.Reachable u v) ↔ u ≠ v ∧ G.Reachable u v
-- Mathlib/LinearAlgebra/BilinearMap.lean
theorem surjective_compr₂_of_equiv (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ ≃ₗ[R] Qₗ) (hf : Surjective f) :
    Surjective (f.compr₂ g.toLinearMap) :=
  surjective_compr₂_of_exists_rightInverse f g.toLinearMap hf ⟨g.symm, by simp⟩

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid Nₗ
inst✝⁵ : AddCommMonoid Pₗ
inst✝⁴ : AddCommMonoid Qₗ
inst✝³ : Module R M
inst✝² : Module R Nₗ
inst✝¹ : Module R Pₗ
inst✝ : Module R Qₗ
f : M →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Pₗ ≃ₗ[R] Qₗ
hf : Surjective ⇑f
⊢ ↑g ∘ₗ ↑g.symm = id

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Distributions/Uniform.lean
theorem mem_support_uniformOfFintype (a : α) : a ∈ (uniformOfFintype α).support

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
a : α
⊢ a ∈ (uniformOfFintype α).support

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem inr_fst' {b : BinaryBicone X Y} (h : b.IsBilimit) :
    IsPullback b.inr (0 : Y ⟶ 0) b.fst (0 : 0 ⟶ X)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPullback b.inr 0 b.fst 0

Tactic:
apply flip

Result:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPullback 0 b.inr 0 b.fst

Proof state:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPullback 0 b.inr 0 b.fst

Tactic:
refine of_bot ?_ (by simp) (of_isBilimit h)

Result:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPullback 0 (b.inr ≫ b.snd) (0 ≫ 0) 0

Proof state:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPullback 0 (b.inr ≫ b.snd) (0 ≫ 0) 0

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ 0 ≫ 0 = b.inr ≫ b.fst

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Irreducible.lean
theorem infPrime_iff_infIrred : InfPrime a ↔ InfIrred a :=
  ⟨InfPrime.infIrred,
    And.imp_right fun h b c => by simp_rw [← sup_eq_left, sup_inf_left]; exact @h _ _⟩

Proof state:
α : Type u_2
inst✝ : DistribLattice α
a : α
h : ∀ ⦃b c : α⦄, b ⊓ c = a → b = a ∨ c = a
b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) = a → a ⊔ b = a ∨ a ⊔ c = a

Tactic:
exact @h _ _

Result:
no goals

Proof state:
α : Type u_2
inst✝ : DistribLattice α
a : α
h : ∀ ⦃b c : α⦄, b ⊓ c = a → b = a ∨ c = a
b c : α
⊢ b ⊓ c ≤ a → b ≤ a ∨ c ≤ a

Tactic:
simp_rw [← sup_eq_left, sup_inf_left]

Result:
α : Type u_2
inst✝ : DistribLattice α
a : α
h : ∀ ⦃b c : α⦄, b ⊓ c = a → b = a ∨ c = a
b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) = a → a ⊔ b = a ∨ a ⊔ c = a
-- Mathlib/Algebra/Field/Defs.lean
@[simp] lemma smul_one_eq_cast (q : ℚ≥0) : q • (1 : K) = q

Proof state:
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
⊢ q • 1 = ↑q

Tactic:
rw [NNRat.smul_def, mul_one]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean
theorem range_eq (e : P₁ ≃ᵃ[k] P₂) : range e = univ

Proof state:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
e : P₁ ≃ᵃ[k] P₂
⊢ range ⇑e = univ

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/HashesTo.lean
theorem HashesTo.containsKey_eq_false [BEq α] [Hashable α] [LawfulHashable α]
    {l : List ((a : α) × β a)} {i : Nat} {size : Nat} (hs : 0 < size) (h : HashesTo l i size)
    (k : α) : (mkIdx size hs (hash k)).1.toNat ≠ i → containsKey k l = false

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
i size : Nat
hs : 0 < size
h : HashesTo l i size
k : α
⊢ ¬containsKey k l = false → ¬(mkIdx size hs (hash k)).val.toNat ≠ i

Tactic:
simp only [Bool.not_eq_false, containsKey_eq_true_iff_exists_mem]

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
i size : Nat
hs : 0 < size
h : HashesTo l i size
k : α
⊢ (∃ p, p ∈ l ∧ (p.fst == k) = true) → ¬(mkIdx size hs (hash k)).val.toNat ≠ i

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
i size : Nat
hs : 0 < size
h : HashesTo l i size
k : α
⊢ (∃ p, p ∈ l ∧ (p.fst == k) = true) → ¬(mkIdx size hs (hash k)).val.toNat ≠ i

Tactic:
rintro ⟨⟨k', v⟩, hmem, heq⟩

Result:
case intro.mk.intro
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
i size : Nat
hs : 0 < size
h : HashesTo l i size
k k' : α
v : β k'
hmem : ⟨k', v⟩ ∈ l
heq : (⟨k', v⟩.fst == k) = true
⊢ ¬(mkIdx size hs (hash k)).val.toNat ≠ i

Proof state:
case intro.mk.intro
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
i size : Nat
hs : 0 < size
h : HashesTo l i size
k k' : α
v : β k'
hmem : ⟨k', v⟩ ∈ l
heq : (⟨k', v⟩.fst == k) = true
⊢ ¬(mkIdx size hs (hash k)).val.toNat ≠ i

Tactic:
simp [← h.hash_self hs _ hmem, hash_eq heq]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
i size : Nat
hs : 0 < size
h : HashesTo l i size
k : α
⊢ (mkIdx size hs (hash k)).val.toNat ≠ i → containsKey k l = false

Tactic:
rw [← Decidable.not_imp_not]

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
i size : Nat
hs : 0 < size
h : HashesTo l i size
k : α
⊢ ¬containsKey k l = false → ¬(mkIdx size hs (hash k)).val.toNat ≠ i
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem_replace [LawfulBEq α] {l : List α} {i : Nat} (h : i < l.length) :
    (l.replace a b)[i]'(by simpa) = if l[i] == a then if a ∈ l.take i then a else b else l[i]

Proof state:
α : Type u_1
inst✝¹ : BEq α
a b : α
inst✝ : LawfulBEq α
l : List α
i : Nat
h : i < l.length
⊢ (l.replace a b)[i] = if (l[i] == a) = true then if a ∈ take i l then a else b else l[i]

Tactic:
apply Option.some.inj

Result:
case x
α : Type u_1
inst✝¹ : BEq α
a b : α
inst✝ : LawfulBEq α
l : List α
i : Nat
h : i < l.length
⊢ some (l.replace a b)[i] = some (if (l[i] == a) = true then if a ∈ take i l then a else b else l[i])

Proof state:
case x
α : Type u_1
inst✝¹ : BEq α
a b : α
inst✝ : LawfulBEq α
l : List α
i : Nat
h : i < l.length
⊢ (if (l[i]? == some a) = true then if a ∈ take i l then some a else some b else l[i]?) =
    some (if (l[i] == a) = true then if a ∈ take i l then a else b else l[i])

Tactic:
split <;> split <;> simp_all

Result:
no goals

Proof state:
α : Type ?u.362613
inst✝¹ : BEq α
a b : α
inst✝ : LawfulBEq α
l : List α
i : Nat
h : i < l.length
⊢ i < (l.replace a b).length

Tactic:
simpa

Result:
no goals

Proof state:
case x
α : Type u_1
inst✝¹ : BEq α
a b : α
inst✝ : LawfulBEq α
l : List α
i : Nat
h : i < l.length
⊢ some (l.replace a b)[i] = some (if (l[i] == a) = true then if a ∈ take i l then a else b else l[i])

Tactic:
rw [← getElem?_eq_getElem, getElem?_replace]

Result:
case x
α : Type u_1
inst✝¹ : BEq α
a b : α
inst✝ : LawfulBEq α
l : List α
i : Nat
h : i < l.length
⊢ (if (l[i]? == some a) = true then if a ∈ take i l then some a else some b else l[i]?) =
    some (if (l[i] == a) = true then if a ∈ take i l then a else b else l[i])