harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Group/Pi/Lemmas.lean
@[to_additive]
lemma mulSingle_comp_equiv {m n : Type*} [DecidableEq n] [DecidableEq m] [One α] (σ : n ≃ m)
    (i : m) (x : α) : Pi.mulSingle i x ∘ σ = Pi.mulSingle (σ.symm i) x

Proof state:
α : Type u_2
m : Type u_3
n : Type u_4
inst✝² : DecidableEq n
inst✝¹ : DecidableEq m
inst✝ : One α
σ : n ≃ m
i : m
x : α
⊢ mulSingle i x ∘ ⇑σ = mulSingle (σ.symm i) x

Tactic:
ext x

Result:
case h
α : Type u_2
m : Type u_3
n : Type u_4
inst✝² : DecidableEq n
inst✝¹ : DecidableEq m
inst✝ : One α
σ : n ≃ m
i : m
x✝ : α
x : n
⊢ (mulSingle i x✝ ∘ ⇑σ) x = mulSingle (σ.symm i) x✝ x

Proof state:
case h
α : Type u_2
m : Type u_3
n : Type u_4
inst✝² : DecidableEq n
inst✝¹ : DecidableEq m
inst✝ : One α
σ : n ≃ m
i : m
x✝ : α
x : n
⊢ (mulSingle i x✝ ∘ ⇑σ) x = mulSingle (σ.symm i) x✝ x

Tactic:
aesop (add simp Pi.mulSingle_apply)

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem comp_sup_eq_sup_comp_of_nonempty [OrderBot α] [SemilatticeSup β] [OrderBot β]
    {g : α → β} (mono_g : Monotone g) (H : s.Nonempty) : g (s.sup f) = s.sup (g ∘ f)

Proof state:
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝³ : LinearOrder α
s : Finset ι
f : ι → α
inst✝² : OrderBot α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
g : α → β
mono_g : Monotone g
H : s.Nonempty
⊢ g (s.sup' H f) = s.sup' H (g ∘ f)

Tactic:
exact Finset.comp_sup'_eq_sup'_comp H g (fun x y ↦ Monotone.map_sup mono_g x y)

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝³ : LinearOrder α
s : Finset ι
f : ι → α
inst✝² : OrderBot α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
g : α → β
mono_g : Monotone g
H : s.Nonempty
⊢ g (s.sup f) = s.sup (g ∘ f)

Tactic:
rw [← Finset.sup'_eq_sup H, ← Finset.sup'_eq_sup H]

Result:
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝³ : LinearOrder α
s : Finset ι
f : ι → α
inst✝² : OrderBot α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
g : α → β
mono_g : Monotone g
H : s.Nonempty
⊢ g (s.sup' H f) = s.sup' H (g ∘ f)
-- Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean
theorem isUnit_iff_range_eq_top [FiniteDimensional K V] (f : V →ₗ[K] V) :
    IsUnit f ↔ (LinearMap.range f) = ⊤

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V
⊢ IsUnit f ↔ range f = ⊤

Tactic:
rw [isUnit_iff_ker_eq_bot, ker_eq_bot_iff_range_eq_top]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Regular.lean
theorem _root_.Set.exists_isOpen_lt_of_lt [OuterRegular μ] (A : Set α) (r : ℝ≥0∞) (hr : μ A < r) :
    ∃ U, U ⊇ A ∧ IsOpen U ∧ μ U < r

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
A : Set α
r : ℝ≥0∞
hr : μ A < r
⊢ ∃ U ⊇ A, IsOpen U ∧ μ U < r

Tactic:
rcases OuterRegular.outerRegular (measurableSet_toMeasurable μ A) r
    (by rwa [measure_toMeasurable]) with
  ⟨U, hAU, hUo, hU⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
A : Set α
r : ℝ≥0∞
hr : μ A < r
U : Set α
hAU : U ⊇ toMeasurable μ A
hUo : IsOpen U
hU : μ U < r
⊢ ∃ U ⊇ A, IsOpen U ∧ μ U < r

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
A : Set α
r : ℝ≥0∞
hr : μ A < r
⊢ r > ?m.12248 (toMeasurable μ A)

Tactic:
rwa [measure_toMeasurable]

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
A : Set α
r : ℝ≥0∞
hr : μ A < r
U : Set α
hAU : U ⊇ toMeasurable μ A
hUo : IsOpen U
hU : μ U < r
⊢ ∃ U ⊇ A, IsOpen U ∧ μ U < r

Tactic:
exact ⟨U, (subset_toMeasurable _ _).trans hAU, hUo, hU⟩

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem MemLp.norm_rpow {f : α → E} (hf : MemLp f p μ) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞) :
    MemLp (fun x : α => ‖f x‖ ^ p.toReal) 1 μ

Proof state:
case h.e'_7
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
⊢ 1 = p / p

Tactic:
rw [div_eq_mul_inv, ENNReal.mul_inv_cancel hp_ne_zero hp_ne_top]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
⊢ MemLp (fun x => ‖f x‖ ^ p.toReal) 1 μ

Tactic:
convert hf.norm_rpow_div p

Result:
case h.e'_7
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
⊢ 1 = p / p
-- Mathlib/Algebra/Order/Field/Canonical.lean
theorem tsub_div (a b c : α) : (a - b) / c = a / c - b / c

Proof state:
α : Type u_1
inst✝³ : LinearOrderedSemifield α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
⊢ (a - b) / c = a / c - b / c

Tactic:
simp_rw [div_eq_mul_inv, tsub_mul]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Content.lean
theorem content_C {r : R} : (C r).content = normalize r

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
⊢ (C r).support.gcd (C r).coeff = normalize r

Tactic:
by_cases h0 : r = 0

Result:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : r = 0
⊢ (C r).support.gcd (C r).coeff = normalize r

case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
⊢ (C r).support.gcd (C r).coeff = normalize r

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
⊢ (C r).support.gcd (C r).coeff = normalize r

Tactic:
have h : (C r).support = {0} := support_monomial _ h0

Result:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
h : (C r).support = {0}
⊢ (C r).support.gcd (C r).coeff = normalize r

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
⊢ (C r).content = normalize r

Tactic:
rw [content]

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
⊢ (C r).support.gcd (C r).coeff = normalize r

Proof state:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : r = 0
⊢ (C r).support.gcd (C r).coeff = normalize r

Tactic:
simp [h0]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
h : (C r).support = {0}
⊢ (C r).support.gcd (C r).coeff = normalize r

Tactic:
simp [h]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Subalgebra.lean
theorem mulMap_range : (A.mulMap B).range = A ⊔ B

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
⊢ (A.mulMap B).range = A ⊔ B

Tactic:
simp_rw [mulMap, Algebra.TensorProduct.productMap_range, Subalgebra.range_val]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Content.lean
theorem mono (K₁ K₂ : Compacts G) (h : (K₁ : Set G) ⊆ K₂) : μ K₁ ≤ μ K₂

Proof state:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K₁ K₂ : Compacts G
h : ↑K₁ ⊆ ↑K₂
⊢ μ K₁ ≤ μ K₂

Tactic:
simpa using μ.mono' _ _ h

Result:
no goals
-- Mathlib/Topology/CWComplex/Classical/Basic.lean
lemma CWComplex.cellFrontier_subset_finite_closedCell [CWComplex C] (n : ℕ) (i : cell C n) :
    ∃ I : Π m, Finset (cell C m), cellFrontier n i ⊆ ⋃ (m < n) (j ∈ I m), closedCell m j

Proof state:
case intro
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
n : ℕ
i : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : MapsTo (↑(map n i)) (sphere 0 1) (∅ ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1)
⊢ ∃ I, cellFrontier n i ⊆ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j

Tactic:
use I

Result:
case h
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
n : ℕ
i : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : MapsTo (↑(map n i)) (sphere 0 1) (∅ ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1)
⊢ cellFrontier n i ⊆ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j

Proof state:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
n : ℕ
i : cell C n
⊢ ∃ I, cellFrontier n i ⊆ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j

Tactic:
rcases RelCWComplex.mapsTo n i with ⟨I, hI⟩

Result:
case intro
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
n : ℕ
i : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : MapsTo (↑(map n i)) (sphere 0 1) (∅ ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1)
⊢ ∃ I, cellFrontier n i ⊆ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j

Proof state:
case h
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
n : ℕ
i : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : ↑(map n i) '' sphere 0 1 ⊆ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1
⊢ cellFrontier n i ⊆ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j

Tactic:
exact hI

Result:
no goals

Proof state:
case h
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
n : ℕ
i : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : MapsTo (↑(map n i)) (sphere 0 1) (∅ ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1)
⊢ cellFrontier n i ⊆ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j

Tactic:
rw [mapsTo', empty_union] at hI

Result:
case h
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
n : ℕ
i : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : ↑(map n i) '' sphere 0 1 ⊆ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1
⊢ cellFrontier n i ⊆ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j
-- Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean
theorem prod_int_mod (s : Multiset ℤ) (n : ℤ) : s.prod % n = (s.map (· % n)).prod % n

Proof state:
s : Multiset ℤ
n : ℤ
⊢ s.prod % n = (map (fun x => x % n) s).prod % n

Tactic:
induction s using Multiset.induction <;> simp [Int.mul_emod, *]

Result:
no goals
-- Mathlib/LinearAlgebra/Projectivization/Subspace.lean
theorem span_univ : span (Set.univ : Set (ℙ K V)) = ⊤

Proof state:
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ ∀ ⦃x : ℙ K V⦄, x ∈ ⊤ → x ∈ span Set.univ

Tactic:
intro x _hx

Result:
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : ℙ K V
_hx : x ∈ ⊤
⊢ x ∈ span Set.univ

Proof state:
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ span Set.univ = ⊤

Tactic:
rw [eq_top_iff, SetLike.le_def]

Result:
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ ∀ ⦃x : ℙ K V⦄, x ∈ ⊤ → x ∈ span Set.univ

Proof state:
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : ℙ K V
_hx : x ∈ ⊤
⊢ x ∈ span Set.univ

Tactic:
exact subset_span _ (Set.mem_univ x)

Result:
no goals
-- Mathlib/CategoryTheory/Filtered/Final.lean
theorem Functor.initial_of_isCofiltered_pUnit [IsCofiltered C] (F : C ⥤ Discrete PUnit) :
    Initial F

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsCofiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝² : Discrete PUnit.{u_1 + 1}
c : C
x✝¹ x✝ : F.obj c ⟶ x✝²
⊢ ∃ t, F.map t ≫ x✝¹ = F.map t ≫ x✝

Tactic:
use 𝟙 c

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsCofiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝² : Discrete PUnit.{u_1 + 1}
c : C
x✝¹ x✝ : F.obj c ⟶ x✝²
⊢ F.map (𝟙 c) ≫ x✝¹ = F.map (𝟙 c) ≫ x✝

Proof state:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsCofiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝ : Discrete PUnit.{u_1 + 1}
⊢ ∃ c, Nonempty (F.obj c ⟶ x✝)

Tactic:
use Classical.choice IsCofiltered.nonempty

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsCofiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝ : Discrete PUnit.{u_1 + 1}
⊢ Nonempty (F.obj (Classical.choice ⋯) ⟶ x✝)

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsCofiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝² : Discrete PUnit.{u_1 + 1}
c : C
x✝¹ x✝ : F.obj c ⟶ x✝²
⊢ F.map (𝟙 c) ≫ x✝¹ = F.map (𝟙 c) ≫ x✝

Tactic:
apply Subsingleton.elim

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsCofiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
⊢ F.Initial

Tactic:
refine initial_of_exists_of_isCofiltered F (fun _ => ?_) (fun {_} {c} _ _ => ?_)

Result:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsCofiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝ : Discrete PUnit.{u_1 + 1}
⊢ ∃ c, Nonempty (F.obj c ⟶ x✝)

case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsCofiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝² : Discrete PUnit.{u_1 + 1}
c : C
x✝¹ x✝ : F.obj c ⟶ x✝²
⊢ ∃ c' t, F.map t ≫ x✝¹ = F.map t ≫ x✝

Proof state:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsCofiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝² : Discrete PUnit.{u_1 + 1}
c : C
x✝¹ x✝ : F.obj c ⟶ x✝²
⊢ ∃ c' t, F.map t ≫ x✝¹ = F.map t ≫ x✝

Tactic:
use c

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsCofiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝² : Discrete PUnit.{u_1 + 1}
c : C
x✝¹ x✝ : F.obj c ⟶ x✝²
⊢ ∃ t, F.map t ≫ x✝¹ = F.map t ≫ x✝

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsCofiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝ : Discrete PUnit.{u_1 + 1}
⊢ Nonempty (F.obj (Classical.choice ⋯) ⟶ x✝)

Tactic:
exact ⟨Discrete.eqToHom (by simp)⟩

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsCofiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝ : Discrete PUnit.{u_1 + 1}
⊢ (F.obj (Classical.choice ⋯)).as = x✝.as

Tactic:
simp

Result:
no goals
-- Mathlib/Computability/Encoding.lean
theorem sectionΓ'Bool_inclusionBoolΓ' {b} : sectionΓ'Bool (inclusionBoolΓ' b) = b

Proof state:
b : Bool
⊢ sectionΓ'Bool (inclusionBoolΓ' b) = b

Tactic:
cases b <;> rfl

Result:
no goals
-- Mathlib/Algebra/Ring/Rat.lean
lemma divInt_div_divInt_cancel_right {x : ℤ} (hx : x ≠ 0) (n d : ℤ) :
    x /. n / (x /. d) = d /. n

Proof state:
x : ℤ
hx : x ≠ 0
n d : ℤ
⊢ x /. n / (x /. d) = d /. n

Tactic:
rw [div_eq_mul_inv, inv_divInt', mul_comm, divInt_mul_divInt_cancel hx]

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem MulDistribMulAction.toMonoidHomZModOfIsCyclic_apply {M : Type*} [Monoid M] [IsCyclic G]
    [MulDistribMulAction M G] {n : ℕ} (hn : Nat.card G = n) (m : M) (g : G) (k : ℤ)
    (h : toMonoidHomZModOfIsCyclic G M hn m = k) : m • g = g ^ k

Proof state:
G : Type u_2
inst✝³ : Group G
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n : ℕ
hn : Nat.card G = n
m : M
g : G
k : ℤ
h : (toMonoidHomZModOfIsCyclic G M hn) m = ↑k
⊢ ⋯.choose ≡ k [ZMOD ↑(Nat.card G)]

Tactic:
rwa [hn, ← ZMod.intCast_eq_intCast_iff]

Result:
no goals

Proof state:
G : Type u_2
inst✝³ : Group G
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n : ℕ
hn : Nat.card G = n
m : M
g : G
k : ℤ
h : (toMonoidHomZModOfIsCyclic G M hn) m = ↑k
⊢ m • g = g ^ k

Tactic:
rw [← MulDistribMulAction.toMonoidHom_apply,
  (MulDistribMulAction.toMonoidHom G m).map_cyclic.choose_spec g, zpow_eq_zpow_iff_modEq]

Result:
G : Type u_2
inst✝³ : Group G
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n : ℕ
hn : Nat.card G = n
m : M
g : G
k : ℤ
h : (toMonoidHomZModOfIsCyclic G M hn) m = ↑k
⊢ ⋯.choose ≡ k [ZMOD ↑(orderOf g)]

Proof state:
G : Type u_2
inst✝³ : Group G
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n : ℕ
hn : Nat.card G = n
m : M
g : G
k : ℤ
h : (toMonoidHomZModOfIsCyclic G M hn) m = ↑k
⊢ ⋯.choose ≡ k [ZMOD ↑(orderOf g)]

Tactic:
apply Int.ModEq.of_dvd (Int.natCast_dvd_natCast.mpr (orderOf_dvd_natCard g))

Result:
G : Type u_2
inst✝³ : Group G
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n : ℕ
hn : Nat.card G = n
m : M
g : G
k : ℤ
h : (toMonoidHomZModOfIsCyclic G M hn) m = ↑k
⊢ ⋯.choose ≡ k [ZMOD ↑(Nat.card G)]
-- Mathlib/Data/List/Perm/Basic.lean
theorem getElem_cons_eraseIdx_perm {n : ℕ} (h : n < l.length) :
    l[n] :: l.eraseIdx n ~ l

Proof state:
α : Type u_1
l : List α
n : ℕ
h : n < l.length
⊢ l[n] :: l.eraseIdx n ~ l

Tactic:
simpa [h] using (set_perm_cons_eraseIdx h l[n]).symm

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[simp]
lemma inl_descCochain :
    (inl φ).comp (descCochain φ α β h) (by omega) = α

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.117985, u_1} C
inst✝³ : Category.{?u.117989, u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
⊢ -1 + n = m

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
⊢ (inl φ).comp (descCochain φ α β h) ⋯ = α

Tactic:
simp [descCochain]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem Disjoint.inv_left (h : Disjoint f g) : Disjoint f⁻¹ g

Proof state:
α : Type u_1
f g : Perm α
h : f.Disjoint g
⊢ f⁻¹.Disjoint g

Tactic:
intro x

Result:
α : Type u_1
f g : Perm α
h : f.Disjoint g
x : α
⊢ f⁻¹ x = x ∨ g x = x

Proof state:
α : Type u_1
f g : Perm α
h : f.Disjoint g
x : α
⊢ f x = x ∨ g x = x

Tactic:
exact h x

Result:
no goals

Proof state:
α : Type u_1
f g : Perm α
h : f.Disjoint g
x : α
⊢ f⁻¹ x = x ∨ g x = x

Tactic:
rw [inv_eq_iff_eq, eq_comm]

Result:
α : Type u_1
f g : Perm α
h : f.Disjoint g
x : α
⊢ f x = x ∨ g x = x
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem U_neg_two : U R (-2) = -1

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ U R (-2) = -1

Tactic:
simpa [zero_sub, Int.reduceNeg, U_neg_one, mul_zero, U_zero] using U_sub_two R 0

Result:
no goals
-- Mathlib/Algebra/Polynomial/Bivariate.lean
lemma evalEvalRingHom_eq (x : R) : evalEvalRingHom x = eval₂RingHom (evalRingHom x)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
x : R
⊢ evalEvalRingHom x = eval₂RingHom (evalRingHom x)

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Analysis/Convex/Gauge.lean
theorem gauge_zero' : gauge (0 : Set E) = 0

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
⊢ gauge 0 = 0

Tactic:
ext x

Result:
case h
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
x : E
⊢ gauge 0 x = 0 x

Proof state:
case h.inr
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
x : E
hx : x ≠ 0
⊢ sInf {r | r ∈ Ioi 0 ∧ (r = 0 ∨ x = 0)} = 0

Tactic:
convert Real.sInf_empty

Result:
case h.e'_2.h.e'_3
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
x : E
hx : x ≠ 0
⊢ {r | r ∈ Ioi 0 ∧ (r = 0 ∨ x = 0)} = ∅

Proof state:
case h
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
x : E
⊢ gauge 0 x = 0 x

Tactic:
rw [gauge_def']

Result:
case h
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
x : E
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ 0} = 0 x

Proof state:
case h
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
x : E
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ 0} = 0 x

Tactic:
obtain rfl | hx := eq_or_ne x 0

Result:
case h.inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • 0 ∈ 0} = 0 0

case h.inr
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
x : E
hx : x ≠ 0
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ 0} = 0 x

Proof state:
case h.inr
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
x : E
hx : x ≠ 0
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ 0} = 0 x

Tactic:
simp only [mem_zero, Pi.zero_apply, inv_eq_zero, smul_eq_zero]

Result:
case h.inr
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
x : E
hx : x ≠ 0
⊢ sInf {r | r ∈ Ioi 0 ∧ (r = 0 ∨ x = 0)} = 0

Proof state:
case h.e'_2.h.e'_3
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
x : E
hx : x ≠ 0
⊢ {r | r ∈ Ioi 0 ∧ (r = 0 ∨ x = 0)} = ∅

Tactic:
exact eq_empty_iff_forall_not_mem.2 fun r hr => hr.2.elim (ne_of_gt hr.1) hx

Result:
no goals

Proof state:
case h.inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • 0 ∈ 0} = 0 0

Tactic:
simp only [csInf_Ioi, mem_zero, Pi.zero_apply, eq_self_iff_true, sep_true, smul_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Opposites.lean
@[reassoc (attr := simp)]
lemma ι_comp_colimitRightOpIsoUnopLimit_hom (F : Jᵒᵖ ⥤ C) [HasLimit F] (j : J) :
    colimit.ι F.rightOp j ≫ (colimitRightOpIsoUnopLimit F).hom = (limit.π F (op j)).op

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ C
inst✝ : HasLimit F
j : J
⊢ colimit.ι F.rightOp j ≫ (colimitRightOpIsoUnopLimit F).hom = (limit.π F (op j)).op

Tactic:
simp [colimitRightOpIsoUnopLimit]

Result:
no goals
-- Mathlib/Data/Set/Countable.lean
theorem Countable.sUnion_iff {s : Set (Set α)} (hs : s.Countable) :
    (⋃₀ s).Countable ↔ ∀ a ∈ s, a.Countable

Proof state:
α : Type u
s : Set (Set α)
hs : s.Countable
⊢ (⋃₀ s).Countable ↔ ∀ a ∈ s, a.Countable

Tactic:
rw [sUnion_eq_biUnion, hs.biUnion_iff]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem one_lt_ncard (hs : s.Finite

Proof state:
α : Type u_1
s : Set α
hs : autoParam s.Finite _auto✝
⊢ 1 < s.ncard ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b

Tactic:
simp_rw [ncard_eq_toFinset_card _ hs, Finset.one_lt_card, Finite.mem_toFinset]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem isEmpty_mkArray : (mkArray n a).isEmpty = decide (n = 0)

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
⊢ (List.replicate n a).isEmpty = decide (n = 0)

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
⊢ (mkArray n a).isEmpty = decide (n = 0)

Tactic:
rw [← List.toArray_replicate, List.isEmpty_toArray]

Result:
n : Nat
α✝ : Type u_1
a : α✝
⊢ (List.replicate n a).isEmpty = decide (n = 0)
-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem toSimpleFunc_eq_toFun (f : Lp.simpleFunc E p μ) : toSimpleFunc f =ᵐ[μ] f :=
  show ⇑(toSimpleFunc f) =ᵐ[μ] ⇑(f : α →ₘ[μ] E) by
    convert (AEEqFun.coeFn_mk (toSimpleFunc f)
          (toSimpleFunc f).aestronglyMeasurable).symm using 2
    exact (Classical.choose_spec f.2).symm

Proof state:
case h.e'_5.h.e'_6
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
⊢ ↑↑f = AEEqFun.mk ⇑(toSimpleFunc f) ⋯

Tactic:
exact (Classical.choose_spec f.2).symm

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
⊢ ⇑(toSimpleFunc f) =ᶠ[ae μ] ↑↑↑f

Tactic:
convert (AEEqFun.coeFn_mk (toSimpleFunc f)
      (toSimpleFunc f).aestronglyMeasurable).symm using 2

Result:
case h.e'_5.h.e'_6
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
⊢ ↑↑f = AEEqFun.mk ⇑(toSimpleFunc f) ⋯