harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/CommSq.lean
lemma IsPushout.epi_shortComplex_g (h : IsPushout f g inl inr) :
    Epi h.shortComplex.g

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
h : IsPushout f g inl inr
⊢ Epi ⋯.shortComplex.g

Tactic:
rw [Preadditive.epi_iff_cancel_zero]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
h : IsPushout f g inl inr
⊢ ∀ (R : C) (g_1 : ⋯.shortComplex.X₃ ⟶ R), ⋯.shortComplex.g ≫ g_1 = 0 → g_1 = 0

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
h : IsPushout f g inl inr
R✝ : C
b : ⋯.shortComplex.X₃ ⟶ R✝
hb : ⋯.shortComplex.g ≫ b = 0
⊢ b = 0

Tactic:
exact Cofork.IsColimit.hom_ext h.isColimitCokernelCofork (by simpa using hb)

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
h : IsPushout f g inl inr
R✝ : C
b : ⋯.shortComplex.X₃ ⟶ R✝
hb : ⋯.shortComplex.g ≫ b = 0
⊢ Cofork.π ⋯.cokernelCofork ≫ b = Cofork.π ⋯.cokernelCofork ≫ 0

Tactic:
simpa using hb

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
h : IsPushout f g inl inr
⊢ ∀ (R : C) (g_1 : ⋯.shortComplex.X₃ ⟶ R), ⋯.shortComplex.g ≫ g_1 = 0 → g_1 = 0

Tactic:
intro _ b hb

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
h : IsPushout f g inl inr
R✝ : C
b : ⋯.shortComplex.X₃ ⟶ R✝
hb : ⋯.shortComplex.g ≫ b = 0
⊢ b = 0
-- Mathlib/Order/Interval/Set/OrdConnected.lean
theorem dual_ordConnected_iff {s : Set α} : OrdConnected (ofDual ⁻¹' s) ↔ OrdConnected s

Proof state:
α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ (∀ (x x_1 : { a // toDual a ∈ ⇑ofDual ⁻¹' s }), ⇑ofDual ⁻¹' Icc ↑x_1 ↑x ⊆ ⇑ofDual ⁻¹' s) ↔
    ∀ (x x_1 : { a // a ∈ s }), Icc ↑x ↑x_1 ⊆ s

Tactic:
exact forall_swap

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ (⇑ofDual ⁻¹' s).OrdConnected ↔ s.OrdConnected

Tactic:
simp_rw [ordConnected_def, toDual.surjective.forall, dual_Icc, Subtype.forall']

Result:
α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ (∀ (x x_1 : { a // toDual a ∈ ⇑ofDual ⁻¹' s }), ⇑ofDual ⁻¹' Icc ↑x_1 ↑x ⊆ ⇑ofDual ⁻¹' s) ↔
    ∀ (x x_1 : { a // a ∈ s }), Icc ↑x ↑x_1 ⊆ s
-- Mathlib/GroupTheory/Coset/Card.lean
theorem card_eq_card_quotient_mul_card_subgroup (s : Subgroup α) :
    Nat.card α = Nat.card (α ⧸ s) * Nat.card s

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ Nat.card α = Nat.card ((α ⧸ s) × ↥s)

Tactic:
exact Nat.card_congr Subgroup.groupEquivQuotientProdSubgroup

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ Nat.card α = Nat.card (α ⧸ s) * Nat.card ↥s

Tactic:
rw [← Nat.card_prod]

Result:
α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ Nat.card α = Nat.card ((α ⧸ s) × ↥s)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue_cons [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} {h} :
    getValue a (⟨k, v⟩ :: l) h = if h' : k == a then v
      else getValue a l (containsKey_of_containsKey_cons (k := k) h (Bool.eq_false_iff.2 h'))

Proof state:
case isFalse
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
k a : α
v : β
h : containsKey a (⟨k, v⟩ :: l) = true
h✝ : ¬(k == a) = true
⊢ getValue? a l = some (getValue a l ⋯)

Tactic:
exact getValue?_eq_some_getValue _

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
k a : α
v : β
h : containsKey a (⟨k, v⟩ :: l) = true
⊢ (if (k == a) = true then some v else getValue? a l) = if h : (k == a) = true then some v else some (getValue a l ⋯)

Tactic:
split

Result:
case isTrue
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
k a : α
v : β
h : containsKey a (⟨k, v⟩ :: l) = true
h✝ : (k == a) = true
⊢ some v = some v

case isFalse
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
k a : α
v : β
h : containsKey a (⟨k, v⟩ :: l) = true
h✝ : ¬(k == a) = true
⊢ getValue? a l = some (getValue a l ⋯)

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
k a : α
v : β
h : containsKey a (⟨k, v⟩ :: l) = true
⊢ getValue a (⟨k, v⟩ :: l) h = if h' : (k == a) = true then v else getValue a l ⋯

Tactic:
rw [← Option.some_inj, ← getValue?_eq_some_getValue, getValue?_cons, apply_dite Option.some,
  cond_eq_if]

Result:
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
k a : α
v : β
h : containsKey a (⟨k, v⟩ :: l) = true
⊢ (if (k == a) = true then some v else getValue? a l) = if h : (k == a) = true then some v else some (getValue a l ⋯)

Proof state:
case isTrue
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
k a : α
v : β
h : containsKey a (⟨k, v⟩ :: l) = true
h✝ : (k == a) = true
⊢ some v = some v

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioc_eq_empty_iff : Ioc a b = ∅ ↔ ¬a < b

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ Ioc a b = ∅ ↔ ¬a < b

Tactic:
rw [← not_nonempty_iff_eq_empty, not_iff_not, nonempty_Ioc]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem algHom_ext_of_eq_adjoin {S : IntermediateField F E} {s : Set E} (hS : S = adjoin F s)
    ⦃φ₁ φ₂ : S →ₐ[F] K⦄
    (h : ∀ x hx, φ₁ ⟨x, hS.ge (subset_adjoin _ _ hx)⟩ = φ₂ ⟨x, hS.ge (subset_adjoin _ _ hx)⟩) :
    φ₁ = φ₂

Proof state:
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_3
inst✝¹ : Semiring K
inst✝ : Algebra F K
S : IntermediateField F E
s : Set E
hS : S = adjoin F s
φ₁ φ₂ : ↥S →ₐ[F] K
h : ∀ (x : E) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
⊢ φ₁ = φ₂

Tactic:
subst hS

Result:
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_3
inst✝¹ : Semiring K
inst✝ : Algebra F K
s : Set E
φ₁ φ₂ : ↥(adjoin F s) →ₐ[F] K
h : ∀ (x : E) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
⊢ φ₁ = φ₂

Proof state:
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_3
inst✝¹ : Semiring K
inst✝ : Algebra F K
s : Set E
φ₁ φ₂ : ↥(adjoin F s) →ₐ[F] K
h : ∀ (x : E) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
⊢ φ₁ = φ₂

Tactic:
exact adjoin_algHom_ext F h

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNorm.lean
theorem int_lt_one_iff (m : ℤ) : padicNorm p m < 1 ↔ (p : ℤ) ∣ m

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ padicNorm p ↑m < 1 ↔ ↑p ∣ m

Tactic:
rw [← not_iff_not, ← int_eq_one_iff, eq_iff_le_not_lt]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ ¬padicNorm p ↑m < 1 ↔ padicNorm p ↑m ≤ 1 ∧ ¬padicNorm p ↑m < 1

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ ¬padicNorm p ↑m < 1 ↔ padicNorm p ↑m ≤ 1 ∧ ¬padicNorm p ↑m < 1

Tactic:
simp only [padicNorm.of_int, true_and]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem setWidth_not {x : BitVec w} (_ : k ≤ w) :
    (~~~x).setWidth k = ~~~(x.setWidth k)

Proof state:
case pred
w k : Nat
x : BitVec w
x✝ : k ≤ w
i : Nat
h : i < k
⊢ x.getLsbD i = false → i < w

Tactic:
omega

Result:
no goals

Proof state:
case pred
w k : Nat
x : BitVec w
x✝ : k ≤ w
i : Nat
h : i < k
⊢ (setWidth k (~~~x)).getLsbD i = (~~~setWidth k x).getLsbD i

Tactic:
simp [h]

Result:
case pred
w k : Nat
x : BitVec w
x✝ : k ≤ w
i : Nat
h : i < k
⊢ x.getLsbD i = false → i < w

Proof state:
w k : Nat
x : BitVec w
x✝ : k ≤ w
⊢ setWidth k (~~~x) = ~~~setWidth k x

Tactic:
ext i h

Result:
case pred
w k : Nat
x : BitVec w
x✝ : k ≤ w
i : Nat
h : i < k
⊢ (setWidth k (~~~x)).getLsbD i = (~~~setWidth k x).getLsbD i
-- Mathlib/CategoryTheory/Sites/NonabelianCohomology/H1.lean
lemma trans {γ₁ γ₂ γ₃ : OneCochain G U} {α β : ZeroCochain G U}
    (h₁₂ : OneCohomologyRelation γ₁ γ₂ α) (h₂₃ : OneCohomologyRelation γ₂ γ₃ β) :
    OneCohomologyRelation γ₁ γ₃ (β * α) := fun i j T a b ↦ by
  dsimp
  rw [map_mul, map_mul, mul_assoc, h₁₂ i j a b, ← mul_assoc,
    h₂₃ i j a b, mul_assoc]

Proof state:
C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ Grp
I : Type w'
U : I → C
γ₁ γ₂ γ₃ : OneCochain G U
α β : ZeroCochain G U
h₁₂ : OneCohomologyRelation γ₁ γ₂ α
h₂₃ : OneCohomologyRelation γ₂ γ₃ β
i j : I
T : C
a : T ⟶ U i
b : T ⟶ U j
⊢ (ConcreteCategory.hom (G.map a.op)) ((β * α) i) * γ₁.ev i j a b =
    γ₃.ev i j a b * (ConcreteCategory.hom (G.map b.op)) ((β * α) j)

Tactic:
dsimp

Result:
C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ Grp
I : Type w'
U : I → C
γ₁ γ₂ γ₃ : OneCochain G U
α β : ZeroCochain G U
h₁₂ : OneCohomologyRelation γ₁ γ₂ α
h₂₃ : OneCohomologyRelation γ₂ γ₃ β
i j : I
T : C
a : T ⟶ U i
b : T ⟶ U j
⊢ (ConcreteCategory.hom (G.map a.op)) (β i * α i) * γ₁.ev i j a b =
    γ₃.ev i j a b * (ConcreteCategory.hom (G.map b.op)) (β j * α j)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ Grp
I : Type w'
U : I → C
γ₁ γ₂ γ₃ : OneCochain G U
α β : ZeroCochain G U
h₁₂ : OneCohomologyRelation γ₁ γ₂ α
h₂₃ : OneCohomologyRelation γ₂ γ₃ β
i j : I
T : C
a : T ⟶ U i
b : T ⟶ U j
⊢ (ConcreteCategory.hom (G.map a.op)) (β i * α i) * γ₁.ev i j a b =
    γ₃.ev i j a b * (ConcreteCategory.hom (G.map b.op)) (β j * α j)

Tactic:
rw [map_mul, map_mul, mul_assoc, h₁₂ i j a b, ← mul_assoc,
  h₂₃ i j a b, mul_assoc]

Result:
no goals
-- Mathlib/Algebra/Small/Group.lean
@[to_additive (attr := simp)]
lemma equivShrink_symm_inv [Inv α] [Small α] (x : Shrink α) :
    (equivShrink α).symm x⁻¹ = ((equivShrink α).symm x)⁻¹

Proof state:
α : Type u_1
inst✝¹ : Inv α
inst✝ : Small.{u_2, u_1} α
x : Shrink.{u_2, u_1} α
⊢ (equivShrink α).symm x⁻¹ = ((equivShrink α).symm x)⁻¹

Tactic:
rw [Equiv.inv_def]

Result:
α : Type u_1
inst✝¹ : Inv α
inst✝ : Small.{u_2, u_1} α
x : Shrink.{u_2, u_1} α
⊢ (equivShrink α).symm ((equivShrink α).symm.symm ((equivShrink α).symm x)⁻¹) = ((equivShrink α).symm x)⁻¹

Proof state:
α : Type u_1
inst✝¹ : Inv α
inst✝ : Small.{u_2, u_1} α
x : Shrink.{u_2, u_1} α
⊢ (equivShrink α).symm ((equivShrink α).symm.symm ((equivShrink α).symm x)⁻¹) = ((equivShrink α).symm x)⁻¹

Tactic:
simp

Result:
no goals
-- Mathlib/Data/PNat/Prime.lean
theorem Coprime.mul {k m n : ℕ+} : m.Coprime k → n.Coprime k → (m * n).Coprime k

Proof state:
k m n : ℕ+
⊢ (↑m).Coprime ↑k → (↑n).Coprime ↑k → (m * n).Coprime k

Tactic:
rw [← coprime_coe]

Result:
k m n : ℕ+
⊢ (↑m).Coprime ↑k → (↑n).Coprime ↑k → (↑(m * n)).Coprime ↑k

Proof state:
k m n : ℕ+
⊢ (↑m).Coprime ↑k → (↑n).Coprime ↑k → (↑m * ↑n).Coprime ↑k

Tactic:
apply Nat.Coprime.mul

Result:
no goals

Proof state:
k m n : ℕ+
⊢ (↑m).Coprime ↑k → (↑n).Coprime ↑k → (↑(m * n)).Coprime ↑k

Tactic:
rw [mul_coe]

Result:
k m n : ℕ+
⊢ (↑m).Coprime ↑k → (↑n).Coprime ↑k → (↑m * ↑n).Coprime ↑k

Proof state:
k m n : ℕ+
⊢ m.Coprime k → n.Coprime k → (m * n).Coprime k

Tactic:
repeat rw [← coprime_coe]

Result:
k m n : ℕ+
⊢ (↑m).Coprime ↑k → (↑n).Coprime ↑k → (↑(m * n)).Coprime ↑k
-- Mathlib/Data/Real/Pi/Irrational.lean
/--
Auxiliary for the proof that `π` is irrational.
Prove a degree bound for `cosPoly n` by induction. Note this is where we find the value in an
explicit description of `cosPoly`.
-/
private lemma cosPoly_natDegree_le : ∀ n : ℕ, (cosPoly n).natDegree ≤ n
  | 0 => by simp [cosPoly]
  | 1 => (natDegree_monomial_le _).trans (by simp)
  | n + 2 => by
      rw [cosPoly]
      refine natDegree_add_le_of_degree_le ((natDegree_smul_le _ _).trans ?_) ?_
      · exact (cosPoly_natDegree_le (n + 1)).trans (by simp)
      exact natDegree_mul_le.trans (by simp [add_comm 2, cosPoly_natDegree_le n])

Proof state:
case refine_2
n : ℕ
⊢ ((monomial 2) (-4) * cosPoly n).natDegree ≤ n + 2

Tactic:
exact natDegree_mul_le.trans (by simp [add_comm 2, cosPoly_natDegree_le n])

Result:
no goals

Proof state:
⊢ (cosPoly 0).natDegree ≤ 0

Tactic:
simp [cosPoly]

Result:
no goals

Proof state:
n : ℕ
⊢ ((2 * (2 * ↑n + 3)) • cosPoly (n + 1) + (monomial 2) (-4) * cosPoly n).natDegree ≤ n + 2

Tactic:
refine natDegree_add_le_of_degree_le ((natDegree_smul_le _ _).trans ?_) ?_

Result:
case refine_1
n : ℕ
⊢ (cosPoly (n + 1)).natDegree ≤ n + 2

case refine_2
n : ℕ
⊢ ((monomial 2) (-4) * cosPoly n).natDegree ≤ n + 2

Proof state:
n : ℕ
⊢ (cosPoly (n + 2)).natDegree ≤ n + 2

Tactic:
rw [cosPoly]

Result:
n : ℕ
⊢ ((2 * (2 * ↑n + 3)) • cosPoly (n + 1) + (monomial 2) (-4) * cosPoly n).natDegree ≤ n + 2

Proof state:
case refine_1
n : ℕ
⊢ (cosPoly (n + 1)).natDegree ≤ n + 2

Tactic:
exact (cosPoly_natDegree_le (n + 1)).trans (by simp)

Result:
no goals

Proof state:
⊢ 1 ≤ 1

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
⊢ n + 1 ≤ n + 2

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
⊢ ((monomial 2) (-4)).natDegree + (cosPoly n).natDegree ≤ n + 2

Tactic:
simp [add_comm 2, cosPoly_natDegree_le n]

Result:
no goals
-- Mathlib/Computability/TMToPartrec.lean
theorem trStmts₁_supports' {S q K} (H₁ : (q : Λ').Supports S) (H₂ : trStmts₁ q ∪ K ⊆ S)
    (H₃ : K ⊆ S → Supports K S) : Supports (trStmts₁ q ∪ K) S

Proof state:
S : Finset Λ'
q : Λ'
K : Finset Λ'
H₁ : Λ'.Supports S q
H₃ : K ⊆ S → Supports K S
H₂ : trStmts₁ q ⊆ S ∧ K ⊆ S
⊢ Supports (trStmts₁ q ∪ K) S

Tactic:
exact supports_union.2 ⟨trStmts₁_supports H₁ H₂.1, H₃ H₂.2⟩

Result:
no goals

Proof state:
S : Finset Λ'
q : Λ'
K : Finset Λ'
H₁ : Λ'.Supports S q
H₂ : trStmts₁ q ∪ K ⊆ S
H₃ : K ⊆ S → Supports K S
⊢ Supports (trStmts₁ q ∪ K) S

Tactic:
simp only [Finset.union_subset_iff] at H₂

Result:
S : Finset Λ'
q : Λ'
K : Finset Λ'
H₁ : Λ'.Supports S q
H₃ : K ⊆ S → Supports K S
H₂ : trStmts₁ q ⊆ S ∧ K ⊆ S
⊢ Supports (trStmts₁ q ∪ K) S
-- Mathlib/Order/PartialSups.lean
protected lemma Pi.partialSups_apply {τ : Type*} {π : τ → Type*} [∀ t, SemilatticeSup (π t)]
    (f : ι → (t : τ) → π t) (i : ι) (t : τ) :
    partialSups f i t = partialSups (f · t) i

Proof state:
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
τ : Type u_3
π : τ → Type u_4
inst✝ : (t : τ) → SemilatticeSup (π t)
f : ι → (t : τ) → π t
i : ι
t : τ
⊢ (partialSups f) i t = (partialSups fun x => f x t) i

Tactic:
simp only [partialSups_apply, Finset.sup'_apply]

Result:
no goals
-- Mathlib/Data/Nat/Fib/Basic.lean
theorem fib_add_two_strictMono : StrictMono fun n => fib (n + 2)

Proof state:
⊢ StrictMono fun n => fib (n + 2)

Tactic:
refine strictMono_nat_of_lt_succ fun n => ?_

Result:
n : ℕ
⊢ fib (n + 2) < fib (n + 1 + 2)

Proof state:
n : ℕ
⊢ fib (n + 2) < fib (n + 2 + 1)

Tactic:
exact fib_lt_fib_succ (self_le_add_left _ _)

Result:
no goals

Proof state:
n : ℕ
⊢ fib (n + 2) < fib (n + 1 + 2)

Tactic:
rw [add_right_comm]

Result:
n : ℕ
⊢ fib (n + 2) < fib (n + 2 + 1)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) :
    x <<< n = x * (BitVec.twoPow w n)

Proof state:
w : Nat
x : BitVec w
n : Nat
⊢ x <<< n = x * twoPow w n

Tactic:
ext i

Result:
case pred
w : Nat
x : BitVec w
n i : Nat
a✝ : i < w
⊢ (x <<< n).getLsbD i = (x * twoPow w n).getLsbD i

Proof state:
case pred
w : Nat
x : BitVec w
n i : Nat
a✝ : i < w
⊢ (x <<< n).getLsbD i = (x * twoPow w n).getLsbD i

Tactic:
simp [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, mul_twoPow_eq_shiftLeft]

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem prod_comm' : f ×ˢ g = comap Prod.swap (g ×ˢ f)

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ f ×ˢ g = comap Prod.swap (g ×ˢ f)

Tactic:
simp only [prod_eq_inf, comap_comap, Function.comp_def, inf_comm, Prod.swap, comap_inf]

Result:
no goals
-- Mathlib/Probability/Kernel/CondDistrib.lean
theorem _root_.MeasureTheory.Integrable.norm_integral_condDistrib_map
    (hY : AEMeasurable Y μ) (hf_int : Integrable f (μ.map fun a => (X a, Y a))) :
    Integrable (fun x => ‖∫ y, f (x, y) ∂condDistrib Y X μ x‖) (μ.map X)

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝ : NormedSpace ℝ F
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a => (X a, Y a)) μ)
⊢ Integrable (fun x => ‖∫ (y : Ω), f (x, y) ∂(condDistrib Y X μ) x‖) (Measure.map X μ)

Tactic:
rw [condDistrib, ← Measure.fst_map_prod_mk₀ (X := X) hY]

Result:
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝ : NormedSpace ℝ F
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a => (X a, Y a)) μ)
⊢ Integrable (fun x => ‖∫ (y : Ω), f (x, y) ∂(Measure.map (fun a => (X a, Y a)) μ).condKernel x‖)
    (Measure.map (fun a => (X a, Y a)) μ).fst

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝ : NormedSpace ℝ F
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a => (X a, Y a)) μ)
⊢ Integrable (fun x => ‖∫ (y : Ω), f (x, y) ∂(Measure.map (fun a => (X a, Y a)) μ).condKernel x‖)
    (Measure.map (fun a => (X a, Y a)) μ).fst

Tactic:
exact hf_int.norm_integral_condKernel

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Sub.lean
theorem restrict_sub_eq_restrict_sub_restrict (h_meas_s : MeasurableSet s) :
    (μ - ν).restrict s = μ.restrict s - ν.restrict s

Proof state:
case a.refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
ν' : Measure α
h_ν'_in : μ.restrict s ≤ ν' + ν.restrict s
⊢ ν' + ⊤.restrict sᶜ ∈ {d | μ ≤ d + ν}

Tactic:
rw [mem_setOf_eq, add_right_comm, Measure.le_iff]

Result:
case a.refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
ν' : Measure α
h_ν'_in : μ.restrict s ≤ ν' + ν.restrict s
⊢ ∀ (s_1 : Set α), MeasurableSet s_1 → μ s_1 ≤ (ν' + ν + ⊤.restrict sᶜ) s_1

Proof state:
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
⊢ sInf {d | μ.restrict s ≤ d + ν.restrict s} ≤ sInf ((fun μ => μ.restrict s) '' {d | μ ≤ d + ν})

Tactic:
refine sInf_le_sInf_of_forall_exists_le ?_

Result:
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
⊢ ∀ x ∈ (fun μ => μ.restrict s) '' {d | μ ≤ d + ν}, ∃ y ∈ {d | μ.restrict s ≤ d + ν.restrict s}, y ≤ x

Proof state:
case a.refine_1.refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
ν' : Measure α
h_ν'_in : μ.restrict s ≤ ν' + ν.restrict s
t : Set α
h_meas_t : MeasurableSet t
h_mu_le_add_top : μ ≤ ν' + ν + ⊤
⊢ μ (t ∩ sᶜ) ≤ (ν' + ν + ⊤) (t ∩ sᶜ)

Tactic:
exact Measure.le_iff'.1 h_mu_le_add_top _

Result:
no goals
-- Mathlib/Data/Multiset/MapFold.lean
theorem map_congr {f g : α → β} {s t : Multiset α} :
    s = t → (∀ x ∈ t, f x = g x) → map f s = map g t

Proof state:
case h
α : Type u_1
β : Type v
f g : α → β
a✝ : List α
h : ∀ x ∈ Quot.mk (⇑(isSetoid α)) a✝, f x = g x
⊢ map f (Quot.mk (⇑(isSetoid α)) a✝) = map g (Quot.mk (⇑(isSetoid α)) a✝)

Tactic:
exact congr_arg _ (List.map_congr_left h)

Result:
no goals

Proof state:
α : Type u_1
β : Type v
f g : α → β
s t : Multiset α
⊢ s = t → (∀ x ∈ t, f x = g x) → map f s = map g t

Tactic:
rintro rfl h

Result:
α : Type u_1
β : Type v
f g : α → β
s : Multiset α
h : ∀ x ∈ s, f x = g x
⊢ map f s = map g s

Proof state:
α : Type u_1
β : Type v
f g : α → β
s : Multiset α
h : ∀ x ∈ s, f x = g x
⊢ map f s = map g s

Tactic:
induction s using Quot.inductionOn

Result:
case h
α : Type u_1
β : Type v
f g : α → β
a✝ : List α
h : ∀ x ∈ Quot.mk (⇑(isSetoid α)) a✝, f x = g x
⊢ map f (Quot.mk (⇑(isSetoid α)) a✝) = map g (Quot.mk (⇑(isSetoid α)) a✝)
-- Mathlib/GroupTheory/GroupExtension/Basic.lean
theorem exists_eq_mul_inl : ∃ n : N, σ g = σ' g * S.inl n

Proof state:
case intro
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
σ σ' : S.Section
g : G
n : N
hn : S.inl n = (σ' g)⁻¹ * σ g
⊢ ∃ n, σ g = σ' g * S.inl n

Tactic:
exact ⟨n, by rw [hn, mul_inv_cancel_left]⟩

Result:
no goals

Proof state:
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
σ σ' : S.Section
g : G
n : N
hn : S.inl n = (σ' g)⁻¹ * σ g
⊢ σ g = σ' g * S.inl n

Tactic:
rw [hn, mul_inv_cancel_left]

Result:
no goals

Proof state:
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
σ σ' : S.Section
g : G
⊢ ∃ n, σ g = σ' g * S.inl n

Tactic:
obtain ⟨n, hn⟩ := inv_mul_mem_range_inl σ' σ g

Result:
case intro
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
σ σ' : S.Section
g : G
n : N
hn : S.inl n = (σ' g)⁻¹ * σ g
⊢ ∃ n, σ g = σ' g * S.inl n
-- Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
theorem orthonormal_iff_ite [DecidableEq ι] {v : ι → E} :
    Orthonormal 𝕜 v ↔ ∀ i j, ⟪v i, v j⟫ = if i = j then (1 : 𝕜) else (0 : 𝕜)

Proof state:
case mpr.left
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
⊢ ∀ (i : ι), ‖v i‖ = 1

Tactic:
intro i

Result:
case mpr.left
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
i : ι
⊢ ‖v i‖ = 1
-- Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
theorem fst : IsBoundedLinearMap 𝕜 fun x : E × F => x.1

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ IsBoundedLinearMap 𝕜 fun x => x.1

Tactic:
refine (LinearMap.fst 𝕜 E F).isLinear.with_bound 1 fun x => ?_

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E × F
⊢ ‖(LinearMap.fst 𝕜 E F) x‖ ≤ 1 * ‖x‖

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E × F
⊢ ‖(LinearMap.fst 𝕜 E F) x‖ ≤ 1 * ‖x‖

Tactic:
rw [one_mul]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E × F
⊢ ‖(LinearMap.fst 𝕜 E F) x‖ ≤ ‖x‖

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E × F
⊢ ‖(LinearMap.fst 𝕜 E F) x‖ ≤ ‖x‖

Tactic:
exact le_max_left _ _

Result:
no goals