harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/AddTorsor/Basic.lean
theorem vsub_sub_vsub_comm (p₁ p₂ p₃ p₄ : P) : p₁ -ᵥ p₂ - (p₃ -ᵥ p₄) = p₁ -ᵥ p₃ - (p₂ -ᵥ p₄)

Proof state:
G : Type u_1
P : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
p₁ p₂ p₃ p₄ : P
⊢ p₁ -ᵥ p₂ - (p₃ -ᵥ p₄) = p₁ -ᵥ p₃ - (p₂ -ᵥ p₄)

Tactic:
rw [← vsub_vadd_eq_vsub_sub, vsub_vadd_comm, vsub_vadd_eq_vsub_sub]

Result:
no goals
-- Mathlib/Algebra/Group/Commute/Basic.lean
@[to_additive]
lemma SemiconjBy.function_semiconj_mul_left (h : SemiconjBy a b c) :
    Semiconj (a * ·) (b * ·) (c * ·) := fun j ↦ by simp only [← mul_assoc, h.eq]

Proof state:
G : Type u_1
inst✝ : Semigroup G
a b c : G
h : SemiconjBy a b c
j : G
⊢ (fun x => a * x) ((fun x => b * x) j) = (fun x => c * x) ((fun x => a * x) j)

Tactic:
simp only [← mul_assoc, h.eq]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iSup_range' (g : β → α) (f : ι → β) : ⨆ b : range f, g b = ⨆ i, g (f i)

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : SupSet α
g : β → α
f : ι → β
⊢ sSup (range (g ∘ f)) = sSup (range fun i => g (f i))

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : SupSet α
g : β → α
f : ι → β
⊢ ⨆ b, g ↑b = ⨆ i, g (f i)

Tactic:
rw [iSup, iSup, ← image_eq_range, ← range_comp]

Result:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : SupSet α
g : β → α
f : ι → β
⊢ sSup (range (g ∘ f)) = sSup (range fun i => g (f i))
-- Mathlib/Data/Finset/Powerset.lean
@[simp] lemma mem_powersetCard : s ∈ powersetCard n t ↔ s ⊆ t ∧ card s = n

Proof state:
case mk
α : Type u_1
n : ℕ
t : Finset α
val✝ : Multiset α
nodup✝ : val✝.Nodup
⊢ { val := val✝, nodup := nodup✝ } ∈ powersetCard n t ↔
    { val := val✝, nodup := nodup✝ } ⊆ t ∧ #{ val := val✝, nodup := nodup✝ } = n

Tactic:
simp [powersetCard, val_le_iff.symm]

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
s t : Finset α
⊢ s ∈ powersetCard n t ↔ s ⊆ t ∧ #s = n

Tactic:
cases s

Result:
case mk
α : Type u_1
n : ℕ
t : Finset α
val✝ : Multiset α
nodup✝ : val✝.Nodup
⊢ { val := val✝, nodup := nodup✝ } ∈ powersetCard n t ↔
    { val := val✝, nodup := nodup✝ } ⊆ t ∧ #{ val := val✝, nodup := nodup✝ } = n
-- Mathlib/Data/Set/Insert.lean
lemma ssubset_iff_sdiff_singleton : s ⊂ t ↔ ∃ a ∈ t, s ⊆ t \ {a}

Proof state:
α : Type u
s t : Set α
⊢ (∃ a ∉ s, a ∈ t ∧ s ⊆ t) ↔ ∃ a ∈ t, s ⊆ t ∧ a ∉ s

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u
s t : Set α
⊢ s ⊂ t ↔ ∃ a ∈ t, s ⊆ t \ {a}

Tactic:
simp [ssubset_iff_insert, subset_diff, insert_subset_iff]

Result:
α : Type u
s t : Set α
⊢ (∃ a ∉ s, a ∈ t ∧ s ⊆ t) ↔ ∃ a ∈ t, s ⊆ t ∧ a ∉ s
-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem CauchySeq.prod_map {γ δ} [UniformSpace β] [Preorder γ] [Preorder δ] {u : γ → α}
    {v : δ → β} (hu : CauchySeq u) (hv : CauchySeq v) : CauchySeq (Prod.map u v)

Proof state:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Type u_1
δ : Type u_2
inst✝² : UniformSpace β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
u : γ → α
v : δ → β
hu : CauchySeq u
hv : CauchySeq v
⊢ CauchySeq (Prod.map u v)

Tactic:
simpa only [CauchySeq, prod_map_map_eq', prod_atTop_atTop_eq] using hu.prod hv

Result:
no goals
-- Mathlib/Probability/Process/Stopping.lean
theorem measurableSet_lt_of_countable_range' (hτ : IsStoppingTime f τ)
    (h_countable : (Set.range τ).Countable) (i : ι) :
    MeasurableSet[hτ.measurableSpace] {ω | τ ω < i}

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
⊢ {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i}

Tactic:
ext1 ω

Result:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
ω : Ω
⊢ ω ∈ {ω | τ ω < i} ↔ ω ∈ {ω | τ ω ≤ i} \ {ω | τ ω = i}

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
⊢ MeasurableSet {ω | τ ω < i}

Tactic:
have : {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i} := by
  ext1 ω
  simp only [lt_iff_le_and_ne, Set.mem_setOf_eq, Set.mem_diff]

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i}
⊢ MeasurableSet {ω | τ ω < i}

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i}
⊢ MeasurableSet {ω | τ ω < i}

Tactic:
rw [this]

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i}
⊢ MeasurableSet ({ω | τ ω ≤ i} \ {ω | τ ω = i})

Proof state:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
ω : Ω
⊢ ω ∈ {ω | τ ω < i} ↔ ω ∈ {ω | τ ω ≤ i} \ {ω | τ ω = i}

Tactic:
simp only [lt_iff_le_and_ne, Set.mem_setOf_eq, Set.mem_diff]

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i}
⊢ MeasurableSet ({ω | τ ω ≤ i} \ {ω | τ ω = i})

Tactic:
exact (hτ.measurableSet_le' i).diff (hτ.measurableSet_eq_of_countable_range' h_countable i)

Result:
no goals
-- Mathlib/Data/Nat/Bitwise.lean
theorem land_assoc (n m k : ℕ) : (n &&& m) &&& k = n &&& (m &&& k)

Proof state:
n m k : ℕ
⊢ n &&& m &&& k = n &&& (m &&& k)

Tactic:
bitwise_assoc_tac

Result:
no goals
-- Mathlib/LinearAlgebra/Ray.lean
theorem sameRay_neg_swap : SameRay R (-x) y ↔ SameRay R x (-y)

Proof state:
R : Type u_1
inst✝² : StrictOrderedCommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ SameRay R (-x) y ↔ SameRay R x (-y)

Tactic:
rw [← sameRay_neg_iff, neg_neg]

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem lift_mul_left (z) : g (f.sec z).2 * f.lift hg z = g (f.sec z).1

Proof state:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
z : N
⊢ g ↑(f.sec z).2 * (f.lift hg) z = g (f.sec z).1

Tactic:
rw [mul_comm, lift_mul_right]

Result:
no goals
-- Mathlib/Analysis/Convex/Strong.lean
@[simp] lemma strongConcaveOn_zero : StrongConcaveOn s 0 f ↔ ConcaveOn ℝ s f

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
f : E → ℝ
⊢ StrongConcaveOn s 0 f ↔ ConcaveOn ℝ s f

Tactic:
simp [StrongConcaveOn, ← Pi.zero_def]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem edgeFinset_inf [DecidableEq V] : (G₁ ⊓ G₂).edgeFinset = G₁.edgeFinset ∩ G₂.edgeFinset

Proof state:
V : Type u_1
G₁ G₂ : SimpleGraph V
inst✝² : Fintype ↑G₁.edgeSet
inst✝¹ : Fintype ↑G₂.edgeSet
inst✝ : DecidableEq V
⊢ (G₁ ⊓ G₂).edgeFinset = G₁.edgeFinset ∩ G₂.edgeFinset

Tactic:
simp [edgeFinset]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem isEmpty_alter_eq_isEmpty_erase [LawfulBEq α] (h : m.1.WF) {k : α}
    {f : Option (β k) → Option (β k)} :
    (m.alter k f).1.isEmpty = ((m.erase k).1.isEmpty && (f (m.get? k)).isNone)

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
f : Option (β k) → Option (β k)
⊢ (m.alter k f).val.isEmpty = ((m.erase k).val.isEmpty && (f (m.get? k)).isNone)

Tactic:
simp_to_model [alter, erase] using List.isEmpty_alterKey_eq_isEmpty_eraseKey

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/FixedPoints.lean
theorem set_mem_fixedBy_iff (s : Set α) (g : G) :
    s ∈ fixedBy (Set α) g ↔ ∀ x, g • x ∈ s ↔ x ∈ s

Proof state:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
⊢ s ∈ fixedBy (Set α) g ↔ ∀ (x : α), g • x ∈ s ↔ x ∈ s

Tactic:
simp_rw [mem_fixedBy, ← eq_inv_smul_iff, Set.ext_iff, Set.mem_inv_smul_set_iff, Iff.comm]

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
lemma injOn_pow {n : ℕ} {ζ : M} (hζ : IsPrimitiveRoot ζ n) :
    Set.InjOn (ζ ^ ·) (Finset.range n)

Proof state:
M : Type u_1
inst✝ : CommMonoid M
n : ℕ
ζ : M
hζ : IsPrimitiveRoot ζ n
i : ℕ
hi : i ∈ ↑(range n)
j : ℕ
hj : j ∈ ↑(range n)
e : (fun x => ζ ^ x) i = (fun x => ζ ^ x) j
⊢ i = j

Tactic:
rw [Finset.coe_range, Set.mem_Iio] at hi hj

Result:
M : Type u_1
inst✝ : CommMonoid M
n : ℕ
ζ : M
hζ : IsPrimitiveRoot ζ n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
e : (fun x => ζ ^ x) i = (fun x => ζ ^ x) j
⊢ i = j

Proof state:
M : Type u_1
inst✝ : CommMonoid M
n : ℕ
ζ : M
hζ : IsPrimitiveRoot ζ n
⊢ Set.InjOn (fun x => ζ ^ x) ↑(range n)

Tactic:
intros i hi j hj e

Result:
M : Type u_1
inst✝ : CommMonoid M
n : ℕ
ζ : M
hζ : IsPrimitiveRoot ζ n
i : ℕ
hi : i ∈ ↑(range n)
j : ℕ
hj : j ∈ ↑(range n)
e : (fun x => ζ ^ x) i = (fun x => ζ ^ x) j
⊢ i = j

Proof state:
M : Type u_1
inst✝ : CommMonoid M
n : ℕ
ζ : M
hζ : IsPrimitiveRoot ζ n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
e : (fun x => ζ ^ x) i = (fun x => ζ ^ x) j
⊢ i = j

Tactic:
exact hζ.pow_inj hi hj e

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Prod.lean
@[simp]
lemma ofProd_ι_mk (m₁ : M₁) (m₂ : M₂) :
    ofProd Q₁ Q₂ (ι _ (m₁, m₂)) = ι Q₁ m₁ ᵍ⊗ₜ 1 + 1 ᵍ⊗ₜ ι Q₂ m₂

Proof state:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m₁ : M₁
m₂ : M₂
⊢ (ofProd Q₁ Q₂) ((ι (QuadraticMap.prod Q₁ Q₂)) (m₁, m₂)) = (ι Q₁) m₁ ᵍ⊗ₜ[R] 1 + 1 ᵍ⊗ₜ[R] (ι Q₂) m₂

Tactic:
rw [ofProd, lift_ι_apply]

Result:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m₁ : M₁
m₂ : M₂
⊢ (((GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂)).toLinearMap ∘ₗ
            (evenOdd Q₁ 1).subtype ∘ₗ LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯).coprod
        ((GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂)).toLinearMap ∘ₗ
          (evenOdd Q₂ 1).subtype ∘ₗ LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯))
      (m₁, m₂) =
    (ι Q₁) m₁ ᵍ⊗ₜ[R] 1 + 1 ᵍ⊗ₜ[R] (ι Q₂) m₂

Proof state:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m₁ : M₁
m₂ : M₂
⊢ (((GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂)).toLinearMap ∘ₗ
            (evenOdd Q₁ 1).subtype ∘ₗ LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯).coprod
        ((GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂)).toLinearMap ∘ₗ
          (evenOdd Q₂ 1).subtype ∘ₗ LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯))
      (m₁, m₂) =
    (ι Q₁) m₁ ᵍ⊗ₜ[R] 1 + 1 ᵍ⊗ₜ[R] (ι Q₂) m₂

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Set/NAry.lean
theorem Subsingleton.image2 (hs : s.Subsingleton) (ht : t.Subsingleton) (f : α → β → γ) :
    (image2 f s t).Subsingleton

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
s : Set α
t : Set β
hs : s.Subsingleton
ht : t.Subsingleton
f : α → β → γ
⊢ (Set.image2 f s t).Subsingleton

Tactic:
rw [← image_prod]

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
s : Set α
t : Set β
hs : s.Subsingleton
ht : t.Subsingleton
f : α → β → γ
⊢ ((fun x => f x.1 x.2) '' s ×ˢ t).Subsingleton

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
s : Set α
t : Set β
hs : s.Subsingleton
ht : t.Subsingleton
f : α → β → γ
⊢ ((fun x => f x.1 x.2) '' s ×ˢ t).Subsingleton

Tactic:
apply (hs.prod ht).image

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem flatMap_assoc {α β} (l : List α) (f : α → List β) (g : β → List γ) :
    (l.flatMap f).flatMap g = l.flatMap fun x => (f x).flatMap g

Proof state:
γ : Type u_1
α : Type u_2
β : Type u_3
l : List α
f : α → List β
g : β → List γ
⊢ flatMap g (flatMap f l) = flatMap (fun x => flatMap g (f x)) l

Tactic:
induction l <;> simp [*]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
theorem separatingLeft_iff_det_ne_zero {B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁} (b : Basis ι R₁ M₁) :
    B.SeparatingLeft ↔ (toMatrix₂ b b B).det ≠ 0

Proof state:
R₁ : Type u_2
M₁ : Type u_6
ι : Type u_15
inst✝⁵ : CommRing R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : IsDomain R₁
B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁
b : Basis ι R₁ M₁
⊢ B.SeparatingLeft ↔ ((toMatrix₂ b b) B).det ≠ 0

Tactic:
rw [← Matrix.nondegenerate_iff_det_ne_zero, nondegenerate_toMatrix_iff]

Result:
no goals
-- Mathlib/Algebra/Homology/QuasiIso.lean
lemma quasiIso_of_arrow_mk_iso (φ : K ⟶ L) (φ' : K' ⟶ L') (e : Arrow.mk φ ≅ Arrow.mk φ')
    [∀ i, K.HasHomology i] [∀ i, L.HasHomology i]
    [∀ i, K'.HasHomology i] [∀ i, L'.HasHomology i]
    [hφ : QuasiIso φ] : QuasiIso φ'

Proof state:
ι : Type u_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
c : ComplexShape ι
K L K' L' : HomologicalComplex C c
φ : K ⟶ L
φ' : K' ⟶ L'
e : Arrow.mk φ ≅ Arrow.mk φ'
inst✝³ : ∀ (i : ι), K.HasHomology i
inst✝² : ∀ (i : ι), L.HasHomology i
inst✝¹ : ∀ (i : ι), K'.HasHomology i
inst✝ : ∀ (i : ι), L'.HasHomology i
hφ : QuasiIso φ
⊢ QuasiIso φ'

Tactic:
simpa only [← quasiIso_iff_of_arrow_mk_iso φ φ' e]

Result:
no goals
-- Mathlib/RingTheory/IsTensorProduct.lean
theorem IsBaseChange.equiv_symm_apply (m : M) : h.equiv.symm (f m) = 1 ⊗ₜ m

Proof state:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
m : M
⊢ h.equiv.symm (f m) = 1 ⊗ₜ[R] m

Tactic:
rw [h.equiv.symm_apply_eq, h.equiv_tmul, one_smul]

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem ker_inr : ker (inr R M M₂) = ⊥

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ ker (inr R M M₂) = ⊥

Tactic:
rw [ker, ← prod_bot, prod_comap_inr]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Operations.lean
theorem map_iSup {β ι} (f : α → β) (m : ι → OuterMeasure α) : map f (⨆ i, m i) = ⨆ i, map f (m i) :=
  ext fun s => by simp only [map_apply, iSup_apply]

Proof state:
α : Type u_1
β : Type u_3
ι : Sort u_4
f : α → β
m : ι → OuterMeasure α
s : Set β
⊢ ((map f) (⨆ i, m i)) s = (⨆ i, (map f) (m i)) s

Tactic:
simp only [map_apply, iSup_apply]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean
lemma esymmAlgHom_injective (hn : n ≤ Fintype.card σ) :
    Function.Injective (esymmAlgHom σ R n)

Proof state:
σ : Type u_1
R : Type u_3
n : ℕ
inst✝¹ : Fintype σ
inst✝ : CommRing R
hn : n ≤ Fintype.card σ
⊢ Function.Injective ⇑(esymmAlgHom σ R n)

Tactic:
rw [← rename_esymmAlgHom (Fintype.equivFin σ).symm, AlgHom.coe_comp]

Result:
σ : Type u_1
R : Type u_3
n : ℕ
inst✝¹ : Fintype σ
inst✝ : CommRing R
hn : n ≤ Fintype.card σ
⊢ Function.Injective
    (⇑↑(renameSymmetricSubalgebra (Fintype.equivFin σ).symm) ∘ ⇑(esymmAlgHom (Fin (Fintype.card σ)) R n))

Proof state:
σ : Type u_1
R : Type u_3
n : ℕ
inst✝¹ : Fintype σ
inst✝ : CommRing R
hn : n ≤ Fintype.card σ
⊢ Function.Injective
    (⇑↑(renameSymmetricSubalgebra (Fintype.equivFin σ).symm) ∘ ⇑(esymmAlgHom (Fin (Fintype.card σ)) R n))

Tactic:
exact (AlgEquiv.injective _).comp (esymmAlgHom_fin_injective R hn)

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem sum_smul_const_vsub_eq_vsub_affineCombination (w : ι → k) (p₂ : ι → P) (p₁ : P)
    (h : ∑ i ∈ s, w i = 1) : (∑ i ∈ s, w i • (p₁ -ᵥ p₂ i)) = p₁ -ᵥ s.affineCombination k p₂ w

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p₂ : ι → P
p₁ : P
h : ∑ i ∈ s, w i = 1
⊢ ∑ i ∈ s, w i • (p₁ -ᵥ p₂ i) = p₁ -ᵥ (affineCombination k s p₂) w

Tactic:
rw [sum_smul_vsub_eq_affineCombination_vsub, affineCombination_apply_const _ _ _ h]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem ext {f₁ f₂ : M →ₛₗ[σ] M₁} (h : ∀ i, f₁ (b i) = f₂ (b i)) : f₁ = f₂

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
b : Basis ι R M
R₁ : Type u_10
inst✝² : Semiring R₁
σ : R →+* R₁
M₁ : Type u_11
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f₁ f₂ : M →ₛₗ[σ] M₁
h : ∀ (i : ι), f₁ (b i) = f₂ (b i)
⊢ f₁ = f₂

Tactic:
ext x

Result:
case h
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
b : Basis ι R M
R₁ : Type u_10
inst✝² : Semiring R₁
σ : R →+* R₁
M₁ : Type u_11
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f₁ f₂ : M →ₛₗ[σ] M₁
h : ∀ (i : ι), f₁ (b i) = f₂ (b i)
x : M
⊢ f₁ x = f₂ x

Proof state:
case h
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
b : Basis ι R M
R₁ : Type u_10
inst✝² : Semiring R₁
σ : R →+* R₁
M₁ : Type u_11
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f₁ f₂ : M →ₛₗ[σ] M₁
h : ∀ (i : ι), f₁ (b i) = f₂ (b i)
x : M
⊢ f₁ (∑ a ∈ (b.repr x).support, (b.repr x) a • b a) = f₂ (∑ a ∈ (b.repr x).support, (b.repr x) a • b a)

Tactic:
simp only [map_sum, LinearMap.map_smulₛₗ, h]

Result:
no goals

Proof state:
case h
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
b : Basis ι R M
R₁ : Type u_10
inst✝² : Semiring R₁
σ : R →+* R₁
M₁ : Type u_11
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f₁ f₂ : M →ₛₗ[σ] M₁
h : ∀ (i : ι), f₁ (b i) = f₂ (b i)
x : M
⊢ f₁ x = f₂ x

Tactic:
rw [← b.linearCombination_repr x, Finsupp.linearCombination_apply, Finsupp.sum]

Result:
case h
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
b : Basis ι R M
R₁ : Type u_10
inst✝² : Semiring R₁
σ : R →+* R₁
M₁ : Type u_11
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f₁ f₂ : M →ₛₗ[σ] M₁
h : ∀ (i : ι), f₁ (b i) = f₂ (b i)
x : M
⊢ f₁ (∑ a ∈ (b.repr x).support, (b.repr x) a • b a) = f₂ (∑ a ∈ (b.repr x).support, (b.repr x) a • b a)
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem mk_cancel_common_right (s s' : S) (m : M) : mk (s' • m) (s * s') = mk m s :=
  mk_eq.mpr ⟨1, by simp [mul_smul]⟩

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s s' : ↥S
m : M
⊢ 1 • s • s' • m = 1 • (s * s') • m

Tactic:
simp [mul_smul]

Result:
no goals
-- Mathlib/Algebra/Star/Conjneg.lean
@[simp] lemma conjneg_conjneg (f : G → R) : conjneg (conjneg f) = f

Proof state:
case h
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
f : G → R
x✝ : G
⊢ conjneg (conjneg f) x✝ = f x✝

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
f : G → R
⊢ conjneg (conjneg f) = f

Tactic:
ext

Result:
case h
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
f : G → R
x✝ : G
⊢ conjneg (conjneg f) x✝ = f x✝
-- Mathlib/Topology/MetricSpace/Defs.lean
theorem dist_ne_zero {x y : γ} : dist x y ≠ 0 ↔ x ≠ y

Proof state:
γ : Type w
inst✝ : MetricSpace γ
x y : γ
⊢ dist x y ≠ 0 ↔ x ≠ y

Tactic:
simpa only [not_iff_not] using dist_eq_zero

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem Monic.add_of_right (hq : Monic q) (hpq : degree p < degree q) : Monic (p + q)

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
hpq : p.degree < q.degree
⊢ (p + q).Monic

Tactic:
rwa [Monic, leadingCoeff_add_of_degree_lt hpq]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem limit.isoLimitCone_hom_π {F : J ⥤ C} [HasLimit F] (t : LimitCone F) (j : J) :
    (limit.isoLimitCone t).hom ≫ t.cone.π.app j = limit.π F j

Proof state:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimit F
t : LimitCone F
j : J
⊢ (isoLimitCone t).hom ≫ t.cone.π.app j = π F j

Tactic:
dsimp [limit.isoLimitCone, IsLimit.conePointUniqueUpToIso]

Result:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimit F
t : LimitCone F
j : J
⊢ t.isLimit.lift (cone F) ≫ t.cone.π.app j = π F j

Proof state:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimit F
t : LimitCone F
j : J
⊢ t.isLimit.lift (cone F) ≫ t.cone.π.app j = π F j

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem pmap_pmap {p : α → Prop} {q : β → Prop} (g : ∀ a, p a → β) (f : ∀ b, q b → γ) (l H₁ H₂) :
    pmap f (pmap g l H₁) H₂ =
      pmap (α := { x // x ∈ l }) (fun a h => f (g a h) (H₂ (g a h) (mem_pmap_of_mem a.2))) l.attach
        (fun a _ => H₁ a a.2)

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
q : β → Prop
g : (a : α) → p a → β
f : (b : β) → q b → γ
toList✝ : List α
H₁ : ∀ (a : α), a ∈ { toList := toList✝ } → p a
H₂ : ∀ (a : β), a ∈ pmap g { toList := toList✝ } H₁ → q a
⊢ pmap f (pmap g { toList := toList✝ } H₁) H₂ = pmap (fun a h => f (g a.val h) ⋯) { toList := toList✝ }.attach ⋯

Tactic:
simp [List.pmap_pmap, List.pmap_map]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
q : β → Prop
g : (a : α) → p a → β
f : (b : β) → q b → γ
l : Array α
H₁ : ∀ (a : α), a ∈ l → p a
H₂ : ∀ (a : β), a ∈ pmap g l H₁ → q a
⊢ pmap f (pmap g l H₁) H₂ = pmap (fun a h => f (g a.val h) ⋯) l.attach ⋯

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
q : β → Prop
g : (a : α) → p a → β
f : (b : β) → q b → γ
toList✝ : List α
H₁ : ∀ (a : α), a ∈ { toList := toList✝ } → p a
H₂ : ∀ (a : β), a ∈ pmap g { toList := toList✝ } H₁ → q a
⊢ pmap f (pmap g { toList := toList✝ } H₁) H₂ = pmap (fun a h => f (g a.val h) ⋯) { toList := toList✝ }.attach ⋯
-- Mathlib/Algebra/Lie/TraceForm.lean
/-- A nilpotent Lie algebra with a representation whose trace form is non-singular is Abelian. -/
lemma isLieAbelian_of_ker_traceForm_eq_bot [Module.Free R M] [Module.Finite R M]
    (h : LinearMap.ker (traceForm R L M) = ⊥) : IsLieAbelian L

Proof state:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
h : LinearMap.ker (traceForm R L M) = ⊥
⊢ IsLieAbelian L

Tactic:
simpa only [← disjoint_lowerCentralSeries_maxTrivSubmodule_iff R L L, disjoint_iff_inf_le,
  LieIdeal.toLieSubalgebra_toSubmodule, LieSubmodule.toSubmodule_eq_bot, h]
  using lowerCentralSeries_one_inf_center_le_ker_traceForm R L M

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
theorem exists_pow_lt_of_lt_one {a b : ℝ≥0} (ha : 0 < a) (hb : b < 1) :
    ∃ n : ℕ, b ^ n < a

Proof state:
a b : ℝ≥0
ha : 0 < a
hb : b < 1
⊢ ∃ n, b ^ n < a

Tactic:
simpa only [← coe_pow, NNReal.coe_lt_coe] using
  exists_pow_lt_of_lt_one (NNReal.coe_pos.2 ha) (NNReal.coe_lt_coe.2 hb)

Result:
no goals