harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Interval/Set/SuccPred.lean
lemma Ico_succ_succ_eq_Ioc_of_not_isMax (hb : ¬ IsMax b) (a : α) :
    Ico (succ a) (succ b) = Ioc a b

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a : α
⊢ Ico (succ a) (succ b) = Ioc a b

Tactic:
rw [Ico_succ_left_eq_Ioo, Ioo_succ_right_eq_Ioc_of_not_isMax hb]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Subcanonical.lean
lemma yonedaULiftEquiv_yonedaULift_map {X Y : C} (f : X ⟶ Y) :
    (yonedaULiftEquiv.{v'} J) (J.yonedaULift.map f) = ⟨f⟩

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
f : X ⟶ Y
⊢ ((yonedaULift.{v', v, u} J).map f).val.app (op X) { down := 𝟙 X } = { down := f }

Tactic:
simp [yonedaULift]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
f : X ⟶ Y
⊢ J.yonedaULiftEquiv ((yonedaULift.{v', v, u} J).map f) = { down := f }

Tactic:
rw [yonedaULiftEquiv_apply]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
f : X ⟶ Y
⊢ ((yonedaULift.{v', v, u} J).map f).val.app (op X) { down := 𝟙 X } = { down := f }
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem isUnit_leadingCoeff_mul_left_eq_zero_iff (h : IsUnit p.leadingCoeff) {q : R[X]} :
    q * p = 0 ↔ q = 0

Proof state:
case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
⊢ 0 * p = 0

Tactic:
rw [zero_mul]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ q * p = 0 ↔ q = 0

Tactic:
constructor

Result:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ q * p = 0 → q = 0

case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ q = 0 → q * p = 0

Proof state:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ q * p = 0 → q = 0

Tactic:
intro hp

Result:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : q * p = 0
⊢ q = 0

Proof state:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : (fun x => x * C ↑h.unit⁻¹) (q * p) = (fun x => x * C ↑h.unit⁻¹) 0
⊢ q = 0

Tactic:
simp only [zero_mul] at hp

Result:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : q * p * C ↑h.unit⁻¹ = 0
⊢ q = 0

Proof state:
case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ q = 0 → q * p = 0

Tactic:
rintro rfl

Result:
case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
⊢ 0 * p = 0

Proof state:
case mp.h
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : q * (p * C ↑h.unit⁻¹) = 0
⊢ (p * C ↑h.unit⁻¹).Monic

Tactic:
refine monic_mul_C_of_leadingCoeff_mul_eq_one ?_

Result:
case mp.h
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : q * (p * C ↑h.unit⁻¹) = 0
⊢ p.leadingCoeff * ↑h.unit⁻¹ = 1

Proof state:
case mp.h
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : q * (p * C ↑h.unit⁻¹) = 0
⊢ p.leadingCoeff * ↑h.unit⁻¹ = 1

Tactic:
simp [Units.mul_inv_eq_iff_eq_mul, IsUnit.unit_spec]

Result:
no goals

Proof state:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : q * p * C ↑h.unit⁻¹ = 0
⊢ q = 0

Tactic:
rwa [mul_assoc, Monic.mul_left_eq_zero_iff] at hp

Result:
case mp.h
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : q * (p * C ↑h.unit⁻¹) = 0
⊢ (p * C ↑h.unit⁻¹).Monic
-- Mathlib/Analysis/InnerProductSpace/Defs.lean
theorem inner_self_of_eq_zero {x : F} : x = 0 → ⟪x, x⟫ = 0

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
⊢ ⟪0, 0⟫_𝕜 = 0

Tactic:
exact inner_zero_left _

Result:
no goals

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ x = 0 → ⟪x, x⟫_𝕜 = 0

Tactic:
rintro rfl

Result:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
⊢ ⟪0, 0⟫_𝕜 = 0
-- Mathlib/Tactic/Ring/Basic.lean
theorem smul_nat {a b c : ℕ} (_ : (a * b : ℕ) = c) : a • b = c

Proof state:
a b : ℕ
⊢ a • b = a * b

Tactic:
simp

Result:
no goals

Proof state:
a b c : ℕ
x✝ : a * b = c
⊢ a • b = c

Tactic:
subst_vars

Result:
a b : ℕ
⊢ a • b = a * b
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
@[simp] lemma _root_.MeasureTheory.OuterMeasure.toMeasure_zero
    [ms : MeasurableSpace α] (h : ms ≤ (0 : OuterMeasure α).caratheodory) :
    (0 : OuterMeasure α).toMeasure h = 0

Proof state:
α : Type u_1
ms : MeasurableSpace α
h : ms ≤ OuterMeasure.caratheodory 0
⊢ OuterMeasure.toMeasure 0 h = 0

Tactic:
ext s hs

Result:
case h
α : Type u_1
ms : MeasurableSpace α
h : ms ≤ OuterMeasure.caratheodory 0
s : Set α
hs : MeasurableSet s
⊢ (OuterMeasure.toMeasure 0 h) s = 0 s

Proof state:
case h
α : Type u_1
ms : MeasurableSpace α
h : ms ≤ OuterMeasure.caratheodory 0
s : Set α
hs : MeasurableSet s
⊢ (OuterMeasure.toMeasure 0 h) s = 0 s

Tactic:
simp [hs]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Ideal.lean
theorem mem_ideal_span_monomial_image_iff_dvd {x : MvPolynomial σ R} {s : Set (σ →₀ ℕ)} :
    x ∈ Ideal.span ((fun s => monomial s (1 : R)) '' s) ↔
      ∀ xi ∈ x.support, ∃ si ∈ s, monomial si 1 ∣ monomial xi (x.coeff xi)

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
xi : σ →₀ ℕ
hxi : xi ∈ x.support
⊢ (∃ si ∈ s, si ≤ xi) ↔ ∃ si ∈ s, (monomial si) 1 ∣ (monomial xi) (coeff xi x)

Tactic:
simp_rw [monomial_dvd_monomial, one_dvd, and_true, mem_support_iff.mp hxi, false_or]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
⊢ x ∈ Ideal.span ((fun s => (monomial s) 1) '' s) ↔
    ∀ xi ∈ x.support, ∃ si ∈ s, (monomial si) 1 ∣ (monomial xi) (coeff xi x)

Tactic:
refine mem_ideal_span_monomial_image.trans (forall₂_congr fun xi hxi => ?_)

Result:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
xi : σ →₀ ℕ
hxi : xi ∈ x.support
⊢ (∃ si ∈ s, si ≤ xi) ↔ ∃ si ∈ s, (monomial si) 1 ∣ (monomial xi) (coeff xi x)
-- Mathlib/Data/Sum/Interval.lean
theorem inr_mem_sumLift₂ {c₂ : γ₂} :
    inr c₂ ∈ sumLift₂ f g a b ↔ ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ c₂ ∈ g a₂ b₂

Proof state:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₂ : γ₂
⊢ ¬∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ inr c₂ = inl c₁ ∧ c₁ ∈ f a₁ b₁

Tactic:
rintro ⟨_, _, c₂, _, _, h, _⟩

Result:
case intro.intro.intro.intro.intro.intro
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₂✝ : γ₂
w✝¹ : α₁
w✝ : β₁
c₂ : γ₁
left✝¹ : a = inl w✝¹
left✝ : b = inl w✝
h : inr c₂✝ = inl c₂
right✝ : c₂ ∈ f w✝¹ w✝
⊢ False

Proof state:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₂ : γ₂
⊢ (∃ a₂ b₂ c₂_1, a = inr a₂ ∧ b = inr b₂ ∧ inr c₂ = inr c₂_1 ∧ c₂_1 ∈ g a₂ b₂) ↔
    ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ c₂ ∈ g a₂ b₂

Tactic:
simp only [inr.injEq, exists_and_left, exists_eq_left']

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₂✝ : γ₂
w✝¹ : α₁
w✝ : β₁
c₂ : γ₁
left✝¹ : a = inl w✝¹
left✝ : b = inl w✝
h : inr c₂✝ = inl c₂
right✝ : c₂ ∈ f w✝¹ w✝
⊢ False

Tactic:
exact inr_ne_inl h

Result:
no goals

Proof state:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₂ : γ₂
⊢ inr c₂ ∈ sumLift₂ f g a b ↔ ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ c₂ ∈ g a₂ b₂

Tactic:
rw [mem_sumLift₂, or_iff_right]

Result:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₂ : γ₂
⊢ (∃ a₂ b₂ c₂_1, a = inr a₂ ∧ b = inr b₂ ∧ inr c₂ = inr c₂_1 ∧ c₂_1 ∈ g a₂ b₂) ↔
    ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ c₂ ∈ g a₂ b₂

α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₂ : γ₂
⊢ ¬∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ inr c₂ = inl c₁ ∧ c₁ ∈ f a₁ b₁
-- Mathlib/Algebra/Lie/Abelian.lean
theorem coe_maxTrivLinearMapEquivLieModuleHom (f : maxTrivSubmodule R L (M →ₗ[R] N)) :
    (maxTrivLinearMapEquivLieModuleHom (M := M) (N := N) f : M → N) = f

Proof state:
case h
R : Type u
L : Type v
M : Type w
N : Type w₁
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✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : ↥(maxTrivSubmodule R L (M →ₗ[R] N))
x✝ : M
⊢ (maxTrivLinearMapEquivLieModuleHom f) x✝ = ↑f x✝

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
N : Type w₁
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✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : ↥(maxTrivSubmodule R L (M →ₗ[R] N))
⊢ ⇑(maxTrivLinearMapEquivLieModuleHom f) = ⇑↑f

Tactic:
ext

Result:
case h
R : Type u
L : Type v
M : Type w
N : Type w₁
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✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : ↥(maxTrivSubmodule R L (M →ₗ[R] N))
x✝ : M
⊢ (maxTrivLinearMapEquivLieModuleHom f) x✝ = ↑f x✝
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
@[to_additive]
lemma mul_right_inj_of_comparable [MulLeftStrictMono α] {a b c : α} (h : b ≤ c ∨ c ≤ b) :
    a * c = a * b ↔ c = b

Proof state:
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulLeftStrictMono α
a b c : α
h : b ≤ c ∨ c ≤ b
h' : ¬c = b
⊢ ¬a * c = a * b

Tactic:
obtain h | h := h

Result:
case inl
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulLeftStrictMono α
a b c : α
h' : ¬c = b
h : b ≤ c
⊢ ¬a * c = a * b

case inr
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulLeftStrictMono α
a b c : α
h' : ¬c = b
h : c ≤ b
⊢ ¬a * c = a * b

Proof state:
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulLeftStrictMono α
a b c : α
h : b ≤ c ∨ c ≤ b
h' : a * c = a * b
⊢ c = b

Tactic:
contrapose h'

Result:
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulLeftStrictMono α
a b c : α
h : b ≤ c ∨ c ≤ b
h' : ¬c = b
⊢ ¬a * c = a * b

Proof state:
case inr
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulLeftStrictMono α
a b c : α
h' : ¬c = b
h : c ≤ b
⊢ ¬a * c = a * b

Tactic:
exact mul_lt_mul_left' (h.lt_of_ne h') a |>.ne

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulLeftStrictMono α
a b c : α
h' : ¬c = b
h : b ≤ c
⊢ ¬a * c = a * b

Tactic:
exact mul_lt_mul_left' (h.lt_of_ne' h') a |>.ne'

Result:
no goals
-- Mathlib/Algebra/AddTorsor/Defs.lean
theorem pointReflection_vsub_right (x y : P) : pointReflection x y -ᵥ y = 2 • (x -ᵥ y)

Proof state:
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
x y : P
⊢ (pointReflection x) y -ᵥ y = 2 • (x -ᵥ y)

Tactic:
simp [pointReflection, two_nsmul, vadd_vsub_assoc]

Result:
no goals
-- Mathlib/Topology/GDelta/Basic.lean
theorem IsGδ.sUnion {S : Set (Set X)} (hS : S.Finite) (h : ∀ s ∈ S, IsGδ s) : IsGδ (⋃₀ S)

Proof state:
case empty
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
h : ∀ s ∈ ∅, IsGδ s
⊢ IsGδ (⋃₀ ∅)

Tactic:
simp

Result:
no goals

Proof state:
case insert
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
a✝¹ : Set X
s✝ : Set (Set X)
a✝ : a✝¹ ∉ s✝
hs✝ : s✝.Finite
ih : (∀ s ∈ s✝, IsGδ s) → IsGδ (⋃₀ s✝)
h : IsGδ a✝¹ ∧ ∀ x ∈ s✝, IsGδ x
⊢ IsGδ (a✝¹ ∪ ⋃₀ s✝)

Tactic:
exact h.1.union (ih h.2)

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hS : S.Finite
h : ∀ s ∈ S, IsGδ s
⊢ IsGδ (⋃₀ S)

Tactic:
induction S, hS using Set.Finite.induction_on with
| empty => simp
| insert _ _ ih =>
  simp only [forall_mem_insert, sUnion_insert] at *
  exact h.1.union (ih h.2)

Result:
no goals

Proof state:
case insert
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
a✝¹ : Set X
s✝ : Set (Set X)
a✝ : a✝¹ ∉ s✝
hs✝ : s✝.Finite
ih : (∀ s ∈ s✝, IsGδ s) → IsGδ (⋃₀ s✝)
h : ∀ s ∈ insert a✝¹ s✝, IsGδ s
⊢ IsGδ (⋃₀ insert a✝¹ s✝)

Tactic:
simp only [forall_mem_insert, sUnion_insert] at *

Result:
case insert
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
a✝¹ : Set X
s✝ : Set (Set X)
a✝ : a✝¹ ∉ s✝
hs✝ : s✝.Finite
ih : (∀ s ∈ s✝, IsGδ s) → IsGδ (⋃₀ s✝)
h : IsGδ a✝¹ ∧ ∀ x ∈ s✝, IsGδ x
⊢ IsGδ (a✝¹ ∪ ⋃₀ s✝)
-- Mathlib/Data/Int/Bitwise.lean
theorem testBit_bitwise (f : Bool → Bool → Bool) (m n k) :
    testBit (bitwise f m n) k = f (testBit m k) (testBit n k)

Proof state:
case ofNat.ofNat
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (match bif f false false then -[Nat.bitwise (fun x y => !f x y) a✝¹ a✝+1] else ↑(Nat.bitwise f a✝¹ a✝), k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (a✝¹.testBit k) (a✝.testBit k)

Tactic:
by_cases h : f false false <;> simp [h]

Result:
no goals

Proof state:
case ofNat.negSucc
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (match
      bif f false !false then -[Nat.bitwise (fun x y => !f x !y) a✝¹ a✝+1]
      else ↑(Nat.bitwise (fun x y => f x !y) a✝¹ a✝),
      k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (a✝¹.testBit k) !a✝.testBit k

Tactic:
by_cases h : f false true <;> simp [h]

Result:
no goals

Proof state:
case negSucc.ofNat
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (match
      bif f (!false) false then -[Nat.bitwise (fun x y => !f (!x) y) a✝¹ a✝+1]
      else ↑(Nat.bitwise (fun x y => f (!x) y) a✝¹ a✝),
      k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (!a✝¹.testBit k) (a✝.testBit k)

Tactic:
by_cases h : f true false <;> simp [h]

Result:
no goals

Proof state:
f : Bool → Bool → Bool
m n : ℤ
k : ℕ
⊢ (bitwise f m n).testBit k = f (m.testBit k) (n.testBit k)

Tactic:
cases m <;> cases n <;> simp only [testBit, bitwise, natBitwise]

Result:
case ofNat.ofNat
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (match bif f false false then -[Nat.bitwise (fun x y => !f x y) a✝¹ a✝+1] else ↑(Nat.bitwise f a✝¹ a✝), k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (a✝¹.testBit k) (a✝.testBit k)

case ofNat.negSucc
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (match
      bif f false !false then -[Nat.bitwise (fun x y => !f x !y) a✝¹ a✝+1]
      else ↑(Nat.bitwise (fun x y => f x !y) a✝¹ a✝),
      k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (a✝¹.testBit k) !a✝.testBit k

case negSucc.ofNat
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (match
      bif f (!false) false then -[Nat.bitwise (fun x y => !f (!x) y) a✝¹ a✝+1]
      else ↑(Nat.bitwise (fun x y => f (!x) y) a✝¹ a✝),
      k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (!a✝¹.testBit k) (a✝.testBit k)

case negSucc.negSucc
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (match
      bif f (!false) !false then -[Nat.bitwise (fun x y => !f (!x) !y) a✝¹ a✝+1]
      else ↑(Nat.bitwise (fun x y => f (!x) !y) a✝¹ a✝),
      k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (!a✝¹.testBit k) !a✝.testBit k

Proof state:
case negSucc.negSucc
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (match
      bif f (!false) !false then -[Nat.bitwise (fun x y => !f (!x) !y) a✝¹ a✝+1]
      else ↑(Nat.bitwise (fun x y => f (!x) !y) a✝¹ a✝),
      k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (!a✝¹.testBit k) !a✝.testBit k

Tactic:
by_cases h : f true true <;> simp [h]

Result:
no goals
-- Mathlib/Algebra/Category/Ring/Constructions.lean
lemma isPushout_tensorProduct (R A B : Type u) [CommRing R] [CommRing A] [CommRing B]
    [Algebra R A] [Algebra R B] :
    IsPushout (ofHom <| algebraMap R A) (ofHom <| algebraMap R B)
      (ofHom (S := A ⊗[R] B) <| Algebra.TensorProduct.includeLeftRingHom)
      (ofHom (S := A ⊗[R] B) <| Algebra.TensorProduct.includeRight.toRingHom) where
  w

Proof state:
case hf.a
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x✝ : ↑(of R)
⊢ (Hom.hom (ofHom (algebraMap R A) ≫ ofHom Algebra.TensorProduct.includeLeftRingHom)) x✝ =
    (Hom.hom (ofHom (algebraMap R B) ≫ ofHom Algebra.TensorProduct.includeRight.toRingHom)) x✝

Tactic:
simp

Result:
no goals

Proof state:
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ ofHom (algebraMap R A) ≫ ofHom Algebra.TensorProduct.includeLeftRingHom =
    ofHom (algebraMap R B) ≫ ofHom Algebra.TensorProduct.includeRight.toRingHom

Tactic:
ext

Result:
case hf.a
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x✝ : ↑(of R)
⊢ (Hom.hom (ofHom (algebraMap R A) ≫ ofHom Algebra.TensorProduct.includeLeftRingHom)) x✝ =
    (Hom.hom (ofHom (algebraMap R B) ≫ ofHom Algebra.TensorProduct.includeRight.toRingHom)) x✝
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Removal.lean
private lemma aux {n k : ℕ} (hk : 0 < k) (hn : k ≤ n) : n < 2 * k * (n / k)

Proof state:
n k : ℕ
hk : 0 < k
hn : k ≤ n
⊢ k ≤ k * (n / k)

Tactic:
simpa using Nat.mul_le_mul_left k ((Nat.one_le_div_iff hk).2 hn)

Result:
no goals

Proof state:
n k : ℕ
hk : 0 < k
hn : k ≤ n
⊢ n < 2 * k * (n / k)

Tactic:
rw [mul_assoc, two_mul, ← add_lt_add_iff_right (n % k), add_right_comm, add_assoc,
  mod_add_div n k, add_comm, add_lt_add_iff_right]

Result:
n k : ℕ
hk : 0 < k
hn : k ≤ n
⊢ n % k < k * (n / k)

Proof state:
n k : ℕ
hk : 0 < k
hn : k ≤ n
⊢ n % k < k * (n / k)

Tactic:
apply (mod_lt n hk).trans_le

Result:
n k : ℕ
hk : 0 < k
hn : k ≤ n
⊢ k ≤ k * (n / k)
-- Mathlib/CategoryTheory/Adjunction/PartialAdjoint.lean
lemma isRightAdjoint_of_leftAdjointObjIsDefined_eq_top
    (h : F.LeftAdjointObjIsDefined = ⊤) : F.IsRightAdjoint

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
h : F.LeftAdjointObjIsDefined = ⊤
X : C
⊢ (F ⋙ coyoneda.obj (op X)).IsCorepresentable

Tactic:
simp only [← leftAdjointObjIsDefined_iff, h, Pi.top_apply, Prop.top_eq_true]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
h : ∀ (X : C), (F ⋙ coyoneda.obj (op X)).IsCorepresentable
⊢ F.IsRightAdjoint

Tactic:
exact (Adjunction.adjunctionOfEquivLeft
  (fun X Y ↦ (F ⋙ coyoneda.obj (op X)).corepresentableBy.homEquiv)
  (fun X Y Y' g f ↦ by apply CorepresentableBy.homEquiv_comp)).isRightAdjoint

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
h : ∀ (X : C), (F ⋙ coyoneda.obj (op X)).IsCorepresentable
X : C
Y Y' : D
g : Y ⟶ Y'
f : (F ⋙ coyoneda.obj (op X)).coreprX ⟶ Y
⊢ ((fun X Y => (F ⋙ coyoneda.obj (op X)).corepresentableBy.homEquiv) X Y') (f ≫ g) =
    ((fun X Y => (F ⋙ coyoneda.obj (op X)).corepresentableBy.homEquiv) X Y) f ≫ F.map g

Tactic:
apply CorepresentableBy.homEquiv_comp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
h : F.LeftAdjointObjIsDefined = ⊤
⊢ F.IsRightAdjoint

Tactic:
replace h : ∀ X, IsCorepresentable (F ⋙ coyoneda.obj (op X)) := fun X ↦ by
  simp only [← leftAdjointObjIsDefined_iff, h, Pi.top_apply, Prop.top_eq_true]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
h : ∀ (X : C), (F ⋙ coyoneda.obj (op X)).IsCorepresentable
⊢ F.IsRightAdjoint
-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem _root_.Matrix.mem_range_scalar_iff_commute_transvectionStruct {M : Matrix n n R} :
    M ∈ Set.range (Matrix.scalar n) ↔ ∀ t : TransvectionStruct n R, Commute t.toMatrix M

Proof state:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
M : Matrix n n R
h : M ∈ Set.range ⇑(scalar n)
t : TransvectionStruct n R
⊢ Commute t.toMatrix M

Tactic:
rw [mem_range_scalar_iff_commute_stdBasisMatrix] at h

Result:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
M : Matrix n n R
h : ∀ (i j : n), i ≠ j → Commute (stdBasisMatrix i j 1) M
t : TransvectionStruct n R
⊢ Commute t.toMatrix M

Proof state:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
M : Matrix n n R
h : ∀ (i j : n), i ≠ j → Commute (stdBasisMatrix i j 1) M
t : TransvectionStruct n R
⊢ Commute (stdBasisMatrix t.i t.j t.c) M

Tactic:
convert (h _ _ t.hij).smul_left t.c using 1

Result:
case h.e'_3
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
M : Matrix n n R
h : ∀ (i j : n), i ≠ j → Commute (stdBasisMatrix i j 1) M
t : TransvectionStruct n R
⊢ stdBasisMatrix t.i t.j t.c = t.c • stdBasisMatrix t.i t.j 1

Proof state:
case h.e'_3
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
M : Matrix n n R
h : ∀ (i j : n), i ≠ j → Commute (stdBasisMatrix i j 1) M
t : TransvectionStruct n R
⊢ stdBasisMatrix t.i t.j t.c = t.c • stdBasisMatrix t.i t.j 1

Tactic:
rw [smul_stdBasisMatrix, smul_eq_mul, mul_one]

Result:
no goals

Proof state:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
M : Matrix n n R
h : ∀ (i j : n), i ≠ j → Commute (stdBasisMatrix i j 1) M
t : TransvectionStruct n R
⊢ Commute t.toMatrix M

Tactic:
refine (Commute.one_left M).add_left ?_

Result:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
M : Matrix n n R
h : ∀ (i j : n), i ≠ j → Commute (stdBasisMatrix i j 1) M
t : TransvectionStruct n R
⊢ Commute (stdBasisMatrix t.i t.j t.c) M

Proof state:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
M : Matrix n n R
⊢ M ∈ Set.range ⇑(scalar n) ↔ ∀ (t : TransvectionStruct n R), Commute t.toMatrix M

Tactic:
refine ⟨fun h t => ?_, mem_range_scalar_of_commute_transvectionStruct⟩

Result:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
M : Matrix n n R
h : M ∈ Set.range ⇑(scalar n)
t : TransvectionStruct n R
⊢ Commute t.toMatrix M
-- Mathlib/Algebra/Jordan/Basic.lean
theorem two_nsmul_lie_lmul_lmul_add_add_eq_zero (a b c : A) :
    2 • (⁅L a, L (b * c)⁆ + ⁅L b, L (c * a)⁆ + ⁅L c, L (a * b)⁆) = 0

Proof state:
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ 2 • (⁅L a, L (b * c)⁆ + ⁅L b, L (c * a)⁆ + ⁅L c, L (a * b)⁆) = 0

Tactic:
symm

Result:
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ 0 = 2 • (⁅L a, L (b * c)⁆ + ⁅L b, L (c * a)⁆ + ⁅L c, L (a * b)⁆)

Proof state:
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ 0 = ⁅L (a + b + c), L ((a + b + c) * (a + b + c))⁆

Tactic:
rw [(commute_lmul_lmul_sq (a + b + c)).lie_eq]

Result:
no goals

Proof state:
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅L (a + b + c), L ((a + b + c) * (a + b + c))⁆ = 2 • (⁅L a, L (b * c)⁆ + ⁅L b, L (c * a)⁆ + ⁅L c, L (a * b)⁆)

Tactic:
rw [aux0, aux1, aux2, aux3, nsmul_add, nsmul_add]

Result:
no goals

Proof state:
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ 0 = 2 • (⁅L a, L (b * c)⁆ + ⁅L b, L (c * a)⁆ + ⁅L c, L (a * b)⁆)

Tactic:
calc
  0 = ⁅L (a + b + c), L ((a + b + c) * (a + b + c))⁆ := by
    rw [(commute_lmul_lmul_sq (a + b + c)).lie_eq]
  _ = _ := by rw [aux0, aux1, aux2, aux3, nsmul_add, nsmul_add]

Result:
no goals