harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
theorem natTrailingDegree_eq_of_trailingDegree_eq [Semiring S] {q : S[X]}
    (h : trailingDegree p = trailingDegree q) : natTrailingDegree p = natTrailingDegree q

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
q : S[X]
h : p.trailingDegree = q.trailingDegree
⊢ p.trailingDegree.toNat = q.trailingDegree.toNat

Tactic:
rw [h]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
q : S[X]
h : p.trailingDegree = q.trailingDegree
⊢ p.natTrailingDegree = q.natTrailingDegree

Tactic:
unfold natTrailingDegree

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
q : S[X]
h : p.trailingDegree = q.trailingDegree
⊢ p.trailingDegree.toNat = q.trailingDegree.toNat
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
@[simp]
lemma penultimate_reverse (p : G.Walk u v) : p.reverse.penultimate = p.snd

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.penultimate = p.snd

Tactic:
cases p <;> simp [snd, penultimate, getVert_append]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem one_comp : comp (1 : R[X]) p = 1

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ comp 1 p = 1

Tactic:
rw [← C_1, C_comp]

Result:
no goals
-- Mathlib/Algebra/Homology/Single.lean
@[simp]
lemma mkHomToSingle_f {K : HomologicalComplex V c} {j : ι} {A : V} (φ : K.X j ⟶ A)
    (hφ : ∀ (i : ι), c.Rel i j → K.d i j ≫ φ = 0) :
    (mkHomToSingle φ hφ).f j = φ ≫ (singleObjXSelf c j A).inv

Proof state:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
φ : K.X j ⟶ A
hφ : ∀ (i : ι), c.Rel i j → K.d i j ≫ φ = 0
⊢ φ ≫ (singleObjXIsoOfEq c j A j ⋯).inv = φ ≫ (singleObjXSelf c j A).inv

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
φ : K.X j ⟶ A
hφ : ∀ (i : ι), c.Rel i j → K.d i j ≫ φ = 0
⊢ (if hi : j = j then 𝟙 (K.X j) ≫ φ ≫ (singleObjXIsoOfEq c j A j hi).inv else 0) = φ ≫ (singleObjXSelf c j A).inv

Tactic:
rw [dif_pos rfl, id_comp]

Result:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
φ : K.X j ⟶ A
hφ : ∀ (i : ι), c.Rel i j → K.d i j ≫ φ = 0
⊢ φ ≫ (singleObjXIsoOfEq c j A j ⋯).inv = φ ≫ (singleObjXSelf c j A).inv

Proof state:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
φ : K.X j ⟶ A
hφ : ∀ (i : ι), c.Rel i j → K.d i j ≫ φ = 0
⊢ (mkHomToSingle φ hφ).f j = φ ≫ (singleObjXSelf c j A).inv

Tactic:
dsimp [mkHomToSingle]

Result:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
φ : K.X j ⟶ A
hφ : ∀ (i : ι), c.Rel i j → K.d i j ≫ φ = 0
⊢ (if hi : j = j then 𝟙 (K.X j) ≫ φ ≫ (singleObjXIsoOfEq c j A j hi).inv else 0) = φ ≫ (singleObjXSelf c j A).inv
-- Mathlib/CategoryTheory/GuitartExact/VerticalComposition.lean
lemma vComp'_iff_of_equivalences (E : C₂ ≌ C₃) (E' : D₂ ≌ D₃)
    (w' : H₂ ⋙ E'.functor ≅ E.functor ⋙ H₃) {L₁₂ : C₁ ⥤ C₃}
    {R₁₂ : D₁ ⥤ D₃} (eL : L₁ ⋙ E.functor ≅ L₁₂)
    (eR : R₁ ⋙ E'.functor ≅ R₁₂) :
    (w.vComp' w'.hom eL eR).GuitartExact ↔ w.GuitartExact

Proof state:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁵ : Category.{u_11, u_1} C₁
inst✝⁴ : Category.{u_7, u_2} C₂
inst✝³ : Category.{u_8, u_3} C₃
inst✝² : Category.{u_12, u_4} D₁
inst✝¹ : Category.{u_9, u_5} D₂
inst✝ : Category.{u_10, u_6} D₃
H₁ : C₁ ⥤ D₁
L₁ : C₁ ⥤ C₂
R₁ : D₁ ⥤ D₂
H₂ : C₂ ⥤ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : C₃ ⥤ D₃
E : C₂ ≌ C₃
E' : D₂ ≌ D₃
w' : H₂ ⋙ E'.functor ≅ E.functor ⋙ H₃
L₁₂ : C₁ ⥤ C₃
R₁₂ : D₁ ⥤ D₃
eL : L₁ ⋙ E.functor ≅ L₁₂
eR : R₁ ⋙ E'.functor ≅ R₁₂
⊢ (w.vComp' w'.hom eL eR).GuitartExact ↔ w.GuitartExact

Tactic:
rw [← vComp_iff_of_equivalences w E E' w', TwoSquare.vComp', whiskerVertical_iff]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem coe_eq_zero_iff : (φ : MvPowerSeries σ R) = 0 ↔ φ = 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
φ : MvPolynomial σ R
⊢ ↑φ = 0 ↔ φ = 0

Tactic:
rw [← coe_zero, coe_inj]

Result:
no goals
-- Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean
@[simp] lemma T_empty (f : (∀ i, A i) → ℝ≥0∞) (x : ∀ i, A i) :
    T μ p f ∅ x = f x ^ (1 + p)

Proof state:
ι : Type u_1
A : ι → Type u_2
inst✝¹ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝ : DecidableEq ι
p : ℝ
f : ((i : ι) → A i) → ℝ≥0∞
x : (i : ι) → A i
⊢ T μ p f ∅ x = f x ^ (1 + p)

Tactic:
simp [T]

Result:
no goals
-- Mathlib/Data/QPF/Univariate/Basic.lean
theorem Cofix.dest_corec {α : Type u} (g : α → F α) (x : α) :
    Cofix.dest (Cofix.corec g x) = Cofix.corec g <$> g x

Proof state:
F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
⊢ (corec g x).dest = corec g <$> g x

Tactic:
conv =>
  lhs
  rw [Cofix.dest, Cofix.corec]

Result:
F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
⊢ Quot.lift (fun x => Quot.mk Mcongr <$> abs x.dest) ⋯ (Quot.mk Mcongr (corecF g x)) = corec g <$> g x

Proof state:
F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
⊢ Quot.mk Mcongr <$> abs (corecF g x).dest = corec g <$> g x

Tactic:
rw [corecF_eq, abs_map, abs_repr, ← comp_map]

Result:
F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
⊢ (Quot.mk Mcongr ∘ corecF g) <$> g x = corec g <$> g x

Proof state:
F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
⊢ Quot.lift (fun x => Quot.mk Mcongr <$> abs x.dest) ⋯ (Quot.mk Mcongr (corecF g x)) = corec g <$> g x

Tactic:
dsimp

Result:
F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
⊢ Quot.mk Mcongr <$> abs (corecF g x).dest = corec g <$> g x

Proof state:
F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
⊢ (Quot.mk Mcongr ∘ corecF g) <$> g x = corec g <$> g x

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
theorem pow_gcd_eq_one {M : Type*} [Monoid M] (x : M) {m n : ℕ} (hm : x ^ m = 1) (hn : x ^ n = 1) :
    x ^ m.gcd n = 1

Proof state:
case succ.intro
M : Type u_1
inst✝ : Monoid M
n m : ℕ
y : Mˣ
hn : y ^ ↑n = 1
hm : y ^ ↑(m + 1) = 1
⊢ y ^ ↑((m + 1).gcd n) = 1

Tactic:
rw [Nat.gcd_eq_gcd_ab, zpow_add, zpow_mul, zpow_mul, hn, hm, one_zpow, one_zpow, one_mul]

Result:
no goals

Proof state:
case zero
M : Type u_1
inst✝ : Monoid M
x : M
n : ℕ
hn : x ^ n = 1
hm : x ^ 0 = 1
⊢ x ^ Nat.gcd 0 n = 1

Tactic:
simp [hn]

Result:
no goals

Proof state:
case succ
M : Type u_1
inst✝ : Monoid M
x : M
n : ℕ
hn : x ^ n = 1
m : ℕ
hm : x ^ (m + 1) = 1
⊢ x ^ (m + 1).gcd n = 1

Tactic:
obtain ⟨y, rfl⟩ := IsUnit.of_pow_eq_one hm m.succ_ne_zero

Result:
case succ.intro
M : Type u_1
inst✝ : Monoid M
n m : ℕ
y : Mˣ
hn : ↑y ^ n = 1
hm : ↑y ^ (m + 1) = 1
⊢ ↑y ^ (m + 1).gcd n = 1

Proof state:
case succ.intro
M : Type u_1
inst✝ : Monoid M
n m : ℕ
y : Mˣ
hn : ↑y ^ n = 1
hm : ↑y ^ (m + 1) = 1
⊢ ↑y ^ (m + 1).gcd n = 1

Tactic:
rw [← Units.val_pow_eq_pow_val, ← Units.val_one (α := M), ← zpow_natCast, ← Units.ext_iff] at *

Result:
case succ.intro
M : Type u_1
inst✝ : Monoid M
n m : ℕ
y : Mˣ
hn : y ^ ↑n = 1
hm : y ^ ↑(m + 1) = 1
⊢ y ^ ↑((m + 1).gcd n) = 1

Proof state:
M : Type u_1
inst✝ : Monoid M
x : M
m n : ℕ
hm : x ^ m = 1
hn : x ^ n = 1
⊢ x ^ m.gcd n = 1

Tactic:
rcases m with (rfl | m)

Result:
case zero
M : Type u_1
inst✝ : Monoid M
x : M
n : ℕ
hn : x ^ n = 1
hm : x ^ 0 = 1
⊢ x ^ Nat.gcd 0 n = 1

case succ
M : Type u_1
inst✝ : Monoid M
x : M
n : ℕ
hn : x ^ n = 1
m : ℕ
hm : x ^ (m + 1) = 1
⊢ x ^ (m + 1).gcd n = 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem xor_self (x : Nat) : x ^^^ x = 0

Proof state:
x : Nat
⊢ x ^^^ x = 0

Tactic:
apply Nat.eq_of_testBit_eq

Result:
case pred
x : Nat
⊢ ∀ (i : Nat), (x ^^^ x).testBit i = testBit 0 i

Proof state:
case pred
x : Nat
⊢ ∀ (i : Nat), (x ^^^ x).testBit i = testBit 0 i

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Turan.lean
theorem isTuranMaximal_of_iso (f : G ≃g turanGraph n r) (hr : 0 < r) : G.IsTuranMaximal r

Proof state:
case intro.intro.intro
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n r : ℕ
f : G ≃g turanGraph n r
hr : 0 < r
J : SimpleGraph V
w✝ : DecidableRel J.Adj
j : J.IsTuranMaximal r
g : J ≃g turanGraph n r
⊢ G.IsTuranMaximal r

Tactic:
use (turanGraph_cliqueFree (n := n) hr).comap f,
  fun H _ cf ↦ (f.symm.comp g).card_edgeFinset_eq ▸ j.2 H cf

Result:
no goals

Proof state:
case intro.intro.intro
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n r : ℕ
f : G ≃g turanGraph n r
hr : 0 < r
J : SimpleGraph V
w✝ : DecidableRel J.Adj
j : J.IsTuranMaximal r
g : J ≃g turanGraph (Fintype.card V) r
⊢ G.IsTuranMaximal r

Tactic:
rw [f.card_eq, Fintype.card_fin] at g

Result:
case intro.intro.intro
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n r : ℕ
f : G ≃g turanGraph n r
hr : 0 < r
J : SimpleGraph V
w✝ : DecidableRel J.Adj
j : J.IsTuranMaximal r
g : J ≃g turanGraph n r
⊢ G.IsTuranMaximal r

Proof state:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n r : ℕ
f : G ≃g turanGraph n r
hr : 0 < r
⊢ G.IsTuranMaximal r

Tactic:
obtain ⟨J, _, j⟩ := exists_isTuranMaximal (V := V) hr

Result:
case intro.intro
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n r : ℕ
f : G ≃g turanGraph n r
hr : 0 < r
J : SimpleGraph V
w✝ : DecidableRel J.Adj
j : J.IsTuranMaximal r
⊢ G.IsTuranMaximal r

Proof state:
case intro.intro
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n r : ℕ
f : G ≃g turanGraph n r
hr : 0 < r
J : SimpleGraph V
w✝ : DecidableRel J.Adj
j : J.IsTuranMaximal r
⊢ G.IsTuranMaximal r

Tactic:
obtain ⟨g⟩ := j.nonempty_iso_turanGraph

Result:
case intro.intro.intro
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n r : ℕ
f : G ≃g turanGraph n r
hr : 0 < r
J : SimpleGraph V
w✝ : DecidableRel J.Adj
j : J.IsTuranMaximal r
g : J ≃g turanGraph (Fintype.card V) r
⊢ G.IsTuranMaximal r
-- Mathlib/Computability/Tape.lean
theorem Tape.move_left_nth {Γ} [Inhabited Γ] :
    ∀ (T : Tape Γ) (i : ℤ), (T.move Dir.left).nth i = T.nth (i - 1)
  | ⟨_, _, _⟩, -(_ + 1 : ℕ) => (ListBlank.nth_succ _ _).symm
  | ⟨_, _, _⟩, 0 => (ListBlank.nth_zero _).symm
  | ⟨_, _, _⟩, 1 => (ListBlank.nth_zero _).trans (ListBlank.head_cons _ _)
  | ⟨a, L, R⟩, (n + 1 : ℕ) + 1 => by
    rw [add_sub_cancel_right]
    change (R.cons a).nth (n + 1) = R.nth n
    rw [ListBlank.nth_succ, ListBlank.tail_cons]

Proof state:
Γ : Type u_1
inst✝ : Inhabited Γ
a : Γ
L R : ListBlank Γ
n : ℕ
⊢ (move Dir.left { head := a, left := L, right := R }).nth (↑(n + 1) + 1) =
    { head := a, left := L, right := R }.nth ↑(n + 1)

Tactic:
change (R.cons a).nth (n + 1) = R.nth n

Result:
Γ : Type u_1
inst✝ : Inhabited Γ
a : Γ
L R : ListBlank Γ
n : ℕ
⊢ (ListBlank.cons a R).nth (n + 1) = R.nth n

Proof state:
Γ : Type u_1
inst✝ : Inhabited Γ
a : Γ
L R : ListBlank Γ
n : ℕ
⊢ (move Dir.left { head := a, left := L, right := R }).nth (↑(n + 1) + 1) =
    { head := a, left := L, right := R }.nth (↑(n + 1) + 1 - 1)

Tactic:
rw [add_sub_cancel_right]

Result:
Γ : Type u_1
inst✝ : Inhabited Γ
a : Γ
L R : ListBlank Γ
n : ℕ
⊢ (move Dir.left { head := a, left := L, right := R }).nth (↑(n + 1) + 1) =
    { head := a, left := L, right := R }.nth ↑(n + 1)

Proof state:
Γ : Type u_1
inst✝ : Inhabited Γ
a : Γ
L R : ListBlank Γ
n : ℕ
⊢ (ListBlank.cons a R).nth (n + 1) = R.nth n

Tactic:
rw [ListBlank.nth_succ, ListBlank.tail_cons]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean
theorem add_le_add_left {a b c : ℚ} : c + a ≤ c + b ↔ a ≤ b

Proof state:
a b c : ℚ
⊢ c + a ≤ c + b ↔ a ≤ b

Tactic:
rw [Rat.le_iff_sub_nonneg, add_sub_add_left_eq_sub, ← Rat.le_iff_sub_nonneg]

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Centralizer.lean
/--
Let `R` be a commutative ring and `A, B` be `R`-algebras where `A` is free as `R`-module.
Then the centralizer of `1 ⊗ B ⊆ A ⊗ B` is `A ⊗ C(B)` where `C(B)` is the center of `B`.
-/
lemma centralizer_range_includeRight_eq_center_tensorProduct [Module.Free R A] :
    Subalgebra.centralizer R
      (Algebra.TensorProduct.includeRight : B →ₐ[R] A ⊗[R] B).range =
    (Algebra.TensorProduct.map (AlgHom.id R A) (center R B).val).range

Proof state:
case h
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Free R A
x✝ : A ⊗[R] B
⊢ x✝ ∈ centralizer R ↑includeRight.range ↔ x✝ ∈ centralizer R ↑(map includeRight ⊤)

Tactic:
simp [includeRight, includeLeftRingHom, Set.range_comp]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Free R A
⊢ centralizer R ↑includeRight.range = centralizer R ↑(map includeRight ⊤)

Tactic:
ext

Result:
case h
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Free R A
x✝ : A ⊗[R] B
⊢ x✝ ∈ centralizer R ↑includeRight.range ↔ x✝ ∈ centralizer R ↑(map includeRight ⊤)

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Free R A
⊢ centralizer R ↑includeRight.range = (Algebra.TensorProduct.map (AlgHom.id R A) (center R B).val).range

Tactic:
rw [← centralizer_univ, ← Algebra.coe_top (R := R) (A := B),
  ← centralizer_coe_map_includeRight_eq_center_tensorProduct R A B ⊤]

Result:
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Free R A
⊢ centralizer R ↑includeRight.range = centralizer R ↑(map includeRight ⊤)
-- Mathlib/Analysis/Fourier/FourierTransform.lean
lemma fourierIntegralInv_comp_linearIsometry (A : W ≃ₗᵢ[ℝ] V) (f : V → E) (w : W) :
    𝓕⁻ (f ∘ A) w = (𝓕⁻ f) (A w)

Proof state:
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
V : Type u_2
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : InnerProductSpace ℝ V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
W : Type u_3
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : InnerProductSpace ℝ W
inst✝³ : MeasurableSpace W
inst✝² : BorelSpace W
inst✝¹ : FiniteDimensional ℝ W
inst✝ : FiniteDimensional ℝ V
A : W ≃ₗᵢ[ℝ] V
f : V → E
w : W
⊢ 𝓕⁻ (f ∘ ⇑A) w = 𝓕⁻ f (A w)

Tactic:
simp [fourierIntegralInv_eq_fourierIntegral_neg, fourierIntegral_comp_linearIsometry]

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Translations.lean
theorem second_contAux_eq {gp : Pair K} (zeroth_s_eq : g.s.get? 0 = some gp) :
    g.contsAux 2 = ⟨gp.b * g.h + gp.a, gp.b⟩

Proof state:
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
gp : Pair K
zeroth_s_eq : g.s.get? 0 = some gp
⊢ g.contsAux 2 = { a := gp.b * g.h + gp.a, b := gp.b }

Tactic:
simp [zeroth_s_eq, contsAux, nextConts, nextDen, nextNum]

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem Filter.coprod_cocompact :
    (Filter.cocompact X).coprod (Filter.cocompact Y) = Filter.cocompact (X × Y)

Proof state:
case a
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ cocompact (X × Y) ≤ (cocompact X).coprod (cocompact Y)

Tactic:
refine (hasBasis_cocompact.coprod hasBasis_cocompact).ge_iff.2 fun K hK ↦ ?_

Result:
case a
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
K : Set X × Set Y
hK : IsCompact K.1 ∧ IsCompact K.2
⊢ Prod.fst ⁻¹' K.1ᶜ ∪ Prod.snd ⁻¹' K.2ᶜ ∈ cocompact (X × Y)

Proof state:
case a
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
K : Set X × Set Y
hK : IsCompact K.1 ∧ IsCompact K.2
⊢ Prod.fst ⁻¹' K.1ᶜ ∪ Prod.snd ⁻¹' K.2ᶜ ∈ cocompact (X × Y)

Tactic:
rw [← univ_prod, ← prod_univ, ← compl_prod_eq_union]

Result:
case a
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
K : Set X × Set Y
hK : IsCompact K.1 ∧ IsCompact K.2
⊢ (K.1 ×ˢ K.2)ᶜ ∈ cocompact (X × Y)

Proof state:
case a
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
K : Set X × Set Y
hK : IsCompact K.1 ∧ IsCompact K.2
⊢ (K.1 ×ˢ K.2)ᶜ ∈ cocompact (X × Y)

Tactic:
exact (hK.1.prod hK.2).compl_mem_cocompact

Result:
no goals

Proof state:
case a
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ (cocompact X).coprod (cocompact Y) ≤ cocompact (X × Y)

Tactic:
exact sup_le (comap_cocompact_le continuous_fst) (comap_cocompact_le continuous_snd)

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ (cocompact X).coprod (cocompact Y) = cocompact (X × Y)

Tactic:
apply le_antisymm

Result:
case a
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ (cocompact X).coprod (cocompact Y) ≤ cocompact (X × Y)

case a
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ cocompact (X × Y) ≤ (cocompact X).coprod (cocompact Y)
-- Mathlib/Combinatorics/Quiver/Covering.lean
theorem Prefunctor.costar_conj_star (u : U) :
    φ.costar u = Quiver.starEquivCostar (φ.obj u) ∘ φ.star u ∘ (Quiver.starEquivCostar u).symm

Proof state:
U : Type u_1
inst✝⁴ : Quiver U
V : Type u_2
inst✝³ : Quiver V
φ : U ⥤q V
inst✝² : HasInvolutiveReverse U
inst✝¹ : HasInvolutiveReverse V
inst✝ : φ.MapReverse
u : U
⊢ φ.costar u = ⇑(starEquivCostar (φ.obj u)) ∘ φ.star u ∘ ⇑(starEquivCostar u).symm

Tactic:
ext ⟨v, f⟩ <;> simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Lemmas.lean
theorem MeasureTheory.MeasurePreserving.aestronglyMeasurable_comp_iff {β : Type*}
    {f : α → β} {mα : MeasurableSpace α} {μa : Measure α} {mβ : MeasurableSpace β} {μb : Measure β}
    (hf : MeasurePreserving f μa μb) (h₂ : MeasurableEmbedding f) {g : β → γ} :
    AEStronglyMeasurable (g ∘ f) μa ↔ AEStronglyMeasurable g μb

Proof state:
α : Type u_1
γ : Type u_3
inst✝ : TopologicalSpace γ
β : Type u_4
f : α → β
mα : MeasurableSpace α
μa : Measure α
mβ : MeasurableSpace β
μb : Measure β
hf : MeasurePreserving f μa μb
h₂ : MeasurableEmbedding f
g : β → γ
⊢ AEStronglyMeasurable (g ∘ f) μa ↔ AEStronglyMeasurable g μb

Tactic:
rw [← hf.map_eq, h₂.aestronglyMeasurable_map_iff]

Result:
no goals
-- Mathlib/Analysis/Convex/Gauge.lean
theorem continuousAt_gauge_zero (hs : s ∈ 𝓝 0) : ContinuousAt (gauge s) 0

Proof state:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hs : s ∈ 𝓝 0
⊢ ContinuousAt (gauge s) 0

Tactic:
rw [ContinuousAt, gauge_zero]

Result:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hs : s ∈ 𝓝 0
⊢ Tendsto (gauge s) (𝓝 0) (𝓝 0)

Proof state:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hs : s ∈ 𝓝 0
⊢ Tendsto (gauge s) (𝓝 0) (𝓝 0)

Tactic:
exact tendsto_gauge_nhds_zero hs

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma iterate_even (hf : Involutive f) (hn : Even n) : f^[n] = id

Proof state:
α : Type u_4
f : α → α
n : ℕ
hf : Involutive f
hn : Even n
⊢ f^[n] = id

Tactic:
obtain ⟨m, rfl⟩ := hn

Result:
case intro
α : Type u_4
f : α → α
hf : Involutive f
m : ℕ
⊢ f^[m + m] = id

Proof state:
case intro
α : Type u_4
f : α → α
hf : Involutive f
m : ℕ
⊢ f^[m + m] = id

Tactic:
rw [← two_mul, hf.iterate_two_mul]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem div_le_div'' (hab : a ≤ b) (hcd : c ≤ d) : a / d ≤ b / c

Proof state:
α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : MulLeftMono α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
⊢ a * c ≤ b * d

Tactic:
exact mul_le_mul' hab hcd

Result:
no goals

Proof state:
α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : MulLeftMono α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
⊢ a / d ≤ b / c

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, mul_comm b, mul_inv_le_inv_mul_iff, mul_comm]

Result:
α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : MulLeftMono α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
⊢ a * c ≤ b * d
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean
theorem go_get (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w)
    (curr : Nat) (hcurr : curr ≤ w) (s : AIG.RefVec aig curr) :
    ∀ (idx : Nat) (hidx : idx < curr),
        (go aig input distance curr hcurr s).vec.get idx (by omega)
          =
        (s.get idx hidx).cast (by apply go_le_size)

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
idx : Nat
hidx : idx < curr
⊢ idx < w

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
idx✝ : Nat
hidx✝ : idx✝ < curr
⊢ (go aig input distance curr hcurr s).vec.get idx✝ ⋯ = (s.get idx✝ hidx✝).cast ⋯

Tactic:
apply go_get_aux

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
⊢ ∀ (idx : Nat) (hidx : idx < curr), (go aig input distance curr hcurr s).vec.get idx ⋯ = (s.get idx hidx).cast ⋯

Tactic:
intros

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
idx✝ : Nat
hidx✝ : idx✝ < curr
⊢ (go aig input distance curr hcurr s).vec.get idx✝ ⋯ = (s.get idx✝ hidx✝).cast ⋯

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
idx : Nat
hidx : idx < curr
⊢ aig.decls.size ≤ (go aig input distance curr hcurr s).aig.decls.size

Tactic:
apply go_le_size

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Pi.lean
lemma disjoint_iInf_maxGenEigenspace {χ₁ χ₂ : ι → R} (h : χ₁ ≠ χ₂) :
    Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (⨅ i, (f i).maxGenEigenspace (χ₂ i))

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
f : ι → End R M
inst✝ : NoZeroSMulDivisors R M
χ₁ χ₂ : ι → R
h : χ₁ ≠ χ₂
⊢ Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (⨅ i, (f i).maxGenEigenspace (χ₂ i))

Tactic:
obtain ⟨j, hj⟩ : ∃ j, χ₁ j ≠ χ₂ j := Function.ne_iff.mp h

Result:
case intro
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
f : ι → End R M
inst✝ : NoZeroSMulDivisors R M
χ₁ χ₂ : ι → R
h : χ₁ ≠ χ₂
j : ι
hj : χ₁ j ≠ χ₂ j
⊢ Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (⨅ i, (f i).maxGenEigenspace (χ₂ i))

Proof state:
case intro
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
f : ι → End R M
inst✝ : NoZeroSMulDivisors R M
χ₁ χ₂ : ι → R
h : χ₁ ≠ χ₂
j : ι
hj : χ₁ j ≠ χ₂ j
⊢ Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (⨅ i, (f i).maxGenEigenspace (χ₂ i))

Tactic:
exact (End.disjoint_genEigenspace (f j) hj ⊤ ⊤).mono (iInf_le _ j) (iInf_le _ j)

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem cond {c : α → Bool} {f : α → σ} {g : α → σ} (hc : Primrec c) (hf : Primrec f)
    (hg : Primrec g) : Primrec fun a => bif (c a) then (f a) else (g a) :=
  (nat_casesOn (encode_iff.2 hc) hg (hf.comp fst).to₂).of_eq fun a => by cases c a <;> rfl

Proof state:
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
c : α → Bool
f g : α → σ
hc : Primrec c
hf : Primrec f
hg : Primrec g
a : α
⊢ (Nat.casesOn (encode (c a)) (g a) fun b => f (a, b).1) = bif c a then f a else g a

Tactic:
cases c a <;> rfl

Result:
no goals