harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueD_eraseKey {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
    {k a : α} {fallback : β} (hl : DistinctKeys l) : getValueD a (eraseKey k l) fallback =
      if k == a then fallback else getValueD a l fallback

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
fallback : β
hl : DistinctKeys l
⊢ getValueD a (eraseKey k l) fallback = if (k == a) = true then fallback else getValueD a l fallback

Tactic:
simp [getValueD_eq_getValue?, getValue?_eraseKey hl, apply_ite (fun x => Option.getD x fallback)]

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
theorem geom_sum_two {x : α} : ∑ i ∈ range 2, x ^ i = x + 1

Proof state:
α : Type u
inst✝ : Semiring α
x : α
⊢ ∑ i ∈ range 2, x ^ i = x + 1

Tactic:
simp [geom_sum_succ']

Result:
no goals
-- Mathlib/LinearAlgebra/TensorAlgebra/Grading.lean
theorem GradedAlgebra.ι_apply (m : M) :
    GradedAlgebra.ι R M m =
      DirectSum.of (fun (i : ℕ) => ↥(LinearMap.range (TensorAlgebra.ι R : M →ₗ[_] _) ^ i)) 1
        ⟨TensorAlgebra.ι R m, by simpa only [pow_one] using LinearMap.mem_range_self _ m⟩ :=
  rfl

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ (TensorAlgebra.ι R) m ∈ LinearMap.range (TensorAlgebra.ι R) ^ 1

Tactic:
simpa only [pow_one] using LinearMap.mem_range_self _ m

Result:
no goals
-- Mathlib/Data/List/Infix.lean
theorem tails_cons (a : α) (l : List α) : tails (a :: l) = (a :: l) :: l.tails

Proof state:
α : Type u_1
a : α
l : List α
⊢ (a :: l).tails = (a :: l) :: l.tails

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Function.lean
lemma bijOn_swap (ha : a ∈ s) (hb : b ∈ s) : BijOn (swap a b) s s :=
  (swap a b).bijOn fun x ↦ by
    obtain rfl | hxa := eq_or_ne x a <;>
    obtain rfl | hxb := eq_or_ne x b <;>
    simp [*, swap_apply_of_ne_of_ne]

Proof state:
α : Type u_1
s : Set α
inst✝ : DecidableEq α
a b : α
ha : a ∈ s
hb : b ∈ s
x : α
⊢ (swap a b) x ∈ s ↔ x ∈ s

Tactic:
obtain rfl | hxa := eq_or_ne x a <;>
obtain rfl | hxb := eq_or_ne x b <;>
simp [*, swap_apply_of_ne_of_ne]

Result:
no goals
-- Mathlib/Algebra/CharP/Lemmas.lean
lemma iterateFrobenius_add_apply :
    iterateFrobenius R p (m + n) x = iterateFrobenius R p m (iterateFrobenius R p n x)

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
p m n : ℕ
inst✝ : ExpChar R p
x : R
⊢ (iterateFrobenius R p (m + n)) x = (iterateFrobenius R p m) ((iterateFrobenius R p n) x)

Tactic:
simp_rw [iterateFrobenius_def, add_comm m n, pow_add, pow_mul]

Result:
no goals
-- Mathlib/GroupTheory/Perm/List.lean
theorem mem_of_formPerm_apply_ne (h : l.formPerm x ≠ x) : x ∈ l

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : l.formPerm x ≠ x
⊢ x ∈ l

Tactic:
simpa [or_iff_left_of_imp mem_of_mem_tail] using mem_or_mem_of_zipWith_swap_prod_ne h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem pow_two (a : Nat) : a ^ 2 = a * a

Proof state:
a : Nat
⊢ a ^ 2 = a * a

Tactic:
rw [Nat.pow_succ, Nat.pow_one]

Result:
no goals
-- Mathlib/MeasureTheory/Covering/DensityTheorem.lean
theorem ae_tendsto_average [NormedSpace ℝ E] [CompleteSpace E]
    {f : α → E} (hf : LocallyIntegrable f μ) (K : ℝ) : ∀ᵐ x ∂μ,
      ∀ {ι : Type*} {l : Filter ι} (w : ι → α) (δ : ι → ℝ) (_ : Tendsto δ l (𝓝[>] 0))
        (_ : ∀ᶠ j in l, x ∈ closedBall (w j) (K * δ j)),
        Tendsto (fun j => ⨍ y in closedBall (w j) (δ j), f y ∂μ) l (𝓝 (f x))

Proof state:
α : Type u_1
inst✝⁸ : PseudoMetricSpace α
inst✝⁷ : MeasurableSpace α
μ : Measure α
inst✝⁶ : IsUnifLocDoublingMeasure μ
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : BorelSpace α
inst✝³ : IsLocallyFiniteMeasure μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf : LocallyIntegrable f μ
K : ℝ
⊢ ∀ᵐ (x : α) ∂μ,
    ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
      Tendsto δ l (𝓝[>] 0) →
        (∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)) →
          Tendsto (fun j => ⨍ (y : α) in closedBall (w j) (δ j), f y ∂μ) l (𝓝 (f x))

Tactic:
filter_upwards [(vitaliFamily μ K).ae_tendsto_average hf] with x hx ι l w δ δlim xmem using
  hx.comp (tendsto_closedBall_filterAt μ _ _ δlim xmem)

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/TruncGE.lean
@[simp]
lemma truncGEMap_id : truncGEMap (𝟙 K) e = 𝟙 _

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{u_4, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
⊢ truncGEMap (𝟙 K) e = 𝟙 (K.truncGE e)

Tactic:
simp [truncGEMap, truncGE]

Result:
no goals
-- Mathlib/Algebra/Star/CHSH.lean
theorem CHSH_id [CommRing R] {A₀ A₁ B₀ B₁ : R} (A₀_inv : A₀ ^ 2 = 1) (A₁_inv : A₁ ^ 2 = 1)
    (B₀_inv : B₀ ^ 2 = 1) (B₁_inv : B₁ ^ 2 = 1) :
    (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) =
      4 * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁)

Proof state:
R : Type u
inst✝ : CommRing R
A₀ A₁ B₀ B₁ : R
A₀_inv : A₀ ^ 2 = 1
A₁_inv : A₁ ^ 2 = 1
B₀_inv : B₀ ^ 2 = 1
B₁_inv : B₁ ^ 2 = 1
⊢ (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) =
    4 * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁)

Tactic:
linear_combination
  (2 * B₀ * B₁ + 2) * A₀_inv + (B₀ ^ 2 - 2 * B₀ * B₁ + B₁ ^ 2) * A₁_inv +
      (A₀ ^ 2 + 2 * A₀ * A₁ + 1) * B₀_inv +
    (A₀ ^ 2 - 2 * A₀ * A₁ + 1) * B₁_inv

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem omega0_le_preOmega_iff {x : Ordinal} : ω ≤ preOmega x ↔ ω ≤ x

Proof state:
x : Ordinal.{u_1}
⊢ ω ≤ preOmega x ↔ ω ≤ x

Tactic:
conv_lhs => rw [← preOmega_omega0, preOmega_le_preOmega]

Result:
no goals
-- Mathlib/NumberTheory/JacobiSum/Basic.lean
private
lemma MulChar.exists_apply_sub_one_eq_mul_sub_one {n : ℕ} [NeZero n] {χ : MulChar F R} {μ : R}
    (hχ : χ ^ n = 1) (hμ : IsPrimitiveRoot μ n) {x : F} (hx : x ≠ 0) :
    ∃ z ∈ Algebra.adjoin ℤ {μ}, χ x - 1 = z * (μ - 1)

Proof state:
F : Type u_1
R : Type u_2
inst✝⁴ : Fintype F
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
χ : MulChar F R
μ : R
hχ : χ ^ n = 1
hμ : IsPrimitiveRoot μ n
x : F
hx : x ≠ 0
⊢ ∃ z ∈ adjoin ℤ {μ}, χ x - 1 = z * (μ - 1)

Tactic:
obtain ⟨k, _, hk⟩ := exists_apply_eq_pow hχ hμ hx

Result:
case intro.intro
F : Type u_1
R : Type u_2
inst✝⁴ : Fintype F
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
χ : MulChar F R
μ : R
hχ : χ ^ n = 1
hμ : IsPrimitiveRoot μ n
x : F
hx : x ≠ 0
k : ℕ
left✝ : k < n
hk : χ x = μ ^ k
⊢ ∃ z ∈ adjoin ℤ {μ}, χ x - 1 = z * (μ - 1)

Proof state:
case intro.intro
F : Type u_1
R : Type u_2
inst✝⁴ : Fintype F
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
χ : MulChar F R
μ : R
hχ : χ ^ n = 1
hμ : IsPrimitiveRoot μ n
x : F
hx : x ≠ 0
k : ℕ
left✝ : k < n
hk : χ x = μ ^ k
⊢ ∑ x ∈ range k, μ ^ x ∈ adjoin ℤ {μ}

Tactic:
exact Subalgebra.sum_mem _ fun m _ ↦ Subalgebra.pow_mem _ (self_mem_adjoin_singleton _ μ) _

Result:
no goals
-- Mathlib/Combinatorics/Additive/ETransform.lean
theorem mulETransformLeft_one : mulETransformLeft 1 x = x

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
x : Finset α × Finset α
⊢ mulETransformLeft 1 x = x

Tactic:
simp [mulETransformLeft]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast_filter_of_pos {p : α → Bool} {l : List α} (w : l ≠ []) (h : p (getLast l w) = true) :
    getLast (filter p l) (ne_nil_of_mem (mem_filter.2 ⟨getLast_mem w, h⟩)) = getLast l w

Proof state:
case h
α : Type u_1
p : α → Bool
l : List α
w : l ≠ []
h : p (l.getLast w) = true
⊢ p (l.reverse.head ⋯) = true

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : List α
w : l ≠ []
h : p (l.getLast w) = true
⊢ (filter p l).getLast ⋯ = l.getLast w

Tactic:
simp only [getLast_eq_head_reverse, ← filter_reverse]

Result:
α : Type u_1
p : α → Bool
l : List α
w : l ≠ []
h : p (l.getLast w) = true
⊢ (filter p l.reverse).head ⋯ = l.reverse.head ⋯

Proof state:
α : Type u_1
p : α → Bool
l : List α
w : l ≠ []
h : p (l.getLast w) = true
⊢ (filter p l.reverse).head ⋯ = l.reverse.head ⋯

Tactic:
rw [head_filter_of_pos]

Result:
case h
α : Type u_1
p : α → Bool
l : List α
w : l ≠ []
h : p (l.getLast w) = true
⊢ p (l.reverse.head ⋯) = true
-- Mathlib/GroupTheory/CoprodI.lean
theorem iSup_mrange_of : ⨆ i, MonoidHom.mrange (of : M i →* CoprodI M) = ⊤

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
⊢ ⨆ i, MonoidHom.mrange of = ⊤

Tactic:
simp [← mrange_eq_iSup]

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem comap_prod (f : α → β × γ) (b : Filter β) (c : Filter γ) :
    comap f (b ×ˢ c) = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
b : Filter β
c : Filter γ
⊢ comap f (b ×ˢ c) = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c

Tactic:
rw [prod_eq_inf, comap_inf, Filter.comap_comap, Filter.comap_comap]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_eq_get!_get? [LawfulBEq α] (h : m.1.WF) {a : α} [Inhabited (β a)] :
    m.get! a = (m.get? a).get!

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.val.WF
a : α
inst✝ : Inhabited (β a)
⊢ m.get! a = (m.get? a).get!

Tactic:
simp_to_model using List.getValueCast!_eq_getValueCast?

Result:
no goals
-- Mathlib/Algebra/Category/Ring/Basic.lean
lemma hom_inv_apply {R S : SemiRingCat} (e : R ≅ S) (s : S) : e.hom (e.inv s) = s

Proof state:
R S : SemiRingCat
e : R ≅ S
s : ↑S
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Card.lean
theorem empty_mem_generateMeasurableRec (s : Set (Set α)) (i : Ordinal) :
    ∅ ∈ generateMeasurableRec s i

Proof state:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
⊢ ∅ ∈
    let S := ⋃ j, ⋃ (_ : j < i), generateMeasurableRec s j;
    s ∪ {∅} ∪ compl '' S ∪ range fun f => ⋃ n, ↑(f n)

Tactic:
exact mem_union_left _ (mem_union_left _ (mem_union_right _ (mem_singleton ∅)))

Result:
no goals

Proof state:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
⊢ ∅ ∈ generateMeasurableRec s i

Tactic:
unfold generateMeasurableRec

Result:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
⊢ ∅ ∈
    let S := ⋃ j, ⋃ (_ : j < i), generateMeasurableRec s j;
    s ∪ {∅} ∪ compl '' S ∪ range fun f => ⋃ n, ↑(f n)
-- Mathlib/Analysis/Convex/Function.lean
theorem ConvexOn.lt_right_of_left_lt (hf : ConvexOn 𝕜 s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s)
    (hz : z ∈ openSegment 𝕜 x y) (hxz : f x < f z) : f z < f y

Proof state:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxz : f x < f (a • x + b • y)
⊢ f (a • x + b • y) < f y

Tactic:
exact hf.lt_right_of_left_lt' hx hy ha hb hab hxz

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y z : E
hx : x ∈ s
hy : y ∈ s
hz : z ∈ openSegment 𝕜 x y
hxz : f x < f z
⊢ f z < f y

Tactic:
obtain ⟨a, b, ha, hb, hab, rfl⟩ := hz

Result:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxz : f x < f (a • x + b • y)
⊢ f (a • x + b • y) < f y
-- Mathlib/SetTheory/Cardinal/ToNat.lean
theorem toNat_eq_iff {n : ℕ} (hn : n ≠ 0) : toNat c = n ↔ c = n

Proof state:
c : Cardinal.{u}
n : ℕ
hn : n ≠ 0
⊢ toNat c = n ↔ c = ↑n

Tactic:
rw [← toNat_toENat, ENat.toNat_eq_iff hn, toENat_eq_nat]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem head?_enum (l : List α) :
    l.enum.head? = l.head?.map fun a => (0, a)

Proof state:
α : Type u_1
l : List α
⊢ l.enum.head? = Option.map (fun a => (0, a)) l.head?

Tactic:
simp [head?_eq_getElem?]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma le_div_two_iff_mul_two_le {n m : ℕ} : m ≤ n / 2 ↔ (m : ℤ) * 2 ≤ n

Proof state:
n m : ℕ
⊢ m ≤ n / 2 ↔ ↑m * 2 ≤ ↑n

Tactic:
rw [Nat.le_div_iff_mul_le Nat.zero_lt_two, ← Int.ofNat_le, Int.ofNat_mul, Int.ofNat_two]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List (α × β)} {k : α}
    (contains_eq_false : (l.map Prod.fst).contains k = false) :
    (insertMany m l).getKey? k = m.getKey? k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List (α × β)
k : α
contains_eq_false : (List.map Prod.fst l).contains k = false
⊢ (insertMany m l).getKey? k = m.getKey? k

Tactic:
simp_to_raw using Raw₀.Const.getKey?_insertMany_list_of_contains_eq_false

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem equivMapDomain_zero {f : α ≃ β} : equivMapDomain f (0 : α →₀ M) = (0 : β →₀ M)

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ≃ β
⊢ equivMapDomain f 0 = 0

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ≃ β
a✝ : β
⊢ (equivMapDomain f 0) a✝ = 0 a✝

Proof state:
case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ≃ β
a✝ : β
⊢ (equivMapDomain f 0) a✝ = 0 a✝

Tactic:
simp only [equivMapDomain_apply, coe_zero, Pi.zero_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem Decidable.and_iff_not_or_not [Decidable a] [Decidable b] : a ∧ b ↔ ¬(¬a ∨ ¬b)

Proof state:
a b : Prop
inst✝¹ : Decidable a
inst✝ : Decidable b
⊢ a ∧ b ↔ ¬(¬a ∨ ¬b)

Tactic:
rw [← not_and_iff_or_not_not, not_not]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem norm_le_of_nonempty [Nonempty α] {f : α →ᵇ β} {M : ℝ} : ‖f‖ ≤ M ↔ ∀ x, ‖f x‖ ≤ M

Proof state:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Nonempty α
f : α →ᵇ β
M : ℝ
⊢ ‖f‖ ≤ M ↔ ∀ (x : α), ‖f x‖ ≤ M

Tactic:
simp_rw [norm_def, ← dist_zero_right]

Result:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Nonempty α
f : α →ᵇ β
M : ℝ
⊢ dist f 0 ≤ M ↔ ∀ (x : α), dist (f x) 0 ≤ M

Proof state:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Nonempty α
f : α →ᵇ β
M : ℝ
⊢ dist f 0 ≤ M ↔ ∀ (x : α), dist (f x) 0 ≤ M

Tactic:
exact dist_le_iff_of_nonempty

Result:
no goals
-- Mathlib/CategoryTheory/NatIso.lean
theorem ofComponents.app (app' : ∀ X : C, F.obj X ≅ G.obj X) (naturality) (X) :
    (ofComponents app' naturality).app X = app' X

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
app' : (X : C) → F.obj X ≅ G.obj X
naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app' Y).hom = (app' X).hom ≫ G.map f
X : C
⊢ (ofComponents app' naturality).app X = app' X

Tactic:
aesop

Result:
no goals
-- Mathlib/Data/Finset/BooleanAlgebra.lean
theorem compl_filter (p : α → Prop) [DecidablePred p] [∀ x, Decidable ¬p x] :
    (univ.filter p)ᶜ = univ.filter fun x => ¬p x :=
  ext <| by simp

Proof state:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : α) → Decidable ¬p x
⊢ ∀ (a : α), a ∈ (filter p univ)ᶜ ↔ a ∈ filter (fun x => ¬p x) univ

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
lemma not_mem_uIoc : a ∉ Ι b c ↔ a ≤ b ∧ a ≤ c ∨ c < a ∧ b < a

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ a ∉ Ι b c ↔ a ≤ b ∧ a ≤ c ∨ c < a ∧ b < a

Tactic:
simp only [uIoc_eq_union, mem_union, mem_Ioc, not_lt, ← not_le]

Result:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast?_eraseKey_self [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α}
    (hl : DistinctKeys l) : getValueCast? k (eraseKey k l) = none

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k : α
hl : DistinctKeys l
⊢ getValueCast? k (eraseKey k l) = none

Tactic:
rw [getValueCast?_eraseKey hl, if_pos BEq.refl]

Result:
no goals
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem succ_descFactorial (n : ℕ) :
    ∀ k, (n + 1 - k) * (n + 1).descFactorial k = (n + 1) * n.descFactorial k
  | 0 => by rw [Nat.sub_zero, descFactorial_zero, descFactorial_zero]
  | k + 1 => by
    rw [descFactorial, succ_descFactorial _ k, descFactorial_succ, succ_sub_succ, Nat.mul_left_comm]

Proof state:
n k : ℕ
⊢ (n + 1 - (k + 1)) * (n + 1).descFactorial (k + 1) = (n + 1) * n.descFactorial (k + 1)

Tactic:
rw [descFactorial, succ_descFactorial _ k, descFactorial_succ, succ_sub_succ, Nat.mul_left_comm]

Result:
no goals

Proof state:
n : ℕ
⊢ (n + 1 - 0) * (n + 1).descFactorial 0 = (n + 1) * n.descFactorial 0

Tactic:
rw [Nat.sub_zero, descFactorial_zero, descFactorial_zero]

Result:
no goals
-- Mathlib/Logic/Function/Conjugate.lean
theorem isAssociative_right [Std.Associative ga] (h : Semiconj₂ f ga gb) (h_surj : Surjective f) :
    Std.Associative gb :=
  ⟨h_surj.forall₃.2 fun x₁ x₂ x₃ ↦ by simp only [← h.eq, Std.Associative.assoc (op := ga)]⟩

Proof state:
α : Type u_1
β : Type u_2
f : α → β
ga : α → α → α
gb : β → β → β
inst✝ : Std.Associative ga
h : Semiconj₂ f ga gb
h_surj : Surjective f
x₁ x₂ x₃ : α
⊢ gb (gb (f x₁) (f x₂)) (f x₃) = gb (f x₁) (gb (f x₂) (f x₃))

Tactic:
simp only [← h.eq, Std.Associative.assoc (op := ga)]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem abs_toReal_eq_pi_div_two_iff {θ : Angle} :
    |θ.toReal| = π / 2 ↔ θ = (π / 2 : ℝ) ∨ θ = (-π / 2 : ℝ)

Proof state:
θ : Angle
⊢ |θ.toReal| = π / 2 ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)

Tactic:
rw [abs_eq (div_nonneg Real.pi_pos.le two_pos.le), ← neg_div, toReal_eq_pi_div_two_iff,
  toReal_eq_neg_pi_div_two_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem repr_reindex : (b.reindex e).repr x = (b.repr x).mapDomain e :=
  DFunLike.ext _ _ <| by simp [repr_reindex_apply]

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
x : M
e : ι ≃ ι'
⊢ ∀ (x_1 : ι'), ((b.reindex e).repr x) x_1 = (mapDomain (⇑e) (b.repr x)) x_1

Tactic:
simp [repr_reindex_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/Alternating/Basic.lean
theorem map_swap_add [DecidableEq ι] {i j : ι} (hij : i ≠ j) :
    f (v ∘ Equiv.swap i j) + f v = 0

Proof state:
R : Type u_1
inst✝⁵ : Semiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ f (v ∘ ⇑(Equiv.swap i j)) + f v = 0

Tactic:
rw [Equiv.comp_swap_eq_update]

Result:
R : Type u_1
inst✝⁵ : Semiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ f (update (update v j (v i)) i (v j)) + f v = 0

Proof state:
case h.e'_2
R : Type u_1
inst✝⁵ : Semiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ f (update (update v j (v i)) i (v j)) + f v = f (update (update v i (v i + v j)) j (v i + v j))

Tactic:
simp [f.map_update_self _ hij, f.map_update_self _ hij.symm,
  Function.update_comm hij (v i + v j) (v _) v, Function.update_comm hij.symm (v i) (v i) v]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : Semiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ f (update (update v j (v i)) i (v j)) + f v = 0

Tactic:
convert f.map_update_update v hij (v i + v j)

Result:
case h.e'_2
R : Type u_1
inst✝⁵ : Semiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ f (update (update v j (v i)) i (v j)) + f v = f (update (update v i (v i + v j)) j (v i + v j))
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem forall_eq_or_imp : (∀ a, a = a' ∨ q a → p a) ↔ p a' ∧ ∀ a, q a → p a

Proof state:
α : Sort u_1
p q : α → Prop
a' : α
⊢ (∀ (a : α), a = a' ∨ q a → p a) ↔ p a' ∧ ∀ (a : α), q a → p a

Tactic:
simp only [or_imp, forall_and, forall_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem dropLast_append_cons : dropLast (l₁ ++ b :: l₂) = l₁ ++ dropLast (b :: l₂)

Proof state:
α✝ : Type u_1
l₁ : List α✝
b : α✝
l₂ : List α✝
⊢ (l₁ ++ b :: l₂).dropLast = l₁ ++ (b :: l₂).dropLast

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem piCongrLeft_symm_preimage_univ_pi (f : ι' ≃ ι) (t : ∀ i, Set (α i)) :
    (f.piCongrLeft α).symm ⁻¹' univ.pi (fun i' => t <| f i') = univ.pi t

Proof state:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
t : (i : ι) → Set (α i)
⊢ (⇑(piCongrLeft α f).symm ⁻¹' univ.pi fun i' => t (f i')) = univ.pi t

Tactic:
simpa [f.surjective.range_eq] using piCongrLeft_symm_preimage_pi f univ t

Result:
no goals
-- Mathlib/NumberTheory/NumberField/FinitePlaces.lean
theorem norm_embedding_eq (w : FinitePlace K) (x : K) :
    ‖embedding (maximalIdeal w) x‖ = w x

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : FinitePlace K
x : K
⊢ ‖(embedding w.maximalIdeal) x‖ = w x

Tactic:
conv_rhs => rw [← mk_maximalIdeal w, mk_apply]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean
theorem prod_map_zpow {n : ℤ} : (m.map fun i => f i ^ n).prod = (m.map f).prod ^ n

Proof state:
case h.e'_2.h.e'_3
ι : Type u_2
α : Type u_3
inst✝ : DivisionCommMonoid α
m : Multiset ι
f : ι → α
n : ℤ
⊢ map (fun i => f i ^ n) m = map (⇑(zpowGroupHom n)) (map f m)

Tactic:
simp only [map_map, Function.comp_apply, zpowGroupHom_apply]

Result:
no goals

Proof state:
ι : Type u_2
α : Type u_3
inst✝ : DivisionCommMonoid α
m : Multiset ι
f : ι → α
n : ℤ
⊢ (map (fun i => f i ^ n) m).prod = (map f m).prod ^ n

Tactic:
convert (m.map f).prod_hom (zpowGroupHom n : α →* α)

Result:
case h.e'_2.h.e'_3
ι : Type u_2
α : Type u_3
inst✝ : DivisionCommMonoid α
m : Multiset ι
f : ι → α
n : ℤ
⊢ map (fun i => f i ^ n) m = map (⇑(zpowGroupHom n)) (map f m)
-- Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
theorem mem_map_equiv {f : R ≃+* S} {K : NonUnitalSubsemiring R} {x : S} :
    x ∈ K.map (f : R →ₙ+* S) ↔ f.symm x ∈ K

Proof state:
R : Type u
S : Type v
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R ≃+* S
K : NonUnitalSubsemiring R
x : S
⊢ x ∈ map (↑f) K ↔ f.symm x ∈ K

Tactic:
convert @Set.mem_image_equiv _ _ (↑K) f.toEquiv x

Result:
no goals