harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/FreeModule/PID.lean
theorem Module.free_of_finite_type_torsion_free [_root_.Finite ι] {s : ι → M}
    (hs : span R (range s) = ⊤) [NoZeroSMulDivisors R M] : Module.Free R M

Proof state:
case intro
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Finite ι
s : ι → M
hs : span R (range s) = ⊤
inst✝ : NoZeroSMulDivisors R M
val✝ : Fintype ι
⊢ Free R M

Tactic:
obtain ⟨n, b⟩ : Σn, Basis (Fin n) R M := Module.basisOfFiniteTypeTorsionFree hs

Result:
case intro.mk
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Finite ι
s : ι → M
hs : span R (range s) = ⊤
inst✝ : NoZeroSMulDivisors R M
val✝ : Fintype ι
n : ℕ
b : Basis (Fin n) R M
⊢ Free R M

Proof state:
case intro.mk
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Finite ι
s : ι → M
hs : span R (range s) = ⊤
inst✝ : NoZeroSMulDivisors R M
val✝ : Fintype ι
n : ℕ
b : Basis (Fin n) R M
⊢ Free R M

Tactic:
exact Module.Free.of_basis b

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Finite ι
s : ι → M
hs : span R (range s) = ⊤
inst✝ : NoZeroSMulDivisors R M
⊢ Free R M

Tactic:
cases nonempty_fintype ι

Result:
case intro
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Finite ι
s : ι → M
hs : span R (range s) = ⊤
inst✝ : NoZeroSMulDivisors R M
val✝ : Fintype ι
⊢ Free R M
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioi_diff_Ici : Ioi a \ Ici b = Ioo a b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ioi a \ Ici b = Ioo a b

Tactic:
rw [diff_eq, compl_Ici, Ioi_inter_Iio]

Result:
no goals
-- Mathlib/NumberTheory/LucasLehmer.lean
theorem ω_pow_eq_neg_one (p' : ℕ) (h : lucasLehmerResidue (p' + 2) = 0) :
    (ω : X (q (p' + 2))) ^ 2 ^ (p' + 1) = -1

Proof state:
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ω ^ 2 ^ (p' + 1) = -1

Tactic:
obtain ⟨k, w⟩ := ω_pow_formula p' h

Result:
case intro
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
k : ℤ
w : ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
⊢ ω ^ 2 ^ (p' + 1) = -1

Proof state:
case intro
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
k : ℤ
w : ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
⊢ ω ^ 2 ^ (p' + 1) = -1

Tactic:
rw [mersenne_coe_X] at w

Result:
case intro
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
k : ℤ
w : ω ^ 2 ^ (p' + 1) = ↑k * 0 * ω ^ 2 ^ p' - 1
⊢ ω ^ 2 ^ (p' + 1) = -1

Proof state:
case intro
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
k : ℤ
w : ω ^ 2 ^ (p' + 1) = ↑k * 0 * ω ^ 2 ^ p' - 1
⊢ ω ^ 2 ^ (p' + 1) = -1

Tactic:
simpa using w

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem algebra_isAlgebraic_bot_left_iff (h : Function.Injective (algebraMap R S)) :
    Algebra.IsAlgebraic (⊥ : Subalgebra R S) S ↔ Algebra.IsAlgebraic R S

Proof state:
R : Type u
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Injective ⇑(algebraMap R S)
⊢ Algebra.IsAlgebraic (↥⊥) S ↔ Algebra.IsAlgebraic R S

Tactic:
simp_rw [Algebra.isAlgebraic_def, isAlgebraic_bot_iff h]

Result:
no goals
-- Mathlib/Data/Finite/Card.lean
theorem card_eq_zero_of_surjective {f : α → β} (hf : Function.Surjective f) (h : Nat.card β = 0) :
    Nat.card α = 0

Proof state:
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
⊢ Nat.card α = 0

Tactic:
cases finite_or_infinite β

Result:
case inl
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Finite β
⊢ Nat.card α = 0

case inr
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Infinite β
⊢ Nat.card α = 0

Proof state:
case inl
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Finite β
this✝ : IsEmpty β
this : IsEmpty α
⊢ Nat.card α = 0

Tactic:
exact Nat.card_of_isEmpty

Result:
no goals

Proof state:
case inl
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Finite β
this : IsEmpty β
⊢ Nat.card α = 0

Tactic:
haveI := Function.isEmpty f

Result:
case inl
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Finite β
this✝ : IsEmpty β
this : IsEmpty α
⊢ Nat.card α = 0

Proof state:
case inr
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Infinite β
this : Infinite α
⊢ Nat.card α = 0

Tactic:
exact Nat.card_eq_zero_of_infinite

Result:
no goals

Proof state:
case inr
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Infinite β
⊢ Nat.card α = 0

Tactic:
haveI := Infinite.of_surjective f hf

Result:
case inr
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Infinite β
this : Infinite α
⊢ Nat.card α = 0

Proof state:
case inl
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Finite β
⊢ Nat.card α = 0

Tactic:
haveI := card_eq_zero_iff.mp h

Result:
case inl
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Finite β
this : IsEmpty β
⊢ Nat.card α = 0
-- Mathlib/LinearAlgebra/Contraction.lean
theorem homTensorHomEquiv_apply (x : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q)) :
    homTensorHomEquiv R M N P Q x = homTensorHomMap R M N P Q x

Proof state:
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : AddCommGroup P
inst✝⁸ : AddCommGroup Q
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module R P
inst✝⁴ : Module R Q
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
x : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q)
⊢ (homTensorHomEquiv R M N P Q) x = (homTensorHomMap R M N P Q) x

Tactic:
rw [← LinearEquiv.coe_toLinearMap, homTensorHomEquiv_toLinearMap]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem rTensor_pow (f : M →ₗ[R] M) (n : ℕ) : f.rTensor N ^ n = (f ^ n).rTensor N

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M →ₗ[R] M
n : ℕ
h : map f id ^ n = map (f ^ n) (id ^ n)
⊢ rTensor N f ^ n = rTensor N (f ^ n)

Tactic:
rwa [id_pow] at h

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M →ₗ[R] M
n : ℕ
⊢ rTensor N f ^ n = rTensor N (f ^ n)

Tactic:
have h := TensorProduct.map_pow f (id : N →ₗ[R] N) n

Result:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M →ₗ[R] M
n : ℕ
h : map f id ^ n = map (f ^ n) (id ^ n)
⊢ rTensor N f ^ n = rTensor N (f ^ n)
-- Mathlib/RingTheory/Polynomial/Wronskian.lean
theorem wronskian_zero_left (a : R[X]) : wronskian 0 a = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
a : R[X]
⊢ wronskian 0 a = 0

Tactic:
rw [← wronskianBilin_apply 0 a, map_zero]

Result:
R : Type u_1
inst✝ : CommRing R
a : R[X]
⊢ 0 a = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
a : R[X]
⊢ 0 a = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem add_le_of_le_neg_add {a b c : Int} (h : b ≤ -a + c) : a + b ≤ c

Proof state:
a b c : Int
h✝ : b ≤ -a + c
h : a + b ≤ a + (-a + c)
⊢ a + b ≤ c

Tactic:
rwa [Int.add_neg_cancel_left] at h

Result:
no goals

Proof state:
a b c : Int
h : b ≤ -a + c
⊢ a + b ≤ c

Tactic:
have h := Int.add_le_add_left h a

Result:
a b c : Int
h✝ : b ≤ -a + c
h : a + b ≤ a + (-a + c)
⊢ a + b ≤ c
-- Mathlib/Data/List/Zip.lean
theorem forall_zipWith {f : α → β → γ} {p : γ → Prop} :
    ∀ {l₁ : List α} {l₂ : List β}, length l₁ = length l₂ →
      (Forall p (zipWith f l₁ l₂) ↔ Forall₂ (fun x y => p (f x y)) l₁ l₂)
  | [], [], _ => by simp
  | a :: l₁, b :: l₂, h => by
    simp only [length_cons, succ_inj'] at h
    simp [forall_zipWith h]

Proof state:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
p : γ → Prop
x✝ : [].length = [].length
⊢ Forall p (zipWith f [] []) ↔ Forall₂ (fun x y => p (f x y)) [] []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
p : γ → Prop
a : α
l₁ : List α
b : β
l₂ : List β
h : (a :: l₁).length = (b :: l₂).length
⊢ Forall p (zipWith f (a :: l₁) (b :: l₂)) ↔ Forall₂ (fun x y => p (f x y)) (a :: l₁) (b :: l₂)

Tactic:
simp only [length_cons, succ_inj'] at h

Result:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
p : γ → Prop
a : α
l₁ : List α
b : β
l₂ : List β
h : l₁.length = l₂.length
⊢ Forall p (zipWith f (a :: l₁) (b :: l₂)) ↔ Forall₂ (fun x y => p (f x y)) (a :: l₁) (b :: l₂)

Proof state:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
p : γ → Prop
a : α
l₁ : List α
b : β
l₂ : List β
h : l₁.length = l₂.length
⊢ Forall p (zipWith f (a :: l₁) (b :: l₂)) ↔ Forall₂ (fun x y => p (f x y)) (a :: l₁) (b :: l₂)

Tactic:
simp [forall_zipWith h]

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
lemma polyCharpolyAux_map_eval [Module.Finite R M] [Module.Free R M]
    (x : ι → R) :
    (polyCharpolyAux φ b bₘ).map (MvPolynomial.eval x) =
      (φ (b.repr.symm (Finsupp.equivFunOnFinite.symm x))).charpoly

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] Module.End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
inst✝¹ : Module.Finite R M
inst✝ : Module.Free R M
x : ι → R
⊢ Polynomial.map (MvPolynomial.eval x) (φ.polyCharpolyAux b bₘ) =
    charpoly (φ (b.repr.symm (Finsupp.equivFunOnFinite.symm x)))

Tactic:
simp only [← polyCharpolyAux_map_eq_charpoly φ b bₘ, LinearEquiv.apply_symm_apply,
  Finsupp.equivFunOnFinite, Equiv.coe_fn_symm_mk, Finsupp.coe_mk]

Result:
no goals
-- Mathlib/Topology/Filter.lean
theorem isOpen_setOf_mem {s : Set α} : IsOpen { l : Filter α | s ∈ l }

Proof state:
α : Type u_2
s : Set α
⊢ IsOpen {l | s ∈ l}

Tactic:
simpa only [Iic_principal] using isOpen_Iic_principal

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Content.lean
theorem innerContent_comap (f : G ≃ₜ G) (h : ∀ ⦃K : Compacts G⦄, μ (K.map f f.continuous) = μ K)
    (U : Opens G) : μ.innerContent (Opens.comap f U) = μ.innerContent U

Proof state:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, μ (Compacts.map ⇑f ⋯ K) = μ K
U : Opens G
K : Compacts G
hK : ↑K ⊆ ↑((Opens.comap ↑f) U)
⊢ μ ((Compacts.equiv f) K) = μ K

Tactic:
simp only [Equiv.coe_fn_mk, Subtype.mk_eq_mk, Compacts.equiv]

Result:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, μ (Compacts.map ⇑f ⋯ K) = μ K
U : Opens G
K : Compacts G
hK : ↑K ⊆ ↑((Opens.comap ↑f) U)
⊢ μ (Compacts.map ⇑f ⋯ K) = μ K

Proof state:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, μ (Compacts.map ⇑f ⋯ K) = μ K
U : Opens G
K : Compacts G
⊢ ↑K ⊆ ↑((Opens.comap ↑f) U) → μ ((Compacts.equiv f) K) = μ K

Tactic:
intro hK

Result:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, μ (Compacts.map ⇑f ⋯ K) = μ K
U : Opens G
K : Compacts G
hK : ↑K ⊆ ↑((Opens.comap ↑f) U)
⊢ μ ((Compacts.equiv f) K) = μ K

Proof state:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, μ (Compacts.map ⇑f ⋯ K) = μ K
U : Opens G
K : Compacts G
hK : ↑K ⊆ ↑((Opens.comap ↑f) U)
⊢ μ (Compacts.map ⇑f ⋯ K) = μ K

Tactic:
apply h

Result:
no goals

Proof state:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, μ (Compacts.map ⇑f ⋯ K) = μ K
U : Opens G
⊢ μ.innerContent ((Opens.comap ↑f) U) = μ.innerContent U

Tactic:
refine (Compacts.equiv f).surjective.iSup_congr _ fun K => iSup_congr_Prop image_subset_iff ?_

Result:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, μ (Compacts.map ⇑f ⋯ K) = μ K
U : Opens G
K : Compacts G
⊢ ↑K ⊆ ↑((Opens.comap ↑f) U) → μ ((Compacts.equiv f) K) = μ K
-- Mathlib/Data/Nat/Init.lean
protected lemma le_of_mul_le_mul_right (h : a * c ≤ b * c) (hc : 0 < c) : a ≤ b :=
  Nat.le_of_mul_le_mul_left (by simpa [Nat.mul_comm]) hc

Proof state:
a b c : ℕ
h : a * c ≤ b * c
hc : 0 < c
⊢ c * a ≤ c * b

Tactic:
simpa [Nat.mul_comm]

Result:
no goals
-- Mathlib/RepresentationTheory/Invariants.lean
theorem mem_invariants_iff_comm {X Y : Rep k G} (f : X.V →ₗ[k] Y.V) (g : G) :
    (linHom X.ρ Y.ρ) g f = f ↔ f.comp (X.ρ g) = (Y.ρ g).comp f

Proof state:
k : Type u
inst✝¹ : CommRing k
G : Type u
inst✝ : Group G
X Y : Rep k G
f : ↑X.V →ₗ[k] ↑Y.V
g : G
⊢ ModuleCat.ofHom f ≫ Y.ρ g = ((ρAut X) g).hom ≫ ModuleCat.ofHom f ↔
    ModuleCat.ofHom (X.ρ g) ≫ ModuleCat.ofHom f = ModuleCat.ofHom f ≫ Y.ρ g

Tactic:
exact comm

Result:
no goals

Proof state:
k : Type u
inst✝¹ : CommRing k
G : Type u
inst✝ : Group G
X Y : Rep k G
f : ↑X.V →ₗ[k] ↑Y.V
g : G
⊢ ((X.ρ.linHom Y.ρ) g) f = f ↔ f ∘ₗ X.ρ g = Y.ρ g ∘ₗ f

Tactic:
dsimp

Result:
k : Type u
inst✝¹ : CommRing k
G : Type u
inst✝ : Group G
X Y : Rep k G
f : ↑X.V →ₗ[k] ↑Y.V
g : G
⊢ Y.ρ g ∘ₗ f ∘ₗ X.ρ g⁻¹ = f ↔ f ∘ₗ X.ρ g = Y.ρ g ∘ₗ f

Proof state:
k : Type u
inst✝¹ : CommRing k
G : Type u
inst✝ : Group G
X Y : Rep k G
f : ↑X.V →ₗ[k] ↑Y.V
g : G
⊢ Y.ρ g ∘ₗ f ∘ₗ X.ρ g⁻¹ = f ↔ f ∘ₗ X.ρ g = Y.ρ g ∘ₗ f

Tactic:
rw [← LinearMap.comp_assoc, ← ModuleCat.hom_ofHom (Y.ρ g), ← ModuleCat.hom_ofHom f,
    ← ModuleCat.hom_comp, ← ModuleCat.hom_ofHom (X.ρ g⁻¹), ← ModuleCat.hom_comp,
    Rep.ofHom_ρ, ← ρAut_apply_inv X g, Rep.ofHom_ρ, ← ρAut_apply_hom Y g,
    ← ModuleCat.hom_ext_iff, Iso.inv_comp_eq, ρAut_apply_hom, ← ModuleCat.hom_ofHom (X.ρ g),
    ← ModuleCat.hom_comp, ← ModuleCat.hom_ext_iff]

Result:
k : Type u
inst✝¹ : CommRing k
G : Type u
inst✝ : Group G
X Y : Rep k G
f : ↑X.V →ₗ[k] ↑Y.V
g : G
⊢ ModuleCat.ofHom f ≫ Y.ρ g = ((ρAut X) g).hom ≫ ModuleCat.ofHom f ↔
    ModuleCat.ofHom (X.ρ g) ≫ ModuleCat.ofHom f = ModuleCat.ofHom f ≫ Y.ρ g
-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem mem_range_toPermHom_iff {τ} : τ ∈ (toPermHom g).range ↔
    ∀ c, (τ c).val.support.card = c.val.support.card

Proof state:
case mpr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
τ : Perm { x // x ∈ g.cycleFactorsFinset }
a : g.Basis
⊢ (∀ (c : { x // x ∈ g.cycleFactorsFinset }), (↑(τ c)).support.card = (↑c).support.card) → τ ∈ (toPermHom g).range

Tactic:
exact fun hτ ↦ ⟨toCentralizer a ⟨τ, hτ⟩, toPermHom_apply_toCentralizer a ⟨τ, hτ⟩⟩

Result:
no goals

Proof state:
case mp.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : ↥(centralizer {g})
c : { x // x ∈ g.cycleFactorsFinset }
⊢ (↑(((toPermHom g) k) c)).support.card = (↑c).support.card

Tactic:
rw [coe_toPermHom, Equiv.Perm.support_conj]

Result:
case mp.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : ↥(centralizer {g})
c : { x // x ∈ g.cycleFactorsFinset }
⊢ (Finset.map (Equiv.toEmbedding ↑k) (↑c).support).card = (↑c).support.card

Proof state:
case mp.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : ↥(centralizer {g})
c : { x // x ∈ g.cycleFactorsFinset }
⊢ (Finset.map (Equiv.toEmbedding ↑k) (↑c).support).card = (↑c).support.card

Tactic:
apply Finset.card_map

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
τ : Perm { x // x ∈ g.cycleFactorsFinset }
⊢ τ ∈ (toPermHom g).range → ∀ (c : { x // x ∈ g.cycleFactorsFinset }), (↑(τ c)).support.card = (↑c).support.card

Tactic:
rintro ⟨k, rfl⟩ c

Result:
case mp.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : ↥(centralizer {g})
c : { x // x ∈ g.cycleFactorsFinset }
⊢ (↑(((toPermHom g) k) c)).support.card = (↑c).support.card

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
τ : Perm { x // x ∈ g.cycleFactorsFinset }
⊢ τ ∈ (toPermHom g).range ↔ ∀ (c : { x // x ∈ g.cycleFactorsFinset }), (↑(τ c)).support.card = (↑c).support.card

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
τ : Perm { x // x ∈ g.cycleFactorsFinset }
⊢ τ ∈ (toPermHom g).range → ∀ (c : { x // x ∈ g.cycleFactorsFinset }), (↑(τ c)).support.card = (↑c).support.card

case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
τ : Perm { x // x ∈ g.cycleFactorsFinset }
⊢ (∀ (c : { x // x ∈ g.cycleFactorsFinset }), (↑(τ c)).support.card = (↑c).support.card) → τ ∈ (toPermHom g).range

Proof state:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
τ : Perm { x // x ∈ g.cycleFactorsFinset }
⊢ (∀ (c : { x // x ∈ g.cycleFactorsFinset }), (↑(τ c)).support.card = (↑c).support.card) → τ ∈ (toPermHom g).range

Tactic:
obtain ⟨a⟩ := Basis.nonempty g

Result:
case mpr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
τ : Perm { x // x ∈ g.cycleFactorsFinset }
a : g.Basis
⊢ (∀ (c : { x // x ∈ g.cycleFactorsFinset }), (↑(τ c)).support.card = (↑c).support.card) → τ ∈ (toPermHom g).range
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem coe_ideal_span_singleton_inv_mul {x : R₁} (hx : x ≠ 0) :
    (Ideal.span ({x} : Set R₁) : FractionalIdeal R₁⁰ K)⁻¹ * Ideal.span ({x} : Set R₁) = 1

Proof state:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x : R₁
hx : x ≠ 0
⊢ (↑(Ideal.span {x}))⁻¹ * ↑(Ideal.span {x}) = 1

Tactic:
rw [mul_comm, coe_ideal_span_singleton_mul_inv K hx]

Result:
no goals
-- Mathlib/Analysis/Calculus/BumpFunction/Convolution.lean
theorem normed_convolution_eq_right {x₀ : G} (hg : ∀ x ∈ ball x₀ φ.rOut, g x = g x₀) :
    (φ.normed μ ⋆[lsmul ℝ ℝ, μ] g : G → E') x₀ = g x₀

Proof state:
G : Type uG
E' : Type uE'
inst✝¹⁰ : NormedAddCommGroup E'
g : G → E'
inst✝⁹ : MeasurableSpace G
μ : Measure G
inst✝⁸ : NormedSpace ℝ E'
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace ℝ G
inst✝⁵ : HasContDiffBump G
inst✝⁴ : CompleteSpace E'
φ : ContDiffBump 0
inst✝³ : BorelSpace G
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : FiniteDimensional ℝ G
x₀ : G
hg : ∀ x ∈ ball x₀ φ.rOut, g x = g x₀
⊢ ∫ (t : G), ((lsmul ℝ ℝ) (φ.normed μ t)) (g x₀) ∂μ = g x₀

Tactic:
exact integral_normed_smul φ μ (g x₀)

Result:
no goals

Proof state:
G : Type uG
E' : Type uE'
inst✝¹⁰ : NormedAddCommGroup E'
g : G → E'
inst✝⁹ : MeasurableSpace G
μ : Measure G
inst✝⁸ : NormedSpace ℝ E'
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace ℝ G
inst✝⁵ : HasContDiffBump G
inst✝⁴ : CompleteSpace E'
φ : ContDiffBump 0
inst✝³ : BorelSpace G
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : FiniteDimensional ℝ G
x₀ : G
hg : ∀ x ∈ ball x₀ φ.rOut, g x = g x₀
⊢ (φ.normed μ ⋆[lsmul ℝ ℝ, μ] g) x₀ = g x₀

Tactic:
rw [convolution_eq_right' _ φ.support_normed_eq.subset hg]

Result:
G : Type uG
E' : Type uE'
inst✝¹⁰ : NormedAddCommGroup E'
g : G → E'
inst✝⁹ : MeasurableSpace G
μ : Measure G
inst✝⁸ : NormedSpace ℝ E'
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace ℝ G
inst✝⁵ : HasContDiffBump G
inst✝⁴ : CompleteSpace E'
φ : ContDiffBump 0
inst✝³ : BorelSpace G
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : FiniteDimensional ℝ G
x₀ : G
hg : ∀ x ∈ ball x₀ φ.rOut, g x = g x₀
⊢ ∫ (t : G), ((lsmul ℝ ℝ) (φ.normed μ t)) (g x₀) ∂μ = g x₀
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem getKeyD_eq [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a fallback : α} :
    m.getKeyD a fallback = Raw₀.getKeyD ⟨m, h.size_buckets_pos⟩ a fallback

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α β
h : m.WF
a fallback : α
⊢ m.getKeyD a fallback = Raw₀.getKeyD ⟨m, ⋯⟩ a fallback

Tactic:
simp [Raw.getKeyD, h.size_buckets_pos]

Result:
no goals
-- Mathlib/Order/Basic.lean
theorem PartialOrder.ext_lt {A B : PartialOrder α}
    (H : ∀ x y : α, (haveI := A; x < y) ↔ x < y) : A = B

Proof state:
α : Type u_2
A B : PartialOrder α
H : ∀ (x y : α), x < y ↔ x < y
⊢ A = B

Tactic:
ext x y

Result:
case a.a.le.h.h.a
α : Type u_2
A B : PartialOrder α
H : ∀ (x y : α), x < y ↔ x < y
x y : α
⊢ x ≤ y ↔ x ≤ y

Proof state:
case a.a.le.h.h.a
α : Type u_2
A B : PartialOrder α
H : ∀ (x y : α), x < y ↔ x < y
x y : α
⊢ x ≤ y ↔ x ≤ y

Tactic:
rw [le_iff_lt_or_eq, @le_iff_lt_or_eq _ A, H]

Result:
no goals
-- Mathlib/CategoryTheory/Enriched/Ordinary/Basic.lean
@[simp, reassoc]
lemma eHomWhiskerRight_comp {X X' X'' : C} (f : X ⟶ X') (f' : X' ⟶ X'') (Y : C) :
    eHomWhiskerRight V (f ≫ f') Y = eHomWhiskerRight V f' Y ≫ eHomWhiskerRight V f Y

Proof state:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X X' X'' : C
f : X ⟶ X'
f' : X' ⟶ X''
Y : C
⊢ eHomWhiskerRight V (f ≫ f') Y = eHomWhiskerRight V f' Y ≫ eHomWhiskerRight V f Y

Tactic:
dsimp [eHomWhiskerRight]

Result:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X X' X'' : C
f : X ⟶ X'
f' : X' ⟶ X''
Y : C
⊢ (λ_ (EnrichedCategory.Hom X'' Y)).inv ≫ (eHomEquiv V) (f ≫ f') ▷ EnrichedCategory.Hom X'' Y ≫ eComp V X X'' Y =
    ((λ_ (EnrichedCategory.Hom X'' Y)).inv ≫ (eHomEquiv V) f' ▷ EnrichedCategory.Hom X'' Y ≫ eComp V X' X'' Y) ≫
      (λ_ (EnrichedCategory.Hom X' Y)).inv ≫ (eHomEquiv V) f ▷ EnrichedCategory.Hom X' Y ≫ eComp V X X' Y

Proof state:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X X' X'' : C
f : X ⟶ X'
f' : X' ⟶ X''
Y : C
⊢ (λ_ (EnrichedCategory.Hom X'' Y)).inv ≫ (eHomEquiv V) (f ≫ f') ▷ EnrichedCategory.Hom X'' Y ≫ eComp V X X'' Y =
    ((λ_ (EnrichedCategory.Hom X'' Y)).inv ≫ (eHomEquiv V) f' ▷ EnrichedCategory.Hom X'' Y ≫ eComp V X' X'' Y) ≫
      (λ_ (EnrichedCategory.Hom X' Y)).inv ≫ (eHomEquiv V) f ▷ EnrichedCategory.Hom X' Y ≫ eComp V X X' Y

Tactic:
rw [assoc, assoc, eHomEquiv_comp, comp_whiskerRight_assoc, comp_whiskerRight_assoc, ← e_assoc',
  tensorHom_def', comp_whiskerRight_assoc, id_whiskerLeft, comp_whiskerRight_assoc,
  ← comp_whiskerRight_assoc, Iso.inv_hom_id, id_whiskerRight_assoc,
  comp_whiskerRight_assoc, leftUnitor_inv_whiskerRight_assoc,
  ← associator_inv_naturality_left_assoc, Iso.inv_hom_id_assoc,
  ← whisker_exchange_assoc, id_whiskerLeft_assoc, Iso.inv_hom_id_assoc]

Result:
no goals