harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/JacobsonSpace.lean
lemma JacobsonSpace.of_isClosedEmbedding [JacobsonSpace Y] (hf : IsClosedEmbedding f) :
    JacobsonSpace X

Proof state:
X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace Y
hf : IsClosedEmbedding f
Z : Set X
hZ : Z.Nonempty
hZ' : IsLocallyClosed Z
⊢ (Z ∩ f ⁻¹' closedPoints Y).Nonempty

Tactic:
obtain ⟨_, ⟨x, hx, rfl⟩, hx'⟩ := nonempty_inter_closedPoints
  (hZ.image f) (hZ'.image hf.isInducing hf.isClosed_range.isLocallyClosed)

Result:
case intro.intro.intro.intro
X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace Y
hf : IsClosedEmbedding f
Z : Set X
hZ : Z.Nonempty
hZ' : IsLocallyClosed Z
x : X
hx : x ∈ Z
hx' : f x ∈ closedPoints Y
⊢ (Z ∩ f ⁻¹' closedPoints Y).Nonempty

Proof state:
X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace Y
hf : IsClosedEmbedding f
⊢ JacobsonSpace X

Tactic:
rw [jacobsonSpace_iff_locallyClosed, ← hf.preimage_closedPoints]

Result:
X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace Y
hf : IsClosedEmbedding f
⊢ ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ f ⁻¹' closedPoints Y).Nonempty

Proof state:
X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace Y
hf : IsClosedEmbedding f
⊢ ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ f ⁻¹' closedPoints Y).Nonempty

Tactic:
intros Z hZ hZ'

Result:
X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace Y
hf : IsClosedEmbedding f
Z : Set X
hZ : Z.Nonempty
hZ' : IsLocallyClosed Z
⊢ (Z ∩ f ⁻¹' closedPoints Y).Nonempty

Proof state:
case intro.intro.intro.intro
X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace Y
hf : IsClosedEmbedding f
Z : Set X
hZ : Z.Nonempty
hZ' : IsLocallyClosed Z
x : X
hx : x ∈ Z
hx' : f x ∈ closedPoints Y
⊢ (Z ∩ f ⁻¹' closedPoints Y).Nonempty

Tactic:
exact ⟨_, hx, hx'⟩

Result:
no goals
-- Mathlib/Data/Fintype/Lattice.lean
theorem Finite.exists_max [Finite α] [Nonempty α] [LinearOrder β] (f : α → β) :
    ∃ x₀ : α, ∀ x, f x ≤ f x₀

Proof state:
α : Type u_2
β : Type u_3
inst✝² : Finite α
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
f : α → β
⊢ ∃ x₀, ∀ (x : α), f x ≤ f x₀

Tactic:
cases nonempty_fintype α

Result:
case intro
α : Type u_2
β : Type u_3
inst✝² : Finite α
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
f : α → β
val✝ : Fintype α
⊢ ∃ x₀, ∀ (x : α), f x ≤ f x₀

Proof state:
case intro
α : Type u_2
β : Type u_3
inst✝² : Finite α
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
f : α → β
val✝ : Fintype α
⊢ ∃ x₀, ∀ (x : α), f x ≤ f x₀

Tactic:
simpa using exists_max_image univ f univ_nonempty

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
protected lemma pow_pos_iff : 0 < a ^ n ↔ 0 < a ∨ n = 0

Proof state:
a n : ℕ
⊢ 0 < a ^ n ↔ 0 < a ∨ n = 0

Tactic:
simp [Nat.pos_iff_ne_zero, Decidable.imp_iff_not_or]

Result:
no goals
-- Mathlib/Data/ZMod/Defs.lean
theorem card (n : ℕ) [Fintype (ZMod n)] : Fintype.card (ZMod n) = n

Proof state:
case succ
n : ℕ
inst✝ : Fintype (ZMod (n + 1))
⊢ Fintype.card (ZMod (n + 1)) = n + 1

Tactic:
convert Fintype.card_fin (n + 1) using 2

Result:
no goals

Proof state:
case zero
inst✝ : Fintype (ZMod 0)
⊢ Fintype.card (ZMod 0) = 0

Tactic:
exact (not_finite (ZMod 0)).elim

Result:
no goals

Proof state:
n : ℕ
inst✝ : Fintype (ZMod n)
⊢ Fintype.card (ZMod n) = n

Tactic:
cases n with
| zero => exact (not_finite (ZMod 0)).elim
| succ n => convert Fintype.card_fin (n + 1) using 2

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
theorem LinearIndependent.ne_zero [Nontrivial R] (i : ι) (hv : LinearIndependent R v) :
    v i ≠ 0

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
i : ι
hv : LinearIndependent R v
h : v i = 0
this : Finsupp.single i 1 = 0
⊢ False

Tactic:
simp at this

Result:
no goals

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
i : ι
hv : LinearIndependent R v
h : v i = 0
⊢ False

Tactic:
have := @hv (Finsupp.single i 1 : ι →₀ R) 0 (by simpa using h)

Result:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
i : ι
hv : LinearIndependent R v
h : v i = 0
this : Finsupp.single i 1 = 0
⊢ False

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
i : ι
hv : LinearIndependent R v
⊢ v i ≠ 0

Tactic:
intro h

Result:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
i : ι
hv : LinearIndependent R v
h : v i = 0
⊢ False

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
i : ι
hv : LinearIndependent R v
h : v i = 0
⊢ (Finsupp.linearCombination R v) (Finsupp.single i 1) = (Finsupp.linearCombination R v) 0

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Topology/Algebra/Module/LinearPMap.lean
theorem closureHasCore (f : E →ₗ.[R] F) : f.closure.HasCore f.domain

Proof state:
case e_f.h'
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
x : E
h1 : x ∈ (f.closure.domRestrict f.domain).domain
h2 : x ∈ f.domain
z : ↥f.closure.domain := ⟨x, ⋯⟩
hyz : x = ↑z
⊢ ↑(f.closure.domRestrict f.domain) ⟨x, h1⟩ = ↑f.closure z

Tactic:
exact domRestrict_apply hyz

Result:
no goals

Proof state:
case e_f.h'
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
x : E
h1 : x ∈ (f.closure.domRestrict f.domain).domain
h2 : x ∈ f.domain
z : ↥f.closure.domain := ⟨x, ⋯⟩
hyz : x = ↑z
⊢ ↑(f.closure.domRestrict f.domain) ⟨x, h1⟩ = ↑f ⟨x, h2⟩

Tactic:
rw [f.le_closure.2 hyz]

Result:
case e_f.h'
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
x : E
h1 : x ∈ (f.closure.domRestrict f.domain).domain
h2 : x ∈ f.domain
z : ↥f.closure.domain := ⟨x, ⋯⟩
hyz : x = ↑z
⊢ ↑(f.closure.domRestrict f.domain) ⟨x, h1⟩ = ↑f.closure z
-- Mathlib/Data/Rat/Lemmas.lean
theorem add_den_dvd_lcm (q₁ q₂ : ℚ) : (q₁ + q₂).den ∣ q₁.den.lcm q₂.den

Proof state:
q₁ q₂ : ℚ
⊢ (q₁ + q₂).den ∣ q₁.den.lcm q₂.den

Tactic:
rw [add_def, normalize_eq, Nat.div_dvd_iff_dvd_mul (Nat.gcd_dvd_right _ _)
  (Nat.gcd_ne_zero_right (by simp)), ← Nat.gcd_mul_lcm,
  mul_dvd_mul_iff_right (Nat.lcm_ne_zero (by simp) (by simp)), Nat.dvd_gcd_iff]

Result:
q₁ q₂ : ℚ
⊢ q₁.den.gcd q₂.den ∣ (q₁.num * ↑q₂.den + q₂.num * ↑q₁.den).natAbs ∧
    q₁.den.gcd q₂.den ∣ q₁.den.gcd q₂.den * q₁.den.lcm q₂.den

Proof state:
q₁ q₂ : ℚ
⊢ ↑(q₁.den.gcd q₂.den) ∣ q₁.num * ↑q₂.den + q₂.num * ↑q₁.den

Tactic:
apply Int.dvd_add
  <;> apply dvd_mul_of_dvd_right <;> rw [Int.natCast_dvd_natCast]
  <;> [exact Nat.gcd_dvd_right _ _; exact Nat.gcd_dvd_left _ _]

Result:
no goals

Proof state:
q₁ q₂ : ℚ
⊢ q₁.den * q₂.den ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
q₁ q₂ : ℚ
⊢ q₁.den.gcd q₂.den ∣ (q₁.num * ↑q₂.den + q₂.num * ↑q₁.den).natAbs

Tactic:
rw [← Int.natCast_dvd_natCast, Int.dvd_natAbs]

Result:
q₁ q₂ : ℚ
⊢ ↑(q₁.den.gcd q₂.den) ∣ q₁.num * ↑q₂.den + q₂.num * ↑q₁.den

Proof state:
q₁ q₂ : ℚ
⊢ q₂.den ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
q₁ q₂ : ℚ
⊢ q₁.den ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
q₁ q₂ : ℚ
⊢ q₁.den.gcd q₂.den ∣ (q₁.num * ↑q₂.den + q₂.num * ↑q₁.den).natAbs ∧
    q₁.den.gcd q₂.den ∣ q₁.den.gcd q₂.den * q₁.den.lcm q₂.den

Tactic:
refine ⟨?_, dvd_mul_right _ _⟩

Result:
q₁ q₂ : ℚ
⊢ q₁.den.gcd q₂.den ∣ (q₁.num * ↑q₂.den + q₂.num * ↑q₁.den).natAbs
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem parent_rootD (self : UnionFind) (x : Nat) :
    self.parent (self.rootD x) = self.rootD x

Proof state:
case isFalse
self : UnionFind
x : Nat
h✝ : ¬x < self.size
⊢ self.parent x = x

Tactic:
simp [parentD_of_not_lt, *]

Result:
no goals

Proof state:
case isTrue
self : UnionFind
x : Nat
h✝ : x < self.size
⊢ self.parent ↑(self.root ⟨x, h✝⟩) = ↑(self.root ⟨x, h✝⟩)

Tactic:
simp [parentD, parent_root, -Array.get_eq_getElem]

Result:
no goals

Proof state:
self : UnionFind
x : Nat
⊢ self.parent (if h : x < self.size then ↑(self.root ⟨x, h⟩) else x) =
    if h : x < self.size then ↑(self.root ⟨x, h⟩) else x

Tactic:
split

Result:
case isTrue
self : UnionFind
x : Nat
h✝ : x < self.size
⊢ self.parent ↑(self.root ⟨x, h✝⟩) = ↑(self.root ⟨x, h✝⟩)

case isFalse
self : UnionFind
x : Nat
h✝ : ¬x < self.size
⊢ self.parent x = x

Proof state:
self : UnionFind
x : Nat
⊢ self.parent (self.rootD x) = self.rootD x

Tactic:
rw [rootD]

Result:
self : UnionFind
x : Nat
⊢ self.parent (if h : x < self.size then ↑(self.root ⟨x, h⟩) else x) =
    if h : x < self.size then ↑(self.root ⟨x, h⟩) else x
-- Mathlib/Algebra/Group/Basic.lean
theorem ite_mul_one {P : Prop} [Decidable P] {a b : M} :
    ite P (a * b) 1 = ite P a 1 * ite P b 1

Proof state:
M : Type u_4
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
⊢ (if P then a * b else 1) = (if P then a else 1) * if P then b else 1

Tactic:
by_cases h : P <;> simp [h]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_dvd_prod_of_dvd {S : Finset α} (g1 g2 : α → β) (h : ∀ a ∈ S, g1 a ∣ g2 a) :
    S.prod g1 ∣ S.prod g2

Proof state:
case cons
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
g1 g2 : α → β
a : α
T : Finset α
haT : a ∉ T
IH : (∀ a ∈ T, g1 a ∣ g2 a) → T.prod g1 ∣ T.prod g2
h : ∀ a_1 ∈ cons a T haT, g1 a_1 ∣ g2 a_1
⊢ (cons a T haT).prod g1 ∣ (cons a T haT).prod g2

Tactic:
rw [Finset.prod_cons, Finset.prod_cons]

Result:
case cons
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
g1 g2 : α → β
a : α
T : Finset α
haT : a ∉ T
IH : (∀ a ∈ T, g1 a ∣ g2 a) → T.prod g1 ∣ T.prod g2
h : ∀ a_1 ∈ cons a T haT, g1 a_1 ∣ g2 a_1
⊢ g1 a * ∏ x ∈ T, g1 x ∣ g2 a * ∏ x ∈ T, g2 x

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
S : Finset α
g1 g2 : α → β
h : ∀ a ∈ S, g1 a ∣ g2 a
⊢ S.prod g1 ∣ S.prod g2

Tactic:
induction S using Finset.cons_induction with
| empty => simp
| cons a T haT IH =>
  rw [Finset.prod_cons, Finset.prod_cons]
  rw [Finset.forall_mem_cons] at h
  exact mul_dvd_mul h.1 <| IH h.2

Result:
no goals

Proof state:
case cons
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
g1 g2 : α → β
a : α
T : Finset α
haT : a ∉ T
IH : (∀ a ∈ T, g1 a ∣ g2 a) → T.prod g1 ∣ T.prod g2
h : ∀ a_1 ∈ cons a T haT, g1 a_1 ∣ g2 a_1
⊢ g1 a * ∏ x ∈ T, g1 x ∣ g2 a * ∏ x ∈ T, g2 x

Tactic:
rw [Finset.forall_mem_cons] at h

Result:
case cons
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
g1 g2 : α → β
a : α
T : Finset α
haT : a ∉ T
IH : (∀ a ∈ T, g1 a ∣ g2 a) → T.prod g1 ∣ T.prod g2
h : g1 a ∣ g2 a ∧ ∀ x ∈ T, g1 x ∣ g2 x
⊢ g1 a * ∏ x ∈ T, g1 x ∣ g2 a * ∏ x ∈ T, g2 x

Proof state:
case cons
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
g1 g2 : α → β
a : α
T : Finset α
haT : a ∉ T
IH : (∀ a ∈ T, g1 a ∣ g2 a) → T.prod g1 ∣ T.prod g2
h : g1 a ∣ g2 a ∧ ∀ x ∈ T, g1 x ∣ g2 x
⊢ g1 a * ∏ x ∈ T, g1 x ∣ g2 a * ∏ x ∈ T, g2 x

Tactic:
exact mul_dvd_mul h.1 <| IH h.2

Result:
no goals

Proof state:
case empty
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
g1 g2 : α → β
h : ∀ a ∈ ∅, g1 a ∣ g2 a
⊢ ∅.prod g1 ∣ ∅.prod g2

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Range.lean
theorem range_inclusion (p q : Submodule R M) (h : p ≤ q) :
    range (inclusion h) = comap q.subtype p

Proof state:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
h : p ≤ q
⊢ range (inclusion h) = comap q.subtype p

Tactic:
rw [← map_top, inclusion, LinearMap.map_codRestrict, map_top, range_subtype]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[reassoc]
lemma cyclesOpIso_inv_naturality (φ : S₁ ⟶ S₂)
    [S₁.HasRightHomology] [S₂.HasRightHomology] :
    (opcyclesMap φ).op ≫ (S₁.cyclesOpIso).inv =
      S₂.cyclesOpIso.inv ≫ cyclesMap (opMap φ)

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ (opcyclesMap φ).op ≫ S₁.cyclesOpIso.inv = S₂.cyclesOpIso.inv ≫ cyclesMap (opMap φ)

Tactic:
rw [← cancel_mono S₁.op.iCycles, assoc, assoc, cyclesOpIso_inv_op_iCycles, cyclesMap_i,
  cyclesOpIso_inv_op_iCycles_assoc, ← op_comp, p_opcyclesMap, op_comp, opMap_τ₂]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma succ_div : ∀ a b : ℕ, (a + 1) / b = a / b + if b ∣ a + 1 then 1 else 0
  | a, 0 => by simp
  | 0, 1 => by simp
  | 0, b + 2 => by
    have hb2 : b + 2 > 1

Proof state:
⊢ (0 + 1) / 1 = 0 / 1 + if 1 ∣ 0 + 1 then 1 else 0

Tactic:
simp

Result:
no goals

Proof state:
case pos
a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0

Tactic:
have h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 := ⟨succ_pos _, Nat.add_le_add_iff_right.2 hb_le_a1⟩

Result:
case pos
a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0

Proof state:
b : ℕ
⊢ b + 2 > 1

Tactic:
simp

Result:
no goals

Proof state:
case neg
a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : ¬b ≤ a + 1
hba : ¬b ≤ a
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0

Tactic:
have hb_dvd_a : ¬b + 1 ∣ a + 2 := fun h =>
  hb_le_a1 (le_of_succ_le_succ (le_of_dvd (succ_pos _) h))

Result:
case neg
a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : ¬b ≤ a + 1
hba : ¬b ≤ a
hb_dvd_a : ¬b + 1 ∣ a + 2
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0

Proof state:
case pos
a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
h₂ : 0 < b + 1 ∧ b + 1 ≤ a + 1
dvd_iff : b + 1 ∣ a - b + 1 ↔ b + 1 ∣ a + 1 + 1
wf : a - b < a + 1
⊢ ((a - b) / (b + 1) + if b + 1 ∣ a - b + 1 then 1 else 0) + 1 =
    (a - b) / (b + 1) + 1 + if b + 1 ∣ 1 + a + 1 then 1 else 0

Tactic:
simp [dvd_iff, Nat.add_comm 1, Nat.add_assoc]

Result:
no goals

Proof state:
case neg
a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : ¬b ≤ a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0

Tactic:
have hba : ¬b ≤ a := Nat.not_le_of_gt
  (Nat.lt_trans (lt_succ_self a) (Nat.lt_of_not_ge hb_le_a1))

Result:
case neg
a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : ¬b ≤ a + 1
hba : ¬b ≤ a
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
theorem linearIndependent_iUnion_finite {η : Type*} {ιs : η → Type*} {f : ∀ j : η, ιs j → M}
    (hindep : ∀ j, LinearIndependent R (f j))
    (hd : ∀ i, ∀ t : Set η,
      t.Finite → i ∉ t → Disjoint (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))) :
    LinearIndependent R fun ji : Σ j, ιs j => f ji.1 ji.2

Proof state:
case hf.mk.mk
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd : ∀ (i : η) (t : Set η), t.Finite → i ∉ t → Disjoint (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : (fun ji => f ji.fst ji.snd) ⟨x₁, x₂⟩ = (fun ji => f ji.fst ji.snd) ⟨y₁, y₂⟩
⊢ ⟨x₁, x₂⟩ = ⟨y₁, y₂⟩

Tactic:
by_cases h_cases : x₁ = y₁

Result:
case pos
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd : ∀ (i : η) (t : Set η), t.Finite → i ∉ t → Disjoint (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : (fun ji => f ji.fst ji.snd) ⟨x₁, x₂⟩ = (fun ji => f ji.fst ji.snd) ⟨y₁, y₂⟩
h_cases : x₁ = y₁
⊢ ⟨x₁, x₂⟩ = ⟨y₁, y₂⟩

case neg
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd : ∀ (i : η) (t : Set η), t.Finite → i ∉ t → Disjoint (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : (fun ji => f ji.fst ji.snd) ⟨x₁, x₂⟩ = (fun ji => f ji.fst ji.snd) ⟨y₁, y₂⟩
h_cases : ¬x₁ = y₁
⊢ ⟨x₁, x₂⟩ = ⟨y₁, y₂⟩
-- Mathlib/FieldTheory/Fixed.lean
theorem toAlgAut_bijective [Finite G] [FaithfulSMul G F] :
    Function.Bijective (MulSemiringAction.toAlgAut G (FixedPoints.subfield G F) F)

Proof state:
G : Type u_1
F : Type u_2
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
⊢ Function.Bijective ⇑(MulSemiringAction.toAlgAut G (↥(subfield G F)) F)

Tactic:
refine ⟨fun _ _ h ↦ (FixedPoints.toAlgHom_bijective G F).injective ?_,
  fun f ↦ ((FixedPoints.toAlgHom_bijective G F).surjective f).imp (fun _ h ↦ ?_)⟩ <;>
    rwa [DFunLike.ext_iff] at h ⊢

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem filter_eq [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {f : (a : α) → β a → Bool} :
    m.filter f = Raw₀.filter f ⟨m, h.size_buckets_pos⟩

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α β
h : m.WF
f : (a : α) → β a → Bool
⊢ Raw.filter f m = (Raw₀.filter f ⟨m, ⋯⟩).val

Tactic:
simp [Raw.filter, h.size_buckets_pos]

Result:
no goals
-- Mathlib/Algebra/Group/End.lean
theorem mul_swap_eq_swap_mul (f : Perm α) (x y : α) : f * swap x y = swap (f x) (f y) * f

Proof state:
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y : α
⊢ f * swap x y = swap (f x) (f y) * f

Tactic:
rw [swap_mul_eq_mul_swap, Perm.inv_apply_self, Perm.inv_apply_self]

Result:
no goals
-- Mathlib/Analysis/SumOverResidueClass.lean
/-- If `f` is a summable function on `ℕ`, and `0 < N`, then we may compute `∑' n : ℕ, f n` by
summing each residue class mod `N` separately. -/
lemma Nat.sumByResidueClasses {R : Type*} [AddCommGroup R] [UniformSpace R] [UniformAddGroup R]
    [CompleteSpace R] [T0Space R] {f : ℕ → R} (hf : Summable f) (N : ℕ) [NeZero N] :
    ∑' n, f n = ∑ j : ZMod N, ∑' m, f (j.val + N * m)

Proof state:
R : Type u_1
inst✝⁵ : AddCommGroup R
inst✝⁴ : UniformSpace R
inst✝³ : UniformAddGroup R
inst✝² : CompleteSpace R
inst✝¹ : T0Space R
f : ℕ → R
hf : Summable f
N : ℕ
inst✝ : NeZero N
⊢ Summable fun c => f (N.residueClassesEquiv.symm c)

Tactic:
exact hf.comp_injective (residueClassesEquiv N).symm.injective

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : AddCommGroup R
inst✝⁴ : UniformSpace R
inst✝³ : UniformAddGroup R
inst✝² : CompleteSpace R
inst✝¹ : T0Space R
f : ℕ → R
hf : Summable f
N : ℕ
inst✝ : NeZero N
⊢ ∑' (n : ℕ), f n = ∑ j : ZMod N, ∑' (m : ℕ), f (j.val + N * m)

Tactic:
rw [← (residueClassesEquiv N).symm.tsum_eq f, tsum_prod, tsum_fintype, residueClassesEquiv,
  Equiv.coe_fn_symm_mk]

Result:
R : Type u_1
inst✝⁵ : AddCommGroup R
inst✝⁴ : UniformSpace R
inst✝³ : UniformAddGroup R
inst✝² : CompleteSpace R
inst✝¹ : T0Space R
f : ℕ → R
hf : Summable f
N : ℕ
inst✝ : NeZero N
⊢ Summable fun c => f (N.residueClassesEquiv.symm c)
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem mul_add_div (a) {b : Ordinal} (b0 : b ≠ 0) (c) : (b * a + c) / b = a + c / b

Proof state:
case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ b * a + c < b * succ (a + c / b)

Tactic:
rw [mul_succ, mul_add, add_assoc, add_lt_add_iff_left]

Result:
case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ c < b * (c / b) + b

Proof state:
case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ b * (c / b) ≤ c

Tactic:
apply mul_div_le

Result:
no goals

Proof state:
case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ (b * a + c) / b ≤ a + c / b

Tactic:
apply (div_le b0).2

Result:
case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ b * a + c < b * succ (a + c / b)

Proof state:
case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ a + c / b ≤ (b * a + c) / b

Tactic:
rw [le_div b0, mul_add, add_le_add_iff_left]

Result:
case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ b * (c / b) ≤ c

Proof state:
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ (b * a + c) / b = a + c / b

Tactic:
apply le_antisymm

Result:
case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ (b * a + c) / b ≤ a + c / b

case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ a + c / b ≤ (b * a + c) / b

Proof state:
case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ c < b * (c / b) + b

Tactic:
apply lt_mul_div_add _ b0

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Final.lean
theorem initial_of_initial_comp [Initial F] [Initial (F ⋙ G)] : Initial G

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.Initial
inst✝ : (F ⋙ G).Initial
⊢ G.Initial

Tactic:
suffices Final G.op from initial_of_final_op _

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.Initial
inst✝ : (F ⋙ G).Initial
⊢ G.op.Final

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.Initial
inst✝ : (F ⋙ G).Initial
⊢ G.op.Final

Tactic:
have : Final (F.op ⋙ G.op) := show Final (F ⋙ G).op from inferInstance

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.Initial
inst✝ : (F ⋙ G).Initial
this : (F.op ⋙ G.op).Final
⊢ G.op.Final

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.Initial
inst✝ : (F ⋙ G).Initial
this : (F.op ⋙ G.op).Final
⊢ G.op.Final

Tactic:
exact final_of_final_comp F.op G.op

Result:
no goals