harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Fourier/FiniteAbelian/Orthogonality.lean
protected lemma linearIndependent [Finite G] : LinearIndependent R ((⇑) : AddChar G R → G → R)

Proof state:
case intro
G : Type u_1
R : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : RCLike R
inst✝ : Finite G
val✝ : Fintype G
⊢ LinearIndependent R DFunLike.coe

Tactic:
exact linearIndependent_of_ne_zero_of_wInner_cWeight_eq_zero coe_ne_zero
  fun ψ₁ ψ₂ ↦ wInner_cWeight_eq_zero_iff_ne.2

Result:
no goals

Proof state:
G : Type u_1
R : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : RCLike R
inst✝ : Finite G
⊢ LinearIndependent R DFunLike.coe

Tactic:
cases nonempty_fintype G

Result:
case intro
G : Type u_1
R : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : RCLike R
inst✝ : Finite G
val✝ : Fintype G
⊢ LinearIndependent R DFunLike.coe
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_mul_const_uIcc (a b c : α) : (· * a) '' [[b, c]] = [[b * a, c * a]] :=
  if ha : a = 0 then by simp [ha]
  else calc
    (fun x => x * a) '' [[b, c]] = (· * a⁻¹) ⁻¹' [[b, c]] :=
      (Units.mk0 a ha).mulRight.image_eq_preimage _
    _ = (fun x => x / a) ⁻¹' [[b, c]]

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b c : α
ha : ¬a = 0
⊢ (fun x => x * a⁻¹) ⁻¹' [[b, c]] = (fun x => x / a) ⁻¹' [[b, c]]

Tactic:
simp only [div_eq_mul_inv]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b c : α
ha : a = 0
⊢ (fun x => x * a) '' [[b, c]] = [[b * a, c * a]]

Tactic:
simp [ha]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Perm.lean
theorem Perm.union_left (l : List α) {t₁ t₂ : List α} (h : t₁ ~ t₂) : l ∪ t₁ ~ l ∪ t₂

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l t₁ t₂ : List α
h : t₁ ~ t₂
⊢ l ∪ t₁ ~ l ∪ t₂

Tactic:
induction l with
| nil => simp only [nil_union, h]
| cons _ _ ih => simp only [cons_union, Perm.insert _ ih]

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
t₁ t₂ : List α
h : t₁ ~ t₂
head✝ : α
tail✝ : List α
ih : tail✝ ∪ t₁ ~ tail✝ ∪ t₂
⊢ head✝ :: tail✝ ∪ t₁ ~ head✝ :: tail✝ ∪ t₂

Tactic:
simp only [cons_union, Perm.insert _ ih]

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
t₁ t₂ : List α
h : t₁ ~ t₂
⊢ [] ∪ t₁ ~ [] ∪ t₂

Tactic:
simp only [nil_union, h]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem hasStrictFDerivAt_inv' {x : R} (hx : x ≠ 0) :
    HasStrictFDerivAt Inv.inv (-mulLeftRight 𝕜 R x⁻¹ x⁻¹) x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
R : Type u_5
inst✝¹ : NormedDivisionRing R
inst✝ : NormedAlgebra 𝕜 R
x : R
hx : x ≠ 0
⊢ HasStrictFDerivAt Inv.inv (-((mulLeftRight 𝕜 R) x⁻¹) x⁻¹) x

Tactic:
simpa using hasStrictFDerivAt_ring_inverse (Units.mk0 _ hx)

Result:
no goals
-- Mathlib/Data/Multiset/AddSub.lean
lemma le_add_left (s t : Multiset α) : s ≤ t + s

Proof state:
α : Type u_1
s t : Multiset α
⊢ s ≤ t + s

Tactic:
simpa using Multiset.add_le_add_right (zero_le t)

Result:
no goals
-- Mathlib/Data/Finset/Density.lean
@[simp]
lemma dens_inter_add_dens_sdiff (s t : Finset α) : dens (s ∩ t) + dens (s \ t) = dens s

Proof state:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s t : Finset α
⊢ (s ∩ t).dens + (s \ t).dens = s.dens

Tactic:
rw [add_comm, dens_sdiff_add_dens_inter]

Result:
no goals
-- Mathlib/Data/Multiset/Lattice.lean
theorem sup_ndunion (s₁ s₂ : Multiset α) : (ndunion s₁ s₂).sup = s₁.sup ⊔ s₂.sup

Proof state:
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁.ndunion s₂ ↔ a ∈ s₁ + s₂

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁.ndunion s₂).sup = s₁.sup ⊔ s₂.sup

Tactic:
rw [← sup_dedup, dedup_ext.2, sup_dedup, sup_add]

Result:
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁.ndunion s₂ ↔ a ∈ s₁ + s₂
-- Mathlib/RingTheory/FractionalIdeal/Basic.lean
theorem den_mul_self_eq_num (I : FractionalIdeal S P) :
    I.den • (I : Submodule R P) = Submodule.map (Algebra.linearMap R P) I.num

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : FractionalIdeal S P
⊢ ⟨Exists.choose ⋯, ⋯⟩ • ↑I ≤ LinearMap.range (Algebra.linearMap R P)

Tactic:
rintro _ ⟨a, ha, rfl⟩

Result:
case intro.intro
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : FractionalIdeal S P
a : P
ha : a ∈ ↑↑I
⊢ (DistribMulAction.toLinearMap R P ↑⟨Exists.choose ⋯, ⋯⟩) a ∈ LinearMap.range (Algebra.linearMap R P)

Proof state:
case intro.intro
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : FractionalIdeal S P
a : P
ha : a ∈ ↑↑I
⊢ (DistribMulAction.toLinearMap R P ↑⟨Exists.choose ⋯, ⋯⟩) a ∈ LinearMap.range (Algebra.linearMap R P)

Tactic:
exact I.2.choose_spec.2 a ha

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : FractionalIdeal S P
⊢ I.den • ↑I = Submodule.map (Algebra.linearMap R P) I.num

Tactic:
rw [den, num, Submodule.map_comap_eq]

Result:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : FractionalIdeal S P
⊢ ⟨Exists.choose ⋯, ⋯⟩ • ↑I = LinearMap.range (Algebra.linearMap R P) ⊓ I.den • ↑I

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : FractionalIdeal S P
⊢ ⟨Exists.choose ⋯, ⋯⟩ • ↑I = LinearMap.range (Algebra.linearMap R P) ⊓ I.den • ↑I

Tactic:
refine (inf_of_le_right ?_).symm

Result:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : FractionalIdeal S P
⊢ ⟨Exists.choose ⋯, ⋯⟩ • ↑I ≤ LinearMap.range (Algebra.linearMap R P)
-- Mathlib/Algebra/Lie/TraceForm.lean
/-- See also `LieModule.traceForm_eq_sum_finrank_nsmul'` for an expression omitting the zero
weights. -/
lemma traceForm_eq_sum_finrank_nsmul :
    traceForm K L M = ∑ χ : Weight K L M, finrank K (genWeightSpace M χ) •
      (χ : L →ₗ[K] K).smulRight (χ : L →ₗ[K] K)

Proof state:
case H
K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : LieRing L
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
inst✝⁷ : Field K
inst✝⁶ : LieAlgebra K L
inst✝⁵ : Module K M
inst✝⁴ : LieModule K L M
inst✝³ : FiniteDimensional K M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : LinearWeights K L M
inst✝ : IsTriangularizable K L M
x✝ y✝ : L
⊢ ∑ x ∈ Finset.univ.attach, finrank K ↥(genWeightSpace M ⇑↑x) • (↑x x✝ * ↑x y✝) =
    ((∑ χ : Weight K L M,
          finrank K ↥(genWeightSpace M ⇑χ) • (Weight.toLinear K L M χ).smulRight (Weight.toLinear K L M χ))
        x✝)
      y✝

Tactic:
simp

Result:
no goals

Proof state:
case H
K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : LieRing L
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
inst✝⁷ : Field K
inst✝⁶ : LieAlgebra K L
inst✝⁵ : Module K M
inst✝⁴ : LieModule K L M
inst✝³ : FiniteDimensional K M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : LinearWeights K L M
inst✝ : IsTriangularizable K L M
x✝ y✝ : L
⊢ ((traceForm K L M) x✝) y✝ =
    ((∑ χ : Weight K L M,
          finrank K ↥(genWeightSpace M ⇑χ) • (Weight.toLinear K L M χ).smulRight (Weight.toLinear K L M χ))
        x✝)
      y✝

Tactic:
rw [traceForm_eq_sum_finrank_nsmul_mul, ← Finset.sum_attach]

Result:
case H
K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : LieRing L
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
inst✝⁷ : Field K
inst✝⁶ : LieAlgebra K L
inst✝⁵ : Module K M
inst✝⁴ : LieModule K L M
inst✝³ : FiniteDimensional K M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : LinearWeights K L M
inst✝ : IsTriangularizable K L M
x✝ y✝ : L
⊢ ∑ x ∈ Finset.univ.attach, finrank K ↥(genWeightSpace M ⇑↑x) • (↑x x✝ * ↑x y✝) =
    ((∑ χ : Weight K L M,
          finrank K ↥(genWeightSpace M ⇑χ) • (Weight.toLinear K L M χ).smulRight (Weight.toLinear K L M χ))
        x✝)
      y✝

Proof state:
K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : LieRing L
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
inst✝⁷ : Field K
inst✝⁶ : LieAlgebra K L
inst✝⁵ : Module K M
inst✝⁴ : LieModule K L M
inst✝³ : FiniteDimensional K M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : LinearWeights K L M
inst✝ : IsTriangularizable K L M
⊢ traceForm K L M =
    ∑ χ : Weight K L M, finrank K ↥(genWeightSpace M ⇑χ) • (Weight.toLinear K L M χ).smulRight (Weight.toLinear K L M χ)

Tactic:
ext

Result:
case H
K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : LieRing L
inst✝⁹ : AddCommGroup M
inst✝⁸ : LieRingModule L M
inst✝⁷ : Field K
inst✝⁶ : LieAlgebra K L
inst✝⁵ : Module K M
inst✝⁴ : LieModule K L M
inst✝³ : FiniteDimensional K M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : LinearWeights K L M
inst✝ : IsTriangularizable K L M
x✝ y✝ : L
⊢ ((traceForm K L M) x✝) y✝ =
    ((∑ χ : Weight K L M,
          finrank K ↥(genWeightSpace M ⇑χ) • (Weight.toLinear K L M χ).smulRight (Weight.toLinear K L M χ))
        x✝)
      y✝
-- Mathlib/GroupTheory/Perm/Support.lean
theorem support_swap {x y : α} (h : x ≠ y) : support (swap x y) = {x, y}

Proof state:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
h : x ≠ y
z : α
hx : ¬z = x
hy : ¬z = y
⊢ z ∈ (swap x y).support ↔ z ∈ {x, y}

Tactic:
simp [swap_apply_of_ne_of_ne, hx, hy]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
h : x ≠ y
⊢ (swap x y).support = {x, y}

Tactic:
ext z

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
h : x ≠ y
z : α
⊢ z ∈ (swap x y).support ↔ z ∈ {x, y}

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
h : x ≠ y
z : α
hx : z = x
⊢ z ∈ (swap x y).support ↔ z ∈ {x, y}

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
h : x ≠ y
z : α
hx : ¬z = x
⊢ z ∈ (swap x y).support ↔ z ∈ {x, y}

Tactic:
any_goals simpa [hx] using h.symm

Result:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
h : x ≠ y
z : α
hx : ¬z = x
⊢ z ∈ (swap x y).support ↔ z ∈ {x, y}

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
h : x ≠ y
z : α
hx : ¬z = x
hy : z = y
⊢ z ∈ (swap x y).support ↔ z ∈ {x, y}

Tactic:
simpa [swap_apply_of_ne_of_ne, hx, hy] using h

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
h : x ≠ y
z : α
hx : ¬z = x
⊢ z ∈ (swap x y).support ↔ z ∈ {x, y}

Tactic:
simpa [hx] using h.symm

Result:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
h : x ≠ y
z : α
hx : ¬z = x
h✝ : ¬y = x
⊢ ¬(swap x y) z = z ↔ z = y

Proof state:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
h : x ≠ y
z : α
hx : ¬z = x
⊢ z ∈ (swap x y).support ↔ z ∈ {x, y}

Tactic:
by_cases hy : z = y

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
h : x ≠ y
z : α
hx : ¬z = x
hy : z = y
⊢ z ∈ (swap x y).support ↔ z ∈ {x, y}

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
h : x ≠ y
z : α
hx : ¬z = x
hy : ¬z = y
⊢ z ∈ (swap x y).support ↔ z ∈ {x, y}

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
h : x ≠ y
z : α
⊢ z ∈ (swap x y).support ↔ z ∈ {x, y}

Tactic:
by_cases hx : z = x

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
h : x ≠ y
z : α
hx : z = x
⊢ z ∈ (swap x y).support ↔ z ∈ {x, y}

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
h : x ≠ y
z : α
hx : ¬z = x
⊢ z ∈ (swap x y).support ↔ z ∈ {x, y}
-- Mathlib/RingTheory/Kaehler/Basic.lean
theorem KaehlerDifferential.mapBaseChange_tmul (x : B) (y : Ω[A⁄R]) :
    KaehlerDifferential.mapBaseChange R A B (x ⊗ₜ y) = x • KaehlerDifferential.map R R A B y

Proof state:
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : B
y : Ω[A⁄R]
⊢ (mapBaseChange R A B) (x ⊗ₜ[A] y) = x • (map R R A B) y

Tactic:
conv_lhs => rw [← mul_one x, ← smul_eq_mul, ← TensorProduct.smul_tmul', LinearMap.map_smul]

Result:
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : B
y : Ω[A⁄R]
⊢ x • (mapBaseChange R A B) (1 ⊗ₜ[A] y) = x • (map R R A B) y

Proof state:
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : B
y : Ω[A⁄R]
⊢ x • (mapBaseChange R A B) (1 ⊗ₜ[A] y) = x • (map R R A B) y

Tactic:
congr 1

Result:
case e_a
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : B
y : Ω[A⁄R]
⊢ (mapBaseChange R A B) (1 ⊗ₜ[A] y) = (map R R A B) y

Proof state:
case e_a
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : B
y : Ω[A⁄R]
⊢ (mapBaseChange R A B) (1 ⊗ₜ[A] y) = (map R R A B) y

Tactic:
exact IsBaseChange.lift_eq _ _ _

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem splitWrtCompositionAux_cons (l : List α) (n ns) :
    l.splitWrtCompositionAux (n::ns) = take n l::(drop n l).splitWrtCompositionAux ns

Proof state:
α : Type u_1
l : List α
n : ℕ
ns : List ℕ
⊢ l.splitWrtCompositionAux (n :: ns) = take n l :: (drop n l).splitWrtCompositionAux ns

Tactic:
simp [splitWrtCompositionAux]

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Finset.lean
theorem Finset.ciSup_mem_image {s : Finset ι} (h : ∃ x ∈ s, sSup ∅ ≤ f x) :
    ⨆ i ∈ s, f i ∈ s.image f

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ (image f s).max' ⋯ ∈ image f s

Tactic:
exact max'_mem (image f s) _

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ⨆ i ∈ s, f i ∈ image f s

Tactic:
rw [ciSup_eq_max'_image _ h]

Result:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ (image f s).max' ⋯ ∈ image f s
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem commute_of_mem_cycleFactorsFinset_commute (k g : Perm α)
    (hk : ∀ c ∈ g.cycleFactorsFinset, Commute k c) :
    Commute k g

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k g : Perm α
hk : ∀ c ∈ g.cycleFactorsFinset, Commute k c
⊢ Commute k g

Tactic:
rw [← cycleFactorsFinset_noncommProd g (cycleFactorsFinset_mem_commute g)]

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k g : Perm α
hk : ∀ c ∈ g.cycleFactorsFinset, Commute k c
⊢ Commute k (g.cycleFactorsFinset.noncommProd id ⋯)

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k g : Perm α
hk : ∀ c ∈ g.cycleFactorsFinset, Commute k c
⊢ Commute k (g.cycleFactorsFinset.noncommProd id ⋯)

Tactic:
apply Finset.noncommProd_commute

Result:
case h
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k g : Perm α
hk : ∀ c ∈ g.cycleFactorsFinset, Commute k c
⊢ ∀ x ∈ g.cycleFactorsFinset, Commute k (id x)

Proof state:
case h
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k g : Perm α
hk : ∀ c ∈ g.cycleFactorsFinset, Commute k c
⊢ ∀ x ∈ g.cycleFactorsFinset, Commute k (id x)

Tactic:
simpa only [id_eq] using hk

Result:
no goals
-- Mathlib/Data/Finset/Insert.lean
theorem toFinset_singleton (a : α) : toFinset ({a} : Multiset α) = {a}

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
⊢ {a}.toFinset = {a}

Tactic:
rw [← cons_zero, toFinset_cons, toFinset_zero, LawfulSingleton.insert_emptyc_eq]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean
theorem sdiff_compl_neighborFinset_inter_eq {v w : V} (h : G.Adj v w) :
    ((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v}) =
      (G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ

Proof state:
case h
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v w : V
h : G.Adj v w
a✝ : V
⊢ ¬G.Adj v a✝ → ¬G.Adj w a✝ → ¬(a✝ = w ∨ a✝ = v)

Tactic:
rintro hnv hnw (rfl | rfl)

Result:
case h.inl
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v a✝ : V
hnv : ¬G.Adj v a✝
h : G.Adj v a✝
hnw : ¬G.Adj a✝ a✝
⊢ False

case h.inr
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
w a✝ : V
hnw : ¬G.Adj w a✝
h : G.Adj a✝ w
hnv : ¬G.Adj a✝ a✝
⊢ False

Proof state:
case h.inl
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v a✝ : V
hnv : ¬G.Adj v a✝
h : G.Adj v a✝
hnw : ¬G.Adj a✝ a✝
⊢ False

Tactic:
exact hnv h

Result:
no goals

Proof state:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v w : V
h : G.Adj v w
⊢ ((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v}) = (G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ

Tactic:
ext

Result:
case h
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v w : V
h : G.Adj v w
a✝ : V
⊢ a✝ ∈ ((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v}) ↔
    a✝ ∈ (G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ

Proof state:
case h.inr
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
w a✝ : V
hnw : ¬G.Adj w a✝
h : G.Adj a✝ w
hnv : ¬G.Adj a✝ a✝
⊢ False

Tactic:
apply hnw

Result:
case h.inr
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
w a✝ : V
hnw : ¬G.Adj w a✝
h : G.Adj a✝ w
hnv : ¬G.Adj a✝ a✝
⊢ G.Adj w a✝

Proof state:
case h
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v w : V
h : G.Adj v w
a✝ : V
⊢ a✝ ∈ ((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v}) ↔
    a✝ ∈ (G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ

Tactic:
simp only [and_imp, mem_union, mem_sdiff, mem_compl, and_iff_left_iff_imp, mem_neighborFinset,
  mem_inter, mem_singleton]

Result:
case h
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v w : V
h : G.Adj v w
a✝ : V
⊢ ¬G.Adj v a✝ → ¬G.Adj w a✝ → ¬(a✝ = w ∨ a✝ = v)

Proof state:
case h.inr
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
w a✝ : V
hnw : ¬G.Adj w a✝
h : G.Adj a✝ w
hnv : ¬G.Adj a✝ a✝
⊢ G.Adj w a✝

Tactic:
rwa [adj_comm]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma decreasingInduction_succ {n} {motive : (m : ℕ) → m ≤ n + 1 → Sort*} (of_succ self)
    (mn : m ≤ n) (msn : m ≤ n + 1) :
    (decreasingInduction (motive := motive) of_succ self msn : motive m msn) =
      decreasingInduction (motive := fun m h => motive m (le_succ_of_le h))
        (fun _ _ => of_succ _ _) (of_succ _ _ self) mn

Proof state:
m n : ℕ
motive : (m : ℕ) → m ≤ n + 1 → Sort u_1
of_succ : (k : ℕ) → (h : k < n + 1) → motive (k + 1) h → motive k ⋯
self : motive (n + 1) ⋯
mn : m ≤ n
msn : m ≤ n + 1
⊢ leRec (motive := fun {n} mn =>
      {motive : (m : ℕ) → m ≤ n → Sort u_1} →
        ((k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯) → motive n ⋯ → motive m mn)
      (fun {motive} of_succ self => self)
      (fun ⦃k⦄ h ih {motive} of_succ self => ih (fun i hi => of_succ i ⋯) (of_succ k ⋯ self)) msn of_succ self =
    leRec (motive := fun {n} mn =>
      {motive : (m : ℕ) → m ≤ n → Sort u_1} →
        ((k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯) → motive n ⋯ → motive m mn)
      (fun {motive} of_succ self => self)
      (fun ⦃k⦄ h ih {motive} of_succ self => ih (fun i hi => of_succ i ⋯) (of_succ k ⋯ self)) mn
      (fun x x_1 => of_succ x ⋯) (of_succ n ⋯ self)

Tactic:
rw [leRec_succ]

Result:
no goals

Proof state:
m n : ℕ
motive : (m : ℕ) → m ≤ n + 1 → Sort u_1
of_succ : (k : ℕ) → (h : k < n + 1) → motive (k + 1) h → motive k ⋯
self : motive (n + 1) ⋯
mn : m ≤ n
msn : m ≤ n + 1
⊢ decreasingInduction of_succ self msn = decreasingInduction (fun x x_1 => of_succ x ⋯) (of_succ n ⋯ self) mn

Tactic:
dsimp only [decreasingInduction]

Result:
m n : ℕ
motive : (m : ℕ) → m ≤ n + 1 → Sort u_1
of_succ : (k : ℕ) → (h : k < n + 1) → motive (k + 1) h → motive k ⋯
self : motive (n + 1) ⋯
mn : m ≤ n
msn : m ≤ n + 1
⊢ leRec (motive := fun {n} mn =>
      {motive : (m : ℕ) → m ≤ n → Sort u_1} →
        ((k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯) → motive n ⋯ → motive m mn)
      (fun {motive} of_succ self => self)
      (fun ⦃k⦄ h ih {motive} of_succ self => ih (fun i hi => of_succ i ⋯) (of_succ k ⋯ self)) msn of_succ self =
    leRec (motive := fun {n} mn =>
      {motive : (m : ℕ) → m ≤ n → Sort u_1} →
        ((k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯) → motive n ⋯ → motive m mn)
      (fun {motive} of_succ self => self)
      (fun ⦃k⦄ h ih {motive} of_succ self => ih (fun i hi => of_succ i ⋯) (of_succ k ⋯ self)) mn
      (fun x x_1 => of_succ x ⋯) (of_succ n ⋯ self)
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
@[to_additive]
lemma mul_left_inj_of_comparable [MulRightStrictMono α] {a b c : α} (h : b ≤ c ∨ c ≤ b) :
    c * a = b * a ↔ c = b

Proof state:
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulRightStrictMono α
a b c : α
h : b ≤ c ∨ c ≤ b
h' : ¬c = b
⊢ ¬c * a = b * a

Tactic:
obtain h | h := h

Result:
case inl
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulRightStrictMono α
a b c : α
h' : ¬c = b
h : b ≤ c
⊢ ¬c * a = b * a

case inr
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulRightStrictMono α
a b c : α
h' : ¬c = b
h : c ≤ b
⊢ ¬c * a = b * a

Proof state:
case inr
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulRightStrictMono α
a b c : α
h' : ¬c = b
h : c ≤ b
⊢ ¬c * a = b * a

Tactic:
exact mul_lt_mul_right' (h.lt_of_ne h') a |>.ne

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulRightStrictMono α
a b c : α
h' : ¬c = b
h : b ≤ c
⊢ ¬c * a = b * a

Tactic:
exact mul_lt_mul_right' (h.lt_of_ne' h') a |>.ne'

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulRightStrictMono α
a b c : α
h : b ≤ c ∨ c ≤ b
h' : c * a = b * a
⊢ c = b

Tactic:
contrapose h'

Result:
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulRightStrictMono α
a b c : α
h : b ≤ c ∨ c ≤ b
h' : ¬c = b
⊢ ¬c * a = b * a
-- Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean
lemma measurableSet_countableGeneratingSet [MeasurableSpace α] [CountablyGenerated α]
    {s : Set α} (hs : s ∈ countableGeneratingSet α) :
    MeasurableSet s

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : s ∈ countableGeneratingSet α
⊢ MeasurableSet s

Tactic:
exact measurableSet_generateFrom hs

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
lemma congr_v {z₁ z₂ : Cochain F G n} (h : z₁ = z₂) (p q : ℤ) (hpq : p + n = q) :
    z₁.v p q hpq = z₂.v p q hpq

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z₁ z₂ : Cochain F G n
h : z₁ = z₂
p q : ℤ
hpq : p + n = q
⊢ z₁.v p q hpq = z₂.v p q hpq

Tactic:
subst h

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z₁ : Cochain F G n
p q : ℤ
hpq : p + n = q
⊢ z₁.v p q hpq = z₁.v p q hpq

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z₁ : Cochain F G n
p q : ℤ
hpq : p + n = q
⊢ z₁.v p q hpq = z₁.v p q hpq

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/ERealExp.lean
@[simp] lemma exp_eq_top_iff {x : EReal} : exp x = ∞ ↔ x = ⊤

Proof state:
x : EReal
⊢ x.exp = ⊤ ↔ x = ⊤

Tactic:
induction x <;> simp

Result:
no goals