harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Complement.lean
theorem mem_rightTransversals_iff_existsUnique_quotient_mk''_eq :
    S ∈ rightTransversals (H : Set G) ↔
      ∀ q : Quotient (QuotientGroup.rightRel H), ∃! s : S, Quotient.mk'' s.1 = q

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
S : Set G
⊢ S ∈ rightTransversals ↑H ↔ ∀ (q : Quotient (QuotientGroup.rightRel H)), ∃! s, Quotient.mk'' ↑s = q

Tactic:
simp_rw [mem_rightTransversals_iff_existsUnique_mul_inv_mem, SetLike.mem_coe, ←
  QuotientGroup.rightRel_apply, ← Quotient.eq'']

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
S : Set G
⊢ (∀ (g : G), ∃! s, Quotient.mk'' ↑s = Quotient.mk'' g) ↔
    ∀ (q : Quotient (QuotientGroup.rightRel H)), ∃! s, Quotient.mk'' ↑s = q

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
S : Set G
⊢ (∀ (g : G), ∃! s, Quotient.mk'' ↑s = Quotient.mk'' g) ↔
    ∀ (q : Quotient (QuotientGroup.rightRel H)), ∃! s, Quotient.mk'' ↑s = q

Tactic:
exact ⟨fun h q => Quotient.inductionOn' q h, fun h g => h (Quotient.mk'' g)⟩

Result:
no goals
-- Mathlib/Tactic/NormNum/IsCoprime.lean
theorem int_not_isCoprime_helper (x y : ℤ) (d : ℕ) (hd : Int.gcd x y = d)
    (h : Nat.beq d 1 = false) : ¬ IsCoprime x y

Proof state:
x y : ℤ
d : ℕ
hd : x.gcd y = d
h : d.beq 1 = false
⊢ ¬d = 1

Tactic:
exact Nat.ne_of_beq_eq_false h

Result:
no goals

Proof state:
x y : ℤ
d : ℕ
hd : x.gcd y = d
h : d.beq 1 = false
⊢ ¬IsCoprime x y

Tactic:
rw [Int.isCoprime_iff_gcd_eq_one, hd]

Result:
x y : ℤ
d : ℕ
hd : x.gcd y = d
h : d.beq 1 = false
⊢ ¬d = 1
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
lemma homologyMap_eq :
    homologyMap φ = h₁.homologyIso.hom ≫ γ.φH ≫ h₂.homologyIso.inv

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
⊢ leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left =
    (leftHomologyMap' (𝟙 S₁) S₁.homologyData.left S₁.leftHomologyData ≫
        leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData h₁) ≫
      γ.φH ≫
        leftHomologyMap' (𝟙 S₂) h₂ S₂.leftHomologyData ≫
          leftHomologyMap' (𝟙 S₂) S₂.leftHomologyData S₂.homologyData.left

Tactic:
simp only [← γ.leftHomologyMap'_eq, ← leftHomologyMap'_comp, id_comp, comp_id]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
⊢ homologyMap φ = h₁.homologyIso.hom ≫ γ.φH ≫ h₂.homologyIso.inv

Tactic:
dsimp [homologyMap, LeftHomologyData.homologyIso, leftHomologyIso,
  LeftHomologyData.leftHomologyIso, homologyMap']

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
⊢ leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left =
    (leftHomologyMap' (𝟙 S₁) S₁.homologyData.left S₁.leftHomologyData ≫
        leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData h₁) ≫
      γ.φH ≫
        leftHomologyMap' (𝟙 S₂) h₂ S₂.leftHomologyData ≫
          leftHomologyMap' (𝟙 S₂) S₂.leftHomologyData S₂.homologyData.left
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem exists_lt_succ_left {p : Nat → Prop} :
    (∃ m, m < n + 1 ∧ p m) ↔ p 0 ∨ (∃ m, m < n ∧ p (m + 1))

Proof state:
n : Nat
p : Nat → Prop
⊢ (∃ m, m < n + 1 ∧ p m) ↔ p 0 ∨ ∃ m, m < n ∧ p (m + 1)

Tactic:
simpa using exists_lt_succ_left' (p := fun m _ => p m)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem dvd_iff_dvd_of_dvd_add {a b c : Int} (H : a ∣ b + c) : a ∣ b ↔ a ∣ c

Proof state:
a b c : Int
H : a ∣ b + c
⊢ a ∣ b ↔ a ∣ c

Tactic:
rw [← Int.sub_neg] at H

Result:
a b c : Int
H : a ∣ b - -c
⊢ a ∣ b ↔ a ∣ c

Proof state:
a b c : Int
H : a ∣ b - -c
⊢ a ∣ b ↔ a ∣ c

Tactic:
rw [Int.dvd_iff_dvd_of_dvd_sub H, Int.dvd_neg]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
theorem LinearMap.toMatrix₂'_mul (B : (n → R) →ₗ[R] (m → R) →ₗ[R] R) (M : Matrix m m' R) :
    toMatrix₂' R B * M = toMatrix₂' R (B.compl₂ <| toLin' M)

Proof state:
n : Type u_11
m : Type u_12
m' : Type u_14
R : Type u_16
inst✝⁶ : CommSemiring R
inst✝⁵ : Fintype n
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : DecidableEq m
inst✝¹ : Fintype m'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
M : Matrix m m' R
⊢ (toMatrix₂' R) B * M = (toMatrix₂' R) (B.compl₂ (toLin' M))

Tactic:
simp only [B.toMatrix₂'_compl₂, toMatrix'_toLin']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/FinRange.lean
theorem finRange_zero : finRange 0 = []

Proof state:
⊢ finRange 0 = []

Tactic:
simp [finRange, ofFn]

Result:
no goals
-- Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean
theorem u_compact_support : HasCompactSupport (u : E → ℝ)

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
⊢ IsCompact (closedBall 0 1)

Tactic:
exact isCompact_closedBall _ _

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
⊢ HasCompactSupport u

Tactic:
rw [hasCompactSupport_def, u_support, closure_ball (0 : E) one_ne_zero]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
⊢ IsCompact (closedBall 0 1)
-- Mathlib/Analysis/Analytic/CPolynomialDef.lean
theorem FormalMultilinearSeries.sum_of_finite (p : FormalMultilinearSeries 𝕜 E F)
    {n : ℕ} (hn : ∀ m, n ≤ m → p m = 0) (x : E) :
    p.sum x = p.partialSum n x :=
  tsum_eq_sum fun m hm ↦ by rw [Finset.mem_range, not_lt] at hm; rw [hn m hm]; rfl

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x : E
m : ℕ
hm : n ≤ m
⊢ (0 fun x_1 => x) = 0

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x : E
m : ℕ
hm : n ≤ m
⊢ ((p m) fun x_1 => x) = 0

Tactic:
rw [hn m hm]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x : E
m : ℕ
hm : n ≤ m
⊢ (0 fun x_1 => x) = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x : E
m : ℕ
hm : m ∉ Finset.range n
⊢ ((p m) fun x_1 => x) = 0

Tactic:
rw [Finset.mem_range, not_lt] at hm

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x : E
m : ℕ
hm : n ≤ m
⊢ ((p m) fun x_1 => x) = 0
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem equiv_refl : b.equiv b (Equiv.refl ι) = LinearEquiv.refl R M :=
  b.ext' fun i => by simp

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
i : ι
⊢ (b.equiv b (Equiv.refl ι)) (b i) = (LinearEquiv.refl R M) (b i)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Module/Presentation/Basic.lean
@[simp]
lemma postcomp_uniq : solution.postcomp (uniq h h').toLinearMap = solution'

Proof state:
A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
solution' : relations.Solution N
h' : solution'.IsPresentation
⊢ solution.postcomp ↑(h.uniq h') = solution'

Tactic:
simp [uniq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem add_mul_mod_self_right (x y z : Nat) : (x + y * z) % z = x % z

Proof state:
x y z : Nat
⊢ (x + y * z) % z = x % z

Tactic:
rw [Nat.mul_comm, add_mul_mod_self_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem erase_append [LawfulBEq α] {a : α} {l₁ l₂ : Array α} :
    (l₁ ++ l₂).erase a = if a ∈ l₁ then l₁.erase a ++ l₂ else l₁ ++ l₂.erase a

Proof state:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₂ : Array α
l₁ : List α
⊢ ({ toList := l₁ } ++ l₂).erase a =
    if a ∈ { toList := l₁ } then { toList := l₁ }.erase a ++ l₂ else { toList := l₁ } ++ l₂.erase a

Tactic:
rcases l₂ with ⟨l₂⟩

Result:
case mk.mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ l₂ : List α
⊢ ({ toList := l₁ } ++ { toList := l₂ }).erase a =
    if a ∈ { toList := l₁ } then { toList := l₁ }.erase a ++ { toList := l₂ }
    else { toList := l₁ } ++ { toList := l₂ }.erase a

Proof state:
case mk.mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ l₂ : List α
⊢ ({ toList := l₁ } ++ { toList := l₂ }).erase a =
    if a ∈ { toList := l₁ } then { toList := l₁ }.erase a ++ { toList := l₂ }
    else { toList := l₁ } ++ { toList := l₂ }.erase a

Tactic:
simp only [List.append_toArray, List.erase_toArray, List.erase_append, mem_toArray]

Result:
case mk.mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ l₂ : List α
⊢ (if a ∈ l₁ then l₁.erase a ++ l₂ else l₁ ++ l₂.erase a).toArray =
    if a ∈ l₁ then (l₁.erase a ++ l₂).toArray else (l₁ ++ l₂.erase a).toArray

Proof state:
case mk.mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ l₂ : List α
⊢ (if a ∈ l₁ then l₁.erase a ++ l₂ else l₁ ++ l₂.erase a).toArray =
    if a ∈ l₁ then (l₁.erase a ++ l₂).toArray else (l₁ ++ l₂.erase a).toArray

Tactic:
split <;> simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ l₂ : Array α
⊢ (l₁ ++ l₂).erase a = if a ∈ l₁ then l₁.erase a ++ l₂ else l₁ ++ l₂.erase a

Tactic:
rcases l₁ with ⟨l₁⟩

Result:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₂ : Array α
l₁ : List α
⊢ ({ toList := l₁ } ++ l₂).erase a =
    if a ∈ { toList := l₁ } then { toList := l₁ }.erase a ++ l₂ else { toList := l₁ } ++ l₂.erase a
-- Mathlib/CategoryTheory/LiftingProperties/Basic.lean
theorem iff_of_arrow_iso_right {A B X Y X' Y' : C} (i : A ⟶ B) {p : X ⟶ Y} {p' : X' ⟶ Y'}
    (e : Arrow.mk p ≅ Arrow.mk p') : HasLiftingProperty i p ↔ HasLiftingProperty i p'

Proof state:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y X' Y' : C
i : A ⟶ B
p : X ⟶ Y
p' : X' ⟶ Y'
e : Arrow.mk p ≅ Arrow.mk p'
a✝ : HasLiftingProperty i p
⊢ HasLiftingProperty i p'

case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y X' Y' : C
i : A ⟶ B
p : X ⟶ Y
p' : X' ⟶ Y'
e : Arrow.mk p ≅ Arrow.mk p'
a✝ : HasLiftingProperty i p'
⊢ HasLiftingProperty i p

Tactic:
exacts [of_arrow_iso_right i e, of_arrow_iso_right i e.symm]

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y X' Y' : C
i : A ⟶ B
p : X ⟶ Y
p' : X' ⟶ Y'
e : Arrow.mk p ≅ Arrow.mk p'
⊢ HasLiftingProperty i p ↔ HasLiftingProperty i p'

Tactic:
constructor <;> intro

Result:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y X' Y' : C
i : A ⟶ B
p : X ⟶ Y
p' : X' ⟶ Y'
e : Arrow.mk p ≅ Arrow.mk p'
a✝ : HasLiftingProperty i p
⊢ HasLiftingProperty i p'

case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y X' Y' : C
i : A ⟶ B
p : X ⟶ Y
p' : X' ⟶ Y'
e : Arrow.mk p ≅ Arrow.mk p'
a✝ : HasLiftingProperty i p'
⊢ HasLiftingProperty i p
-- Mathlib/Data/Finset/Insert.lean
theorem coe_eq_singleton {s : Finset α} {a : α} : (s : Set α) = {a} ↔ s = {a}

Proof state:
α : Type u_1
s : Finset α
a : α
⊢ ↑s = {a} ↔ s = {a}

Tactic:
rw [← coe_singleton, coe_inj]

Result:
no goals
-- Mathlib/Analysis/Normed/Operator/Banach.lean
lemma _root_.ContinuousLinearMap.isUnit_iff_bijective {f : E →L[𝕜] E} :
    IsUnit f ↔ Bijective f

Proof state:
case mpr
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
⊢ Bijective ⇑f → IsUnit f

Tactic:
refine fun h ↦ ⟨toUnit <| .ofBijective f ?_ ?_, rfl⟩ <;>
simp only [LinearMap.range_eq_top, LinearMapClass.ker_eq_bot, h.1, h.2]

Result:
no goals

Proof state:
case mp.intro
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : (E →L[𝕜] E)ˣ
⊢ Bijective ⇑↑f

Tactic:
exact ofUnit f |>.bijective

Result:
no goals

Proof state:
case mp
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
⊢ IsUnit f → Bijective ⇑f

Tactic:
rintro ⟨f, rfl⟩

Result:
case mp.intro
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : (E →L[𝕜] E)ˣ
⊢ Bijective ⇑↑f

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
⊢ IsUnit f ↔ Bijective ⇑f

Tactic:
constructor

Result:
case mp
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
⊢ IsUnit f → Bijective ⇑f

case mpr
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
⊢ Bijective ⇑f → IsUnit f
-- Mathlib/Algebra/Order/Floor.lean
lemma ceil_le_mul (hb : 1 < b) (hba : ⌈(b - 1)⁻¹⌉ / b ≤ a) : ⌈a⌉ ≤ b * a

Proof state:
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a b : k
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉ / b ≤ a
⊢ ↑⌈a⌉ ≤ b * a

Tactic:
obtain rfl | hba := hba.eq_or_lt

Result:
case inl
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉ / b ≤ ↑⌈(b - 1)⁻¹⌉ / b
⊢ ↑⌈↑⌈(b - 1)⁻¹⌉ / b⌉ ≤ b * (↑⌈(b - 1)⁻¹⌉ / b)

case inr
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a b : k
hb : 1 < b
hba✝ : ↑⌈(b - 1)⁻¹⌉ / b ≤ a
hba : ↑⌈(b - 1)⁻¹⌉ / b < a
⊢ ↑⌈a⌉ ≤ b * a

Proof state:
case inl.hb
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉ / b ≤ ↑⌈(b - 1)⁻¹⌉ / b
⊢ b ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
case inl
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉ / b ≤ ↑⌈(b - 1)⁻¹⌉ / b
⊢ ↑⌈↑⌈(b - 1)⁻¹⌉ / b⌉ ≤ b * (↑⌈(b - 1)⁻¹⌉ / b)

Tactic:
rw [ceil_div_ceil_inv_sub_one hb.le, mul_div_cancel₀]

Result:
case inl.hb
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b : k
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉ / b ≤ ↑⌈(b - 1)⁻¹⌉ / b
⊢ b ≠ 0

Proof state:
case inr
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a b : k
hb : 1 < b
hba✝ : ↑⌈(b - 1)⁻¹⌉ / b ≤ a
hba : ↑⌈(b - 1)⁻¹⌉ / b < a
⊢ ↑⌈a⌉ ≤ b * a

Tactic:
exact (ceil_lt_mul hb hba).le

Result:
no goals
-- Mathlib/Algebra/Group/Int/Even.lean
lemma two_not_dvd_two_mul_add_one (n : ℤ) : ¬2 ∣ 2 * n + 1

Proof state:
n : ℤ
⊢ ¬2 ∣ 2 * n + 1

Tactic:
simp [add_emod]

Result:
no goals
-- Mathlib/Data/DFinsupp/Order.lean
theorem support_inf_union_support_sup : (f ⊓ g).support ∪ (f ⊔ g).support = f.support ∪ g.support :=
  coe_injective <| compl_injective <| by ext; simp [inf_eq_and_sup_eq_iff]

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → Zero (α i)
inst✝² : (i : ι) → Lattice (α i)
f g : Π₀ (i : ι), α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
⊢ (↑((f ⊓ g).support ∪ (f ⊔ g).support))ᶜ = (↑(f.support ∪ g.support))ᶜ

Tactic:
ext

Result:
case h
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → Zero (α i)
inst✝² : (i : ι) → Lattice (α i)
f g : Π₀ (i : ι), α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x✝ : ι
⊢ x✝ ∈ (↑((f ⊓ g).support ∪ (f ⊔ g).support))ᶜ ↔ x✝ ∈ (↑(f.support ∪ g.support))ᶜ

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → Zero (α i)
inst✝² : (i : ι) → Lattice (α i)
f g : Π₀ (i : ι), α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x✝ : ι
⊢ x✝ ∈ (↑((f ⊓ g).support ∪ (f ⊔ g).support))ᶜ ↔ x✝ ∈ (↑(f.support ∪ g.support))ᶜ

Tactic:
simp [inf_eq_and_sup_eq_iff]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem coeff_ne_zero_C {a : R} {n : ℕ} (h : n ≠ 0) : coeff R n (C R a) = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
a : R
n : ℕ
h : n ≠ 0
⊢ (coeff R n) ((C R) a) = 0

Tactic:
rw [coeff_C, if_neg h]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/ExtendHomology.lean
@[reassoc (attr := simp)]
lemma extendCyclesIso_hom_naturality :
    cyclesMap (extendMap φ e) j' ≫ (L.extendCyclesIso e hj').hom =
      (K.extendCyclesIso e hj').hom ≫ cyclesMap φ j

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁶ : Category.{u_4, u_3} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasZeroObject C
K L : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝³ : K.HasHomology j
inst✝² : L.HasHomology j
inst✝¹ : (K.extend e).HasHomology j'
inst✝ : (L.extend e).HasHomology j'
⊢ cyclesMap (extendMap φ e) j' ≫ (L.extendCyclesIso e hj').hom = (K.extendCyclesIso e hj').hom ≫ cyclesMap φ j

Tactic:
simp [← cancel_mono (L.iCycles j), extendMap_f φ e hj']

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem sup_iSup [Nonempty ι] {f : ι → α} {a : α} : (a ⊔ ⨆ x, f x) = ⨆ x, a ⊔ f x

Proof state:
α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
inst✝ : Nonempty ι
f : ι → α
a : α
⊢ a ⊔ ⨆ x, f x = ⨆ x, a ⊔ f x

Tactic:
rw [iSup_sup_eq, iSup_const]

Result:
no goals
-- Mathlib/Data/PFun.lean
theorem mem_prodLift {f : α →. β} {g : α →. γ} {x : α} {y : β × γ} :
    y ∈ f.prodLift g x ↔ y.1 ∈ f x ∧ y.2 ∈ g x

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α →. β
g : α →. γ
x : α
y : β × γ
⊢ y ∈ f.prodLift g x ↔ ∃ (hp : (f x).Dom) (hq : (g x).Dom), (f x).get hp = y.1 ∧ (g x).get hq = y.2

Tactic:
simp only [prodLift, Part.mem_mk_iff, And.exists, Prod.ext_iff]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α →. β
g : α →. γ
x : α
y : β × γ
⊢ y ∈ f.prodLift g x ↔ y.1 ∈ f x ∧ y.2 ∈ g x

Tactic:
trans ∃ hp hq, (f x).get hp = y.1 ∧ (g x).get hq = y.2

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α →. β
g : α →. γ
x : α
y : β × γ
⊢ y ∈ f.prodLift g x ↔ ∃ (hp : (f x).Dom) (hq : (g x).Dom), (f x).get hp = y.1 ∧ (g x).get hq = y.2

α : Type u_1
β : Type u_2
γ : Type u_3
f : α →. β
g : α →. γ
x : α
y : β × γ
⊢ (∃ (hp : (f x).Dom) (hq : (g x).Dom), (f x).get hp = y.1 ∧ (g x).get hq = y.2) ↔ y.1 ∈ f x ∧ y.2 ∈ g x

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α →. β
g : α →. γ
x : α
y : β × γ
⊢ (∃ (hp : (f x).Dom) (hq : (g x).Dom), (f x).get hp = y.1 ∧ (g x).get hq = y.2) ↔ y.1 ∈ f x ∧ y.2 ∈ g x

Tactic:
simp only [exists_and_left, exists_and_right, Membership.mem, Part.Mem]

Result:
no goals
-- Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean
@[reassoc (attr := simp)]
lemma ι_colimitIsoColimitGrothendieck_inv (X : Grothendieck (CostructuredArrow.functor L)) :
    colimit.ι (CostructuredArrow.grothendieckProj L ⋙ G) X ≫
      (colimitIsoColimitGrothendieck L G).inv =
    colimit.ι G ((CostructuredArrow.proj L X.base).obj X.fiber)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Category.{u_4, u_2} D
L : C ⥤ D
H : Type u_3
inst✝³ : Category.{u_6, u_3} H
G : C ⥤ H
inst✝² : L.HasPointwiseLeftKanExtension G
inst✝¹ : HasColimitsOfShape D H
inst✝ : HasColimitsOfShape C H
X : Grothendieck (CostructuredArrow.functor L)
⊢ colimit.ι (CostructuredArrow.grothendieckProj L ⋙ G) X ≫ (L.colimitIsoColimitGrothendieck G).inv =
    colimit.ι G ((CostructuredArrow.proj L X.base).obj X.fiber)

Tactic:
simp [colimitIsoColimitGrothendieck]

Result:
no goals
-- Mathlib/GroupTheory/Schreier.lean
theorem closure_mul_image_eq_top' [DecidableEq G] {R S : Finset G}
    (hR : IsComplement (H : Set G) R) (hR1 : (1 : G) ∈ R)
    (hS : closure (S : Set G) = ⊤) :
    closure (((R * S).image fun g => ⟨_, hR.mul_inv_toRightFun_mem g⟩ : Finset H) : Set H) = ⊤

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : DecidableEq G
R S : Finset G
hR : IsComplement ↑H ↑R
hR1 : 1 ∈ R
hS : closure ↑S = ⊤
⊢ closure ↑(Finset.image (fun g => ⟨g * (↑(hR.toRightFun g))⁻¹, ⋯⟩) (R * S)) = ⊤

Tactic:
rw [Finset.coe_image, Finset.coe_mul]

Result:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : DecidableEq G
R S : Finset G
hR : IsComplement ↑H ↑R
hR1 : 1 ∈ R
hS : closure ↑S = ⊤
⊢ closure ((fun g => ⟨g * (↑(hR.toRightFun g))⁻¹, ⋯⟩) '' (↑R * ↑S)) = ⊤

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : DecidableEq G
R S : Finset G
hR : IsComplement ↑H ↑R
hR1 : 1 ∈ R
hS : closure ↑S = ⊤
⊢ closure ((fun g => ⟨g * (↑(hR.toRightFun g))⁻¹, ⋯⟩) '' (↑R * ↑S)) = ⊤

Tactic:
exact closure_mul_image_eq_top hR hR1 hS

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem mixedEmbedding_preimageOfMemIntegerSet (a : integerSet K) :
    mixedEmbedding K (preimageOfMemIntegerSet a : 𝓞 K) = (a : mixedSpace K)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
⊢ (mixedEmbedding K) ↑↑(preimageOfMemIntegerSet a) = ↑a

Tactic:
rw [preimageOfMemIntegerSet, (mem_integerSet.mp a.prop).2.choose_spec]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorPower/Pairing.lean
theorem multilinearMapToDual_apply_tprod (f : (_ : Fin n) → Module.Dual R M) (v : Fin n → M) :
    multilinearMapToDual R M n f (tprod _ v) = ∏ i, (f i (v i))

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
f : Fin n → Module.Dual R M
v : Fin n → M
⊢ ((multilinearMapToDual R M n) f) ((tprod R) v) = ∏ i : Fin n, (f i) (v i)

Tactic:
simp [multilinearMapToDual]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem thickening_singleton (δ : ℝ) (x : X) : thickening δ ({x} : Set X) = ball x δ

Proof state:
case h
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
x x✝ : X
⊢ x✝ ∈ thickening δ {x} ↔ x✝ ∈ ball x δ

Tactic:
simp [mem_thickening_iff]

Result:
no goals

Proof state:
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
x : X
⊢ thickening δ {x} = ball x δ

Tactic:
ext

Result:
case h
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
x x✝ : X
⊢ x✝ ∈ thickening δ {x} ↔ x✝ ∈ ball x δ
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem ofList_singleton {k : α} {v : β k} :
    ofList [⟨k, v⟩] = (∅ : Raw α β).insert k v

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
k : α
v : β k
⊢ ofList [⟨k, v⟩] = ∅.insert k v

Tactic:
simp_to_raw

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
k : α
v : β k
⊢ (Raw₀.empty.insertMany [⟨k, v⟩]).val.val = (Raw₀.insert ⟨Raw₀.empty.val, ⋯⟩ k v).val

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
k : α
v : β k
⊢ (Raw₀.empty.insertMany [⟨k, v⟩]).val.val = (Raw₀.insert ⟨Raw₀.empty.val, ⋯⟩ k v).val

Tactic:
rw [Raw₀.insertMany_empty_list_singleton]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem insert_replicate_self {a : α} (h : 0 < n) : (replicate n a).insert a = replicate n a

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
n : Nat
a : α
h : 0 < n
⊢ List.insert a (replicate n a) = replicate n a

Tactic:
cases n <;> simp_all

Result:
no goals