harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Colimit/Module.lean
@[simp] lemma map_id :
    map (fun _ ↦ LinearMap.id) (fun _ _ _ ↦ rfl) = LinearMap.id (R := R) (M := DirectLimit G f) :=
  DFunLike.ext _ _ <| by
    rintro ⟨x⟩; refine x.induction_on (by simp) (fun _ ↦ map_apply_of _ _) (by simp +contextual)

Proof state:
R : Type u_1
inst✝⁴ : Semiring R
ι : Type u_2
inst✝³ : Preorder ι
G : ι → Type u_3
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommMonoid (G i)
inst✝ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
x✝ : DirectLimit G f
x : DirectSum ι G
⊢ (map (fun x => LinearMap.id) ⋯) (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) 0) =
    LinearMap.id (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) 0)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : Semiring R
ι : Type u_2
inst✝³ : Preorder ι
G : ι → Type u_3
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommMonoid (G i)
inst✝ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
x✝ : DirectLimit G f
x : DirectSum ι G
⊢ ∀ (x y : DirectSum ι fun i => G i),
    (map (fun x => LinearMap.id) ⋯) (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) x) =
        LinearMap.id (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) x) →
      (map (fun x => LinearMap.id) ⋯) (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) y) =
          LinearMap.id (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) y) →
        (map (fun x => LinearMap.id) ⋯) (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) (x + y)) =
          LinearMap.id (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) (x + y))

Tactic:
simp +contextual

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : Semiring R
ι : Type u_2
inst✝³ : Preorder ι
G : ι → Type u_3
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommMonoid (G i)
inst✝ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
⊢ ∀ (x : DirectLimit G f), (map (fun x => LinearMap.id) ⋯) x = LinearMap.id x

Tactic:
rintro ⟨x⟩

Result:
case mk
R : Type u_1
inst✝⁴ : Semiring R
ι : Type u_2
inst✝³ : Preorder ι
G : ι → Type u_3
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommMonoid (G i)
inst✝ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
x✝ : DirectLimit G f
x : DirectSum ι G
⊢ (map (fun x => LinearMap.id) ⋯) (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) x) =
    LinearMap.id (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) x)

Proof state:
case mk
R : Type u_1
inst✝⁴ : Semiring R
ι : Type u_2
inst✝³ : Preorder ι
G : ι → Type u_3
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommMonoid (G i)
inst✝ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
x✝ : DirectLimit G f
x : DirectSum ι G
⊢ (map (fun x => LinearMap.id) ⋯) (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) x) =
    LinearMap.id (Quot.mk (⇑(addConGen (Eqv f)).toSetoid) x)

Tactic:
refine x.induction_on (by simp) (fun _ ↦ map_apply_of _ _) (by simp +contextual)

Result:
no goals
-- Mathlib/Data/Int/Basic.lean
lemma dvd_natCast {n : ℕ} : m ∣ (n : ℤ) ↔ m.natAbs ∣ n

Proof state:
m : ℤ
n : ℕ
⊢ m ∣ ↑n ↔ m.natAbs ∣ n

Tactic:
obtain hn | hn := natAbs_eq m <;> rw [hn] <;> simp [← natCast_dvd_natCast, Int.neg_dvd]

Result:
no goals
-- Mathlib/Topology/Filter.lean
theorem closure_singleton (l : Filter α) : closure {l} = Ici l

Proof state:
case h
α : Type u_2
l l' : Filter α
⊢ l' ∈ closure {l} ↔ l' ∈ Ici l

Tactic:
simp [Filter.mem_closure, Filter.le_def]

Result:
no goals

Proof state:
α : Type u_2
l : Filter α
⊢ closure {l} = Ici l

Tactic:
ext l'

Result:
case h
α : Type u_2
l l' : Filter α
⊢ l' ∈ closure {l} ↔ l' ∈ Ici l
-- Mathlib/Data/Nat/Prime/Basic.lean
theorem Prime.not_dvd_mul {p m n : ℕ} (pp : Prime p) (Hm : ¬p ∣ m) (Hn : ¬p ∣ n) : ¬p ∣ m * n :=
  mt pp.dvd_mul.1 <| by simp [Hm, Hn]

Proof state:
p m n : ℕ
pp : Prime p
Hm : ¬p ∣ m
Hn : ¬p ∣ n
⊢ ¬(p ∣ m ∨ p ∣ n)

Tactic:
simp [Hm, Hn]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem image_pair (f : α → β) (a b : α) : f '' {a, b} = {f a, f b}

Proof state:
α : Type u_1
β : Type u_2
f : α → β
a b : α
⊢ f '' {a, b} = {f a, f b}

Tactic:
simp only [image_insert_eq, image_singleton]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem map_set {f : α → β} {l : Array α} {i : Nat} {h : i < l.size} {a : α} :
    (l.set i a).map f = (l.map f).set i (f a) (by simpa using h)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : Array α
i : Nat
h : i < l.size
a : α
⊢ map f (l.set i a h) = (map f l).set i (f a) ⋯

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
f : α → β
i : Nat
a : α
toList✝ : List α
h : i < { toList := toList✝ }.size
⊢ map f ({ toList := toList✝ }.set i a h) = (map f { toList := toList✝ }).set i (f a) ⋯

Proof state:
α : Type ?u.171672
β : Type ?u.171700
f : α → β
l : Array α
i : Nat
h : i < l.size
a : α
⊢ i < (map f l).size

Tactic:
simpa using h

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → β
i : Nat
a : α
toList✝ : List α
h : i < { toList := toList✝ }.size
⊢ map f ({ toList := toList✝ }.set i a h) = (map f { toList := toList✝ }).set i (f a) ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem map_apply_ofFractionRing_mk [MonoidHomClass F R[X] S[X]] (φ : F)
    (hφ : R[X]⁰ ≤ S[X]⁰.comap φ) (n : R[X]) (d : R[X]⁰) :
    map φ hφ (ofFractionRing (Localization.mk n d)) =
      ofFractionRing (Localization.mk (φ n) ⟨φ d, hφ d.prop⟩)

Proof state:
R : Type u_3
S : Type u_4
F : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
n : R[X]
d : ↥R[X]⁰
⊢ (map φ hφ) { toFractionRing := Localization.mk n d } = { toFractionRing := Localization.mk (φ n) ⟨φ ↑d, ⋯⟩ }

Tactic:
simp only [map, MonoidHom.coe_mk, OneHom.coe_mk, liftOn_ofFractionRing_mk,
  Submonoid.mem_comap.mp (hφ d.2), ↓reduceDIte]

Result:
no goals
-- Mathlib/GroupTheory/Subgroup/Center.lean
theorem center_le_normalizer : center G ≤ H.normalizer := fun x hx y => by
  simp [← mem_center_iff.mp hx y, mul_assoc]

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
x : G
hx : x ∈ center G
y : G
⊢ y ∈ H ↔ x * y * x⁻¹ ∈ H

Tactic:
simp [← mem_center_iff.mp hx y, mul_assoc]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem nmul_succ (a b) : a ⨳ succ b = a ⨳ b ♯ a

Proof state:
a b : Ordinal.{u_1}
⊢ a ⨳ succ b = a ⨳ b ♯ a

Tactic:
rw [← nadd_one, nmul_nadd_one]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_mono_ae (h : f ≤ᵐ[μ] g) : (∫ u in a..b, f u ∂μ) ≤ ∫ u in a..b, g u ∂μ

Proof state:
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
h : f ≤ᶠ[ae μ] g
⊢ ∫ (u : ℝ) in a..b, f u ∂μ ≤ ∫ (u : ℝ) in a..b, g u ∂μ

Tactic:
simpa only [integral_of_le hab] using setIntegral_mono_ae hf.1 hg.1 h

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem toDual_inj (m : M) (a : b.toDual m = 0) : m = 0 :=
  b.toDual_injective (by rwa [_root_.map_zero])

Proof state:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
m : M
a : b.toDual m = 0
⊢ b.toDual m = b.toDual 0

Tactic:
rwa [_root_.map_zero]

Result:
no goals
-- Mathlib/Data/Fintype/Fin.lean
theorem Iio_castSucc (i : Fin n) : Iio (castSucc i) = (Iio i).map Fin.castSuccEmb

Proof state:
case a
n : ℕ
i : Fin n
⊢ map valEmbedding (Iio i.castSucc) = map valEmbedding (map castSuccEmb (Iio i))

Tactic:
rw [Finset.map_map, Fin.map_valEmbedding_Iio]

Result:
case a
n : ℕ
i : Fin n
⊢ Iio ↑i.castSucc = map (castSuccEmb.trans valEmbedding) (Iio i)

Proof state:
n : ℕ
i : Fin n
⊢ Iio i.castSucc = map castSuccEmb (Iio i)

Tactic:
apply Finset.map_injective Fin.valEmbedding

Result:
case a
n : ℕ
i : Fin n
⊢ map valEmbedding (Iio i.castSucc) = map valEmbedding (map castSuccEmb (Iio i))

Proof state:
case a
n : ℕ
i : Fin n
⊢ Iio ↑i.castSucc = map (castSuccEmb.trans valEmbedding) (Iio i)

Tactic:
exact (Fin.map_valEmbedding_Iio i).symm

Result:
no goals
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem nfpFamily_eq_self [Small.{u} ι] {a} (h : ∀ i, f i a = a) : nfpFamily f a = a

Proof state:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
a : Ordinal.{u}
h : ∀ (i : ι), f i a = a
⊢ nfpFamily f a = a

Tactic:
apply (Ordinal.iSup_le ?_).antisymm (le_nfpFamily f a)

Result:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
a : Ordinal.{u}
h : ∀ (i : ι), f i a = a
⊢ ∀ (i : List ι), List.foldr f a i ≤ a

Proof state:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
a : Ordinal.{u}
h : ∀ (i : ι), f i a = a
⊢ ∀ (i : List ι), List.foldr f a i ≤ a

Tactic:
intro l

Result:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
a : Ordinal.{u}
h : ∀ (i : ι), f i a = a
l : List ι
⊢ List.foldr f a l ≤ a

Proof state:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
a : Ordinal.{u}
h : ∀ (i : ι), f i a = a
l : List ι
⊢ List.foldr f a l ≤ a

Tactic:
rw [List.foldr_fixed' h l]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Bounded.lean
theorem exists_isOpen_isBounded_image_of_isCompact_of_forall_continuousAt [TopologicalSpace β]
    {k : Set β} {f : β → α} (hk : IsCompact k) (hf : ∀ x ∈ k, ContinuousAt f x) :
    ∃ t, k ⊆ t ∧ IsOpen t ∧ IsBounded (f '' t)

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f univ x
⊢ ∃ t, k ⊆ t ∧ IsOpen t ∧ Bornology.IsBounded (f '' t)

Tactic:
simpa only [inter_univ] using
  exists_isOpen_isBounded_image_inter_of_isCompact_of_forall_continuousWithinAt hk hf

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousAt f x
⊢ ∃ t, k ⊆ t ∧ IsOpen t ∧ Bornology.IsBounded (f '' t)

Tactic:
simp_rw [← continuousWithinAt_univ] at hf

Result:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f univ x
⊢ ∃ t, k ⊆ t ∧ IsOpen t ∧ Bornology.IsBounded (f '' t)
-- Mathlib/Order/UpperLower/Basic.lean
theorem Iic_iInf (f : ι → α) : Iic (⨅ i, f i) = ⨅ i, Iic (f i) :=
  SetLike.ext fun c => by simp only [mem_Iic_iff, mem_iInf_iff, le_iInf_iff]

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
c : α
⊢ c ∈ Iic (⨅ i, f i) ↔ c ∈ ⨅ i, Iic (f i)

Tactic:
simp only [mem_Iic_iff, mem_iInf_iff, le_iInf_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Pi.lean
theorem mem_iInf_maxGenEigenspace_iff (χ : ι → R) (m : M) :
    m ∈ ⨅ i, (f i).maxGenEigenspace (χ i) ↔ ∀ j, ∃ k : ℕ, ((f j - χ j • ↑1) ^ k) m = 0

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → End R M
χ : ι → R
m : M
⊢ m ∈ ⨅ i, (f i).maxGenEigenspace (χ i) ↔ ∀ (j : ι), ∃ k, ((f j - χ j • 1) ^ k) m = 0

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Projective/Resolution.lean
lemma exact_succ (n : ℕ) :
    (ShortComplex.mk _ _ (P.complex.d_comp_d (n + 2) (n + 1) n)).Exact :=
  ((HomologicalComplex.exactAt_iff' _ (n + 2) (n + 1) n) (by simp only [prev]; rfl)
    (by simp)).1 (P.complex_exactAt_succ n)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
n : ℕ
⊢ (ComplexShape.down ℕ).next (n + 1) = n

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
n : ℕ
⊢ n + 1 + 1 = n + 2

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
n : ℕ
⊢ (ComplexShape.down ℕ).prev (n + 1) = n + 2

Tactic:
simp only [prev]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
n : ℕ
⊢ n + 1 + 1 = n + 2
-- Mathlib/CategoryTheory/Limits/Constructions/EventuallyConstant.lean
lemma isIso_map {i j : J} (φ : i ⟶ j) (π : j ⟶ i₀) : IsIso (F.map φ)

Proof state:
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
i j : J
φ : i ⟶ j
π : j ⟶ i₀
⊢ IsIso (F.map φ)

Tactic:
have := h π

Result:
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
i j : J
φ : i ⟶ j
π : j ⟶ i₀
this : IsIso (F.map π)
⊢ IsIso (F.map φ)

Proof state:
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
i j : J
φ : i ⟶ j
π : j ⟶ i₀
this✝ : IsIso (F.map π)
this : IsIso (F.map (φ ≫ π))
⊢ IsIso (F.map φ)

Tactic:
exact IsIso.of_isIso_fac_right (F.map_comp φ π).symm

Result:
no goals

Proof state:
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
i j : J
φ : i ⟶ j
π : j ⟶ i₀
this : IsIso (F.map π)
⊢ IsIso (F.map φ)

Tactic:
have := h (φ ≫ π)

Result:
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
i j : J
φ : i ⟶ j
π : j ⟶ i₀
this✝ : IsIso (F.map π)
this : IsIso (F.map (φ ≫ π))
⊢ IsIso (F.map φ)
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem sizeUpTo_strict_mono {i : ℕ} (h : i < c.length) : c.sizeUpTo i < c.sizeUpTo (i + 1)

Proof state:
n : ℕ
c : Composition n
i : ℕ
h : i < c.length
⊢ c.sizeUpTo i < c.sizeUpTo (i + 1)

Tactic:
rw [c.sizeUpTo_succ h]

Result:
n : ℕ
c : Composition n
i : ℕ
h : i < c.length
⊢ c.sizeUpTo i < c.sizeUpTo i + c.blocks[i]

Proof state:
n : ℕ
c : Composition n
i : ℕ
h : i < c.length
⊢ c.sizeUpTo i < c.sizeUpTo i + c.blocks[i]

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_setWidth (m : Nat) (x : BitVec n) (i : Nat) :
    getLsbD (setWidth m x) i = (decide (i < m) && getLsbD x i)

Proof state:
n m : Nat
x : BitVec n
i : Nat
⊢ (setWidth m x).getLsbD i = (decide (i < m) && x.getLsbD i)

Tactic:
simp [getLsbD, toNat_setWidth, Nat.testBit_mod_two_pow]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem _root_.Function.invFunOn_injOn_image [Nonempty α] (f : α → β) (s : Set α) :
    Set.InjOn (invFunOn f s) (f '' s)

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : Nonempty α
f : α → β
s : Set α
x : α
hx : x ∈ s
x' : α
hx' : x' ∈ s
he : invFunOn f s (f x) = invFunOn f s (f x')
⊢ f x = f x'

Tactic:
rw [← invFunOn_apply_eq (f := f) hx, he, invFunOn_apply_eq (f := f) hx']

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Nonempty α
f : α → β
s : Set α
⊢ InjOn (invFunOn f s) (f '' s)

Tactic:
rintro _ ⟨x, hx, rfl⟩ _ ⟨x', hx', rfl⟩ he

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : Nonempty α
f : α → β
s : Set α
x : α
hx : x ∈ s
x' : α
hx' : x' ∈ s
he : invFunOn f s (f x) = invFunOn f s (f x')
⊢ f x = f x'
-- Mathlib/Data/List/Infix.lean
theorem IsPrefix.get_eq {x y : List α} (h : x <+: y) {n} (hn : n < x.length) :
    x.get ⟨n, hn⟩ = y.get ⟨n, hn.trans_le h.length_le⟩

Proof state:
α : Type u_1
x y : List α
h : x <+: y
n : ℕ
hn : n < x.length
⊢ x.get ⟨n, hn⟩ = y.get ⟨n, ⋯⟩

Tactic:
simp only [get_eq_getElem, IsPrefix.getElem h hn]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem or_and_distrib_right (x y z : Nat) : (x &&& y) ||| z = (x ||| z) &&& (y ||| z)

Proof state:
case pred
x y z : Nat
⊢ ∀ (i : Nat), (x &&& y ||| z).testBit i = ((x ||| z) &&& (y ||| z)).testBit i

Tactic:
simp [Bool.or_and_distrib_right]

Result:
no goals

Proof state:
x y z : Nat
⊢ x &&& y ||| z = (x ||| z) &&& (y ||| z)

Tactic:
apply Nat.eq_of_testBit_eq

Result:
case pred
x y z : Nat
⊢ ∀ (i : Nat), (x &&& y ||| z).testBit i = ((x ||| z) &&& (y ||| z)).testBit i
-- Mathlib/Combinatorics/Additive/DoublingConst.lean
@[to_additive (attr := simp)]
lemma mulConst_inv_left (A B : Finset G) : σₘ[A⁻¹, B] = δₘ[A, B]

Proof state:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A B : Finset G
⊢ σₘ[A⁻¹, B] = δₘ[A, B]

Tactic:
rw [mulConst, divConst, card_inv, ← card_inv, mul_inv_rev, inv_inv, inv_mul_eq_div]

Result:
no goals
-- Mathlib/Order/GaloisConnection/Basic.lean
theorem l_inf_u [SemilatticeInf α] [SemilatticeInf β] (gi : GaloisInsertion l u) (a b : β) :
    l (u a ⊓ u b) = a ⊓ b :=
  calc
    l (u a ⊓ u b) = l (u (a ⊓ b)) := congr_arg l gi.gc.u_inf.symm
    _ = a ⊓ b

Proof state:
α : Type u
β : Type v
l : α → β
u : β → α
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
gi : GaloisInsertion l u
a b : β
⊢ l (u (a ⊓ b)) = a ⊓ b

Tactic:
simp only [gi.l_u_eq]

Result:
no goals
-- Mathlib/Algebra/Group/Operations.lean
@[to_additive]
lemma div_dite (a : α) (b : P → α) (c : ¬ P → α) :
    (a / if h : P then b h else c h) = if h : P then a / b h else a / c h

Proof state:
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : α
b : P → α
c : ¬P → α
⊢ (a / if h : P then b h else c h) = if h : P then a / b h else a / c h

Tactic:
split <;> rfl

Result:
no goals
-- Mathlib/Geometry/RingedSpace/OpenImmersion.lean
theorem isoRestrict_inv_ofRestrict : (isoRestrict f).inv ≫ f = Y.ofRestrict _

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
⊢ (isoRestrict f).inv ≫ f = Y.ofRestrict ⋯

Tactic:
rw [Iso.inv_comp_eq, isoRestrict_hom_ofRestrict]

Result:
no goals
-- Mathlib/RingTheory/AdicCompletion/Functoriality.lean
theorem component_sumInv (x : AdicCompletion I (⨁ j, M j)) (j : ι) :
    component (AdicCompletion I R) ι _ j (sumInv I M x) =
      map I (component R ι _ j) x

Proof state:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : Fintype ι
x : AdicCompletion I (⨁ (j : ι), M j)
j : ι
⊢ (component (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) j) ((sumInv I M) x) =
    (map I (component R ι M j)) x

Tactic:
apply induction_on I _ x (fun x ↦ ?_)

Result:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : Fintype ι
x✝ : AdicCompletion I (⨁ (j : ι), M j)
j : ι
x : AdicCauchySequence I (⨁ (j : ι), M j)
⊢ (component (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) j) ((sumInv I M) ((mk I (⨁ (j : ι), M j)) x)) =
    (map I (component R ι M j)) ((mk I (⨁ (j : ι), M j)) x)

Proof state:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : Fintype ι
x✝ : AdicCompletion I (⨁ (j : ι), M j)
j : ι
x : AdicCauchySequence I (⨁ (j : ι), M j)
⊢ (component (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) j) ((sumInv I M) ((mk I (⨁ (j : ι), M j)) x)) =
    (map I (component R ι M j)) ((mk I (⨁ (j : ι), M j)) x)

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem isAlgebraic_one [Nontrivial R] : IsAlgebraic R (1 : A)

Proof state:
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
⊢ IsAlgebraic R ((algebraMap R A) 1)

Tactic:
exact isAlgebraic_algebraMap 1

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
⊢ IsAlgebraic R 1

Tactic:
rw [← map_one (algebraMap R A)]

Result:
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
⊢ IsAlgebraic R ((algebraMap R A) 1)
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem spanSingleton_eq_zero_iff {y : P} : spanSingleton S y = 0 ↔ y = 0 :=
  ⟨fun h =>
    span_eq_bot.mp (by simpa using congr_arg Subtype.val h : span R {y} = ⊥) y (mem_singleton y),
    fun h => by simp [h]⟩

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
y : P
h : spanSingleton S y = 0
⊢ span R {y} = ⊥

Tactic:
simpa using congr_arg Subtype.val h

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
y : P
h : y = 0
⊢ spanSingleton S y = 0

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem totalDegree_pow (a : MvPolynomial σ R) (n : ℕ) :
    (a ^ n).totalDegree ≤ n * a.totalDegree

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
a : MvPolynomial σ R
n : ℕ
x✝¹ x✝ : σ →₀ ℕ
⊢ ((x✝¹ + x✝).sum fun x e => e) = (x✝¹.sum fun x e => e) + x✝.sum fun x e => e

Tactic:
exact Finsupp.sum_add_index' (fun _ => rfl) (fun _ _ _ => rfl)

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
a : MvPolynomial σ R
n : ℕ
⊢ (a ^ n).totalDegree ≤ n * a.totalDegree

Tactic:
rw [Finset.pow_eq_prod_const, ← Nat.nsmul_eq_mul, Finset.nsmul_eq_sum_const]

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
a : MvPolynomial σ R
n : ℕ
⊢ (∏ _k ∈ Finset.range n, a).totalDegree ≤ ∑ _k ∈ Finset.range n, a.totalDegree

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
a : MvPolynomial σ R
n : ℕ
⊢ (∏ _k ∈ Finset.range n, a).totalDegree ≤ ∑ _k ∈ Finset.range n, a.totalDegree

Tactic:
refine supDegree_prod_le rfl (fun _ _ => ?_)

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
a : MvPolynomial σ R
n : ℕ
x✝¹ x✝ : σ →₀ ℕ
⊢ ((x✝¹ + x✝).sum fun x e => e) = (x✝¹.sum fun x e => e) + x✝.sum fun x e => e
-- Mathlib/Data/List/Lemmas.lean
theorem mapAccumr₂_eq_foldr {σ φ : Type*} (f : α → β → σ → σ × φ) :
    ∀ (as : List α) (bs : List β) (s : σ),
    mapAccumr₂ f as bs s = foldr (fun ab s =>
                              let r := f ab.1 ab.2 s.1
                              (r.1, r.2 :: s.2)
                            ) (s, []) (as.zip bs)
  | [], [], _ => rfl
  | _ :: _, [], _ => rfl
  | [], _ :: _, _ => rfl
  | a :: as, b :: bs, s => by
    simp only [mapAccumr₂, foldr, mapAccumr₂_eq_foldr f as]
    rfl

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_4
φ : Type u_5
f : α → β → σ → σ × φ
a : α
as : List α
b : β
bs : List β
s : σ
⊢ mapAccumr₂ f (a :: as) (b :: bs) s =
    foldr
      (fun ab s =>
        let r := f ab.1 ab.2 s.1;
        (r.1, r.2 :: s.2))
      (s, []) ((a :: as).zip (b :: bs))

Tactic:
simp only [mapAccumr₂, foldr, mapAccumr₂_eq_foldr f as]

Result:
α : Type u_1
β : Type u_2
σ : Type u_4
φ : Type u_5
f : α → β → σ → σ × φ
a : α
as : List α
b : β
bs : List β
s : σ
⊢ ((f a b (foldr (fun ab s => ((f ab.1 ab.2 s.1).1, (f ab.1 ab.2 s.1).2 :: s.2)) (s, []) (as.zip bs)).1).1,
      (f a b (foldr (fun ab s => ((f ab.1 ab.2 s.1).1, (f ab.1 ab.2 s.1).2 :: s.2)) (s, []) (as.zip bs)).1).2 ::
        (foldr (fun ab s => ((f ab.1 ab.2 s.1).1, (f ab.1 ab.2 s.1).2 :: s.2)) (s, []) (as.zip bs)).2) =
    foldr (fun ab s => ((f ab.1 ab.2 s.1).1, (f ab.1 ab.2 s.1).2 :: s.2)) (s, []) ((a :: as).zip (b :: bs))

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_4
φ : Type u_5
f : α → β → σ → σ × φ
a : α
as : List α
b : β
bs : List β
s : σ
⊢ ((f a b (foldr (fun ab s => ((f ab.1 ab.2 s.1).1, (f ab.1 ab.2 s.1).2 :: s.2)) (s, []) (as.zip bs)).1).1,
      (f a b (foldr (fun ab s => ((f ab.1 ab.2 s.1).1, (f ab.1 ab.2 s.1).2 :: s.2)) (s, []) (as.zip bs)).1).2 ::
        (foldr (fun ab s => ((f ab.1 ab.2 s.1).1, (f ab.1 ab.2 s.1).2 :: s.2)) (s, []) (as.zip bs)).2) =
    foldr (fun ab s => ((f ab.1 ab.2 s.1).1, (f ab.1 ab.2 s.1).2 :: s.2)) (s, []) ((a :: as).zip (b :: bs))

Tactic:
rfl

Result:
no goals