harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/Permutation.lean
theorem map_permutationsAux (f : α → β) :
    ∀ ts is :
    List α, map (map f) (permutationsAux ts is) = permutationsAux (map f ts) (map f is)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
t : α
ts is : List α
IH1 : map (map f) (ts.permutationsAux (t :: is)) = (map f ts).permutationsAux (map f (t :: is))
IH2 : map (map f) (is.permutationsAux []) = (map f is).permutationsAux []
⊢ map (map f) ((t :: ts).permutationsAux is) = (map f (t :: ts)).permutationsAux (map f is)

Tactic:
simp only [foldr_permutationsAux2, map_append, map, map_map_permutationsAux2, permutations,
  flatMap_map, IH1, append_assoc, permutationsAux_cons, flatMap_cons, ← IH2, map_flatMap]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
⊢ ∀ (t : α) (ts is : List α),
    map (map f) (ts.permutationsAux (t :: is)) = (map f ts).permutationsAux (map f (t :: is)) →
      map (map f) (is.permutationsAux []) = (map f is).permutationsAux (map f []) →
        map (map f) ((t :: ts).permutationsAux is) = (map f (t :: ts)).permutationsAux (map f is)

Tactic:
introv IH1 IH2

Result:
α : Type u_1
β : Type u_2
f : α → β
t : α
ts is : List α
IH1 : map (map f) (ts.permutationsAux (t :: is)) = (map f ts).permutationsAux (map f (t :: is))
IH2 : map (map f) (is.permutationsAux []) = (map f is).permutationsAux (map f [])
⊢ map (map f) ((t :: ts).permutationsAux is) = (map f (t :: ts)).permutationsAux (map f is)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
⊢ ∀ (is : List α), map (map f) ([].permutationsAux is) = (map f []).permutationsAux (map f is)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
t : α
ts is : List α
IH1 : map (map f) (ts.permutationsAux (t :: is)) = (map f ts).permutationsAux (map f (t :: is))
IH2 : map (map f) (is.permutationsAux []) = (map f is).permutationsAux (map f [])
⊢ map (map f) ((t :: ts).permutationsAux is) = (map f (t :: ts)).permutationsAux (map f is)

Tactic:
rw [map] at IH2

Result:
α : Type u_1
β : Type u_2
f : α → β
t : α
ts is : List α
IH1 : map (map f) (ts.permutationsAux (t :: is)) = (map f ts).permutationsAux (map f (t :: is))
IH2 : map (map f) (is.permutationsAux []) = (map f is).permutationsAux []
⊢ map (map f) ((t :: ts).permutationsAux is) = (map f (t :: ts)).permutationsAux (map f is)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
⊢ ∀ (ts is : List α), map (map f) (ts.permutationsAux is) = (map f ts).permutationsAux (map f is)

Tactic:
refine permutationsAux.rec (by simp) ?_

Result:
α : Type u_1
β : Type u_2
f : α → β
⊢ ∀ (t : α) (ts is : List α),
    map (map f) (ts.permutationsAux (t :: is)) = (map f ts).permutationsAux (map f (t :: is)) →
      map (map f) (is.permutationsAux []) = (map f is).permutationsAux (map f []) →
        map (map f) ((t :: ts).permutationsAux is) = (map f (t :: ts)).permutationsAux (map f is)
-- Mathlib/Data/Finset/Update.lean
lemma updateFinset_updateFinset_of_subset {s t : Finset ι} (hst : s ⊆ t)
    (x : Π i, π i) (y : Π i : s, π i) (z : Π i : t, π i) :
    updateFinset (updateFinset x s y) t z = updateFinset x t z

Proof state:
case neg
ι : Type u_1
π : ι → Sort u_2
inst✝ : DecidableEq ι
s t : Finset ι
hst : s ⊆ t
x : (i : ι) → π i
y : (i : { x // x ∈ s }) → π ↑i
z : (i : { x // x ∈ t }) → π ↑i
i : ι
h1 : i ∉ t
h2 : i ∉ s
⊢ x i = x i

Tactic:
rfl

Result:
no goals

Proof state:
case h
ι : Type u_1
π : ι → Sort u_2
inst✝ : DecidableEq ι
s t : Finset ι
hst : s ⊆ t
x : (i : ι) → π i
y : (i : { x // x ∈ s }) → π ↑i
z : (i : { x // x ∈ t }) → π ↑i
i : ι
⊢ updateFinset (updateFinset x s y) t z i = updateFinset x t z i

Tactic:
simp only [updateFinset]

Result:
case h
ι : Type u_1
π : ι → Sort u_2
inst✝ : DecidableEq ι
s t : Finset ι
hst : s ⊆ t
x : (i : ι) → π i
y : (i : { x // x ∈ s }) → π ↑i
z : (i : { x // x ∈ t }) → π ↑i
i : ι
⊢ (if h : i ∈ t then z ⟨i, ⋯⟩ else if hi : i ∈ s then y ⟨i, hi⟩ else x i) = if hi : i ∈ t then z ⟨i, hi⟩ else x i

Proof state:
ι : Type u_1
π : ι → Sort u_2
inst✝ : DecidableEq ι
s t : Finset ι
hst : s ⊆ t
x : (i : ι) → π i
y : (i : { x // x ∈ s }) → π ↑i
z : (i : { x // x ∈ t }) → π ↑i
⊢ updateFinset (updateFinset x s y) t z = updateFinset x t z

Tactic:
ext i

Result:
case h
ι : Type u_1
π : ι → Sort u_2
inst✝ : DecidableEq ι
s t : Finset ι
hst : s ⊆ t
x : (i : ι) → π i
y : (i : { x // x ∈ s }) → π ↑i
z : (i : { x // x ∈ t }) → π ↑i
i : ι
⊢ updateFinset (updateFinset x s y) t z i = updateFinset x t z i

Proof state:
case h
ι : Type u_1
π : ι → Sort u_2
inst✝ : DecidableEq ι
s t : Finset ι
hst : s ⊆ t
x : (i : ι) → π i
y : (i : { x // x ∈ s }) → π ↑i
z : (i : { x // x ∈ t }) → π ↑i
i : ι
⊢ (if h : i ∈ t then z ⟨i, ⋯⟩ else if hi : i ∈ s then y ⟨i, hi⟩ else x i) = if hi : i ∈ t then z ⟨i, hi⟩ else x i

Tactic:
split_ifs with h1 h2 <;> try rfl

Result:
case pos
ι : Type u_1
π : ι → Sort u_2
inst✝ : DecidableEq ι
s t : Finset ι
hst : s ⊆ t
x : (i : ι) → π i
y : (i : { x // x ∈ s }) → π ↑i
z : (i : { x // x ∈ t }) → π ↑i
i : ι
h1 : i ∉ t
h2 : i ∈ s
⊢ y ⟨i, h2⟩ = x i

Proof state:
case pos
ι : Type u_1
π : ι → Sort u_2
inst✝ : DecidableEq ι
s t : Finset ι
hst : s ⊆ t
x : (i : ι) → π i
y : (i : { x // x ∈ s }) → π ↑i
z : (i : { x // x ∈ t }) → π ↑i
i : ι
h1 : i ∉ t
h2 : i ∈ s
⊢ y ⟨i, h2⟩ = x i

Tactic:
exact (h1 (hst h2)).elim

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem mod_right' (a : ℕ) {b : ℕ} (hb : Odd b) : J(a | b) = J(a | b % (4 * a))

Proof state:
case inr.intro.intro.intro.e_a
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ χ₈ ↑b ^ e = χ₈ ↑(b % (4 * a)) ^ e

case inr.intro.intro.intro.e_a
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ qrSign b a' * J(↑b | a') = qrSign (b % (4 * a)) a' * J(↑(b % (4 * a)) | a')

Tactic:
swap

Result:
case inr.intro.intro.intro.e_a
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ qrSign b a' * J(↑b | a') = qrSign (b % (4 * a)) a' * J(↑(b % (4 * a)) | a')

case inr.intro.intro.intro.e_a
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ χ₈ ↑b ^ e = χ₈ ↑(b % (4 * a)) ^ e

Proof state:
case inr.intro.intro.intro.e_a.e_a
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ J(χ₄ ↑b | a') = J(χ₄ ↑(b % (4 * a)) | a')

Tactic:
rw [χ₄_nat_mod_four, χ₄_nat_mod_four (b % (4 * a)), mod_mod_of_dvd b (dvd_mul_right 4 a)]

Result:
no goals

Proof state:
case inr.intro.intro.intro.e_a
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ qrSign b a' * J(↑b | a') = qrSign (b % (4 * a)) a' * J(↑(b % (4 * a)) | a')

Tactic:
congr 1

Result:
case inr.intro.intro.intro.e_a.e_a
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ qrSign b a' = qrSign (b % (4 * a)) a'

case inr.intro.intro.intro.e_a.e_a
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ J(↑b | a') = J(↑(b % (4 * a)) | a')
-- Mathlib/Analysis/MeanInequalitiesPow.lean
theorem rpow_add_le_mul_rpow_add_rpow (z₁ z₂ : ℝ≥0) {p : ℝ} (hp : 1 ≤ p) :
    (z₁ + z₂) ^ p ≤ (2 : ℝ≥0) ^ (p - 1) * (z₁ ^ p + z₂ ^ p)

Proof state:
case h.e'_4
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
A : p - 1 ≠ 0
⊢ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p) = 1 / 2 * (2 * z₁) ^ p + 1 / 2 * (2 * z₂) ^ p

Tactic:
simp only [mul_rpow, rpow_sub' A, div_eq_inv_mul, rpow_one, mul_one]

Result:
case h.e'_4
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
A : p - 1 ≠ 0
⊢ 2⁻¹ * 2 ^ p * (z₁ ^ p + z₂ ^ p) = 2⁻¹ * (2 ^ p * z₁ ^ p) + 2⁻¹ * (2 ^ p * z₂ ^ p)

Proof state:
case inl
z₁ z₂ : ℝ≥0
hp : 1 ≤ 1
⊢ z₁ + z₂ ≤ z₁ + z₂

Tactic:
rfl

Result:
no goals

Proof state:
case h.e'_4
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
⊢ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p) = 1 / 2 * (2 * z₁) ^ p + 1 / 2 * (2 * z₂) ^ p

Tactic:
have A : p - 1 ≠ 0 := ne_of_gt (sub_pos.2 h'p)

Result:
case h.e'_4
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
A : p - 1 ≠ 0
⊢ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p) = 1 / 2 * (2 * z₁) ^ p + 1 / 2 * (2 * z₂) ^ p

Proof state:
case h.e'_3
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
⊢ (z₁ + z₂) ^ p = (1 / 2 * (2 * z₁) + 1 / 2 * (2 * z₂)) ^ p

Tactic:
simp only [one_div, inv_mul_cancel_left₀, Ne, mul_eq_zero, two_ne_zero, one_ne_zero,
  not_false_iff]

Result:
no goals

Proof state:
case h.e'_4
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
A : p - 1 ≠ 0
⊢ 2⁻¹ * 2 ^ p * (z₁ ^ p + z₂ ^ p) = 2⁻¹ * (2 ^ p * z₁ ^ p) + 2⁻¹ * (2 ^ p * z₂ ^ p)

Tactic:
ring

Result:
no goals

Proof state:
case inl
z₁ z₂ : ℝ≥0
hp : 1 ≤ 1
⊢ (z₁ + z₂) ^ 1 ≤ 2 ^ (1 - 1) * (z₁ ^ 1 + z₂ ^ 1)

Tactic:
simp only [rpow_one, sub_self, rpow_zero, one_mul]

Result:
case inl
z₁ z₂ : ℝ≥0
hp : 1 ≤ 1
⊢ z₁ + z₂ ≤ z₁ + z₂

Proof state:
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
⊢ (z₁ + z₂) ^ p ≤ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p)

Tactic:
rcases eq_or_lt_of_le hp with (rfl | h'p)

Result:
case inl
z₁ z₂ : ℝ≥0
hp : 1 ≤ 1
⊢ (z₁ + z₂) ^ 1 ≤ 2 ^ (1 - 1) * (z₁ ^ 1 + z₂ ^ 1)

case inr
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
⊢ (z₁ + z₂) ^ p ≤ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p)

Proof state:
case inr
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
⊢ (z₁ + z₂) ^ p ≤ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p)

Tactic:
convert rpow_arith_mean_le_arith_mean2_rpow (1 / 2) (1 / 2) (2 * z₁) (2 * z₂) (add_halves 1) hp
  using 1

Result:
case h.e'_3
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
⊢ (z₁ + z₂) ^ p = (1 / 2 * (2 * z₁) + 1 / 2 * (2 * z₂)) ^ p

case h.e'_4
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
⊢ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p) = 1 / 2 * (2 * z₁) ^ p + 1 / 2 * (2 * z₂) ^ p
-- Mathlib/CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean
/-- If a functor preserves coequalizers and the appropriate coproducts, it preserves colimits. -/
lemma preservesColimit_of_preservesCoequalizers_and_coproduct :
    PreservesColimitsOfShape J G where
  preservesColimit {K}

Proof state:
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.1
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.1 }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ Cofork (G.map s) (G.map t)

Tactic:
refine Cofork.ofπ (G.map i) ?_

Result:
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.1
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.1 }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ G.map s ≫ G.map i = G.map t ≫ G.map i
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_dirac [MeasurableSingletonClass α] (a : α) (f : α → ℝ≥0∞) :
    ∫⁻ a, f a ∂dirac a = f a

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α), f a ∂dirac a = f a

Tactic:
simp [lintegral_congr_ae (ae_eq_dirac f)]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
/-- A matrix is positive semidefinite if and only if it has the form `Bᴴ * B` for some `B`. -/
lemma posSemidef_iff_eq_transpose_mul_self {A : Matrix n n 𝕜} :
    PosSemidef A ↔ ∃ (B : Matrix n n 𝕜), A = Bᴴ * B

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
A : Matrix n n 𝕜
hA : A.PosSemidef
⊢ A = hA.sqrtᴴ * hA.sqrt

Tactic:
simp_rw [← PosSemidef.sq_sqrt hA, pow_two]

Result:
n : Type u_2
𝕜 : Type u_4
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
A : Matrix n n 𝕜
hA : A.PosSemidef
⊢ hA.sqrt * hA.sqrt = hA.sqrtᴴ * hA.sqrt

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
A : Matrix n n 𝕜
⊢ A.PosSemidef ↔ ∃ B, A = Bᴴ * B

Tactic:
classical
refine ⟨fun hA ↦ ⟨hA.sqrt, ?_⟩, fun ⟨B, hB⟩ ↦ (hB ▸ posSemidef_conjTranspose_mul_self B)⟩
simp_rw [← PosSemidef.sq_sqrt hA, pow_two]
rw [hA.posSemidef_sqrt.1]

Result:
no goals

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
A : Matrix n n 𝕜
hA : A.PosSemidef
⊢ hA.sqrt * hA.sqrt = hA.sqrtᴴ * hA.sqrt

Tactic:
rw [hA.posSemidef_sqrt.1]

Result:
no goals

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
A : Matrix n n 𝕜
⊢ A.PosSemidef ↔ ∃ B, A = Bᴴ * B

Tactic:
refine ⟨fun hA ↦ ⟨hA.sqrt, ?_⟩, fun ⟨B, hB⟩ ↦ (hB ▸ posSemidef_conjTranspose_mul_self B)⟩

Result:
n : Type u_2
𝕜 : Type u_4
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
A : Matrix n n 𝕜
hA : A.PosSemidef
⊢ A = hA.sqrtᴴ * hA.sqrt
-- Mathlib/SetTheory/Game/PGame.lean
theorem lt_or_equiv_or_gt_or_fuzzy (x y : PGame) : x < y ∨ (x ≈ y) ∨ y < x ∨ x ‖ y

Proof state:
case inl.inr.h
x y : PGame
h₁ : x ≤ y
h₂ : x ⧏ y
⊢ x < y

Tactic:
exact ⟨h₁, h₂⟩

Result:
no goals

Proof state:
case inr.inl.h.h.h
x y : PGame
h₁ : y ⧏ x
h₂ : y ≤ x
⊢ y < x

Tactic:
exact ⟨h₂, h₁⟩

Result:
no goals

Proof state:
x y : PGame
⊢ x < y ∨ x ≈ y ∨ y < x ∨ x ‖ y

Tactic:
rcases le_or_gf x y with h₁ | h₁ <;> rcases le_or_gf y x with h₂ | h₂

Result:
case inl.inl
x y : PGame
h₁ : x ≤ y
h₂ : y ≤ x
⊢ x < y ∨ x ≈ y ∨ y < x ∨ x ‖ y

case inl.inr
x y : PGame
h₁ : x ≤ y
h₂ : x ⧏ y
⊢ x < y ∨ x ≈ y ∨ y < x ∨ x ‖ y

case inr.inl
x y : PGame
h₁ : y ⧏ x
h₂ : y ≤ x
⊢ x < y ∨ x ≈ y ∨ y < x ∨ x ‖ y

case inr.inr
x y : PGame
h₁ : y ⧏ x
h₂ : x ⧏ y
⊢ x < y ∨ x ≈ y ∨ y < x ∨ x ‖ y

Proof state:
case inr.inl.h.h
x y : PGame
h₁ : y ⧏ x
h₂ : y ≤ x
⊢ y < x ∨ x ‖ y

Tactic:
left

Result:
case inr.inl.h.h.h
x y : PGame
h₁ : y ⧏ x
h₂ : y ≤ x
⊢ y < x

Proof state:
case inr.inr.h
x y : PGame
h₁ : y ⧏ x
h₂ : x ⧏ y
⊢ x ≈ y ∨ y < x ∨ x ‖ y

Tactic:
right

Result:
case inr.inr.h.h
x y : PGame
h₁ : y ⧏ x
h₂ : x ⧏ y
⊢ y < x ∨ x ‖ y

Proof state:
case inl.inl
x y : PGame
h₁ : x ≤ y
h₂ : y ≤ x
⊢ x < y ∨ x ≈ y ∨ y < x ∨ x ‖ y

Tactic:
right

Result:
case inl.inl.h
x y : PGame
h₁ : x ≤ y
h₂ : y ≤ x
⊢ x ≈ y ∨ y < x ∨ x ‖ y

Proof state:
case inr.inr.h.h
x y : PGame
h₁ : y ⧏ x
h₂ : x ⧏ y
⊢ y < x ∨ x ‖ y

Tactic:
right

Result:
case inr.inr.h.h.h
x y : PGame
h₁ : y ⧏ x
h₂ : x ⧏ y
⊢ x ‖ y

Proof state:
case inr.inl
x y : PGame
h₁ : y ⧏ x
h₂ : y ≤ x
⊢ x < y ∨ x ≈ y ∨ y < x ∨ x ‖ y

Tactic:
right

Result:
case inr.inl.h
x y : PGame
h₁ : y ⧏ x
h₂ : y ≤ x
⊢ x ≈ y ∨ y < x ∨ x ‖ y

Proof state:
case inl.inl.h
x y : PGame
h₁ : x ≤ y
h₂ : y ≤ x
⊢ x ≈ y ∨ y < x ∨ x ‖ y

Tactic:
left

Result:
case inl.inl.h.h
x y : PGame
h₁ : x ≤ y
h₂ : y ≤ x
⊢ x ≈ y

Proof state:
case inr.inr.h.h.h
x y : PGame
h₁ : y ⧏ x
h₂ : x ⧏ y
⊢ x ‖ y

Tactic:
exact ⟨h₂, h₁⟩

Result:
no goals

Proof state:
case inr.inl.h
x y : PGame
h₁ : y ⧏ x
h₂ : y ≤ x
⊢ x ≈ y ∨ y < x ∨ x ‖ y

Tactic:
right

Result:
case inr.inl.h.h
x y : PGame
h₁ : y ⧏ x
h₂ : y ≤ x
⊢ y < x ∨ x ‖ y

Proof state:
case inl.inr
x y : PGame
h₁ : x ≤ y
h₂ : x ⧏ y
⊢ x < y ∨ x ≈ y ∨ y < x ∨ x ‖ y

Tactic:
left

Result:
case inl.inr.h
x y : PGame
h₁ : x ≤ y
h₂ : x ⧏ y
⊢ x < y

Proof state:
case inl.inl.h.h
x y : PGame
h₁ : x ≤ y
h₂ : y ≤ x
⊢ x ≈ y

Tactic:
exact ⟨h₁, h₂⟩

Result:
no goals

Proof state:
case inr.inr
x y : PGame
h₁ : y ⧏ x
h₂ : x ⧏ y
⊢ x < y ∨ x ≈ y ∨ y < x ∨ x ‖ y

Tactic:
right

Result:
case inr.inr.h
x y : PGame
h₁ : y ⧏ x
h₂ : x ⧏ y
⊢ x ≈ y ∨ y < x ∨ x ‖ y
-- Mathlib/Order/ConditionallyCompleteLattice/Finset.lean
theorem Set.Finite.lt_ciInf_iff {s : Set ι} {f : ι → α} (hs : s.Finite)
    (h : ∃ x ∈ s, f x ≤ sInf ∅) :
    a < ⨅ i ∈ s, f i ↔ ∀ x ∈ s, a < f x

Proof state:
case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
a✝ : α
⊢ ∀ (x : ι), (if x ∈ s then f x else sInf ∅) = a✝ → a✝ = sInf ∅ ∨ ∃ x ∈ s, f x = a✝

Tactic:
intro x hx

Result:
case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x✝ : ι
hx✝ : x✝ ∈ s
a✝ : α
x : ι
hx : (if x ∈ s then f x else sInf ∅) = a✝
⊢ a✝ = sInf ∅ ∨ ∃ x ∈ s, f x = a✝

Proof state:
case mp.refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
⊢ ⨅ (_ : x ∈ s), f x = f x

Tactic:
simp [hx]

Result:
no goals

Proof state:
case neg
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝¹ : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x✝ : ι
hx✝ : x✝ ∈ s
a✝ : α
x : ι
h✝ : x ∉ s
hx : sInf ∅ = a✝
⊢ a✝ = sInf ∅ ∨ ∃ x ∈ s, f x = a✝

Tactic:
simp_all

Result:
no goals

Proof state:
case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
a✝ : α
⊢ (a✝ ∈ range fun i => ⨅ (_ : i ∈ s), f i) → a✝ ∈ f '' s ∪ {sInf ∅}

Tactic:
simp only [ciInf_eq_ite, dite_eq_ite, mem_range, union_singleton, mem_insert_iff, mem_image,
  forall_exists_index]

Result:
case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
a✝ : α
⊢ ∀ (x : ι), (if x ∈ s then f x else sInf ∅) = a✝ → a✝ = sInf ∅ ∨ ∃ x ∈ s, f x = a✝

Proof state:
case mp.refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
⊢ f x ∈ range fun i => ⨅ (_ : i ∈ s), f i

Tactic:
simp only [mem_range]

Result:
case mp.refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
⊢ ∃ y, ⨅ (_ : y ∈ s), f y = f x
-- Mathlib/CategoryTheory/Shift/Basic.lean
theorem shift_shiftFunctorCompIsoId_hom_app (n m : A) (h : n + m = 0) (X : C) :
    ((shiftFunctorCompIsoId C n m h).hom.app X)⟦n⟧' =
    (shiftFunctorCompIsoId C m n
      (by rw [← neg_eq_of_add_eq_zero_left h, add_neg_cancel])).hom.app (X⟦n⟧)

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
n m : A
h : n + m = 0
X : C
⊢ (shiftFunctor C n).map ((shiftFunctorCompIsoId C n m h).hom.app X) =
    (shiftFunctorCompIsoId C m n ⋯).hom.app ((shiftFunctor C n).obj X)

Tactic:
dsimp [shiftFunctorCompIsoId]

Result:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
n m : A
h : n + m = 0
X : C
⊢ (shiftFunctor C n).map ((shiftFunctorAdd' C n m 0 h).inv.app X ≫ (shiftFunctorZero C A).hom.app X) =
    (shiftFunctorAdd' C m n 0 ⋯).inv.app ((shiftFunctor C n).obj X) ≫
      (shiftFunctorZero C A).hom.app ((shiftFunctor C n).obj X)

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
n m : A
h : n + m = 0
X : C
⊢ (shiftFunctor C n).map ((shiftFunctorAdd' C n m 0 h).inv.app X ≫ (shiftFunctorZero C A).hom.app X) =
    (shiftFunctorAdd' C m n 0 ⋯).inv.app ((shiftFunctor C n).obj X) ≫
      (shiftFunctorZero C A).hom.app ((shiftFunctor C n).obj X)

Tactic:
simpa only [Functor.map_comp, ← shiftFunctorAdd'_zero_add_inv_app n X,
  ← shiftFunctorAdd'_add_zero_inv_app n X]
  using shiftFunctorAdd'_assoc_inv_app n m n 0 0 n h
    (by rw [← neg_eq_of_add_eq_zero_left h, add_neg_cancel]) (by rw [h, zero_add]) X

Result:
no goals

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
n m : A
h : n + m = 0
X : C
⊢ m + n = 0

Tactic:
rw [← neg_eq_of_add_eq_zero_left h, add_neg_cancel]

Result:
no goals

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
n m : A
h : n + m = 0
X : C
⊢ m + n = 0

Tactic:
rw [← neg_eq_of_add_eq_zero_left h, add_neg_cancel]

Result:
no goals

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
n m : A
h : n + m = 0
X : C
⊢ n + m + n = n

Tactic:
rw [h, zero_add]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Expand.lean
theorem rename_expand (f : σ → τ) (p : ℕ) (φ : MvPolynomial σ R) :
    rename f (expand p φ) = expand p (rename f φ)

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
f : σ → τ
p : ℕ
φ : MvPolynomial σ R
⊢ (rename f) ((expand p) φ) = (expand p) ((rename f) φ)

Tactic:
simp [expand, bind₁_rename, rename_bind₁, Function.comp_def]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Finite.lean
lemma disjoint_ofSubtype_of_memFixedPoints_self {g : Perm α}
    (u : Perm (Function.fixedPoints g)) :
    Disjoint (ofSubtype u) g

Proof state:
α : Type u
inst✝ : DecidableEq α
g : Perm α
u : Perm ↑(fixedPoints ⇑g)
⊢ (ofSubtype u).Disjoint g

Tactic:
rw [disjoint_iff_eq_or_eq]

Result:
α : Type u
inst✝ : DecidableEq α
g : Perm α
u : Perm ↑(fixedPoints ⇑g)
⊢ ∀ (x : α), (ofSubtype u) x = x ∨ g x = x

Proof state:
case pos
α : Type u
inst✝ : DecidableEq α
g : Perm α
u : Perm ↑(fixedPoints ⇑g)
x : α
hx : x ∈ fixedPoints ⇑g
⊢ (ofSubtype u) x = x ∨ g x = x

Tactic:
right

Result:
case pos.h
α : Type u
inst✝ : DecidableEq α
g : Perm α
u : Perm ↑(fixedPoints ⇑g)
x : α
hx : x ∈ fixedPoints ⇑g
⊢ g x = x

Proof state:
case pos.h
α : Type u
inst✝ : DecidableEq α
g : Perm α
u : Perm ↑(fixedPoints ⇑g)
x : α
hx : x ∈ fixedPoints ⇑g
⊢ g x = x

Tactic:
exact hx

Result:
no goals

Proof state:
α : Type u
inst✝ : DecidableEq α
g : Perm α
u : Perm ↑(fixedPoints ⇑g)
x : α
⊢ (ofSubtype u) x = x ∨ g x = x

Tactic:
by_cases hx : x ∈ Function.fixedPoints g

Result:
case pos
α : Type u
inst✝ : DecidableEq α
g : Perm α
u : Perm ↑(fixedPoints ⇑g)
x : α
hx : x ∈ fixedPoints ⇑g
⊢ (ofSubtype u) x = x ∨ g x = x

case neg
α : Type u
inst✝ : DecidableEq α
g : Perm α
u : Perm ↑(fixedPoints ⇑g)
x : α
hx : x ∉ fixedPoints ⇑g
⊢ (ofSubtype u) x = x ∨ g x = x

Proof state:
case neg.h
α : Type u
inst✝ : DecidableEq α
g : Perm α
u : Perm ↑(fixedPoints ⇑g)
x : α
hx : x ∉ fixedPoints ⇑g
⊢ (ofSubtype u) x = x

Tactic:
rw [ofSubtype_apply_of_not_mem u hx]

Result:
no goals

Proof state:
case neg
α : Type u
inst✝ : DecidableEq α
g : Perm α
u : Perm ↑(fixedPoints ⇑g)
x : α
hx : x ∉ fixedPoints ⇑g
⊢ (ofSubtype u) x = x ∨ g x = x

Tactic:
left

Result:
case neg.h
α : Type u
inst✝ : DecidableEq α
g : Perm α
u : Perm ↑(fixedPoints ⇑g)
x : α
hx : x ∉ fixedPoints ⇑g
⊢ (ofSubtype u) x = x

Proof state:
α : Type u
inst✝ : DecidableEq α
g : Perm α
u : Perm ↑(fixedPoints ⇑g)
⊢ ∀ (x : α), (ofSubtype u) x = x ∨ g x = x

Tactic:
intro x

Result:
α : Type u
inst✝ : DecidableEq α
g : Perm α
u : Perm ↑(fixedPoints ⇑g)
x : α
⊢ (ofSubtype u) x = x ∨ g x = x
-- Mathlib/Algebra/Order/Ring/Abs.lean
lemma sq_le_sq : a ^ 2 ≤ b ^ 2 ↔ |a| ≤ |b|

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
a b : α
⊢ a ^ 2 ≤ b ^ 2 ↔ |a| ≤ |b|

Tactic:
simpa only [sq_abs] using sq_le_sq₀ (abs_nonneg a) (abs_nonneg b)

Result:
no goals