harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Dynamics/Ergodic/AddCircle.lean
theorem ergodic_zsmul {n : ℤ} (hn : 1 < |n|) : Ergodic fun y : AddCircle T => n • y :=
  { measurePreserving_zsmul volume (abs_pos.mp <| lt_trans zero_lt_one hn) with
    aeconst_set := fun s hs hs' => by
      let u : ℕ → AddCircle T := fun j => ↑((↑1 : ℝ) / ↑(n.natAbs ^ j) * T)
      replace hn : 1 < n.natAbs

Proof state:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(n.natAbs ^ j) * T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
hnu : ∀ (j : ℕ), n ^ j • u j = 0
hu₁ : ∀ (j : ℕ), u j +ᵥ s =ᶠ[ae volume] s
⊢ Tendsto (fun j => addOrderOf (u j)) atTop atTop

Tactic:
simp_rw [hu₀]

Result:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(n.natAbs ^ j) * T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
hnu : ∀ (j : ℕ), n ^ j • u j = 0
hu₁ : ∀ (j : ℕ), u j +ᵥ s =ᶠ[ae volume] s
⊢ Tendsto (fun j => n.natAbs ^ j) atTop atTop

Proof state:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(n.natAbs ^ j) * T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
hnu : ∀ (j : ℕ), n ^ j • u j = 0
j : ℕ
⊢ u j +ᵥ s =ᶠ[ae volume] s

Tactic:
rw [vadd_eq_self_of_preimage_zsmul_eq_self hs' (hnu j)]

Result:
no goals

Proof state:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(n.natAbs ^ j) * T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
hnu : ∀ (j : ℕ), n ^ j • u j = 0
hu₁ : ∀ (j : ℕ), u j +ᵥ s =ᶠ[ae volume] s
⊢ Tendsto (fun j => n.natAbs ^ j) atTop atTop

Tactic:
exact Nat.tendsto_pow_atTop_atTop_of_one_lt hn

Result:
no goals

Proof state:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(n.natAbs ^ j) * T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
j : ℕ
⊢ n ^ j • u j = 0

Tactic:
rw [← addOrderOf_dvd_iff_zsmul_eq_zero, hu₀, Int.natCast_pow, Int.natCast_natAbs, ← abs_pow,
  abs_dvd]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/CompatibleSheafification.lean
theorem toSheafify_comp_sheafifyCompIso_inv :
    J.toSheafify _ ≫ (J.sheafifyCompIso F P).inv = whiskerRight (J.toSheafify _) _

Proof state:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
⊢ J.toSheafify (P ⋙ F) = whiskerRight (J.toSheafify P) F ≫ (J.sheafifyCompIso F P).hom

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
⊢ J.toSheafify (P ⋙ F) ≫ (J.sheafifyCompIso F P).inv = whiskerRight (J.toSheafify P) F

Tactic:
rw [Iso.comp_inv_eq]

Result:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
⊢ J.toSheafify (P ⋙ F) = whiskerRight (J.toSheafify P) F ≫ (J.sheafifyCompIso F P).hom
-- Mathlib/Algebra/Polynomial/Eval/SMul.lean
theorem eval₂_smul (g : R →+* S) (p : R[X]) (x : S) {s : R} :
    eval₂ g x (s • p) = g s * eval₂ g x p

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
B : (s • p).natDegree < p.natDegree.succ
⊢ eval₂ g x (s • p) = g s * eval₂ g x p

Tactic:
rw [eval₂_eq_sum, eval₂_eq_sum, sum_over_range' _ _ _ A, sum_over_range' _ _ _ B] <;>
  simp [mul_sum, mul_assoc]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
⊢ eval₂ g x (s • p) = g s * eval₂ g x p

Tactic:
have A : p.natDegree < p.natDegree.succ := Nat.lt_succ_self _

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
⊢ eval₂ g x (s • p) = g s * eval₂ g x p

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
⊢ eval₂ g x (s • p) = g s * eval₂ g x p

Tactic:
have B : (s • p).natDegree < p.natDegree.succ := (natDegree_smul_le _ _).trans_lt A

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
B : (s • p).natDegree < p.natDegree.succ
⊢ eval₂ g x (s • p) = g s * eval₂ g x p
-- Mathlib/Data/ZMod/Basic.lean
theorem addOrderOf_coe (a : ℕ) {n : ℕ} (n0 : n ≠ 0) : addOrderOf (a : ZMod n) = n / n.gcd a

Proof state:
a n : ℕ
n0 : n ≠ 0
⊢ addOrderOf ↑a = n / n.gcd a

Tactic:
rcases a with - | a

Result:
case zero
n : ℕ
n0 : n ≠ 0
⊢ addOrderOf ↑0 = n / n.gcd 0

case succ
n : ℕ
n0 : n ≠ 0
a : ℕ
⊢ addOrderOf ↑(a + 1) = n / n.gcd (a + 1)

Proof state:
case succ
n : ℕ
n0 : n ≠ 0
a : ℕ
⊢ addOrderOf ↑(a + 1) = n / n.gcd (a + 1)

Tactic:
rw [← Nat.smul_one_eq_cast, addOrderOf_nsmul' _ a.succ_ne_zero, ZMod.addOrderOf_one]

Result:
no goals

Proof state:
case zero
n : ℕ
n0 : n ≠ 0
⊢ addOrderOf ↑0 = n / n.gcd 0

Tactic:
simp only [Nat.cast_zero, addOrderOf_zero, Nat.gcd_zero_right,
  Nat.pos_of_ne_zero n0, Nat.div_self]

Result:
no goals
-- Mathlib/Analysis/Convex/Cone/Basic.lean
theorem mem_iInf {ι : Sort*} {x : E} {f : ι → ConvexCone 𝕜 E} : x ∈ iInf f ↔ ∀ i, x ∈ f i :=
  mem_iInter₂.trans <| by simp

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
ι : Sort u_5
x : E
f : ι → ConvexCone 𝕜 E
⊢ (∀ i ∈ Set.range f, x ∈ ↑i) ↔ ∀ (i : ι), x ∈ f i

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem image_union (f : α → β) (s t : Set α) : f '' (s ∪ t) = f '' s ∪ f '' t :=
  ext fun x =>
    ⟨by rintro ⟨a, h | h, rfl⟩ <;> [left; right] <;> exact ⟨_, h, rfl⟩, by
      rintro (⟨a, h, rfl⟩ | ⟨a, h, rfl⟩) <;> refine ⟨_, ?_, rfl⟩
      · exact mem_union_left t h
      · exact mem_union_right s h⟩

Proof state:
case inr.intro.intro
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
a : α
h : a ∈ t
⊢ a ∈ s ∪ t

Tactic:
exact mem_union_right s h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
x : β
⊢ x ∈ f '' s ∪ f '' t → x ∈ f '' (s ∪ t)

Tactic:
rintro (⟨a, h, rfl⟩ | ⟨a, h, rfl⟩) <;> refine ⟨_, ?_, rfl⟩

Result:
case inl.intro.intro
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
a : α
h : a ∈ s
⊢ a ∈ s ∪ t

case inr.intro.intro
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
a : α
h : a ∈ t
⊢ a ∈ s ∪ t

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
x : β
⊢ x ∈ f '' (s ∪ t) → x ∈ f '' s ∪ f '' t

Tactic:
rintro ⟨a, h | h, rfl⟩ <;> [left; right] <;> exact ⟨_, h, rfl⟩

Result:
no goals

Proof state:
case inl.intro.intro
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
a : α
h : a ∈ s
⊢ a ∈ s ∪ t

Tactic:
exact mem_union_left t h

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem size_erase_of_mem [DecidableRel (α := α) (· ≤ ·)] {x : α} {t a₁ a₂} (h : Valid' a₁ t a₂)
    (h_mem : x ∈ t) : size (erase x t) = size t - 1

Proof state:
case node.lt.intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_l = true
t_ih_l : (erase x t_l).size = t_l.size - 1
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
⊢ t_l.size - 1 + t_r.size + 1 = (node (t_l.size + t_r.size + 1) t_l t_x t_r).size - 1

Tactic:
have h_pos_t_l_size := pos_size_of_mem h.left.sz h_mem

Result:
case node.lt.intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_l = true
t_ih_l : (erase x t_l).size = t_l.size - 1
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
h_pos_t_l_size : 0 < t_l.size
⊢ t_l.size - 1 + t_r.size + 1 = (node (t_l.size + t_r.size + 1) t_l t_x t_r).size - 1

Proof state:
case node.gt.intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : (erase x t_r).size = t_r.size - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
h_pos_t_r_size : 0 < t_r.size
⊢ t_l.size + (t_r.size - 1) + 1 = (node (t_l.size + t_r.size + 1) t_l t_x t_r).size - 1

Tactic:
revert h_pos_t_r_size

Result:
case node.gt.intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : (erase x t_r).size = t_r.size - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ 0 < t_r.size → t_l.size + (t_r.size - 1) + 1 = (node (t_l.size + t_r.size + 1) t_l t_x t_r).size - 1

Proof state:
case node.eq
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
t_ih_l' : x ∈ t_l → (erase x t_l).size = t_l.size - 1
t_ih_r' : x ∈ t_r → (erase x t_r).size = t_r.size - 1
h_mem : true = true
⊢ t_l.size + t_r.size = (node (t_l.size + t_r.size + 1) t_l t_x t_r).size - 1

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
lemma δ_rightShift (a n' m' : ℤ) (hn' : n' + a = n) (m : ℤ) (hm' : m' + a = m) :
    δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'

Proof state:
case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : ¬n + 1 = m
hnm' : ¬n' + 1 = m'
⊢ δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'

Tactic:
rw [δ_shape _ _ hnm', δ_shape _ _ hnm, rightShift_zero, smul_zero]

Result:
no goals

Proof state:
case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : ¬n + 1 = m
⊢ δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'

Tactic:
have hnm' : ¬ n' + 1 = m' := fun _ => hnm (by omega)

Result:
case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : ¬n + 1 = m
hnm' : ¬n' + 1 = m'
⊢ δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : n + 1 = m
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
⊢ p + n' = q - 1

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Vector/Mem.lean
theorem mem_of_mem_tail (v : Vector α n) (ha : a ∈ v.tail.toList) : a ∈ v.toList

Proof state:
case zero
α : Type u_1
n : ℕ
a : α
v : Vector α 0
ha : a ∈ v.tail.toList
⊢ a ∈ v.toList

Tactic:
exact False.elim (Vector.not_mem_zero a v.tail ha)

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
a : α
v : Vector α n
ha : a ∈ v.tail.toList
⊢ a ∈ v.toList

Tactic:
induction n with
| zero => exact False.elim (Vector.not_mem_zero a v.tail ha)
| succ n _ => exact (mem_succ_iff a v).2 (Or.inr ha)

Result:
no goals

Proof state:
case succ
α : Type u_1
n✝ : ℕ
a : α
n : ℕ
a✝ : ∀ (v : Vector α n), a ∈ v.tail.toList → a ∈ v.toList
v : Vector α (n + 1)
ha : a ∈ v.tail.toList
⊢ a ∈ v.toList

Tactic:
exact (mem_succ_iff a v).2 (Or.inr ha)

Result:
no goals
-- Mathlib/AlgebraicGeometry/Scheme.lean
@[simp]
lemma zeroLocus_univ {U : X.Opens} :
    X.zeroLocus (U := U) Set.univ = (↑U)ᶜ

Proof state:
case h
X : Scheme
U : X.Opens
x : ↑↑X.toPresheafedSpace
⊢ (∃ x_1, x ∈ X.basicOpen x_1) ↔ x ∈ U

Tactic:
exact ⟨fun ⟨f, hf⟩ ↦ X.basicOpen_le f hf, fun _ ↦ ⟨1, by rwa [X.basicOpen_of_isUnit isUnit_one]⟩⟩

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
x : ↑↑X.toPresheafedSpace
x✝ : x ∈ U
⊢ x ∈ X.basicOpen 1

Tactic:
rwa [X.basicOpen_of_isUnit isUnit_one]

Result:
no goals

Proof state:
case h
X : Scheme
U : X.Opens
x : ↑↑X.toPresheafedSpace
⊢ x ∈ X.zeroLocus Set.univ ↔ x ∈ (↑U)ᶜ

Tactic:
simp only [Scheme.mem_zeroLocus_iff, Set.mem_univ, forall_const, Set.mem_compl_iff,
  SetLike.mem_coe, ← not_exists, not_iff_not]

Result:
case h
X : Scheme
U : X.Opens
x : ↑↑X.toPresheafedSpace
⊢ (∃ x_1, x ∈ X.basicOpen x_1) ↔ x ∈ U

Proof state:
X : Scheme
U : X.Opens
⊢ X.zeroLocus Set.univ = (↑U)ᶜ

Tactic:
ext x

Result:
case h
X : Scheme
U : X.Opens
x : ↑↑X.toPresheafedSpace
⊢ x ∈ X.zeroLocus Set.univ ↔ x ∈ (↑U)ᶜ
-- Mathlib/Order/Filter/Basic.lean
theorem frequently_false (f : Filter α) : ¬∃ᶠ _ in f, False

Proof state:
α : Type u
f : Filter α
⊢ ¬∃ᶠ (x : α) in f, False

Tactic:
simp

Result:
no goals
-- Mathlib/Order/RelSeries.lean
@[simp] lemma last_smash {p q : RelSeries r} (h : p.last = q.head) :
    (smash p q h).last = q.last

Proof state:
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
⊢ { length := p.length + q.length,
          toFun := fun i => if H : ↑i < p.length then p.toFun ⟨↑i, ⋯⟩ else q.toFun ⟨↑i - p.length, ⋯⟩, step := ⋯ }.toFun
      (Fin.last
        { length := p.length + q.length,
            toFun := fun i => if H : ↑i < p.length then p.toFun ⟨↑i, ⋯⟩ else q.toFun ⟨↑i - p.length, ⋯⟩,
            step := ⋯ }.length) =
    q.toFun (Fin.last q.length)

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
⊢ (p.smash q h).last = q.last

Tactic:
delta smash last

Result:
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
⊢ { length := p.length + q.length,
          toFun := fun i => if H : ↑i < p.length then p.toFun ⟨↑i, ⋯⟩ else q.toFun ⟨↑i - p.length, ⋯⟩, step := ⋯ }.toFun
      (Fin.last
        { length := p.length + q.length,
            toFun := fun i => if H : ↑i < p.length then p.toFun ⟨↑i, ⋯⟩ else q.toFun ⟨↑i - p.length, ⋯⟩,
            step := ⋯ }.length) =
    q.toFun (Fin.last q.length)
-- Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
theorem homothety_mul_apply (c : P1) (r₁ r₂ : k) (p : P1) :
    homothety c (r₁ * r₂) p = homothety c r₁ (homothety c r₂ p)

Proof state:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst✝³ : CommRing k
inst✝² : AddCommGroup V1
inst✝¹ : AffineSpace V1 P1
inst✝ : Module k V1
c : P1
r₁ r₂ : k
p : P1
⊢ (homothety c (r₁ * r₂)) p = (homothety c r₁) ((homothety c r₂) p)

Tactic:
simp only [homothety_apply, mul_smul, vadd_vsub]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/GiryMonad.lean
theorem _root_.Measurable.measure_of_isPiSystem_of_isProbabilityMeasure {μ : α → Measure β}
    [∀ a, IsProbabilityMeasure (μ a)]
    {S : Set (Set β)} (hgen : ‹MeasurableSpace β› = .generateFrom S) (hpi : IsPiSystem S)
    (h_basic : ∀ s ∈ S, Measurable fun a ↦ μ a s) : Measurable μ :=
  .measure_of_isPiSystem hgen hpi h_basic <| by simp

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst✝ : ∀ (a : α), IsProbabilityMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable fun a => (μ a) s
⊢ Measurable fun a => (μ a) univ

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Coset/Basic.lean
@[to_additive]
lemma orbit_eq_out_smul (x : α ⧸ s) : MulAction.orbitRel.Quotient.orbit x = x.out • s

Proof state:
case H
α : Type u_1
inst✝ : Group α
s : Subgroup α
z✝ : α
⊢ MulAction.orbitRel.Quotient.orbit ↑z✝ = Quotient.out ↑z✝ • ↑s

Tactic:
simp only [orbit_mk_eq_smul, ← eq_class_eq_leftCoset, Quotient.out_eq']

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
x : α ⧸ s
⊢ MulAction.orbitRel.Quotient.orbit x = Quotient.out x • ↑s

Tactic:
induction x using QuotientGroup.induction_on

Result:
case H
α : Type u_1
inst✝ : Group α
s : Subgroup α
z✝ : α
⊢ MulAction.orbitRel.Quotient.orbit ↑z✝ = Quotient.out ↑z✝ • ↑s
-- Mathlib/RingTheory/TwoSidedIdeal/Operations.lean
lemma gc : GaloisConnection fromIdeal (asIdeal (R := R)) :=
  fun I J => ⟨fun h x hx ↦ h <| mem_span_iff.2 fun _ H ↦ H hx, fun h x hx ↦ by
    simp only [fromIdeal, OrderHom.coe_mk, mem_span_iff] at hx
    exact hx _ h⟩

Proof state:
R : Type u_1
inst✝ : Ring R
I : Ideal R
J : TwoSidedIdeal R
h : I ≤ asIdeal J
x : R
hx : ∀ (I_1 : TwoSidedIdeal R), ↑I ⊆ ↑I_1 → x ∈ I_1
⊢ x ∈ J

Tactic:
exact hx _ h

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Ring R
I : Ideal R
J : TwoSidedIdeal R
h : I ≤ asIdeal J
x : R
hx : x ∈ fromIdeal I
⊢ x ∈ J

Tactic:
simp only [fromIdeal, OrderHom.coe_mk, mem_span_iff] at hx

Result:
R : Type u_1
inst✝ : Ring R
I : Ideal R
J : TwoSidedIdeal R
h : I ≤ asIdeal J
x : R
hx : ∀ (I_1 : TwoSidedIdeal R), ↑I ⊆ ↑I_1 → x ∈ I_1
⊢ x ∈ J
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem get_find?_mkVector (n : Nat) (a : α) (p : α → Bool) (h) :
    ((mkVector n a).find? p).get h = a

Proof state:
α : Type
n : Nat
a : α
p : α → Bool
h : (find? p (mkVector n a)).isSome = true
⊢ (find? p (mkVector n a)).get h = a

Tactic:
simp only [mkVector_eq_mk_mkArray, find?_mk]

Result:
α : Type
n : Nat
a : α
p : α → Bool
h : (find? p (mkVector n a)).isSome = true
⊢ (Array.find? p (mkArray n a)).get ⋯ = a

Proof state:
α : Type
n : Nat
a : α
p : α → Bool
h : (find? p (mkVector n a)).isSome = true
⊢ (Array.find? p (mkArray n a)).get ⋯ = a

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem eq_push_append_of_mem {xs : Array α} {x : α} (h : x ∈ xs) :
    ∃ (as bs : Array α), xs = as.push x ++ bs ∧ x ∉ as

Proof state:
α : Type u_1
xs : Array α
x : α
h : x ∈ xs
⊢ ∃ as bs, xs = as.push x ++ bs ∧ ¬x ∈ as

Tactic:
rcases xs with ⟨xs⟩

Result:
case mk
α : Type u_1
x : α
xs : List α
h : x ∈ { toList := xs }
⊢ ∃ as bs, { toList := xs } = as.push x ++ bs ∧ ¬x ∈ as

Proof state:
case mk.intro.intro.intro
α : Type u_1
x : α
xs : List α
h✝ : x ∈ { toList := xs }
as bs : List α
h : { toList := xs }.toList = as ++ x :: bs
w : ¬x ∈ as
⊢ ∃ as bs, { toList := xs } = as.push x ++ bs ∧ ¬x ∈ as

Tactic:
simp only at h

Result:
case mk.intro.intro.intro
α : Type u_1
x : α
xs : List α
h✝ : x ∈ { toList := xs }
as bs : List α
h : xs = as ++ x :: bs
w : ¬x ∈ as
⊢ ∃ as bs, { toList := xs } = as.push x ++ bs ∧ ¬x ∈ as

Proof state:
α : Type u_1
x : α
as bs : List α
w : ¬x ∈ as
h : x ∈ { toList := as ++ x :: bs }
⊢ { toList := as ++ x :: bs } = as.toArray.push x ++ bs.toArray

Tactic:
simp

Result:
no goals

Proof state:
case mk.intro.intro.intro
α : Type u_1
x : α
xs : List α
h✝ : x ∈ { toList := xs }
as bs : List α
h : xs = as ++ x :: bs
w : ¬x ∈ as
⊢ ∃ as bs, { toList := xs } = as.push x ++ bs ∧ ¬x ∈ as

Tactic:
obtain rfl := h

Result:
case mk.intro.intro.intro
α : Type u_1
x : α
as bs : List α
w : ¬x ∈ as
h : x ∈ { toList := as ++ x :: bs }
⊢ ∃ as_1 bs_1, { toList := as ++ x :: bs } = as_1.push x ++ bs_1 ∧ ¬x ∈ as_1

Proof state:
α : Type u_1
x : α
as bs : List α
w : ¬x ∈ as
h : x ∈ { toList := as ++ x :: bs }
⊢ ¬x ∈ as.toArray

Tactic:
simpa using w

Result:
no goals

Proof state:
case mk.intro.intro.intro
α : Type u_1
x : α
as bs : List α
w : ¬x ∈ as
h : x ∈ { toList := as ++ x :: bs }
⊢ ∃ as_1 bs_1, { toList := as ++ x :: bs } = as_1.push x ++ bs_1 ∧ ¬x ∈ as_1

Tactic:
exact ⟨as.toArray, bs.toArray, by simp, by simpa using w⟩

Result:
no goals

Proof state:
case mk
α : Type u_1
x : α
xs : List α
h : x ∈ { toList := xs }
⊢ ∃ as bs, { toList := xs } = as.push x ++ bs ∧ ¬x ∈ as

Tactic:
obtain ⟨as, bs, h, w⟩ := List.eq_append_cons_of_mem (mem_def.1 h)

Result:
case mk.intro.intro.intro
α : Type u_1
x : α
xs : List α
h✝ : x ∈ { toList := xs }
as bs : List α
h : { toList := xs }.toList = as ++ x :: bs
w : ¬x ∈ as
⊢ ∃ as bs, { toList := xs } = as.push x ++ bs ∧ ¬x ∈ as