harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Ideal/Span.lean
theorem mem_span_singleton_sup {x y : α} {I : Ideal α} :
    x ∈ Ideal.span {y} ⊔ I ↔ ∃ a : α, ∃ b ∈ I, a * y + b = x

Proof state:
case mp.intro.intro.intro.intro.intro
α : Type u
inst✝ : Semiring α
y : α
I : Ideal α
b : α
hb : b ∈ I
a : α
hya : a * y ∈ span {y}
⊢ ∃ a_1, ∃ b_1 ∈ I, a_1 * y + b_1 = a * y + b

Tactic:
exact ⟨a, b, hb, rfl⟩

Result:
no goals

Proof state:
α : Type u
inst✝ : Semiring α
x y : α
I : Ideal α
⊢ x ∈ span {y} ⊔ I ↔ ∃ a, ∃ b ∈ I, a * y + b = x

Tactic:
rw [Submodule.mem_sup]

Result:
α : Type u
inst✝ : Semiring α
x y : α
I : Ideal α
⊢ (∃ y_1 ∈ span {y}, ∃ z ∈ I, y_1 + z = x) ↔ ∃ a, ∃ b ∈ I, a * y + b = x

Proof state:
case mp.intro.intro.intro.intro
α : Type u
inst✝ : Semiring α
y : α
I : Ideal α
ya : α
hya : ya ∈ span {y}
b : α
hb : b ∈ I
⊢ ∃ a, ∃ b_1 ∈ I, a * y + b_1 = ya + b

Tactic:
obtain ⟨a, rfl⟩ := mem_span_singleton'.mp hya

Result:
case mp.intro.intro.intro.intro.intro
α : Type u
inst✝ : Semiring α
y : α
I : Ideal α
b : α
hb : b ∈ I
a : α
hya : a * y ∈ span {y}
⊢ ∃ a_1, ∃ b_1 ∈ I, a_1 * y + b_1 = a * y + b

Proof state:
case mp
α : Type u
inst✝ : Semiring α
x y : α
I : Ideal α
⊢ (∃ y_1 ∈ span {y}, ∃ z ∈ I, y_1 + z = x) → ∃ a, ∃ b ∈ I, a * y + b = x

Tactic:
rintro ⟨ya, hya, b, hb, rfl⟩

Result:
case mp.intro.intro.intro.intro
α : Type u
inst✝ : Semiring α
y : α
I : Ideal α
ya : α
hya : ya ∈ span {y}
b : α
hb : b ∈ I
⊢ ∃ a, ∃ b_1 ∈ I, a * y + b_1 = ya + b

Proof state:
α : Type u
inst✝ : Semiring α
x y : α
I : Ideal α
⊢ (∃ y_1 ∈ span {y}, ∃ z ∈ I, y_1 + z = x) ↔ ∃ a, ∃ b ∈ I, a * y + b = x

Tactic:
constructor

Result:
case mp
α : Type u
inst✝ : Semiring α
x y : α
I : Ideal α
⊢ (∃ y_1 ∈ span {y}, ∃ z ∈ I, y_1 + z = x) → ∃ a, ∃ b ∈ I, a * y + b = x

case mpr
α : Type u
inst✝ : Semiring α
x y : α
I : Ideal α
⊢ (∃ a, ∃ b ∈ I, a * y + b = x) → ∃ y_1 ∈ span {y}, ∃ z ∈ I, y_1 + z = x

Proof state:
case mpr
α : Type u
inst✝ : Semiring α
x y : α
I : Ideal α
⊢ (∃ a, ∃ b ∈ I, a * y + b = x) → ∃ y_1 ∈ span {y}, ∃ z ∈ I, y_1 + z = x

Tactic:
rintro ⟨a, b, hb, rfl⟩

Result:
case mpr.intro.intro.intro
α : Type u
inst✝ : Semiring α
y : α
I : Ideal α
a b : α
hb : b ∈ I
⊢ ∃ y_1 ∈ span {y}, ∃ z ∈ I, y_1 + z = a * y + b

Proof state:
case mpr.intro.intro.intro
α : Type u
inst✝ : Semiring α
y : α
I : Ideal α
a b : α
hb : b ∈ I
⊢ ∃ y_1 ∈ span {y}, ∃ z ∈ I, y_1 + z = a * y + b

Tactic:
exact ⟨a * y, Ideal.mem_span_singleton'.mpr ⟨a, rfl⟩, b, hb, rfl⟩

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem sdiff_sdiff_sup_sdiff' : z \ (x \ y ⊔ y \ x) = z ⊓ x ⊓ y ⊔ z \ x ⊓ z \ y :=
  calc
    z \ (x \ y ⊔ y \ x) = z \ (x \ y) ⊓ z \ (y \ x) := sdiff_sup
    _ = (z \ x ⊔ z ⊓ x ⊓ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x)

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ z \ (x \ y) ⊓ z \ (y \ x) = (z \ x ⊔ z ⊓ x ⊓ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x)

Tactic:
rw [sdiff_sdiff_right, sdiff_sdiff_right]

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (z \ x ⊔ z ⊓ x ⊓ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x) = (z \ x ⊔ z ⊓ y ⊓ x) ⊓ (z \ y ⊔ z ⊓ y ⊓ x)

Tactic:
ac_rfl

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (z \ x ⊔ z ⊓ y ⊓ x) ⊓ (z \ y ⊔ z ⊓ y ⊓ x) = z \ x ⊓ z \ y ⊔ z ⊓ y ⊓ x

Tactic:
rw [← sup_inf_right]

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ z \ x ⊓ z \ y ⊔ z ⊓ y ⊓ x = z ⊓ x ⊓ y ⊔ z \ x ⊓ z \ y

Tactic:
ac_rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem shiftLeft_and_distrib (x y : BitVec w) (n : Nat) :
    (x &&& y) <<< n = (x <<< n) &&& (y <<< n)

Proof state:
case pred
w : Nat
x y : BitVec w
n i : Nat
h : i < w
⊢ (!decide (i < n) && (x.getLsbD (i - n) && y.getLsbD (i - n))) =
    (!decide (i < n) && x.getLsbD (i - n) && (!decide (i < n) && y.getLsbD (i - n)))

Tactic:
by_cases h' : i < n <;> simp [h']

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
n : Nat
⊢ (x &&& y) <<< n = x <<< n &&& y <<< n

Tactic:
ext i h

Result:
case pred
w : Nat
x y : BitVec w
n i : Nat
h : i < w
⊢ ((x &&& y) <<< n).getLsbD i = (x <<< n &&& y <<< n).getLsbD i

Proof state:
case pred
w : Nat
x y : BitVec w
n i : Nat
h : i < w
⊢ ((x &&& y) <<< n).getLsbD i = (x <<< n &&& y <<< n).getLsbD i

Tactic:
simp only [getLsbD_shiftLeft, h, decide_true, Bool.true_and, getLsbD_and]

Result:
case pred
w : Nat
x y : BitVec w
n i : Nat
h : i < w
⊢ (!decide (i < n) && (x.getLsbD (i - n) && y.getLsbD (i - n))) =
    (!decide (i < n) && x.getLsbD (i - n) && (!decide (i < n) && y.getLsbD (i - n)))
-- Mathlib/NumberTheory/MulChar/Lemmas.lean
/-- If `χ` is a multiplicative character with `χ^n = 1` and `μ` is a primitive `n`th root
of unity, then, for `a ≠ 0`, there is some `k` such that `χ a = μ^k`. -/
lemma exists_apply_eq_pow {χ : MulChar F R} {n : ℕ} [NeZero n] (hχ : χ ^ n = 1) {μ : R}
    (hμ : IsPrimitiveRoot μ n) {a : F} (ha : a ≠ 0) :
    ∃ k < n, χ a = μ ^ k

Proof state:
case intro.intro
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Finite F
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
χ : MulChar F R
n : ℕ
inst✝ : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
ha : a ≠ 0
ζ : Rˣ
hζ₁ : ζ ∈ rootsOfUnity n R
hζ₂ : ↑ζ = χ a
hζ' : ↑ζ ^ n = 1
⊢ ∃ k < n, χ a = μ ^ k

Tactic:
obtain ⟨k, hk₁, hk₂⟩ := hμ.eq_pow_of_pow_eq_one hζ'

Result:
case intro.intro.intro.intro
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Finite F
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
χ : MulChar F R
n : ℕ
inst✝ : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
ha : a ≠ 0
ζ : Rˣ
hζ₁ : ζ ∈ rootsOfUnity n R
hζ₂ : ↑ζ = χ a
hζ' : ↑ζ ^ n = 1
k : ℕ
hk₁ : k < n
hk₂ : μ ^ k = ↑ζ
⊢ ∃ k < n, χ a = μ ^ k

Proof state:
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Finite F
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
χ : MulChar F R
n : ℕ
inst✝ : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
ha : a ≠ 0
⊢ ∃ k < n, χ a = μ ^ k

Tactic:
obtain ⟨ζ, hζ₁, hζ₂⟩ := apply_mem_rootsOfUnity_of_pow_eq_one hχ ha

Result:
case intro.intro
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Finite F
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
χ : MulChar F R
n : ℕ
inst✝ : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
ha : a ≠ 0
ζ : Rˣ
hζ₁ : ζ ∈ rootsOfUnity n R
hζ₂ : ↑ζ = χ a
⊢ ∃ k < n, χ a = μ ^ k

Proof state:
case intro.intro
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Finite F
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
χ : MulChar F R
n : ℕ
inst✝ : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
ha : a ≠ 0
ζ : Rˣ
hζ₁ : ζ ∈ rootsOfUnity n R
hζ₂ : ↑ζ = χ a
⊢ ∃ k < n, χ a = μ ^ k

Tactic:
have hζ' : ζ.val ^ n = 1 := (mem_rootsOfUnity' n ↑ζ).mp hζ₁

Result:
case intro.intro
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Finite F
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
χ : MulChar F R
n : ℕ
inst✝ : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
ha : a ≠ 0
ζ : Rˣ
hζ₁ : ζ ∈ rootsOfUnity n R
hζ₂ : ↑ζ = χ a
hζ' : ↑ζ ^ n = 1
⊢ ∃ k < n, χ a = μ ^ k

Proof state:
case intro.intro.intro.intro
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Finite F
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
χ : MulChar F R
n : ℕ
inst✝ : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
ha : a ≠ 0
ζ : Rˣ
hζ₁ : ζ ∈ rootsOfUnity n R
hζ₂ : ↑ζ = χ a
hζ' : ↑ζ ^ n = 1
k : ℕ
hk₁ : k < n
hk₂ : μ ^ k = ↑ζ
⊢ ∃ k < n, χ a = μ ^ k

Tactic:
exact ⟨k, hk₁, (hζ₂ ▸ hk₂).symm⟩

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem exp_four_lt : exp 4 < 64

Proof state:
⊢ 64 = 2 ^ ↑6

Tactic:
rw [rpow_natCast]

Result:
⊢ 64 = 2 ^ 6

Proof state:
⊢ 4 / ↑6 ≤ 0.6931471803

Tactic:
norm_num1

Result:
no goals

Proof state:
⊢ 0 < ↑6

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ rexp 4 < 64

Tactic:
rw [show (64 : ℝ) = 2 ^ ((6 : ℕ) : ℝ) by rw [rpow_natCast]; norm_num1,
  ← lt_log_iff_exp_lt (rpow_pos_of_pos zero_lt_two _), log_rpow zero_lt_two, ← div_lt_iff₀']

Result:
⊢ 4 / ↑6 < log 2


⊢ 0 < ↑6

Proof state:
⊢ 64 = 2 ^ 6

Tactic:
norm_num1

Result:
no goals

Proof state:
⊢ 4 / ↑6 < log 2

Tactic:
exact log_two_gt_d9.trans_le' (by norm_num1)

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Logic.lean
theorem cast_eq_iff_heq : cast e a = a' ↔ HEq a a' :=
  ⟨heq_of_cast_eq _, fun h => by cases h; rfl⟩

Proof state:
a✝¹ a✝ : Sort u_1
e : a✝¹ = a✝
a : a✝¹
a' : a✝
h : HEq a a'
⊢ cast e a = a'

Tactic:
cases h

Result:
case refl
a✝ : Sort u_1
a : a✝
e : a✝ = a✝
⊢ cast e a = a

Proof state:
case refl
a✝ : Sort u_1
a : a✝
e : a✝ = a✝
⊢ cast e a = a

Tactic:
rfl

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
lemma exists_eq_of_iSup_eq_of_not_isSuccLimit
    {ι : Type u} [hι : Nonempty ι] (f : ι → Cardinal.{v}) (hf : BddAbove (range f))
    {c : Cardinal.{v}} (hc : ¬ IsSuccLimit c)
    (h : ⨆ i, f i = c) : ∃ i, f i = c

Proof state:
ι : Type u
hι : Nonempty ι
f : ι → Cardinal.{v}
hf : BddAbove (range f)
c : Cardinal.{v}
hc : ¬IsSuccLimit c
h : ⨆ i, f i = c
⊢ ∃ i, f i = c

Tactic:
rw [Cardinal.isSuccLimit_iff] at hc

Result:
ι : Type u
hι : Nonempty ι
f : ι → Cardinal.{v}
hf : BddAbove (range f)
c : Cardinal.{v}
hc : ¬(c ≠ 0 ∧ IsSuccPrelimit c)
h : ⨆ i, f i = c
⊢ ∃ i, f i = c

Proof state:
ι : Type u
hι : Nonempty ι
f : ι → Cardinal.{v}
hf : BddAbove (range f)
c : Cardinal.{v}
hc : ¬(c ≠ 0 ∧ IsSuccPrelimit c)
h : ⨆ i, f i = c
e : ¬c ≠ 0
⊢ f hι.some = c

Tactic:
cases not_not.mp e

Result:
case refl
ι : Type u
hι : Nonempty ι
f : ι → Cardinal.{v}
hf : BddAbove (range f)
hc : ¬(0 ≠ 0 ∧ IsSuccPrelimit 0)
h : ⨆ i, f i = 0
e : ¬0 ≠ 0
⊢ f hι.some = 0

Proof state:
case refl
ι : Type u
hι : Nonempty ι
f : ι → Cardinal.{v}
hf : BddAbove (range f)
hc : ¬(0 ≠ 0 ∧ IsSuccPrelimit 0)
h : ⨆ i, f i = 0
e : ¬0 ≠ 0
⊢ f hι.some = 0

Tactic:
rw [← le_zero_iff] at h ⊢

Result:
case refl
ι : Type u
hι : Nonempty ι
f : ι → Cardinal.{v}
hf : BddAbove (range f)
hc : ¬(0 ≠ 0 ∧ IsSuccPrelimit 0)
h : ⨆ i, f i ≤ 0
e : ¬0 ≠ 0
⊢ f hι.some ≤ 0

Proof state:
case refl
ι : Type u
hι : Nonempty ι
f : ι → Cardinal.{v}
hf : BddAbove (range f)
hc : ¬(0 ≠ 0 ∧ IsSuccPrelimit 0)
h : ⨆ i, f i ≤ 0
e : ¬0 ≠ 0
⊢ f hι.some ≤ 0

Tactic:
exact (le_ciSup hf _).trans h

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Subcategory.lean
lemma W_of_isIso {X Y : C} (f : X ⟶ Y) [IsIso f] : S.W f

Proof state:
C : Type u_1
inst✝⁶ : Category.{u_2, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
S : Subcategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ S.W f

Tactic:
refine (S.W.arrow_mk_iso_iff ?_).1 (MorphismProperty.id_mem _ X)

Result:
C : Type u_1
inst✝⁶ : Category.{u_2, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
S : Subcategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ Arrow.mk (𝟙 X) ≅ Arrow.mk f

Proof state:
C : Type u_1
inst✝⁶ : Category.{u_2, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
S : Subcategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ Arrow.mk (𝟙 X) ≅ Arrow.mk f

Tactic:
exact Arrow.isoMk (Iso.refl _) (asIso f)

Result:
no goals
-- Mathlib/Analysis/Convex/Side.lean
theorem sSameSide_vadd_left_iff {s : AffineSubspace R P} {x y : P} {v : V} (hv : v ∈ s.direction) :
    s.SSameSide (v +ᵥ x) y ↔ s.SSameSide x y

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
⊢ s.SSameSide (v +ᵥ x) y ↔ s.SSameSide x y

Tactic:
rw [SSameSide, SSameSide, wSameSide_vadd_left_iff hv, vadd_mem_iff_mem_of_mem_direction hv]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
    (m.insert k v).getKey? k = some k

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k : α
v : β k
⊢ (m.insert k v).getKey? k = some k

Tactic:
simp_to_raw using Raw₀.getKey?_insert_self

Result:
no goals
-- Mathlib/Algebra/Group/Defs.lean
@[to_additive succ_nsmul'] lemma pow_succ' (a : M) : ∀ n, a ^ (n + 1) = a * a ^ n
  | 0 => by simp
  | n + 1 => by rw [pow_succ _ n, pow_succ, pow_succ', mul_assoc]

Proof state:
M : Type u_2
inst✝ : Monoid M
a : M
⊢ a ^ (0 + 1) = a * a ^ 0

Tactic:
simp

Result:
no goals

Proof state:
M : Type u_2
inst✝ : Monoid M
a : M
n : ℕ
⊢ a ^ (n + 1 + 1) = a * a ^ (n + 1)

Tactic:
rw [pow_succ _ n, pow_succ, pow_succ', mul_assoc]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Adjunction.lean
/-- Given an adjunction `adj : F ⊣ G`, `a` in `A` and commutation isomorphisms
`e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a` and
`e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a`, if `e₁` and `e₂` are compatible with the
counit of the adjunction `adj`, then we get a formula for `e₁.hom` in terms of `e₂`.
-/
lemma compatibilityCounit_left (h : CompatibilityCounit adj e₁ e₂) (X : C) :
    e₁.hom.app X = F.map ((adj.unit.app X)⟦a⟧') ≫ F.map (e₂.inv.app _) ≫ adj.counit.app _

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityCounit adj e₁ e₂
X : C
this :
  adj.counit.app ((shiftFunctor D a).obj (F.obj X)) =
    F.map (e₂.hom.app (F.obj X)) ≫ e₁.hom.app (G.obj (F.obj X)) ≫ (shiftFunctor D a).map (adj.counit.app (F.obj X))
⊢ e₁.hom.app X =
    F.map ((shiftFunctor C a).map (adj.unit.app X)) ≫
      F.map (e₂.inv.app (F.obj X)) ≫ adj.counit.app ((shiftFunctor D a).obj (F.obj X))

Tactic:
rw [← cancel_epi (F.map (e₂.inv.app _)), ← assoc, ← F.map_comp, Iso.inv_hom_id_app, F.map_id,
  id_comp] at this

Result:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityCounit adj e₁ e₂
X : C
this :
  F.map (e₂.inv.app (F.obj X)) ≫ adj.counit.app ((shiftFunctor D a).obj (F.obj X)) =
    e₁.hom.app (G.obj (F.obj X)) ≫ (shiftFunctor D a).map (adj.counit.app (F.obj X))
⊢ e₁.hom.app X =
    F.map ((shiftFunctor C a).map (adj.unit.app X)) ≫
      F.map (e₂.inv.app (F.obj X)) ≫ adj.counit.app ((shiftFunctor D a).obj (F.obj X))
-- Mathlib/NumberTheory/Divisors.lean
theorem prod_divisorsAntidiagonal' {M : Type*} [CommMonoid M] (f : ℕ → ℕ → M) {n : ℕ} :
    ∏ i ∈ n.divisorsAntidiagonal, f i.1 i.2 = ∏ i ∈ n.divisors, f (n / i) i

Proof state:
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ i ∈ n.divisorsAntidiagonal, f i.1 i.2 = ∏ i ∈ n.divisors, f (n / i) i

Tactic:
rw [← map_swap_divisorsAntidiagonal, Finset.prod_map]

Result:
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ x ∈ n.divisorsAntidiagonal, f ((Equiv.prodComm ℕ ℕ).toEmbedding x).1 ((Equiv.prodComm ℕ ℕ).toEmbedding x).2 =
    ∏ i ∈ n.divisors, f (n / i) i

Proof state:
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ x ∈ n.divisorsAntidiagonal, f ((Equiv.prodComm ℕ ℕ).toEmbedding x).1 ((Equiv.prodComm ℕ ℕ).toEmbedding x).2 =
    ∏ i ∈ n.divisors, f (n / i) i

Tactic:
exact prod_divisorsAntidiagonal fun i j => f j i

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem degree_smul_of_isRightRegular_leadingCoeff (ha : a ≠ 0)
    (hp : IsRightRegular p.leadingCoeff) : (a • p).degree = p.degree

Proof state:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ha : a ≠ 0
hp : IsRightRegular p.leadingCoeff
⊢ (a • p).coeff p.natDegree ≠ 0

Tactic:
rw [coeff_smul, coeff_natDegree, smul_eq_mul, ne_eq]

Result:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ha : a ≠ 0
hp : IsRightRegular p.leadingCoeff
⊢ ¬a * p.leadingCoeff = 0

Proof state:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ha : a ≠ 0
hp : IsRightRegular p.leadingCoeff
⊢ (a • p).degree = p.degree

Tactic:
refine le_antisymm (degree_smul_le a p) <| degree_le_degree ?_

Result:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ha : a ≠ 0
hp : IsRightRegular p.leadingCoeff
⊢ (a • p).coeff p.natDegree ≠ 0

Proof state:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ha : a ≠ 0
hp : IsRightRegular p.leadingCoeff
⊢ ¬a * p.leadingCoeff = 0

Tactic:
exact hp.mul_right_eq_zero_iff.ne.mpr ha

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma d_comp_ofHom_v (φ : F ⟶ G) (p' p q : ℤ) (hpq : p + 0 = q) :
    F.d p' p ≫ (ofHom φ).v p q hpq = F.d p' q ≫ φ.f q

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
p' p q : ℤ
hpq : p + 0 = q
⊢ F.d p' p ≫ (ofHom φ).v p q hpq = F.d p' q ≫ φ.f q

Tactic:
simp only [ofHom, d_comp_ofHoms_v]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ioo_insert_right (h : a < b) : insert b (Ioo a b) = Ioc a b

Proof state:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a < b
⊢ insert b (Ioo a b) = Ioc a b

Tactic:
rw [← coe_inj, coe_insert, coe_Ioo, coe_Ioc, Set.insert_eq, Set.union_comm, Set.Ioo_union_right h]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Card.lean
theorem compl_mem_generateMeasurableRec {s : Set (Set α)} {i j : Ordinal} (h : j < i) {t : Set α}
    (ht : t ∈ generateMeasurableRec s j) : tᶜ ∈ generateMeasurableRec s i

Proof state:
α : Type u
s : Set (Set α)
i j : Ordinal.{u_1}
h : j < i
t : Set α
ht : t ∈ generateMeasurableRec s j
⊢ tᶜ ∈ generateMeasurableRec s i

Tactic:
unfold generateMeasurableRec

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

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

Tactic:
exact mem_union_left _ (mem_union_right _ ⟨t, mem_iUnion₂.2 ⟨j, h, ht⟩, rfl⟩)

Result:
no goals
-- Mathlib/Topology/Sheaves/Stalks.lean
@[reassoc (attr := simp)]
lemma pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk
    (f : X ⟶ Y) (F : Y.Presheaf C) (U : Opens X) (x : X) (hx : x ∈ U) (V : Opens Y)
    (hV : U ≤ (Opens.map f).obj V) :
    ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫
      ((pullback C f).obj F).map (homOfLE hV).op ≫ germToPullbackStalk C f F U x hx  =
        F.germ _ (f x) (hV hx)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
F : Presheaf C Y
U : Opens ↑X
x : ↑X
hx : x ∈ U
V : Opens ↑Y
hV : U ≤ (Opens.map f).obj V
⊢ ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫
      ((pullback C f).obj F).map (homOfLE hV).op ≫ germToPullbackStalk C f F U x hx =
    F.germ V ((ConcreteCategory.hom f) x) ⋯

Tactic:
simpa [pushforwardPullbackAdjunction] using
  ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit F (op U)).fac _
    (CostructuredArrow.mk (homOfLE hV).op)

Result:
no goals
-- Mathlib/RingTheory/Congruence/Basic.lean
theorem sSup_eq_ringConGen (S : Set (RingCon R)) :
    sSup S = ringConGen fun x y => ∃ c : RingCon R, c ∈ S ∧ c x y

Proof state:
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
⊢ sSup S = sInf {s | ∀ (x y : R), (∃ c ∈ S, c x y) → s x y}

Tactic:
apply congr_arg sInf

Result:
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
⊢ upperBounds S = {s | ∀ (x y : R), (∃ c ∈ S, c x y) → s x y}

Proof state:
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
⊢ upperBounds S = {s | ∀ (x y : R), (∃ c ∈ S, c x y) → s x y}

Tactic:
ext

Result:
case h
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
x✝ : RingCon R
⊢ x✝ ∈ upperBounds S ↔ x✝ ∈ {s | ∀ (x y : R), (∃ c ∈ S, c x y) → s x y}

Proof state:
case h
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
x✝ : RingCon R
⊢ x✝ ∈ upperBounds S ↔ x✝ ∈ {s | ∀ (x y : R), (∃ c ∈ S, c x y) → s x y}

Tactic:
exact ⟨fun h _ _ ⟨r, hr⟩ => h hr.1 hr.2, fun h r hS _ _ hr => h _ _ ⟨r, hS, hr⟩⟩

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
⊢ sSup S = ringConGen fun x y => ∃ c ∈ S, c x y

Tactic:
rw [ringConGen_eq]

Result:
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
⊢ sSup S = sInf {s | ∀ (x y : R), (∃ c ∈ S, c x y) → s x y}
-- Mathlib/CategoryTheory/Adjunction/Reflective.lean
theorem unit_obj_eq_map_unit [Reflective i] (X : C) :
    (reflectorAdjunction i).unit.app (i.obj ((reflector i).obj X)) =
      i.map ((reflector i).map ((reflectorAdjunction i).unit.app X))

Proof state:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
i : D ⥤ C
inst✝ : Reflective i
X : C
⊢ (reflectorAdjunction i).unit.app (i.obj ((reflector i).obj X)) ≫
      i.map ((reflectorAdjunction i).counit.app ((reflector i).obj X)) =
    i.map
      ((reflector i).map ((reflectorAdjunction i).unit.app X) ≫
        (reflectorAdjunction i).counit.app ((reflector i).obj X))

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
i : D ⥤ C
inst✝ : Reflective i
X : C
⊢ (reflectorAdjunction i).unit.app (i.obj ((reflector i).obj X)) =
    i.map ((reflector i).map ((reflectorAdjunction i).unit.app X))

Tactic:
rw [← cancel_mono (i.map ((reflectorAdjunction i).counit.app ((reflector i).obj X))),
  ← i.map_comp]

Result:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
i : D ⥤ C
inst✝ : Reflective i
X : C
⊢ (reflectorAdjunction i).unit.app (i.obj ((reflector i).obj X)) ≫
      i.map ((reflectorAdjunction i).counit.app ((reflector i).obj X)) =
    i.map
      ((reflector i).map ((reflectorAdjunction i).unit.app X) ≫
        (reflectorAdjunction i).counit.app ((reflector i).obj X))
-- Mathlib/Tactic/Module.lean
theorem eval_cons [AddMonoid M] [SMul R M] (p : R × M) (l : NF R M) :
    (p ::ᵣ l).eval = p.1 • p.2 + l.eval

Proof state:
R : Type u_2
M : Type u_3
inst✝¹ : AddMonoid M
inst✝ : SMul R M
p : R × M
l : NF R M
⊢ ((match p with
        | (r, x) => r • x) ::
        map
          (fun x =>
            match x with
            | (r, x) => r • x)
          l).sum =
    p.1 • p.2 +
      (map
          (fun x =>
            match x with
            | (r, x) => r • x)
          l).sum

Tactic:
rw [List.sum_cons]

Result:
no goals

Proof state:
R : Type u_2
M : Type u_3
inst✝¹ : AddMonoid M
inst✝ : SMul R M
p : R × M
l : NF R M
⊢ (p ::ᵣ l).eval = p.1 • p.2 + l.eval

Tactic:
unfold eval cons

Result:
R : Type u_2
M : Type u_3
inst✝¹ : AddMonoid M
inst✝ : SMul R M
p : R × M
l : NF R M
⊢ (map
        (fun x =>
          match x with
          | (r, x) => r • x)
        (p :: l)).sum =
    p.1 • p.2 +
      (map
          (fun x =>
            match x with
            | (r, x) => r • x)
          l).sum

Proof state:
R : Type u_2
M : Type u_3
inst✝¹ : AddMonoid M
inst✝ : SMul R M
p : R × M
l : NF R M
⊢ (map
        (fun x =>
          match x with
          | (r, x) => r • x)
        (p :: l)).sum =
    p.1 • p.2 +
      (map
          (fun x =>
            match x with
            | (r, x) => r • x)
          l).sum

Tactic:
rw [List.map_cons]

Result:
R : Type u_2
M : Type u_3
inst✝¹ : AddMonoid M
inst✝ : SMul R M
p : R × M
l : NF R M
⊢ ((match p with
        | (r, x) => r • x) ::
        map
          (fun x =>
            match x with
            | (r, x) => r • x)
          l).sum =
    p.1 • p.2 +
      (map
          (fun x =>
            match x with
            | (r, x) => r • x)
          l).sum
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
/-- `binEntropy` is symmetric about 1/2. -/
@[simp] lemma binEntropy_one_sub (p : ℝ) : binEntropy (1 - p) = binEntropy p

Proof state:
p : ℝ
⊢ binEntropy (1 - p) = binEntropy p

Tactic:
simp [binEntropy, add_comm]

Result:
no goals