harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get_insert [LawfulBEq α] (h : m.1.WF) {k a : α} {v : β k} {h₁} :
    (m.insert k v).get a h₁ =
      if h₂ : k == a then
        cast (congrArg β (eq_of_beq h₂)) v
      else
        m.get a (contains_of_contains_insert _ h h₁ (Bool.eq_false_iff.2 h₂))

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k a : α
v : β k
h₁ : (m.insert k v).contains a = true
⊢ (m.insert k v).get a h₁ = if h₂ : (k == a) = true then cast ⋯ v else m.get a ⋯

Tactic:
simp_to_model [insert] using List.getValueCast_insertEntry

Result:
no goals
-- Mathlib/Order/PartialSups.lean
lemma partialSups_iff_forall {f : ι → α} (p : α → Prop)
    (hp : ∀ {a b}, p (a ⊔ b) ↔ p a ∧ p b) {i : ι} :
    p (partialSups f i) ↔ ∀ j ≤ i, p (f j)

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
⊢ p ((partialSups f) i) ↔ ∀ j ≤ i, p (f j)

Tactic:
rw [partialSups_apply, comp_sup'_eq_sup'_comp (γ := Propᵒᵈ) _ p, sup'_eq_sup]

Result:
α : Type u_1
ι : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
⊢ (Iic i).sup (p ∘ f) ↔ ∀ j ≤ i, p (f j)

α : Type u_1
ι : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
⊢ ∀ (x y : α), p (x ⊔ y) = p x ⊔ p y

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
x y : α
⊢ p (x ⊔ y) = p x ⊔ p y

Tactic:
rw [hp]

Result:
α : Type u_1
ι : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
x y : α
⊢ (p x ∧ p y) = p x ⊔ p y

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
⊢ (Iic i).inf (p ∘ f) ↔ ∀ j ≤ i, p (f j)

Tactic:
simp [Finset.inf_eq_iInf]

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
x y : α
⊢ (p x ∧ p y) = p x ⊔ p y

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
⊢ ∀ (x y : α), p (x ⊔ y) = p x ⊔ p y

Tactic:
intro x y

Result:
α : Type u_1
ι : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
x y : α
⊢ p (x ⊔ y) = p x ⊔ p y

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
⊢ (Iic i).sup (p ∘ f) ↔ ∀ j ≤ i, p (f j)

Tactic:
show (Iic i).inf (p ∘ f) ↔ _

Result:
α : Type u_1
ι : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
⊢ (Iic i).inf (p ∘ f) ↔ ∀ j ≤ i, p (f j)
-- Mathlib/Data/Fintype/Sets.lean
theorem toFinset_empty [Fintype (∅ : Set α)] : (∅ : Set α).toFinset = ∅

Proof state:
α : Type u_1
inst✝ : Fintype ↑∅
⊢ ∅.toFinset = ∅

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : Fintype ↑∅
a✝ : α
⊢ a✝ ∈ ∅.toFinset ↔ a✝ ∈ ∅

Proof state:
case h
α : Type u_1
inst✝ : Fintype ↑∅
a✝ : α
⊢ a✝ ∈ ∅.toFinset ↔ a✝ ∈ ∅

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Unbundled/Basic.lean
theorem lt_tsub_iff_right_of_le (hc : AddLECancellable c) (h : c ≤ b) :
    a < b - c ↔ a + c < b

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ b
⊢ a < b - c ↔ a + c < b

Tactic:
refine ⟨fun h' => (add_le_of_le_tsub_right_of_le h h'.le).lt_of_ne ?_, hc.lt_tsub_of_add_lt_right⟩

Result:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ b
h' : a < b - c
⊢ a + c ≠ b

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ b
h' : a < b - c
⊢ a + c ≠ b

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a c : α
hc : AddLECancellable c
h : c ≤ a + c
h' : a < a + c - c
⊢ False

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a c : α
hc : AddLECancellable c
h : c ≤ a + c
h' : a < a + c - c
⊢ False

Tactic:
exact h'.ne' hc.add_tsub_cancel_right

Result:
no goals
-- Mathlib/Order/ScottContinuity.lean
@[simp] lemma ScottContinuousOn.id : ScottContinuousOn D (id : α → α)

Proof state:
α : Type u_1
inst✝ : Preorder α
D : Set (Set α)
⊢ ScottContinuousOn D _root_.id

Tactic:
simp [ScottContinuousOn]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Contracting.lean
theorem aposteriori_dist_iterate_fixedPoint_le (x n) :
    dist (f^[n] x) (fixedPoint f hf) ≤ dist (f^[n] x) (f^[n + 1] x) / (1 - K)

Proof state:
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
n : ℕ
⊢ dist (f^[n] x) (fixedPoint f hf) ≤ dist (f^[n] x) ((f ∘ f^[n]) x) / (1 - ↑K)

Tactic:
apply hf.dist_fixedPoint_le

Result:
no goals

Proof state:
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
n : ℕ
⊢ dist (f^[n] x) (fixedPoint f hf) ≤ dist (f^[n] x) (f^[n + 1] x) / (1 - ↑K)

Tactic:
rw [iterate_succ']

Result:
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
n : ℕ
⊢ dist (f^[n] x) (fixedPoint f hf) ≤ dist (f^[n] x) ((f ∘ f^[n]) x) / (1 - ↑K)
-- Mathlib/Order/LiminfLimsup.lean
theorem limsSup_bot : limsSup (⊥ : Filter α) = ⊥ :=
  bot_unique <| sInf_le <| by simp

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
⊢ ⊥ ∈ {a | ∀ᶠ (n : α) in ⊥, n ≤ a}

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Theta.lean
theorem isTheta_const_const_iff [NeBot l] {c₁ : E''} {c₂ : F''} :
    ((fun _ : α ↦ c₁) =Θ[l] fun _ ↦ c₂) ↔ (c₁ = 0 ↔ c₂ = 0)

Proof state:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝² : NormedAddCommGroup E''
inst✝¹ : NormedAddCommGroup F''
l : Filter α
inst✝ : l.NeBot
c₁ : E''
c₂ : F''
⊢ ((fun x => c₁) =Θ[l] fun x => c₂) ↔ (c₁ = 0 ↔ c₂ = 0)

Tactic:
simpa only [IsTheta, isBigO_const_const_iff, ← iff_def] using Iff.comm

Result:
no goals
-- Mathlib/Data/Real/Pi/Bounds.lean
theorem pi_lt_d20 : π < 3.14159265358979323847

Proof state:
⊢ π < 3.14159265358979323847

Tactic:
pi_upper_bound [
  215157040700/152139002499, 936715022285/506946517009, 1760670193473/897581880893,
  2-6049918861/628200981455, 2-8543385003/3546315642356, 2-2687504973/4461606579043,
  2-1443277808/9583752057175, 2-546886849/14525765179168, 2-650597193/69121426717657,
  2-199969519/84981432264454, 2-226282901/384655467333100, 2-60729699/412934601558121,
  2-25101251/682708800188252, 2-7156464/778571703825145, 2-7524725/3274543383827551,
  2-4663362/8117442793616861, 2-1913009/13319781840326041, 2-115805/3225279830894912,
  2-708749/78957345705688293, 2-131255/58489233342660393, 2-101921/181670219085488669,
  2-44784/319302953916238627, 2-82141/2342610212364552264, 2-4609/525783249231842696,
  2-4567/2083967975041722089, 2-2273/4148770928197796067, 2-563/4110440884426500846,
  2-784/22895812812720260289, 2-1717/200571992854289218531, 2-368/171952226838388893139,
  2-149/278487845640434185590, 2-207/1547570041545500037992, 2-20/598094702046570062987,
  2-7/837332582865198088180]

Result:
no goals
-- Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
theorem fourierIntegral_iteratedFDeriv {N : ℕ∞} (hf : ContDiff ℝ N f)
    (h'f : ∀ (n : ℕ), n ≤ N → Integrable (iteratedFDeriv ℝ n f)) {n : ℕ} (hn : n ≤ N) :
    𝓕 (iteratedFDeriv ℝ n f)
      = (fun w ↦ fourierPowSMulRight (-innerSL ℝ) (𝓕 f) w n)

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : V → E
N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n f) volume
n : ℕ
hn : ↑n ≤ N
⊢ 𝓕 (iteratedFDeriv ℝ n f) = fun w => fourierPowSMulRight (-innerSL ℝ) (𝓕 f) w n

Tactic:
rw [← innerSL_real_flip V]

Result:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : V → E
N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n f) volume
n : ℕ
hn : ↑n ≤ N
⊢ 𝓕 (iteratedFDeriv ℝ n f) = fun w => fourierPowSMulRight (-(innerSL ℝ).flip) (𝓕 f) w n

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : V → E
N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n f) volume
n : ℕ
hn : ↑n ≤ N
⊢ 𝓕 (iteratedFDeriv ℝ n f) = fun w => fourierPowSMulRight (-(innerSL ℝ).flip) (𝓕 f) w n

Tactic:
exact VectorFourier.fourierIntegral_iteratedFDeriv (innerSL ℝ) hf h'f hn

Result:
no goals
-- Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean
theorem inclusionOfMooreComplexMap_f (X : SimplicialObject A) (n : ℕ) :
    (inclusionOfMooreComplexMap X).f n = (NormalizedMooreComplex.objX X n).arrow

Proof state:
A : Type u_2
inst✝¹ : Category.{u_3, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ (id
          (ChainComplex.ofHom (fun n => underlying.obj (NormalizedMooreComplex.objX X n))
            (NormalizedMooreComplex.objD X) ⋯ (fun n => X _⦋n⦌) (AlternatingFaceMapComplex.objD X) ⋯
            (fun n => (NormalizedMooreComplex.objX X n).arrow) ⋯)).f
      n =
    (NormalizedMooreComplex.objX X n).arrow

Tactic:
exact ChainComplex.ofHom_f _ _ _ _ _ _ _ _ n

Result:
no goals

Proof state:
A : Type u_2
inst✝¹ : Category.{u_3, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ (inclusionOfMooreComplexMap X).f n = (NormalizedMooreComplex.objX X n).arrow

Tactic:
dsimp only [inclusionOfMooreComplexMap]

Result:
A : Type u_2
inst✝¹ : Category.{u_3, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ (id
          (ChainComplex.ofHom (fun n => underlying.obj (NormalizedMooreComplex.objX X n))
            (NormalizedMooreComplex.objD X) ⋯ (fun n => X _⦋n⦌) (AlternatingFaceMapComplex.objD X) ⋯
            (fun n => (NormalizedMooreComplex.objX X n).arrow) ⋯)).f
      n =
    (NormalizedMooreComplex.objX X n).arrow
-- Mathlib/CategoryTheory/Localization/SmallHom.lean
lemma hasSmallLocalizedHom_iff :
    HasSmallLocalizedHom.{w} W X Y ↔ Small.{w} (L.obj X ⟶ L.obj Y)

Proof state:
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝ : L.IsLocalization W
X Y : C
h : HasSmallLocalizedHom W X Y
⊢ Small.{w, v₂} (L.obj X ⟶ L.obj Y)

Tactic:
have := h.small

Result:
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝ : L.IsLocalization W
X Y : C
h : HasSmallLocalizedHom W X Y
this : Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y)
⊢ Small.{w, v₂} (L.obj X ⟶ L.obj Y)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝ : L.IsLocalization W
X Y : C
⊢ HasSmallLocalizedHom W X Y ↔ Small.{w, v₂} (L.obj X ⟶ L.obj Y)

Tactic:
constructor

Result:
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝ : L.IsLocalization W
X Y : C
⊢ HasSmallLocalizedHom W X Y → Small.{w, v₂} (L.obj X ⟶ L.obj Y)

case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝ : L.IsLocalization W
X Y : C
⊢ Small.{w, v₂} (L.obj X ⟶ L.obj Y) → HasSmallLocalizedHom W X Y

Proof state:
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝ : L.IsLocalization W
X Y : C
⊢ HasSmallLocalizedHom W X Y → Small.{w, v₂} (L.obj X ⟶ L.obj Y)

Tactic:
intro h

Result:
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝ : L.IsLocalization W
X Y : C
h : HasSmallLocalizedHom W X Y
⊢ Small.{w, v₂} (L.obj X ⟶ L.obj Y)

Proof state:
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝ : L.IsLocalization W
X Y : C
h : Small.{w, v₂} (L.obj X ⟶ L.obj Y)
⊢ HasSmallLocalizedHom W X Y

Tactic:
exact ⟨small_map (homEquiv W W.Q L)⟩

Result:
no goals

Proof state:
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝ : L.IsLocalization W
X Y : C
⊢ Small.{w, v₂} (L.obj X ⟶ L.obj Y) → HasSmallLocalizedHom W X Y

Tactic:
intro h

Result:
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝ : L.IsLocalization W
X Y : C
h : Small.{w, v₂} (L.obj X ⟶ L.obj Y)
⊢ HasSmallLocalizedHom W X Y

Proof state:
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝ : L.IsLocalization W
X Y : C
h : HasSmallLocalizedHom W X Y
this : Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y)
⊢ Small.{w, v₂} (L.obj X ⟶ L.obj Y)

Tactic:
exact small_map (homEquiv W W.Q L).symm

Result:
no goals
-- Mathlib/Data/Int/Bitwise.lean
theorem shiftLeft_add : ∀ (m : ℤ) (n : ℕ) (k : ℤ), m <<< (n + k) = (m <<< (n : ℤ)) <<< k
  | (m : ℕ), n, (k : ℕ) =>
    congr_arg ofNat (by simp [Nat.shiftLeft_eq, Nat.pow_add, mul_assoc])
  | -[_+1], _, (k : ℕ) => congr_arg negSucc (Nat.shiftLeft'_add _ _ _ _)
  | (m : ℕ), n, -[k+1] =>
    subNatNat_elim n k.succ (fun n k i => (↑m) <<< i = (Nat.shiftLeft' false m n) >>> k)
      (fun (i n : ℕ) =>
        by dsimp; simp [← Nat.shiftLeft_sub _ , Nat.add_sub_cancel_left])
      fun i n => by
        dsimp
        simp_rw [negSucc_eq, shiftLeft_neg, Nat.shiftLeft'_false, Nat.shiftRight_add,
          ← Nat.shiftLeft_sub _ le_rfl, Nat.sub_self, Nat.shiftLeft_zero, ← shiftRight_coe_nat,
          ← shiftRight_add', Nat.cast_one]
  | -[m+1], n, -[k+1] =>
    subNatNat_elim n k.succ
      (fun n k i => -[m+1] <<< i = -[(Nat.shiftLeft' true m n) >>> k+1])
      (fun i n =>
        congr_arg negSucc <| by
          rw [← Nat.shiftLeft'_sub, Nat.add_sub_cancel_left]; apply Nat.le_add_right)
      fun i n =>
      congr_arg negSucc <| by rw [add_assoc, Nat.shiftRight_add, ← Nat.shiftLeft'_sub _ _ le_rfl,
          Nat.sub_self, Nat.shiftLeft']

Proof state:
m n✝ k i n : ℕ
⊢ Nat.shiftLeft' true m i = Nat.shiftLeft' true m (n + i) >>> n

Tactic:
rw [← Nat.shiftLeft'_sub, Nat.add_sub_cancel_left]

Result:
case a
m n✝ k i n : ℕ
⊢ n ≤ n + i

Proof state:
case a
m n✝ k i n : ℕ
⊢ n ≤ n + i

Tactic:
apply Nat.le_add_right

Result:
no goals

Proof state:
m n✝ k i n : ℕ
⊢ ↑m <<< ↑i = ↑(Nat.shiftLeft' false m (n + i) >>> n)

Tactic:
simp [← Nat.shiftLeft_sub _ , Nat.add_sub_cancel_left]

Result:
no goals

Proof state:
m n✝ k i n : ℕ
⊢ (fun n k i => ↑m <<< i = ↑(Nat.shiftLeft' false m n >>> k)) (n + i) n ↑i

Tactic:
dsimp

Result:
m n✝ k i n : ℕ
⊢ ↑m <<< ↑i = ↑(Nat.shiftLeft' false m (n + i) >>> n)

Proof state:
m n✝ k i n : ℕ
⊢ m >>> i.succ = Nat.shiftLeft' true m n >>> (n + i + 1)

Tactic:
rw [add_assoc, Nat.shiftRight_add, ← Nat.shiftLeft'_sub _ _ le_rfl,
Nat.sub_self, Nat.shiftLeft']

Result:
no goals

Proof state:
m n✝ k i n : ℕ
⊢ ↑m <<< -[i+1] = ↑(Nat.shiftLeft' false m n >>> (n + i + 1))

Tactic:
simp_rw [negSucc_eq, shiftLeft_neg, Nat.shiftLeft'_false, Nat.shiftRight_add,
  ← Nat.shiftLeft_sub _ le_rfl, Nat.sub_self, Nat.shiftLeft_zero, ← shiftRight_coe_nat,
  ← shiftRight_add', Nat.cast_one]

Result:
no goals

Proof state:
m n k : ℕ
⊢ Nat.shiftLeft' false m (n + k) = Nat.shiftLeft' false (Nat.shiftLeft' false m n) k

Tactic:
simp [Nat.shiftLeft_eq, Nat.pow_add, mul_assoc]

Result:
no goals

Proof state:
m n✝ k i n : ℕ
⊢ (fun n k i => ↑m <<< i = ↑(Nat.shiftLeft' false m n >>> k)) n (n + i + 1) -[i+1]

Tactic:
dsimp

Result:
m n✝ k i n : ℕ
⊢ ↑m <<< -[i+1] = ↑(Nat.shiftLeft' false m n >>> (n + i + 1))
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[reassoc (attr := simp)]
lemma rightHomologyIso_inv_comp_rightHomologyι :
    h.rightHomologyIso.inv ≫ S.rightHomologyι = h.ι ≫ h.opcyclesIso.inv

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
inst✝ : S.HasRightHomology
⊢ rightHomologyMap' (𝟙 S) h S.rightHomologyData ≫ S.rightHomologyData.ι = h.ι ≫ opcyclesMap' (𝟙 S) h S.rightHomologyData

Tactic:
rw [rightHomologyι_naturality']

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
inst✝ : S.HasRightHomology
⊢ h.rightHomologyIso.inv ≫ S.rightHomologyι = h.ι ≫ h.opcyclesIso.inv

Tactic:
dsimp only [rightHomologyι, rightHomologyIso, opcyclesIso, rightHomologyMapIso',
  opcyclesMapIso', Iso.refl]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
inst✝ : S.HasRightHomology
⊢ rightHomologyMap' (𝟙 S) h S.rightHomologyData ≫ S.rightHomologyData.ι = h.ι ≫ opcyclesMap' (𝟙 S) h S.rightHomologyData
-- Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean
theorem prod_add (s t : Multiset α) : prod (s + t) = prod s * prod t :=
  Quotient.inductionOn₂ s t fun l₁ l₂ => by simp

Proof state:
α : Type u_3
inst✝ : CommMonoid α
s t : Multiset α
l₁ l₂ : List α
⊢ (⟦l₁⟧ + ⟦l₂⟧).prod = prod ⟦l₁⟧ * prod ⟦l₂⟧

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem map_mono : Monotone (map f) := fun I₁ I₂ h ↦ by
  rw [SetLike.le_def] at h
  apply LieSubmodule.lieSpan_mono (Set.image_subset (⇑f) h)

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I₁ I₂ : LieIdeal R L
h : ∀ ⦃x : L⦄, x ∈ I₁ → x ∈ I₂
⊢ map f I₁ ≤ map f I₂

Tactic:
apply LieSubmodule.lieSpan_mono (Set.image_subset (⇑f) h)

Result:
no goals

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I₁ I₂ : LieIdeal R L
h : I₁ ≤ I₂
⊢ map f I₁ ≤ map f I₂

Tactic:
rw [SetLike.le_def] at h

Result:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I₁ I₂ : LieIdeal R L
h : ∀ ⦃x : L⦄, x ∈ I₁ → x ∈ I₂
⊢ map f I₁ ≤ map f I₂
-- Mathlib/GroupTheory/SpecificGroups/Dihedral.lean
lemma commutative_iff : Std.Commutative (fun x y : DihedralGroup n ↦ x * y) ↔ n = 1 ∨ n = 2 where
  mp

Proof state:
n : ℕ
⊢ n = 1 ∨ n = 2 → Std.Commutative fun x y => x * y

Tactic:
rintro (rfl | rfl) <;> exact ⟨by decide⟩

Result:
no goals

Proof state:
n : ℕ
⊢ n ≠ 1 ∧ n ≠ 2 → ¬Std.Commutative fun x y => x * y

Tactic:
rintro ⟨h1, h2⟩

Result:
case intro
n : ℕ
h1 : n ≠ 1
h2 : n ≠ 2
⊢ ¬Std.Commutative fun x y => x * y

Proof state:
case intro
n : ℕ
h1 : n ≠ 1
h2 : n ≠ 2
⊢ ¬Std.Commutative fun x y => x * y

Tactic:
exact not_commutative h1 h2

Result:
no goals

Proof state:
⊢ ∀ (a b : DihedralGroup 2), a * b = b * a

Tactic:
decide

Result:
no goals

Proof state:
n : ℕ
⊢ (Std.Commutative fun x y => x * y) → n = 1 ∨ n = 2

Tactic:
contrapose!

Result:
n : ℕ
⊢ n ≠ 1 ∧ n ≠ 2 → ¬Std.Commutative fun x y => x * y
-- Mathlib/Data/Ordmap/Ordset.lean
theorem insert.valid [IsTotal α (· ≤ ·)] [DecidableRel (α := α) (· ≤ ·)] (x : α) {t} (h : Valid t) :
    Valid (Ordnode.insert x t)

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : IsTotal α fun x1 x2 => x1 ≤ x2
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
t : Ordnode α
h : t.Valid
⊢ (insertWith (fun x_1 => x) x t).Valid

Tactic:
exact insertWith.valid _ _ (fun _ _ => ⟨le_rfl, le_rfl⟩) h

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : IsTotal α fun x1 x2 => x1 ≤ x2
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
t : Ordnode α
h : t.Valid
⊢ (Ordnode.insert x t).Valid

Tactic:
rw [insert_eq_insertWith]

Result:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : IsTotal α fun x1 x2 => x1 ≤ x2
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
t : Ordnode α
h : t.Valid
⊢ (insertWith (fun x_1 => x) x t).Valid
-- Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
theorem pullback_fst_map_snd_isPullback :
    IsPullback (fst _ _ ≫ i₁ ≫ fst _ _)
      (map i₁ i₂ (i₁ ≫ snd _ _) (i₂ ≫ snd _ _) _ _ _
        (Category.id_comp _).symm (Category.id_comp _).symm)
      (diagonal f)
      (map (i₁ ≫ snd _ _) (i₂ ≫ snd _ _) f f (i₁ ≫ fst _ _) (i₂ ≫ fst _ _) i (by simp [condition])
        (by simp [condition])) :=
  IsPullback.of_iso_pullback ⟨by ext <;> simp [condition_assoc]⟩
    (pullbackDiagonalMapIso f i i₁ i₂).symm (pullbackDiagonalMapIso.inv_fst f i i₁ i₂)
    (by aesop_cat)

Proof state:
C : Type u_1
inst✝² : Category.{?u.739784, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (i₁ ≫ snd f i) ≫ i = (i₁ ≫ fst f i) ≫ f

Tactic:
simp [condition]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (pullbackDiagonalMapIso f i i₁ i₂).symm.hom ≫
      snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) =
    map i₁ i₂ (i₁ ≫ snd f i) (i₂ ≫ snd f i) (𝟙 V₁) (𝟙 V₂) (snd f i) ⋯ ⋯

Tactic:
aesop_cat

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{?u.739784, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (i₂ ≫ snd f i) ≫ i = (i₂ ≫ fst f i) ≫ f

Tactic:
simp [condition]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (fst i₁ i₂ ≫ i₁ ≫ fst f i) ≫ diagonal f =
    map i₁ i₂ (i₁ ≫ snd f i) (i₂ ≫ snd f i) (𝟙 V₁) (𝟙 V₂) (snd f i) ⋯ ⋯ ≫
      map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯

Tactic:
ext <;> simp [condition_assoc]

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem orderOf_dvd_iff_pow_eq_one {n : ℕ} : orderOf x ∣ n ↔ x ^ n = 1 :=
  ⟨fun h => by rw [← pow_mod_orderOf, Nat.mod_eq_zero_of_dvd h, _root_.pow_zero],
    orderOf_dvd_of_pow_eq_one⟩

Proof state:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : orderOf x ∣ n
⊢ x ^ n = 1

Tactic:
rw [← pow_mod_orderOf, Nat.mod_eq_zero_of_dvd h, _root_.pow_zero]

Result:
no goals