harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/WittVector/Truncated.lean
theorem mem_ker_truncate (x : 𝕎 R) :
    x ∈ RingHom.ker (truncate (p := p) n) ↔ ∀ i < n, x.coeff i = 0

Proof state:
p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
⊢ x ∈ RingHom.ker (truncate n) ↔ ∀ i < n, x.coeff i = 0

Tactic:
simp only [RingHom.mem_ker, truncate, truncateFun, RingHom.coe_mk, TruncatedWittVector.ext_iff,
  TruncatedWittVector.coeff_mk, coeff_zero]

Result:
p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
⊢ (∀ (i : Fin n), TruncatedWittVector.coeff i ({ toFun := truncateFun n, map_one' := ⋯, map_mul' := ⋯ } x) = 0) ↔
    ∀ i < n, x.coeff i = 0

Proof state:
p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
⊢ (∀ (i : Fin n), TruncatedWittVector.coeff i ({ toFun := truncateFun n, map_one' := ⋯, map_mul' := ⋯ } x) = 0) ↔
    ∀ i < n, x.coeff i = 0

Tactic:
exact Fin.forall_iff

Result:
no goals
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem mul_sum {S : Type*} [NonUnitalNonAssocSemiring S] (b : S) (s : SkewMonoidAlgebra k G)
    {f : G → k → S} : b * s.sum f = s.sum fun a c ↦ b * f a c

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
S : Type u_3
inst✝ : NonUnitalNonAssocSemiring S
b : S
s : SkewMonoidAlgebra k G
f : G → k → S
⊢ b * s.sum f = s.sum fun a c => b * f a c

Tactic:
simp only [sum, Finsupp.sum, Finset.mul_sum]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem nhdsWithin_inter (a : α) (s t : Set α) : 𝓝[s ∩ t] a = 𝓝[s] a ⊓ 𝓝[t] a

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ 𝓟 s ⊓ (𝓝 a ⊓ 𝓟 t)

Tactic:
rw [inf_left_comm, inf_assoc, inf_principal, ← inf_assoc, inf_idem]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝[s ∩ t] a = 𝓝[s] a ⊓ 𝓝[t] a

Tactic:
delta nhdsWithin

Result:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ 𝓟 s ⊓ (𝓝 a ⊓ 𝓟 t)
-- Mathlib/Data/Multiset/ZeroCons.lean
theorem singleton_inj {a b : α} : ({a} : Multiset α) = {b} ↔ a = b

Proof state:
α : Type u_1
a b : α
⊢ {a} = {b} ↔ a = b

Tactic:
simp_rw [← cons_zero]

Result:
α : Type u_1
a b : α
⊢ a ::ₘ 0 = b ::ₘ 0 ↔ a = b

Proof state:
α : Type u_1
a b : α
⊢ a ::ₘ 0 = b ::ₘ 0 ↔ a = b

Tactic:
exact cons_inj_left _

Result:
no goals
-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem locallyIntegrableOn_univ : LocallyIntegrableOn f univ μ ↔ LocallyIntegrable f μ

Proof state:
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
⊢ LocallyIntegrableOn f univ μ ↔ LocallyIntegrable f μ

Tactic:
simp only [LocallyIntegrableOn, nhdsWithin_univ, mem_univ, true_imp_iff]

Result:
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
⊢ (∀ (x : X), IntegrableAtFilter f (𝓝 x) μ) ↔ LocallyIntegrable f μ

Proof state:
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
⊢ (∀ (x : X), IntegrableAtFilter f (𝓝 x) μ) ↔ LocallyIntegrable f μ

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem mem_dualAnnihilator (φ : Module.Dual R M) : φ ∈ W.dualAnnihilator ↔ ∀ w ∈ W, φ w = 0

Proof state:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
φ : Dual R M
⊢ φ ∈ W.dualAnnihilator ↔ ∀ w ∈ W, φ w = 0

Tactic:
refine LinearMap.mem_ker.trans ?_

Result:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
φ : Dual R M
⊢ W.dualRestrict φ = 0 ↔ ∀ w ∈ W, φ w = 0

Proof state:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
φ : Dual R M
⊢ W.dualRestrict φ = 0 ↔ ∀ w ∈ W, φ w = 0

Tactic:
simp_rw [LinearMap.ext_iff, dualRestrict_apply]

Result:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
φ : Dual R M
⊢ (∀ (x : ↥W), φ ↑x = 0 x) ↔ ∀ w ∈ W, φ w = 0

Proof state:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
φ : Dual R M
⊢ (∀ (x : ↥W), φ ↑x = 0 x) ↔ ∀ w ∈ W, φ w = 0

Tactic:
exact ⟨fun h w hw => h ⟨w, hw⟩, fun h w => h w.1 w.2⟩

Result:
no goals
-- Mathlib/Data/Matrix/Notation.lean
theorem natCast_fin_three (n : ℕ) :
    (n : Matrix (Fin 3) (Fin 3) α) = !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n]

Proof state:
case a
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
i j : Fin 3
⊢ ↑n i j = !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] i j

Tactic:
fin_cases i <;> fin_cases j <;> rfl

Result:
no goals

Proof state:
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n = !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n]

Tactic:
ext i j

Result:
case a
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
i j : Fin 3
⊢ ↑n i j = !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] i j
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
theorem convexBodyLT_mem {x : K} :
    mixedEmbedding K x ∈ (convexBodyLT K f) ↔ ∀ w : InfinitePlace K, w x < f w

Proof state:
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
x : K
⊢ (mixedEmbedding K) x ∈ convexBodyLT K f ↔ ∀ (w : InfinitePlace K), w x < ↑(f w)

Tactic:
simp_rw [mixedEmbedding, RingHom.prod_apply, Set.mem_prod, Set.mem_pi, Set.mem_univ,
  forall_true_left, mem_ball_zero_iff, Pi.ringHom_apply, ← Complex.norm_real,
  embedding_of_isReal_apply, Subtype.forall, ← forall₂_or_left, ← not_isReal_iff_isComplex, em,
  forall_true_left, norm_embedding_eq]

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem isCobounded_top : IsCobounded r ⊤ ↔ Nonempty α

Proof state:
α : Type u_1
r : α → α → Prop
⊢ IsCobounded r ⊤ ↔ Nonempty α

Tactic:
simp +contextual [IsCobounded, eq_univ_iff_forall,
  exists_true_iff_nonempty]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem _root_.Int.addRight_one_isCycle : (Equiv.addRight 1 : Perm ℤ).IsCycle :=
  ⟨0, one_ne_zero, fun n _ => ⟨n, by simp⟩⟩

Proof state:
n : ℤ
x✝ : (Equiv.addRight 1) n ≠ n
⊢ (Equiv.addRight 1 ^ n) 0 = n

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/Topology.lean
lemma closedBall_eq_segment (hε : 0 ≤ ε) : closedBall r ε = segment ℝ (r - ε) (r + ε)

Proof state:
r ε : ℝ
hε : 0 ≤ ε
⊢ closedBall r ε = [r - ε-[ℝ]r + ε]

Tactic:
rw [closedBall_eq_Icc, segment_eq_Icc ((sub_le_self _ hε).trans <| le_add_of_nonneg_right hε)]

Result:
no goals
-- Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean
@[simp]
private lemma mem_triangleIndices :
    x ∈ triangleIndices s ↔ ∃ y, ∃ a ∈ s, (y, y + a, y + 2 * a) = x

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : CommRing α
s : Finset α
x : α × α × α
⊢ x ∈ triangleIndices s ↔ ∃ y, ∃ a ∈ s, (y, y + a, y + 2 * a) = x

Tactic:
simp [triangleIndices]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem restrict_apply (f : α →ₛ β) {s : Set α} (hs : MeasurableSet s) (a) :
    restrict f s a = indicator s f a

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
a : α
⊢ (f.restrict s) a = s.indicator (⇑f) a

Tactic:
simp only [f.coe_restrict hs]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Bool.lean
theorem if_eq_cond {b : Bool} {x y : α} : (if b = true then x else y) = (bif b then x else y)

Proof state:
α : Type u_1
b : Bool
x y : α
⊢ (if b = true then x else y) = bif b then x else y

Tactic:
rw [cond_eq_if]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Nonvanishing.lean
/-- A variant of `DirichletCharacter.norm_LSeries_product_ge_one` in terms of the L-functions. -/
lemma norm_LFunction_product_ge_one {x : ℝ} (hx : 0 < x) (y : ℝ) :
    ‖LFunctionTrivChar N (1 + x) ^ 3 * LFunction χ (1 + x + I * y) ^ 4 *
      LFunction (χ ^ 2) (1 + x + 2 * I * y)‖ ≥ 1

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
⊢ ‖LFunctionTrivChar N (1 + ↑x) ^ 3 * LFunction χ (1 + ↑x + I * ↑y) ^ 4 * LFunction (χ ^ 2) (1 + ↑x + 2 * I * ↑y)‖ ≥ 1

Tactic:
rw [LFunctionTrivChar, DirichletCharacter.LFunction_eq_LSeries 1 h₀,
  χ.LFunction_eq_LSeries h₁, (χ ^ 2).LFunction_eq_LSeries h₂]

Result:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
⊢ ‖LSeries (fun x => 1 ↑x) (1 + ↑x) ^ 3 * LSeries (fun x => χ ↑x) (1 + ↑x + I * ↑y) ^ 4 *
        LSeries (fun x => (χ ^ 2) ↑x) (1 + ↑x + 2 * I * ↑y)‖ ≥
    1

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
⊢ ‖LSeries (fun x => 1 ↑x) (1 + ↑x) ^ 3 * LSeries (fun x => χ ↑x) (1 + ↑x + I * ↑y) ^ 4 *
        LSeries (fun x => (χ ^ 2) ↑x) (1 + ↑x + 2 * I * ↑y)‖ ≥
    1

Tactic:
exact norm_LSeries_product_ge_one χ hx y

Result:
no goals

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
x : ℝ
hx : 0 < x
y : ℝ
⊢ ‖LFunctionTrivChar N (1 + ↑x) ^ 3 * LFunction χ (1 + ↑x + I * ↑y) ^ 4 * LFunction (χ ^ 2) (1 + ↑x + 2 * I * ↑y)‖ ≥ 1

Tactic:
have ⟨h₀, h₁, h₂⟩ := one_lt_re_one_add hx y

Result:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
⊢ ‖LFunctionTrivChar N (1 + ↑x) ^ 3 * LFunction χ (1 + ↑x + I * ↑y) ^ 4 * LFunction (χ ^ 2) (1 + ↑x + 2 * I * ↑y)‖ ≥ 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Monadic.lean
theorem forIn_pure_yield_eq_elim [Monad m] [LawfulMonad m]
    (o : Option α) (f : (a : α) → β → β) (b : β) :
    forIn o b (fun a b => pure (.yield (f a b))) =
      pure (f := m) (o.elim b (fun a => f a b))

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
o : Option α
f : α → β → β
b : β
⊢ (forIn o b fun a b => pure (ForInStep.yield (f a b))) = pure (o.elim b fun a => f a b)

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma inv_smul_le_iff_of_neg (h : a < 0) : a⁻¹ • b₁ ≤ b₂ ↔ a • b₂ ≤ b₁

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedField α
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module α β
a : α
b₁ b₂ : β
inst✝ : PosSMulMono α β
h : a < 0
⊢ a⁻¹ • b₁ ≤ b₂ ↔ a • b₂ ≤ b₁

Tactic:
rw [← smul_le_smul_iff_of_neg_left h, smul_inv_smul₀ h.ne]

Result:
no goals
-- Mathlib/Data/List/DropRight.lean
theorem dropWhile_idempotent : dropWhile p (dropWhile p l) = dropWhile p l

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ dropWhile p (dropWhile p l) = dropWhile p l

Tactic:
simp only [dropWhile_eq_self_iff]

Result:
α : Type u_1
p : α → Bool
l : List α
⊢ ∀ (hl : 0 < (dropWhile p l).length), ¬p ((dropWhile p l).get ⟨0, hl⟩) = true

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ ∀ (hl : 0 < (dropWhile p l).length), ¬p ((dropWhile p l).get ⟨0, hl⟩) = true

Tactic:
exact fun h => dropWhile_get_zero_not p l h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem get?_set_ne (a : Array α) (i : Nat) (h' : i < a.size) {j : Nat} (v : α)
    (h : i ≠ j) : (a.set i v)[j]? = a[j]?

Proof state:
α : Type u_1
a : Array α
i : Nat
h' : i < a.size
j : Nat
v : α
h : i ≠ j
⊢ (a.set i v h')[j]? = a[j]?

Tactic:
by_cases j < a.size <;> simp [getElem?_pos, getElem?_neg, *]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem mem_eraseIdx_iff_getElem {x : α} {l} {k} {h} : x ∈ eraseIdx l k h ↔ ∃ i w, i ≠ k ∧ l[i]'w = x

Proof state:
α : Type u_1
x : α
l : Array α
k : Nat
h : k < l.size
⊢ x ∈ l.eraseIdx k h ↔ ∃ i w, i ≠ k ∧ l[i] = x

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
x : α
k : Nat
l : List α
h : k < { toList := l }.size
⊢ x ∈ { toList := l }.eraseIdx k h ↔ ∃ i w, i ≠ k ∧ { toList := l }[i] = x

Proof state:
case mk
α : Type u_1
x : α
k : Nat
l : List α
h : k < { toList := l }.size
⊢ x ∈ { toList := l }.eraseIdx k h ↔ ∃ i w, i ≠ k ∧ { toList := l }[i] = x

Tactic:
simp [List.mem_eraseIdx_iff_getElem, *]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Basis.lean
theorem linear_combination_coord_eq_self [Fintype ι] (b : AffineBasis ι k V) (v : V) :
    ∑ i, b.coord i v • b i = v

Proof state:
ι : Type u_1
k : Type u_5
V : Type u_6
inst✝³ : AddCommGroup V
inst✝² : Ring k
inst✝¹ : Module k V
inst✝ : Fintype ι
b : AffineBasis ι k V
v : V
⊢ ∑ i : ι, (b.coord i) v • b i = v

Tactic:
have hb := b.affineCombination_coord_eq_self v

Result:
ι : Type u_1
k : Type u_5
V : Type u_6
inst✝³ : AddCommGroup V
inst✝² : Ring k
inst✝¹ : Module k V
inst✝ : Fintype ι
b : AffineBasis ι k V
v : V
hb : ((Finset.affineCombination k Finset.univ ⇑b) fun i => (b.coord i) v) = v
⊢ ∑ i : ι, (b.coord i) v • b i = v

Proof state:
ι : Type u_1
k : Type u_5
V : Type u_6
inst✝³ : AddCommGroup V
inst✝² : Ring k
inst✝¹ : Module k V
inst✝ : Fintype ι
b : AffineBasis ι k V
v : V
hb : ((Finset.affineCombination k Finset.univ ⇑b) fun i => (b.coord i) v) = v
⊢ ∑ i : ι, (b.coord i) v • b i = v

Tactic:
rwa [Finset.univ.affineCombination_eq_linear_combination _ _ (b.sum_coord_apply_eq_one v)] at hb

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc]
lemma homologyOpIso_hom_naturality [S₁.HasHomology] [S₂.HasHomology] :
    homologyMap (opMap φ) ≫ (S₁.homologyOpIso).hom =
      S₂.homologyOpIso.hom ≫ (homologyMap φ).op

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
⊢ homologyMap (opMap φ) ≫ S₁.homologyOpIso.hom = S₂.homologyOpIso.hom ≫ (homologyMap φ).op

Tactic:
simp [homologyMap_op]

Result:
no goals
-- Mathlib/GroupTheory/FixedPointFree.lean
theorem coe_eq_inv_of_sq_eq_one (hφ : FixedPointFree φ) (h2 : φ^[2] = _root_.id) : ⇑φ = (·⁻¹)

Proof state:
case h
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : (⇑φ)^[2] = _root_.id
g : G
⊢ φ g = g⁻¹

Tactic:
have key : g * φ g = 1 := by simpa [List.range_succ] using hφ.prod_pow_eq_one h2 g

Result:
case h
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : (⇑φ)^[2] = _root_.id
g : G
key : g * φ g = 1
⊢ φ g = g⁻¹

Proof state:
case h
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : (⇑φ)^[2] = _root_.id
g : G
key : g * φ g = 1
⊢ φ g = g⁻¹

Tactic:
rwa [← inv_eq_iff_mul_eq_one, eq_comm] at key

Result:
no goals

Proof state:
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : (⇑φ)^[2] = _root_.id
⊢ ⇑φ = fun x => x⁻¹

Tactic:
ext g

Result:
case h
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : (⇑φ)^[2] = _root_.id
g : G
⊢ φ g = g⁻¹

Proof state:
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : (⇑φ)^[2] = _root_.id
g : G
⊢ g * φ g = 1

Tactic:
simpa [List.range_succ] using hφ.prod_pow_eq_one h2 g

Result:
no goals
-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem range_toPermHom_eq_range_toPermHom' :
    (toPermHom g).range = range_toPermHom' g

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ (toPermHom g).range = range_toPermHom' g

Tactic:
ext τ

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
τ : Perm { x // x ∈ g.cycleFactorsFinset }
⊢ τ ∈ (toPermHom g).range ↔ τ ∈ range_toPermHom' g

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
τ : Perm { x // x ∈ g.cycleFactorsFinset }
⊢ τ ∈ (toPermHom g).range ↔ τ ∈ range_toPermHom' g

Tactic:
rw [mem_range_toPermHom_iff, mem_range_toPermHom'_iff]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Basic.lean
lemma map_id (P : MorphismProperty C) [RespectsIso P] :
    P.map (𝟭 _) = P

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
⊢ P.map (𝟭 C) = P

Tactic:
rw [map_id_eq_isoClosure, P.isoClosure_eq_self]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Defs.lean
theorem zero_coeff (n : ℕ) : (0 : 𝕎 R).coeff n = 0 :=
  show (aeval _ (wittZero p n) : R) = 0 by simp only [wittZero_eq_zero, map_zero]

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
⊢ (aeval (Function.uncurry fun i => (![] i).coeff)) (wittZero p n) = 0

Tactic:
simp only [wittZero_eq_zero, map_zero]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
@[simp]
lemma sqrt_nnrpow {a : A} {x : ℝ≥0} : sqrt (a ^ x) = a ^ (x / 2)

Proof state:
A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
⊢ sqrt (a ^ x) = a ^ (x / 2)

Tactic:
simp [sqrt_eq_nnrpow, div_eq_mul_inv]

Result:
no goals
-- Mathlib/Algebra/Lie/Classical.lean
theorem pb_inv [Invertible (2 : R)] : PB l R * Matrix.fromBlocks 1 0 0 (⅟ (PD l R)) = 1

Proof state:
l : Type u_4
R : Type u₂
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ fromBlocks (1 * 1 + 0 * 0) (1 * 0 + 0 * ⅟(PD l R)) (0 * 1 + PD l R * 0) (0 * 0 + 1) = 1

Tactic:
simp only [Matrix.mul_zero, Matrix.mul_one, Matrix.zero_mul, zero_add, add_zero,
  Matrix.fromBlocks_one]

Result:
no goals

Proof state:
l : Type u_4
R : Type u₂
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ PB l R * fromBlocks 1 0 0 ⅟(PD l R) = 1

Tactic:
rw [PB, Matrix.fromBlocks_multiply, mul_invOf_self]

Result:
l : Type u_4
R : Type u₂
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ fromBlocks (1 * 1 + 0 * 0) (1 * 0 + 0 * ⅟(PD l R)) (0 * 1 + PD l R * 0) (0 * 0 + 1) = 1
-- Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
lemma rTensor.inverse_of_rightInverse_comp_rTensor
    {h : P → N} (hgh : Function.RightInverse h g) :
    (rTensor.inverse_of_rightInverse Q hfg hgh).comp (rTensor Q g) =
      Submodule.mkQ (p := LinearMap.range (rTensor Q f))

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
h : P → N
hgh : RightInverse h ⇑g
y : N ⊗[R] Q
⊢ (inverse_of_rightInverse Q hfg hgh ∘ₗ rTensor Q g) y = (range (rTensor Q f)).mkQ y

Tactic:
simp only [coe_comp, Function.comp_apply, Submodule.mkQ_apply,
  rTensor.inverse_of_rightInverse_apply]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
h : P → N
hgh : RightInverse h ⇑g
⊢ inverse_of_rightInverse Q hfg hgh ∘ₗ rTensor Q g = (range (rTensor Q f)).mkQ

Tactic:
rw [LinearMap.ext_iff]

Result:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
h : P → N
hgh : RightInverse h ⇑g
⊢ ∀ (x : N ⊗[R] Q), (inverse_of_rightInverse Q hfg hgh ∘ₗ rTensor Q g) x = (range (rTensor Q f)).mkQ x

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
h : P → N
hgh : RightInverse h ⇑g
⊢ ∀ (x : N ⊗[R] Q), (inverse_of_rightInverse Q hfg hgh ∘ₗ rTensor Q g) x = (range (rTensor Q f)).mkQ x

Tactic:
intro y

Result:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
h : P → N
hgh : RightInverse h ⇑g
y : N ⊗[R] Q
⊢ (inverse_of_rightInverse Q hfg hgh ∘ₗ rTensor Q g) y = (range (rTensor Q f)).mkQ y
-- Mathlib/Algebra/Group/Indicator.lean
theorem mulIndicator_eq_self_of_superset (h1 : s.mulIndicator f = f) (h2 : s ⊆ t) :
    t.mulIndicator f = f

Proof state:
α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f : α → M
h1 : mulSupport f ⊆ s
h2 : s ⊆ t
⊢ mulSupport f ⊆ t

Tactic:
exact Subset.trans h1 h2

Result:
no goals

Proof state:
α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f : α → M
h1 : s.mulIndicator f = f
h2 : s ⊆ t
⊢ t.mulIndicator f = f

Tactic:
rw [mulIndicator_eq_self] at h1 ⊢

Result:
α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f : α → M
h1 : mulSupport f ⊆ s
h2 : s ⊆ t
⊢ mulSupport f ⊆ t
-- Mathlib/Logic/Relation.lean
theorem reflTransGen_iff_eq (h : ∀ b, ¬r a b) : ReflTransGen r a b ↔ b = a

Proof state:
α : Type u_1
r : α → α → Prop
a b : α
h : ∀ (b : α), ¬r a b
⊢ (a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b) ↔ b = a

Tactic:
simp [h, eq_comm]

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
a b : α
h : ∀ (b : α), ¬r a b
⊢ ReflTransGen r a b ↔ b = a

Tactic:
rw [cases_head_iff]

Result:
α : Type u_1
r : α → α → Prop
a b : α
h : ∀ (b : α), ¬r a b
⊢ (a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b) ↔ b = a
-- Mathlib/Algebra/Polynomial/Bivariate.lean
@[simp]
lemma evalEval_smul [Monoid S] [DistribMulAction S R] [IsScalarTower S R R] (x y : R) (s : S)
    (p : R[X][Y]) : (s • p).evalEval x y = s • p.evalEval x y

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : Monoid S
inst✝¹ : DistribMulAction S R
inst✝ : IsScalarTower S R R
x y : R
s : S
p : R[X][Y]
⊢ evalEval x y (s • p) = s • evalEval x y p

Tactic:
simp only [evalEval, eval_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem all_bne [BEq α] {xs : Array α} : (xs.all fun x => a != x) = !xs.contains a

Proof state:
case mk
α : Type u_1
a : α
inst✝ : BEq α
toList✝ : List α
⊢ ({ toList := toList✝ }.all fun x => a != x) = !{ toList := toList✝ }.contains a

Tactic:
simp [List.all_bne]

Result:
no goals

Proof state:
α : Type u_1
a : α
inst✝ : BEq α
xs : Array α
⊢ (xs.all fun x => a != x) = !xs.contains a

Tactic:
cases xs

Result:
case mk
α : Type u_1
a : α
inst✝ : BEq α
toList✝ : List α
⊢ ({ toList := toList✝ }.all fun x => a != x) = !{ toList := toList✝ }.contains a
-- Mathlib/Data/Set/Function.lean
theorem BijOn.sdiff_singleton (h₁ : BijOn f s t) (h₂ : a ∈ s) :
    BijOn f (s \ {a}) (t \ {f a})

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
h₁ : BijOn f s t
h₂ : a ∈ s
⊢ BijOn f (s \ {a}) (t \ {f a})

Tactic:
convert h₁.subset_left diff_subset

Result:
case h.e'_5
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
h₁ : BijOn f s t
h₂ : a ∈ s
⊢ t \ {f a} = f '' (s \ {a})

Proof state:
case h.e'_5
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
h₁ : BijOn f s t
h₂ : a ∈ s
⊢ t \ {f a} = f '' (s \ {a})

Tactic:
simp [h₁.injOn.image_diff, h₁.image_eq, h₂, inter_eq_self_of_subset_right]

Result:
no goals