harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
theorem IsBlockSystem.of_normal {N : Subgroup G} [N.Normal] :
    IsBlockSystem G (Set.range fun a : X => orbit N a)

Proof state:
case right
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
b : Set X
⊢ (b ∈ range fun a => orbit (↥N) a) → IsBlock G b

Tactic:
rintro ⟨a, rfl⟩

Result:
case right.intro
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
a : X
⊢ IsBlock G ((fun a => orbit (↥N) a) a)

Proof state:
case left
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
⊢ Setoid.IsPartition (range fun a => orbit (↥N) a)

Tactic:
apply IsPartition.of_orbits

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
⊢ IsBlockSystem G (range fun a => orbit (↥N) a)

Tactic:
constructor

Result:
case left
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
⊢ Setoid.IsPartition (range fun a => orbit (↥N) a)

case right
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
⊢ ∀ ⦃B : Set X⦄, (B ∈ range fun a => orbit (↥N) a) → IsBlock G B

Proof state:
case right.intro
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
a : X
⊢ IsBlock G ((fun a => orbit (↥N) a) a)

Tactic:
exact .orbit_of_normal a

Result:
no goals

Proof state:
case right
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
⊢ ∀ ⦃B : Set X⦄, (B ∈ range fun a => orbit (↥N) a) → IsBlock G B

Tactic:
intro b

Result:
case right
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
b : Set X
⊢ (b ∈ range fun a => orbit (↥N) a) → IsBlock G b
-- Mathlib/Combinatorics/SimpleGraph/Sum.lean
theorem chromaticNumber_sum :
    (G ⊕g H).chromaticNumber = max G.chromaticNumber H.chromaticNumber

Proof state:
case coe
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
n : ℕ
hG : G.chromaticNumber ≤ ↑n
hH : H.chromaticNumber ≤ ↑n
cG : G.Coloring (Fin n) := Nonempty.some ⋯
cH : H.Coloring (Fin n) := Nonempty.some ⋯
⊢ (G ⊕g H).chromaticNumber ≤ ↑n

Tactic:
exact chromaticNumber_le_iff_colorable.mpr (Nonempty.intro (cG.sum cH))

Result:
no goals

Proof state:
case coe
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
n : ℕ
hG : G.chromaticNumber ≤ ↑n
hH : H.chromaticNumber ≤ ↑n
cG : G.Coloring (Fin n) := Nonempty.some ⋯
⊢ (G ⊕g H).chromaticNumber ≤ ↑n

Tactic:
let cH : H.Coloring (Fin n) := (chromaticNumber_le_iff_colorable.mp hH).some

Result:
case coe
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
n : ℕ
hG : G.chromaticNumber ≤ ↑n
hH : H.chromaticNumber ≤ ↑n
cG : G.Coloring (Fin n) := Nonempty.some ⋯
cH : H.Coloring (Fin n) := Nonempty.some ⋯
⊢ (G ⊕g H).chromaticNumber ≤ ↑n

Proof state:
case top
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
hG : G.chromaticNumber ≤ ⊤
hH : H.chromaticNumber ≤ ⊤
⊢ (G ⊕g H).chromaticNumber ≤ ⊤

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
⊢ (G ⊕g H).chromaticNumber = G.chromaticNumber ⊔ H.chromaticNumber

Tactic:
refine eq_max chromaticNumber_le_sum_left chromaticNumber_le_sum_right fun {d} hG hH => ?_

Result:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
d : ℕ∞
hG : G.chromaticNumber ≤ d
hH : H.chromaticNumber ≤ d
⊢ (G ⊕g H).chromaticNumber ≤ d

Proof state:
case coe
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
n : ℕ
hG : G.chromaticNumber ≤ ↑n
hH : H.chromaticNumber ≤ ↑n
⊢ (G ⊕g H).chromaticNumber ≤ ↑n

Tactic:
let cG : G.Coloring (Fin n) := (chromaticNumber_le_iff_colorable.mp hG).some

Result:
case coe
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
n : ℕ
hG : G.chromaticNumber ≤ ↑n
hH : H.chromaticNumber ≤ ↑n
cG : G.Coloring (Fin n) := Nonempty.some ⋯
⊢ (G ⊕g H).chromaticNumber ≤ ↑n

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
d : ℕ∞
hG : G.chromaticNumber ≤ d
hH : H.chromaticNumber ≤ d
⊢ (G ⊕g H).chromaticNumber ≤ d

Tactic:
cases d with
| top => simp
| coe n =>
  let cG : G.Coloring (Fin n) := (chromaticNumber_le_iff_colorable.mp hG).some
  let cH : H.Coloring (Fin n) := (chromaticNumber_le_iff_colorable.mp hH).some
  exact chromaticNumber_le_iff_colorable.mpr (Nonempty.intro (cG.sum cH))

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem cons_injective2 : Function.Injective2 (cons : α → Seq α → Seq α) := fun x y s t h =>
  ⟨by rw [← Option.some_inj, ← get?_cons_zero, h, get?_cons_zero],
    Seq.ext fun n => by simp_rw [← get?_cons_succ x s n, h, get?_cons_succ]⟩

Proof state:
α : Type u
x y : α
s t : Seq α
h : cons x s = cons y t
⊢ x = y

Tactic:
rw [← Option.some_inj, ← get?_cons_zero, h, get?_cons_zero]

Result:
no goals

Proof state:
α : Type u
x y : α
s t : Seq α
h : cons x s = cons y t
n : ℕ
⊢ s.get? n = t.get? n

Tactic:
simp_rw [← get?_cons_succ x s n, h, get?_cons_succ]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
lemma comp (hp : p.Monic) (hq : q.Monic) (h : q.natDegree ≠ 0) : (p.comp q).Monic

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : q.natDegree ≠ 0
a✝ : Nontrivial R
⊢ p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0

Tactic:
simp [hp.leadingCoeff, hq.leadingCoeff]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : q.natDegree ≠ 0
⊢ (p.comp q).Monic

Tactic:
nontriviality R

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : q.natDegree ≠ 0
a✝ : Nontrivial R
⊢ (p.comp q).Monic

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : q.natDegree ≠ 0
a✝ : Nontrivial R
⊢ (p.comp q).Monic

Tactic:
have : (p.comp q).natDegree = p.natDegree * q.natDegree :=
  natDegree_comp_eq_of_mul_ne_zero <| by simp [hp.leadingCoeff, hq.leadingCoeff]

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : q.natDegree ≠ 0
a✝ : Nontrivial R
this : (p.comp q).natDegree = p.natDegree * q.natDegree
⊢ (p.comp q).Monic

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : q.natDegree ≠ 0
a✝ : Nontrivial R
this : (p.comp q).natDegree = p.natDegree * q.natDegree
⊢ (p.comp q).Monic

Tactic:
rw [Monic.def, Polynomial.leadingCoeff, this, coeff_comp_degree_mul_degree h, hp.leadingCoeff,
  hq.leadingCoeff, one_pow, mul_one]

Result:
no goals
-- Mathlib/Data/Set/Countable.lean
theorem Countable.image {s : Set α} (hs : s.Countable) (f : α → β) : (f '' s).Countable

Proof state:
α : Type u
β : Type v
s : Set α
hs : s.Countable
f : α → β
⊢ (f '' s).Countable

Tactic:
rw [image_eq_range]

Result:
α : Type u
β : Type v
s : Set α
hs : s.Countable
f : α → β
⊢ (range fun x => f ↑x).Countable

Proof state:
α : Type u
β : Type v
s : Set α
hs : s.Countable
f : α → β
⊢ (range fun x => f ↑x).Countable

Tactic:
have := hs.to_subtype

Result:
α : Type u
β : Type v
s : Set α
hs : s.Countable
f : α → β
this : Countable ↑s
⊢ (range fun x => f ↑x).Countable

Proof state:
α : Type u
β : Type v
s : Set α
hs : s.Countable
f : α → β
this : Countable ↑s
⊢ (range fun x => f ↑x).Countable

Tactic:
apply countable_range

Result:
no goals
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem natSepDegree_eq_one_iff_eq_X_sub_C_pow : (minpoly F x).natSepDegree = 1 ↔
    ∃ n : ℕ, (minpoly F x).map (algebraMap F E) = (X - C x) ^ q ^ n

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
⊢ (minpoly F x).natSepDegree = 1 ↔ ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨n, h⟩ ↦ (natSepDegree_eq_one_iff_pow_mem q).2 ?_⟩

Result:
case refine_1
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
h : (minpoly F x).natSepDegree = 1
⊢ ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n

case refine_2
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
x✝ : ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n
n : ℕ
h : Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n
⊢ ∃ n, x ^ q ^ n ∈ (algebraMap F E).range

Proof state:
case refine_2
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
x✝ : ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n
n : ℕ
h : (algebraMap F E) ((minpoly F x).coeff 0) = -1 * x ^ q ^ n
⊢ ∃ n, x ^ q ^ n ∈ (algebraMap F E).range

Tactic:
exact ⟨n, -(minpoly F x).coeff 0, by rw [map_neg, h, neg_mul, one_mul, neg_neg]⟩

Result:
no goals

Proof state:
case refine_1.intro.intro
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
h✝ : (minpoly F x).natSepDegree = 1
n : ℕ
y : F
h : minpoly F x = X ^ q ^ n - C y
⊢ ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n

Tactic:
have hx := congr_arg (Polynomial.aeval x) h.symm

Result:
case refine_1.intro.intro
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
h✝ : (minpoly F x).natSepDegree = 1
n : ℕ
y : F
h : minpoly F x = X ^ q ^ n - C y
hx : (Polynomial.aeval x) (X ^ q ^ n - C y) = (Polynomial.aeval x) (minpoly F x)
⊢ ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma Y_ne_negY_of_Y_ne [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P)
    (hQ : W'.Equation Q) (hx : P x * Q z ^ 2 = Q x * P z ^ 2) (hy : P y * Q z ^ 3 ≠ Q y * P z ^ 3) :
    P y ≠ W'.negY P

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 ≠ Q y * P z ^ 3
hy' : P y * Q z ^ 3 - W'.negY Q * P z ^ 3 = 0
⊢ P y ≠ W'.negY P

Tactic:
contrapose! hy

Result:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy' : P y * Q z ^ 3 - W'.negY Q * P z ^ 3 = 0
hy : P y = W'.negY P
⊢ P y * Q z ^ 3 = Q y * P z ^ 3

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy' : P y * Q z ^ 3 - W'.negY Q * P z ^ 3 = 0
hy : P y = W'.negY P
⊢ P y * Q z ^ 3 = Q y * P z ^ 3

Tactic:
linear_combination (norm := ring1) Y_sub_Y_add_Y_sub_negY hx + Q z ^ 3 * hy - hy'

Result:
no goals

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 ≠ Q y * P z ^ 3
⊢ P y ≠ W'.negY P

Tactic:
have hy' : P y * Q z ^ 3 - W'.negY Q * P z ^ 3 = 0 :=
  (mul_eq_zero.mp <| Y_sub_Y_mul_Y_sub_negY hP hQ hx).resolve_left <| sub_ne_zero_of_ne hy

Result:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 ≠ Q y * P z ^ 3
hy' : P y * Q z ^ 3 - W'.negY Q * P z ^ 3 = 0
⊢ P y ≠ W'.negY P
-- Mathlib/Analysis/RCLike/Basic.lean
@[simp, rclike_simps, norm_cast] lemma nnnorm_natCast (n : ℕ) : ‖(n : K)‖₊ = n

Proof state:
K : Type u_1
inst✝ : RCLike K
n : ℕ
⊢ ‖↑n‖₊ = ↑n

Tactic:
simp [nnnorm]

Result:
no goals
-- Mathlib/Data/List/Permutation.lean
theorem mem_permutationsAux_of_perm :
    ∀ {ts is l : List α},
      l ~ is ++ ts → (∃ (is' : _) (_ : is' ~ is), l = is' ++ ts) ∨ l ∈ permutationsAux ts is

Proof state:
case inr
α : Type u_1
t : α
ts is : List α
IH1 :
  ∀ (l : List α), l ~ t :: is ++ ts → (∃ is', ∃ (_ : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is', ∃ (_ : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []
l : List α
p : l ~ is ++ t :: ts
m : l ∈ ts.permutationsAux (t :: is)
⊢ (∃ is', ∃ (_ : is' ~ is), l = is' ++ t :: ts) ∨
    l ∈ ts.permutationsAux (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts

Tactic:
exact Or.inr (Or.inl m)

Result:
no goals
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem xz_sub {m n} (h : n ≤ m) :
    xz a1 (m - n) = xz a1 m * xz a1 n - d a1 * yz a1 m * yz a1 n

Proof state:
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
⊢ xz a1 (m - n) = xz a1 m * xz a1 n + ↑(Pell.d a1) * yz a1 m * -yz a1 n

Tactic:
exact congr_arg Zsqrtd.re (pellZd_sub a1 h)

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
⊢ xz a1 (m - n) = xz a1 m * xz a1 n - ↑(Pell.d a1) * yz a1 m * yz a1 n

Tactic:
rw [sub_eq_add_neg, ← mul_neg]

Result:
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
⊢ xz a1 (m - n) = xz a1 m * xz a1 n + ↑(Pell.d a1) * yz a1 m * -yz a1 n
-- Mathlib/Order/OmegaCompletePartialOrder.lean
lemma ωSup_eq_of_isLUB {c : Chain α} {a : α} (h : IsLUB (Set.range c) a) : a = ωSup c

Proof state:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
a : α
h : IsLUB (Set.range ⇑c) a
⊢ a = ωSup c

Tactic:
rw [le_antisymm_iff]

Result:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
a : α
h : IsLUB (Set.range ⇑c) a
⊢ a ≤ ωSup c ∧ ωSup c ≤ a

Proof state:
case left
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), c a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), c a ≤ a_1) → a ≤ a_1
⊢ a ≤ ωSup c

Tactic:
apply h.2

Result:
case left.a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), c a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), c a ≤ a_1) → a ≤ a_1
⊢ ∀ (a : ℕ), c a ≤ ωSup c

Proof state:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
a : α
h : IsLUB (Set.range ⇑c) a
⊢ a ≤ ωSup c ∧ ωSup c ≤ a

Tactic:
simp only [IsLUB, IsLeast, upperBounds, lowerBounds, Set.mem_range, forall_exists_index,
  forall_apply_eq_imp_iff, Set.mem_setOf_eq] at h

Result:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), c a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), c a ≤ a_1) → a ≤ a_1
⊢ a ≤ ωSup c ∧ ωSup c ≤ a

Proof state:
case right
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), c a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), c a ≤ a_1) → a ≤ a_1
⊢ ωSup c ≤ a

Tactic:
rw [ωSup_le_iff]

Result:
case right
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), c a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), c a ≤ a_1) → a ≤ a_1
⊢ ∀ (i : ℕ), c i ≤ a

Proof state:
case left.a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), c a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), c a ≤ a_1) → a ≤ a_1
⊢ ∀ (a : ℕ), c a ≤ ωSup c

Tactic:
exact fun a ↦ le_ωSup c a

Result:
no goals

Proof state:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), c a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), c a ≤ a_1) → a ≤ a_1
⊢ a ≤ ωSup c ∧ ωSup c ≤ a

Tactic:
constructor

Result:
case left
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), c a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), c a ≤ a_1) → a ≤ a_1
⊢ a ≤ ωSup c

case right
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), c a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), c a ≤ a_1) → a ≤ a_1
⊢ ωSup c ≤ a

Proof state:
case right
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), c a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), c a ≤ a_1) → a ≤ a_1
⊢ ∀ (i : ℕ), c i ≤ a

Tactic:
apply h.1

Result:
no goals
-- Mathlib/Data/Finset/Prod.lean
theorem offDiag_card : (offDiag s).card = s.card * s.card - s.card :=
  suffices (diag s).card + (offDiag s).card = s.card * s.card by rw [s.diag_card] at this; omega
  by rw [← card_product, diag, offDiag]
     conv_rhs => rw [← filter_card_add_filter_neg_card_eq_card (fun a => a.1 = a.2)]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
this : #s.diag + #s.offDiag = #s * #s
⊢ #s.offDiag = #s * #s - #s

Tactic:
rw [s.diag_card] at this

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
this : #s + #s.offDiag = #s * #s
⊢ #s.offDiag = #s * #s - #s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ #s.diag + #s.offDiag = #s * #s

Tactic:
rw [← card_product, diag, offDiag]

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ #(filter (fun a => a.1 = a.2) (s ×ˢ s)) + #(filter (fun a => a.1 ≠ a.2) (s ×ˢ s)) = #(s ×ˢ s)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
this : #s + #s.offDiag = #s * #s
⊢ #s.offDiag = #s * #s - #s

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ #(filter (fun a => a.1 = a.2) (s ×ˢ s)) + #(filter (fun a => a.1 ≠ a.2) (s ×ˢ s)) = #(s ×ˢ s)

Tactic:
conv_rhs => rw [← filter_card_add_filter_neg_card_eq_card (fun a => a.1 = a.2)]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma rpow_sub_intCast {x : ℝ} (hx : x ≠ 0) (y : ℝ) (n : ℕ) : x ^ (y - n) = x ^ y / x ^ n

Proof state:
x : ℝ
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ x ^ (y - ↑n) = x ^ y / x ^ n

Tactic:
simpa using rpow_add_intCast hx y (-n)

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem symm_trans_swap_trans [DecidableEq β] (a b : α) (e : α ≃ β) :
    (e.symm.trans (swap a b)).trans e = swap (e a) (e b) :=
  Equiv.ext fun x => by
    have : ∀ a, e.symm x = a ↔ x = e a := fun a => by
      rw [@eq_comm _ (e.symm x)]
      constructor <;> intros <;> simp_all
    simp only [trans_apply, swap_apply_def, this]
    split_ifs <;> simp

Proof state:
α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a✝ b : α
e : α ≃ β
x : β
a : α
⊢ a = e.symm x ↔ x = e a

Tactic:
constructor <;> intros <;> simp_all

Result:
no goals

Proof state:
α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b : α
e : α ≃ β
x : β
this : ∀ (a : α), e.symm x = a ↔ x = e a
⊢ e (if x = e a then b else if x = e b then a else e.symm x) = if x = e a then e b else if x = e b then e a else x

Tactic:
split_ifs <;> simp

Result:
no goals

Proof state:
α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a✝ b : α
e : α ≃ β
x : β
a : α
⊢ e.symm x = a ↔ x = e a

Tactic:
rw [@eq_comm _ (e.symm x)]

Result:
α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a✝ b : α
e : α ≃ β
x : β
a : α
⊢ a = e.symm x ↔ x = e a

Proof state:
α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b : α
e : α ≃ β
x : β
this : ∀ (a : α), e.symm x = a ↔ x = e a
⊢ ((e.symm.trans (swap a b)).trans e) x = (swap (e a) (e b)) x

Tactic:
simp only [trans_apply, swap_apply_def, this]

Result:
α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b : α
e : α ≃ β
x : β
this : ∀ (a : α), e.symm x = a ↔ x = e a
⊢ e (if x = e a then b else if x = e b then a else e.symm x) = if x = e a then e b else if x = e b then e a else x

Proof state:
α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b : α
e : α ≃ β
x : β
⊢ ((e.symm.trans (swap a b)).trans e) x = (swap (e a) (e b)) x

Tactic:
have : ∀ a, e.symm x = a ↔ x = e a := fun a => by
  rw [@eq_comm _ (e.symm x)]
  constructor <;> intros <;> simp_all

Result:
α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b : α
e : α ≃ β
x : β
this : ∀ (a : α), e.symm x = a ↔ x = e a
⊢ ((e.symm.trans (swap a b)).trans e) x = (swap (e a) (e b)) x
-- Mathlib/LinearAlgebra/Alternating/DomCoprod.lean
theorem domCoprod.summand_eq_zero_of_smul_invariant (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁)
    (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) (σ : Perm.ModSumCongr ιa ιb) {v : ιa ⊕ ιb → Mᵢ}
    {i j : ιa ⊕ ιb} (hv : v i = v j) (hij : i ≠ j) :
    swap i j • σ = σ → domCoprod.summand a b σ v = 0

Proof state:
case h.e'_2.h.e'_10
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ✝ : Perm.ModSumCongr ιa ιb
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
i' j' : ιb
hv : v (σ (Sum.inr i')) = v (σ (Sum.inr j'))
hij : σ (Sum.inr i') ≠ σ (Sum.inr j')
hσ✝ : swap (σ (Sum.inr i')) (σ (Sum.inr j')) • Quotient.mk'' σ = Quotient.mk'' σ
⊢ (↑b fun i => v (σ (Sum.inr i))) = 0

Tactic:
exact AlternatingMap.map_eq_zero_of_eq _ _ hv fun hij' => hij (hij' ▸ rfl)

Result:
no goals
-- Mathlib/Topology/MetricSpace/Defs.lean
theorem subsingleton_closedBall (x : γ) {r : ℝ} (hr : r ≤ 0) : (closedBall x r).Subsingleton

Proof state:
case inl
γ : Type w
inst✝ : MetricSpace γ
x : γ
r : ℝ
hr✝ : r ≤ 0
hr : r < 0
⊢ (closedBall x r).Subsingleton

Tactic:
rw [closedBall_eq_empty.2 hr]

Result:
case inl
γ : Type w
inst✝ : MetricSpace γ
x : γ
r : ℝ
hr✝ : r ≤ 0
hr : r < 0
⊢ ∅.Subsingleton

Proof state:
γ : Type w
inst✝ : MetricSpace γ
x : γ
r : ℝ
hr : r ≤ 0
⊢ (closedBall x r).Subsingleton

Tactic:
rcases hr.lt_or_eq with (hr | rfl)

Result:
case inl
γ : Type w
inst✝ : MetricSpace γ
x : γ
r : ℝ
hr✝ : r ≤ 0
hr : r < 0
⊢ (closedBall x r).Subsingleton

case inr
γ : Type w
inst✝ : MetricSpace γ
x : γ
hr : 0 ≤ 0
⊢ (closedBall x 0).Subsingleton

Proof state:
case inr
γ : Type w
inst✝ : MetricSpace γ
x : γ
hr : 0 ≤ 0
⊢ (closedBall x 0).Subsingleton

Tactic:
rw [closedBall_zero]

Result:
case inr
γ : Type w
inst✝ : MetricSpace γ
x : γ
hr : 0 ≤ 0
⊢ {x}.Subsingleton

Proof state:
case inl
γ : Type w
inst✝ : MetricSpace γ
x : γ
r : ℝ
hr✝ : r ≤ 0
hr : r < 0
⊢ ∅.Subsingleton

Tactic:
exact subsingleton_empty

Result:
no goals

Proof state:
case inr
γ : Type w
inst✝ : MetricSpace γ
x : γ
hr : 0 ≤ 0
⊢ {x}.Subsingleton

Tactic:
exact subsingleton_singleton

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mem_set (v : Vector α n) (i : Nat) (hi : i < n) (a : α) :
    a ∈ v.set i a hi

Proof state:
α : Type u_1
n : Nat
v : Vector α n
i : Nat
hi : i < n
a : α
⊢ i < n

Tactic:
simpa using hi

Result:
no goals

Proof state:
α : Type u_1
n : Nat
v : Vector α n
i : Nat
hi : i < n
a : α
⊢ (v.set i a hi)[i] = a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
v : Vector α n
i : Nat
hi : i < n
a : α
⊢ a ∈ v.set i a hi

Tactic:
simp [mem_iff_getElem]

Result:
α : Type u_1
n : Nat
v : Vector α n
i : Nat
hi : i < n
a : α
⊢ ∃ i_1 h, (v.set i a hi)[i_1] = a

Proof state:
α : Type u_1
n : Nat
v : Vector α n
i : Nat
hi : i < n
a : α
⊢ ∃ i_1 h, (v.set i a hi)[i_1] = a

Tactic:
exact ⟨i, (by simpa using hi), by simp⟩

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Basic.lean
theorem mem_zero_iff {x : P} : x ∈ (0 : FractionalIdeal S P) ↔ x = 0 :=
  ⟨fun ⟨x', x'_mem_zero, x'_eq_x⟩ => by
    have x'_eq_zero : x' = 0 := x'_mem_zero
    simp [x'_eq_x.symm, x'_eq_zero], fun hx => ⟨0, rfl, by simp [hx]⟩⟩

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
x : P
hx : x = 0
⊢ (Algebra.linearMap R P) 0 = x

Tactic:
simp [hx]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
x : P
x✝ : x ∈ 0
x' : R
x'_mem_zero : x' ∈ ↑0
x'_eq_x : (Algebra.linearMap R P) x' = x
⊢ x = 0

Tactic:
have x'_eq_zero : x' = 0 := x'_mem_zero

Result:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
x : P
x✝ : x ∈ 0
x' : R
x'_mem_zero : x' ∈ ↑0
x'_eq_x : (Algebra.linearMap R P) x' = x
x'_eq_zero : x' = 0
⊢ x = 0

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
x : P
x✝ : x ∈ 0
x' : R
x'_mem_zero : x' ∈ ↑0
x'_eq_x : (Algebra.linearMap R P) x' = x
x'_eq_zero : x' = 0
⊢ x = 0

Tactic:
simp [x'_eq_x.symm, x'_eq_zero]

Result:
no goals