harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Maps/Basic.lean
theorem of_inverse {f' : Y → X} (h : Continuous f') (l_inv : LeftInverse f f')
    (r_inv : RightInverse f f') : IsClosedMap f := fun s hs => by
  rw [image_eq_preimage_of_inverse r_inv l_inv]
  exact hs.preimage h

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f' : Y → X
h : Continuous f'
l_inv : LeftInverse f f'
r_inv : RightInverse f f'
s : Set X
hs : IsClosed s
⊢ IsClosed (f '' s)

Tactic:
rw [image_eq_preimage_of_inverse r_inv l_inv]

Result:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f' : Y → X
h : Continuous f'
l_inv : LeftInverse f f'
r_inv : RightInverse f f'
s : Set X
hs : IsClosed s
⊢ IsClosed (f' ⁻¹' s)

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f' : Y → X
h : Continuous f'
l_inv : LeftInverse f f'
r_inv : RightInverse f f'
s : Set X
hs : IsClosed s
⊢ IsClosed (f' ⁻¹' s)

Tactic:
exact hs.preimage h

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
lemma cycleOf_ne_one_iff_mem_cycleFactorsFinset {g : Equiv.Perm α} {x : α} :
    g.cycleOf x ≠ 1 ↔ g.cycleOf x ∈ g.cycleFactorsFinset

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
⊢ g.cycleOf x ≠ 1 ↔ g.cycleOf x ∈ g.cycleFactorsFinset

Tactic:
rw [cycleOf_mem_cycleFactorsFinset_iff, mem_support, ne_eq, cycleOf_eq_one_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filterMap_flatten (f : α → Option β) (L : Array (Array α)) :
    filterMap f (flatten L) = flatten (map (filterMap f) L)

Proof state:
case of
α : Type u_1
β : Type u_2
f : α → Option β
xss✝ : List (List α)
⊢ filterMap f (List.map List.toArray xss✝).toArray.flatten =
    (map (fun as => filterMap f as) (List.map List.toArray xss✝).toArray).flatten

Tactic:
simp only [flatten_toArray_map, size_toArray, List.length_flatten, List.filterMap_toArray',
  List.filterMap_flatten, List.map_toArray, List.map_map, Function.comp_def]

Result:
case of
α : Type u_1
β : Type u_2
f : α → Option β
xss✝ : List (List α)
⊢ (List.map (List.filterMap f) xss✝).flatten.toArray =
    (List.map (fun x => (List.filterMap f x).toArray) xss✝).toArray.flatten

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
L : Array (Array α)
⊢ filterMap f L.flatten = (map (fun as => filterMap f as) L).flatten

Tactic:
induction L using array₂_induction

Result:
case of
α : Type u_1
β : Type u_2
f : α → Option β
xss✝ : List (List α)
⊢ filterMap f (List.map List.toArray xss✝).toArray.flatten =
    (map (fun as => filterMap f as) (List.map List.toArray xss✝).toArray).flatten

Proof state:
case of
α : Type u_1
β : Type u_2
f : α → Option β
xss✝ : List (List α)
⊢ (List.map (List.filterMap f) xss✝).flatten.toArray =
    (List.map (fun x => (List.filterMap f x).toArray) xss✝).toArray.flatten

Tactic:
rw [← Function.comp_def, ← List.map_map, flatten_toArray_map]

Result:
no goals
-- Mathlib/Data/Complex/Order.lean
@[simp]
lemma re_eq_neg_norm {z : ℂ} : z.re = -‖z‖ ↔ z ≤ 0

Proof state:
z : ℂ
⊢ z.re = -‖z‖ ↔ z ≤ 0

Tactic:
rw [← neg_eq_iff_eq_neg, neg_re_eq_norm]

Result:
no goals
-- Mathlib/Data/Nat/PrimeFin.lean
@[simp]
lemma nonempty_primeFactors {n : ℕ} : n.primeFactors.Nonempty ↔ 1 < n

Proof state:
n : ℕ
⊢ n.primeFactors.Nonempty ↔ 1 < n

Tactic:
rw [← not_iff_not, Finset.not_nonempty_iff_eq_empty, primeFactors_eq_empty, not_lt,
  Nat.le_one_iff_eq_zero_or_eq_one]

Result:
no goals
-- Mathlib/Topology/Ultrafilter.lean
theorem mapClusterPt_iff_ultrafilter :
    MapClusterPt x F u ↔ ∃ U : Ultrafilter α, U ≤ F ∧ Tendsto u U (𝓝 x)

Proof state:
X : Type u
α : Type u_1
x : X
inst✝ : TopologicalSpace X
F : Filter α
u : α → X
⊢ MapClusterPt x F u ↔ ∃ U, ↑U ≤ F ∧ Tendsto u (↑U) (𝓝 x)

Tactic:
simp_rw [MapClusterPt, ClusterPt, ← Filter.push_pull', map_neBot_iff, tendsto_iff_comap,
  ← le_inf_iff, exists_ultrafilter_iff, inf_comm]

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem coinduction2 (s) (f g : Seq α → Seq β)
    (H :
      ∀ s,
        BisimO (fun s1 s2 : Seq β => ∃ s : Seq α, s1 = f s ∧ s2 = g s) (destruct (f s))
          (destruct (g s))) :
    f s = g s

Proof state:
α : Type u
β : Type v
s : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
⊢ f s = g s

Tactic:
refine eq_of_bisim (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) ?_ ⟨s, rfl, rfl⟩

Result:
α : Type u
β : Type v
s : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
⊢ IsBisimulation fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s

Proof state:
case intro.intro
α : Type u
β : Type v
s✝ : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
s1 s2 : Seq β
s : Seq α
h1 : s1 = f s
h2 : s2 = g s
⊢ BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct

Tactic:
apply H

Result:
no goals

Proof state:
case intro.intro
α : Type u
β : Type v
s✝ : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
s1 s2 : Seq β
s : Seq α
h1 : s1 = f s
h2 : s2 = g s
⊢ BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) s1.destruct s2.destruct

Tactic:
rw [h1, h2]

Result:
case intro.intro
α : Type u
β : Type v
s✝ : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
s1 s2 : Seq β
s : Seq α
h1 : s1 = f s
h2 : s2 = g s
⊢ BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct

Proof state:
α : Type u
β : Type v
s : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
s1 s2 : Seq β
h : ∃ s, s1 = f s ∧ s2 = g s
⊢ BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) s1.destruct s2.destruct

Tactic:
rcases h with ⟨s, h1, h2⟩

Result:
case intro.intro
α : Type u
β : Type v
s✝ : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
s1 s2 : Seq β
s : Seq α
h1 : s1 = f s
h2 : s2 = g s
⊢ BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) s1.destruct s2.destruct

Proof state:
α : Type u
β : Type v
s : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
⊢ IsBisimulation fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s

Tactic:
intro s1 s2 h

Result:
α : Type u
β : Type v
s : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
s1 s2 : Seq β
h : ∃ s, s1 = f s ∧ s2 = g s
⊢ BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) s1.destruct s2.destruct
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
lemma sum_ne_zero_of_injOn_supDegree' (hs : ∃ i ∈ s, f i ≠ 0)
    (hd : (s : Set ι).InjOn (supDegree D ∘ f)) :
    ∑ i ∈ s, f i ≠ 0

Proof state:
case neg.intro.intro
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst✝ : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) ↑s
j✝ : ι
hj✝ : j✝ ∈ s
hne✝ : f j✝ ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
j : ι
hj : j ∈ s
hne : j ≠ i
⊢ supDegree D (∑ i ∈ s, f i) ≠ ⊥

Tactic:
have (k) (hk : k ∈ s) (hne : k ≠ i) : supDegree D (f k) < supDegree D (f i) :=
  ((le_sup hk).trans_eq he).lt_of_ne (hd.ne hk hi hne)

Result:
case neg.intro.intro
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst✝ : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) ↑s
j✝ : ι
hj✝ : j✝ ∈ s
hne✝ : f j✝ ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
j : ι
hj : j ∈ s
hne : j ≠ i
this : ∀ k ∈ s, k ≠ i → supDegree D (f k) < supDegree D (f i)
⊢ supDegree D (∑ i ∈ s, f i) ≠ ⊥

Proof state:
case pos
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst✝ : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) ↑s
j : ι
hj : j ∈ s
hne✝ : f j ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
h : ∀ k ∈ s, k = i
k : ι
hk : k ∈ s
hne : k ≠ j
⊢ f k = 0

Tactic:
rw [h k hk, h j hj] at hne

Result:
case pos
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst✝ : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) ↑s
j : ι
hj : j ∈ s
hne✝ : f j ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
h : ∀ k ∈ s, k = i
k : ι
hk : k ∈ s
hne : i ≠ i
⊢ f k = 0

Proof state:
case intro.intro
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst✝ : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) ↑s
j : ι
hj : j ∈ s
hne : f j ≠ 0
⊢ ∑ i ∈ s, f i ≠ 0

Tactic:
obtain ⟨i, hi, he⟩ := exists_mem_eq_sup _ ⟨j, hj⟩ (supDegree D ∘ f)

Result:
case intro.intro.intro.intro
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst✝ : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) ↑s
j : ι
hj : j ∈ s
hne : f j ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
⊢ ∑ i ∈ s, f i ≠ 0
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cosh_zero : cosh 0 = 1

Proof state:
⊢ cosh 0 = 1

Tactic:
simp [cosh]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem isClosed_zeroLocus (s : Set R) : IsClosed (zeroLocus s)

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ IsClosed (zeroLocus s)

Tactic:
rw [isClosed_iff_zeroLocus]

Result:
R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ ∃ s_1, zeroLocus s = zeroLocus s_1

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ ∃ s_1, zeroLocus s = zeroLocus s_1

Tactic:
exact ⟨s, rfl⟩

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem IsCompact.inv (hs : IsCompact s) : IsCompact s⁻¹

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : InvolutiveInv G
inst✝ : ContinuousInv G
s : Set G
hs : IsCompact s
⊢ IsCompact s⁻¹

Tactic:
rw [← image_inv_eq_inv]

Result:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : InvolutiveInv G
inst✝ : ContinuousInv G
s : Set G
hs : IsCompact s
⊢ IsCompact ((fun x => x⁻¹) '' s)

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : InvolutiveInv G
inst✝ : ContinuousInv G
s : Set G
hs : IsCompact s
⊢ IsCompact ((fun x => x⁻¹) '' s)

Tactic:
exact hs.image continuous_inv

Result:
no goals
-- Mathlib/LinearAlgebra/AnnihilatingPolynomial.lean
theorem annIdealGenerator_eq_zero_iff {a : A} : annIdealGenerator 𝕜 a = 0 ↔ annIdeal 𝕜 a = ⊥

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
⊢ annIdealGenerator 𝕜 a = 0 ↔ annIdeal 𝕜 a = ⊥

Tactic:
simp only [annIdealGenerator, mul_eq_zero, IsPrincipal.eq_bot_iff_generator_eq_zero,
  Polynomial.C_eq_zero, inv_eq_zero, Polynomial.leadingCoeff_eq_zero, or_self_iff]

Result:
no goals
-- Mathlib/RingTheory/WittVector/StructurePolynomial.lean
theorem wittStructureInt_rename {σ : Type*} (Φ : MvPolynomial idx ℤ) (f : idx → σ) (n : ℕ) :
    wittStructureInt p (rename f Φ) n = rename (Prod.map f id) (wittStructureInt p Φ n)

Proof state:
case a
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
σ : Type u_3
Φ : MvPolynomial idx ℤ
f : idx → σ
n : ℕ
⊢ (map (Int.castRingHom ℚ)) (wittStructureInt p ((rename f) Φ) n) =
    (map (Int.castRingHom ℚ)) ((rename (Prod.map f id)) (wittStructureInt p Φ n))

Tactic:
simp only [map_rename, map_wittStructureInt, wittStructureRat, rename_bind₁, rename_rename,
  bind₁_rename]

Result:
case a
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
σ : Type u_3
Φ : MvPolynomial idx ℤ
f : idx → σ
n : ℕ
⊢ (bind₁ fun k => (bind₁ ((fun i => (rename (Prod.mk i)) (W_ ℚ k)) ∘ f)) ((map (Int.castRingHom ℚ)) Φ))
      (xInTermsOfW p ℚ n) =
    (bind₁ fun i => (bind₁ fun i_1 => (rename (Prod.map f id ∘ Prod.mk i_1)) (W_ ℚ i)) ((map (Int.castRingHom ℚ)) Φ))
      (xInTermsOfW p ℚ n)

Proof state:
case a
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
σ : Type u_3
Φ : MvPolynomial idx ℤ
f : idx → σ
n : ℕ
⊢ (bind₁ fun k => (bind₁ ((fun i => (rename (Prod.mk i)) (W_ ℚ k)) ∘ f)) ((map (Int.castRingHom ℚ)) Φ))
      (xInTermsOfW p ℚ n) =
    (bind₁ fun i => (bind₁ fun i_1 => (rename (Prod.map f id ∘ Prod.mk i_1)) (W_ ℚ i)) ((map (Int.castRingHom ℚ)) Φ))
      (xInTermsOfW p ℚ n)

Tactic:
rfl

Result:
no goals

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
σ : Type u_3
Φ : MvPolynomial idx ℤ
f : idx → σ
n : ℕ
⊢ wittStructureInt p ((rename f) Φ) n = (rename (Prod.map f id)) (wittStructureInt p Φ n)

Tactic:
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective

Result:
case a
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
σ : Type u_3
Φ : MvPolynomial idx ℤ
f : idx → σ
n : ℕ
⊢ (map (Int.castRingHom ℚ)) (wittStructureInt p ((rename f) Φ) n) =
    (map (Int.castRingHom ℚ)) ((rename (Prod.map f id)) (wittStructureInt p Φ n))
-- Mathlib/Algebra/Lie/Basic.lean
theorem lie_skew : -⁅y, x⁆ = ⁅x, y⁆

Proof state:
L : Type v
inst✝ : LieRing L
x y : L
⊢ ⁅x + y, x + y⁆ = 0

Tactic:
apply lie_self

Result:
no goals

Proof state:
L : Type v
inst✝ : LieRing L
x y : L
⊢ ⁅x + y, x⁆ + ⁅x + y, y⁆ = 0

Tactic:
rw [← lie_add]

Result:
L : Type v
inst✝ : LieRing L
x y : L
⊢ ⁅x + y, x + y⁆ = 0

Proof state:
L : Type v
inst✝ : LieRing L
x y : L
⊢ -⁅y, x⁆ = ⁅x, y⁆

Tactic:
have h : ⁅x + y, x⁆ + ⁅x + y, y⁆ = 0 := by rw [← lie_add]; apply lie_self

Result:
L : Type v
inst✝ : LieRing L
x y : L
h : ⁅x + y, x⁆ + ⁅x + y, y⁆ = 0
⊢ -⁅y, x⁆ = ⁅x, y⁆

Proof state:
L : Type v
inst✝ : LieRing L
x y : L
h : ⁅x + y, x⁆ + ⁅x + y, y⁆ = 0
⊢ -⁅y, x⁆ = ⁅x, y⁆

Tactic:
simpa [neg_eq_iff_add_eq_zero] using h

Result:
no goals
-- Mathlib/Order/Filter/Subsingleton.lean
lemma Subsingleton.isCountablyGenerated (hl : l.Subsingleton) : IsCountablyGenerated l

Proof state:
case inr.intro
α : Type u_1
x : α
hl : (pure x).Subsingleton
⊢ (pure x).IsCountablyGenerated

Tactic:
exact isCountablyGenerated_pure x

Result:
no goals

Proof state:
case inl
α : Type u_1
hl : ⊥.Subsingleton
⊢ ⊥.IsCountablyGenerated

Tactic:
exact isCountablyGenerated_bot

Result:
no goals

Proof state:
α : Type u_1
l : Filter α
hl : l.Subsingleton
⊢ l.IsCountablyGenerated

Tactic:
rcases subsingleton_iff_bot_or_pure.1 hl with rfl|⟨x, rfl⟩

Result:
case inl
α : Type u_1
hl : ⊥.Subsingleton
⊢ ⊥.IsCountablyGenerated

case inr.intro
α : Type u_1
x : α
hl : (pure x).Subsingleton
⊢ (pure x).IsCountablyGenerated
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem degreeOf_eq_sup (n : σ) (f : MvPolynomial σ R) :
    degreeOf n f = f.support.sup fun m => m n

Proof state:
case e_f
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f : MvPolynomial σ R
⊢ (fun a => Multiset.count n (toMultiset a)) = fun m => m n

Tactic:
ext

Result:
case e_f.h
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f : MvPolynomial σ R
x✝ : σ →₀ ℕ
⊢ Multiset.count n (toMultiset x✝) = x✝ n

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f : MvPolynomial σ R
⊢ degreeOf n f = f.support.sup fun m => m n

Tactic:
classical
rw [degreeOf_def, degrees, Multiset.count_finset_sup]
congr
ext
simp only [count_toMultiset]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f : MvPolynomial σ R
⊢ degreeOf n f = f.support.sup fun m => m n

Tactic:
rw [degreeOf_def, degrees, Multiset.count_finset_sup]

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f : MvPolynomial σ R
⊢ (f.support.sup fun a => Multiset.count n (toMultiset a)) = f.support.sup fun m => m n

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f : MvPolynomial σ R
⊢ (f.support.sup fun a => Multiset.count n (toMultiset a)) = f.support.sup fun m => m n

Tactic:
congr

Result:
case e_f
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f : MvPolynomial σ R
⊢ (fun a => Multiset.count n (toMultiset a)) = fun m => m n

Proof state:
case e_f.h
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f : MvPolynomial σ R
x✝ : σ →₀ ℕ
⊢ Multiset.count n (toMultiset x✝) = x✝ n

Tactic:
simp only [count_toMultiset]

Result:
no goals
-- Mathlib/Algebra/Group/Fin/Tuple.lean
@[simp] lemma cons_sub (x : α) (v : Fin n → α) (w : Fin n.succ → α) :
    vecCons x v - w = vecCons (x - vecHead w) (v - vecTail w)

Proof state:
α : Type u_1
n : ℕ
inst✝ : Sub α
x : α
v : Fin n → α
w : Fin n.succ → α
⊢ vecCons x v - w = vecCons (x - vecHead w) (v - vecTail w)

Tactic:
ext i

Result:
case h
α : Type u_1
n : ℕ
inst✝ : Sub α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
⊢ (vecCons x v - w) i = vecCons (x - vecHead w) (v - vecTail w) i

Proof state:
case h
α : Type u_1
n : ℕ
inst✝ : Sub α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
⊢ (vecCons x v - w) i = vecCons (x - vecHead w) (v - vecTail w) i

Tactic:
refine i.cases ?_ ?_ <;> simp [vecHead, vecTail]

Result:
no goals
-- Mathlib/Data/Nat/Sqrt.lean
lemma le_three_of_sqrt_eq_one (h : sqrt n = 1) : n ≤ 3 :=
  le_of_lt_succ <| (@sqrt_lt n 2).1 <| by rw [h]; decide

Proof state:
n : ℕ
h : n.sqrt = 1
⊢ n.sqrt < 2

Tactic:
rw [h]

Result:
n : ℕ
h : n.sqrt = 1
⊢ 1 < 2

Proof state:
n : ℕ
h : n.sqrt = 1
⊢ 1 < 2

Tactic:
decide

Result:
no goals
-- Mathlib/Data/Vector/Basic.lean
theorem get_cons_zero (a : α) (v : Vector α n) : get (a ::ᵥ v) 0 = a

Proof state:
α : Type u_1
n : ℕ
a : α
v : Vector α n
⊢ (a ::ᵥ v).get 0 = a

Tactic:
simp [get_zero]

Result:
no goals
-- Mathlib/Data/Finset/Sigma.lean
theorem sigmaLift_nonempty :
    (sigmaLift f a b).Nonempty ↔ ∃ h : a.1 = b.1, (f (h ▸ a.2) b.2).Nonempty

Proof state:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ (if h : a.fst = b.fst then map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) else ∅) ≠ ∅ ↔
    ∃ (h : a.fst = b.fst), f (⋯ ▸ a.snd) b.snd ≠ ∅

Tactic:
split_ifs with h <;> simp [h]

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ (sigmaLift f a b).Nonempty ↔ ∃ (h : a.fst = b.fst), (f (h ▸ a.snd) b.snd).Nonempty

Tactic:
simp_rw [nonempty_iff_ne_empty, sigmaLift]

Result:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ (if h : a.fst = b.fst then map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) else ∅) ≠ ∅ ↔
    ∃ (h : a.fst = b.fst), f (⋯ ▸ a.snd) b.snd ≠ ∅
-- Mathlib/Algebra/Group/Semiconj/Units.lean
/-- `a` semiconjugates `x` to `a * x * a⁻¹`. -/
@[to_additive "`a` semiconjugates `x` to `a + x + -a`."]
lemma mk_semiconjBy (u : Mˣ) (x : M) : SemiconjBy (↑u) x (u * x * ↑u⁻¹)

Proof state:
M : Type u_1
inst✝ : Monoid M
u : Mˣ
x : M
⊢ ↑u * x = ↑u * x * ↑u⁻¹ * ↑u

Tactic:
rw [Units.inv_mul_cancel_right]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
u : Mˣ
x : M
⊢ SemiconjBy (↑u) x (↑u * x * ↑u⁻¹)

Tactic:
unfold SemiconjBy

Result:
M : Type u_1
inst✝ : Monoid M
u : Mˣ
x : M
⊢ ↑u * x = ↑u * x * ↑u⁻¹ * ↑u
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Erase.lean
theorem getElem_eraseIdx (l : List α) (i : Nat) (j : Nat) (h : j < (l.eraseIdx i).length) :
    (l.eraseIdx i)[j] = if h' : j < i then
        l[j]'(by have := length_eraseIdx_le l i; omega)
      else
        l[j + 1]'(by rw [length_eraseIdx] at h; split at h <;> omega)

Proof state:
case x
α : Type u_1
l : List α
i j : Nat
h : j < (l.eraseIdx i).length
⊢ some (l.eraseIdx i)[j] = some (if h' : j < i then l[j] else l[j + 1])

Tactic:
rw [← getElem?_eq_getElem, getElem?_eraseIdx]

Result:
case x
α : Type u_1
l : List α
i j : Nat
h : j < (l.eraseIdx i).length
⊢ (if j < i then l[j]? else l[j + 1]?) = some (if h' : j < i then l[j] else l[j + 1])

Proof state:
α : Type ?u.6532
l : List α
i j : Nat
h : j < (l.eraseIdx i).length
h' : j < i
⊢ j < l.length

Tactic:
have := length_eraseIdx_le l i

Result:
α : Type ?u.6532
l : List α
i j : Nat
h : j < (l.eraseIdx i).length
h' : j < i
this : (l.eraseIdx i).length ≤ l.length
⊢ j < l.length

Proof state:
α : Type u_1
l : List α
i j : Nat
h : j < (l.eraseIdx i).length
⊢ (l.eraseIdx i)[j] = if h' : j < i then l[j] else l[j + 1]

Tactic:
apply Option.some.inj

Result:
case x
α : Type u_1
l : List α
i j : Nat
h : j < (l.eraseIdx i).length
⊢ some (l.eraseIdx i)[j] = some (if h' : j < i then l[j] else l[j + 1])

Proof state:
case x
α : Type u_1
l : List α
i j : Nat
h : j < (l.eraseIdx i).length
⊢ (if j < i then l[j]? else l[j + 1]?) = some (if h' : j < i then l[j] else l[j + 1])

Tactic:
split <;> simp

Result:
no goals

Proof state:
α : Type ?u.6532
l : List α
i j : Nat
h : j < (l.eraseIdx i).length
h' : ¬j < i
⊢ j + 1 < l.length

Tactic:
rw [length_eraseIdx] at h

Result:
α : Type ?u.6532
l : List α
i j : Nat
h : j < if i < l.length then l.length - 1 else l.length
h' : ¬j < i
⊢ j + 1 < l.length

Proof state:
α : Type ?u.6532
l : List α
i j : Nat
h : j < if i < l.length then l.length - 1 else l.length
h' : ¬j < i
⊢ j + 1 < l.length

Tactic:
split at h <;> omega

Result:
no goals

Proof state:
α : Type ?u.6532
l : List α
i j : Nat
h : j < (l.eraseIdx i).length
h' : j < i
this : (l.eraseIdx i).length ≤ l.length
⊢ j < l.length

Tactic:
omega

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem norm_add_eq_norm_sub_iff_angle_eq_pi_div_two (x y : V) :
    ‖x + y‖ = ‖x - y‖ ↔ angle x y = π / 2

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ ‖x‖ ^ 2 + 2 * inner x y + ‖y‖ ^ 2 = ‖x‖ ^ 2 - 2 * inner x y + ‖y‖ ^ 2 ↔ inner x y = 0

Tactic:
constructor <;> intro h <;> linarith

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ ‖x + y‖ = ‖x - y‖ ↔ angle x y = π / 2

Tactic:
rw [← sq_eq_sq₀ (norm_nonneg (x + y)) (norm_nonneg (x - y)),
  ← inner_eq_zero_iff_angle_eq_pi_div_two x y, norm_add_pow_two_real, norm_sub_pow_two_real]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ ‖x‖ ^ 2 + 2 * inner x y + ‖y‖ ^ 2 = ‖x‖ ^ 2 - 2 * inner x y + ‖y‖ ^ 2 ↔ inner x y = 0