harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Vandermonde.lean
theorem vandermonde_cons {n : ℕ} (v0 : R) (v : Fin n → R) :
    vandermonde (Fin.cons v0 v : Fin n.succ → R) =
      Fin.cons (fun (j : Fin n.succ) => v0 ^ (j : ℕ)) fun i => Fin.cons 1
      fun j => v i * vandermonde v i j

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
v0 : R
v : Fin n → R
⊢ vandermonde (Fin.cons v0 v) = Fin.cons (fun j => v0 ^ ↑j) fun i => Fin.cons 1 fun j => v i * vandermonde v i j

Tactic:
ext i j

Result:
case a
R : Type u_1
inst✝ : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i j : Fin (n + 1)
⊢ vandermonde (Fin.cons v0 v) i j =
    Fin.cons (fun j => v0 ^ ↑j) (fun i => Fin.cons 1 fun j => v i * vandermonde v i j) i j

Proof state:
case a
R : Type u_1
inst✝ : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i✝ j✝ : Fin (n + 1)
i j : Fin n
⊢ vandermonde (Fin.cons v0 v) i.succ j.succ =
    Fin.cons (fun j => v0 ^ ↑j) (fun i => Fin.cons 1 fun j => v i * vandermonde v i j) i.succ j.succ

Tactic:
simp [pow_succ']

Result:
no goals

Proof state:
case a
R : Type u_1
inst✝ : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i✝ j : Fin (n + 1)
i : Fin n
⊢ vandermonde (Fin.cons v0 v) i.succ j =
    Fin.cons (fun j => v0 ^ ↑j) (fun i => Fin.cons 1 fun j => v i * vandermonde v i j) i.succ j

Tactic:
refine Fin.cases (by simp) (fun j => ?_) j

Result:
case a
R : Type u_1
inst✝ : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i✝ j✝ : Fin (n + 1)
i j : Fin n
⊢ vandermonde (Fin.cons v0 v) i.succ j.succ =
    Fin.cons (fun j => v0 ^ ↑j) (fun i => Fin.cons 1 fun j => v i * vandermonde v i j) i.succ j.succ

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i j : Fin (n + 1)
⊢ vandermonde (Fin.cons v0 v) 0 j =
    Fin.cons (fun j => v0 ^ ↑j) (fun i => Fin.cons 1 fun j => v i * vandermonde v i j) 0 j

Tactic:
simp

Result:
no goals

Proof state:
case a
R : Type u_1
inst✝ : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i j : Fin (n + 1)
⊢ vandermonde (Fin.cons v0 v) i j =
    Fin.cons (fun j => v0 ^ ↑j) (fun i => Fin.cons 1 fun j => v i * vandermonde v i j) i j

Tactic:
refine Fin.cases (by simp) (fun i => ?_) i

Result:
case a
R : Type u_1
inst✝ : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i✝ j : Fin (n + 1)
i : Fin n
⊢ vandermonde (Fin.cons v0 v) i.succ j =
    Fin.cons (fun j => v0 ^ ↑j) (fun i => Fin.cons 1 fun j => v i * vandermonde v i j) i.succ j

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i✝ j : Fin (n + 1)
i : Fin n
⊢ vandermonde (Fin.cons v0 v) i.succ 0 =
    Fin.cons (fun j => v0 ^ ↑j) (fun i => Fin.cons 1 fun j => v i * vandermonde v i j) i.succ 0

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsCycleOn.isCycle_subtypePerm (hf : f.IsCycleOn s) (hs : s.Nontrivial) :
    (f.subtypePerm fun _ => hf.apply_mem_iff.symm : Perm s).IsCycle

Proof state:
case intro
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
a : α
ha : a ∈ s
⊢ (f.subtypePerm ⋯).IsCycle

Tactic:
exact
  ⟨⟨a, ha⟩, ne_of_apply_ne ((↑) : s → α) (hf.apply_ne hs ha), fun b _ =>
    (hf.2 (⟨a, ha⟩ : s).2 b.2).subtypePerm⟩

Result:
no goals

Proof state:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
⊢ (f.subtypePerm ⋯).IsCycle

Tactic:
obtain ⟨a, ha⟩ := hs.nonempty

Result:
case intro
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
a : α
ha : a ∈ s
⊢ (f.subtypePerm ⋯).IsCycle
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See `inv_anti₀` for the implication from right-to-left with one fewer assumption. -/
lemma inv_le_inv₀ (ha : 0 < a) (hb : 0 < b) : a⁻¹ ≤ b⁻¹ ↔ b ≤ a

Proof state:
G₀ : Type u_2
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : PartialOrder G₀
inst✝³ : ZeroLEOneClass G₀
inst✝² : PosMulReflectLT G₀
a b : G₀
inst✝¹ : MulPosMono G₀
inst✝ : PosMulMono G₀
ha : 0 < a
hb : 0 < b
⊢ a⁻¹ ≤ b⁻¹ ↔ b ≤ a

Tactic:
rw [inv_le_iff_one_le_mul₀' ha, le_mul_inv_iff₀ hb, one_mul]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Equiv.lean
lemma sumAlgEquiv_comp_rename_inr :
    (sumAlgEquiv R S₁ S₂).toAlgHom.comp (rename Sum.inr) = IsScalarTower.toAlgHom R
        (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R))

Proof state:
R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
⊢ (↑(sumAlgEquiv R S₁ S₂)).comp (rename Sum.inr) =
    IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R))

Tactic:
ext i

Result:
case hf.a.a
R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
i : S₂
m✝¹ : S₁ →₀ ℕ
m✝ : S₂ →₀ ℕ
⊢ coeff m✝ (coeff m✝¹ (((↑(sumAlgEquiv R S₁ S₂)).comp (rename Sum.inr)) (X i))) =
    coeff m✝ (coeff m✝¹ ((IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R))) (X i)))

Proof state:
case hf.a.a
R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
i : S₂
m✝¹ : S₁ →₀ ℕ
m✝ : S₂ →₀ ℕ
⊢ coeff m✝ (coeff m✝¹ (((↑(sumAlgEquiv R S₁ S₂)).comp (rename Sum.inr)) (X i))) =
    coeff m✝ (coeff m✝¹ ((IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R))) (X i)))

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} {f : Option β → Option β}
    (h : m.WF) : Const.getD (Const.alter m k f) k' fallback =
      if k == k' then
        f (Const.get? m k) |>.getD fallback
      else
        Const.getD m k' fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' : α
fallback : β
f : Option β → Option β
h : m.WF
⊢ getD (alter m k f) k' fallback = if (k == k') = true then (f (get? m k)).getD fallback else getD m k' fallback

Tactic:
simp_to_raw using Raw₀.Const.getD_alter

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem mem_map : b ∈ map f s ↔ f.symm b ∈ s

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : UpperSet α
b : β
⊢ b ∈ (map f.symm).symm s ↔ f.symm b ∈ s

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : UpperSet α
b : β
⊢ b ∈ (map f) s ↔ f.symm b ∈ s

Tactic:
rw [← f.symm_symm, ← symm_map, f.symm_symm]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : UpperSet α
b : β
⊢ b ∈ (map f.symm).symm s ↔ f.symm b ∈ s
-- Mathlib/Combinatorics/Colex.lean
@[simp]
lemma ofColex_inj {s t : Colex α} : ofColex s = ofColex t ↔ s = t

Proof state:
case toColex.toColex
α : Type u_1
ofColex✝¹ ofColex✝ : Finset α
⊢ { ofColex := ofColex✝¹ }.ofColex = { ofColex := ofColex✝ }.ofColex ↔
    { ofColex := ofColex✝¹ } = { ofColex := ofColex✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
s t : Colex α
⊢ s.ofColex = t.ofColex ↔ s = t

Tactic:
cases s

Result:
case toColex
α : Type u_1
t : Colex α
ofColex✝ : Finset α
⊢ { ofColex := ofColex✝ }.ofColex = t.ofColex ↔ { ofColex := ofColex✝ } = t

Proof state:
case toColex
α : Type u_1
t : Colex α
ofColex✝ : Finset α
⊢ { ofColex := ofColex✝ }.ofColex = t.ofColex ↔ { ofColex := ofColex✝ } = t

Tactic:
cases t

Result:
case toColex.toColex
α : Type u_1
ofColex✝¹ ofColex✝ : Finset α
⊢ { ofColex := ofColex✝¹ }.ofColex = { ofColex := ofColex✝ }.ofColex ↔
    { ofColex := ofColex✝¹ } = { ofColex := ofColex✝ }
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_cons_zero : (cons a x).getMsbD 0 = a

Proof state:
a : Bool
w✝ : Nat
x : BitVec w✝
⊢ (cons a x).getMsbD 0 = a

Tactic:
rw [← BitVec.msb, msb_cons]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/Basic.lean
theorem norm_id_le : ‖id 𝕜 E‖ ≤ 1 :=
  opNorm_le_bound _ zero_le_one fun x => by simp

Proof state:
𝕜 : Type u_1
E : Type u_4
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
x : E
⊢ ‖(id 𝕜 E) x‖ ≤ 1 * ‖x‖

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Choose/Lucas.lean
theorem choose_modEq_choose_mod_mul_choose_div_nat :
    choose n k ≡ choose (n % p) (k % p) * choose (n / p) (k / p) [MOD p]

Proof state:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ↑(n.choose k) ≡ ↑((n % p).choose (k % p) * (n / p).choose (k / p)) [ZMOD ↑p]

Tactic:
exact_mod_cast choose_modEq_choose_mod_mul_choose_div

Result:
no goals

Proof state:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ n.choose k ≡ (n % p).choose (k % p) * (n / p).choose (k / p) [MOD p]

Tactic:
rw [← Int.natCast_modEq_iff]

Result:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ↑(n.choose k) ≡ ↑((n % p).choose (k % p) * (n / p).choose (k / p)) [ZMOD ↑p]
-- Mathlib/Data/Nat/PartENat.lean
theorem get_natCast' (x : ℕ) (h : (x : PartENat).Dom) : get (x : PartENat) h = x

Proof state:
x : ℕ
h : (↑x).Dom
⊢ (↑x).get h = x

Tactic:
rw [← natCast_inj, natCast_get]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
theorem measurableSet_of_differentiableWithinAt_Ici_of_isComplete {K : Set F} (hK : IsComplete K) :
    MeasurableSet { x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K }

Proof state:
case h
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
b✝⁵ b✝⁴ b✝³ : ℕ
b✝² : b✝³ ≥ b✝⁴
b✝¹ : ℕ
b✝ : b✝¹ ≥ b✝⁴
⊢ MeasurableSet (B f K ((1 / 2) ^ b✝³) ((1 / 2) ^ b✝¹) ((1 / 2) ^ b✝⁵))

Tactic:
exact measurableSet_B

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
⊢ MeasurableSet {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}

Tactic:
simp only [differentiable_set_eq_D K hK, D]

Result:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
⊢ MeasurableSet (⋂ e, ⋃ n, ⋂ p, ⋂ (_ : p ≥ n), ⋂ q, ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e))

Proof state:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
⊢ MeasurableSet (⋂ e, ⋃ n, ⋂ p, ⋂ (_ : p ≥ n), ⋂ q, ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e))

Tactic:
repeat apply_rules [MeasurableSet.iUnion, MeasurableSet.iInter] <;> intro

Result:
case h
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
b✝⁵ b✝⁴ b✝³ : ℕ
b✝² : b✝³ ≥ b✝⁴
b✝¹ : ℕ
b✝ : b✝¹ ≥ b✝⁴
⊢ MeasurableSet (B f K ((1 / 2) ^ b✝³) ((1 / 2) ^ b✝¹) ((1 / 2) ^ b✝⁵))

Proof state:
case h
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
b✝⁵ b✝⁴ b✝³ : ℕ
b✝² : b✝³ ≥ b✝⁴
b✝¹ : ℕ
b✝ : b✝¹ ≥ b✝⁴
⊢ MeasurableSet (B f K ((1 / 2) ^ b✝³) ((1 / 2) ^ b✝¹) ((1 / 2) ^ b✝⁵))

Tactic:
apply_rules [MeasurableSet.iUnion, MeasurableSet.iInter] <;> intro

Result:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
b✝⁵ b✝⁴ b✝³ : ℕ
b✝² : b✝³ ≥ b✝⁴
b✝¹ : ℕ
b✝ : b✝¹ ≥ b✝⁴
⊢ Countable F
-- Mathlib/Data/Finsupp/Single.lean
theorem erase_single_ne {a a' : α} {b : M} (h : a ≠ a') : erase a (single a' b) = single a' b

Proof state:
case pos
α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
b : M
h : a ≠ a'
s : α
hs : s = a
⊢ (erase a (single a' b)) s = (single a' b) s

Tactic:
rw [hs, erase_same, single_eq_of_ne h.symm]

Result:
no goals

Proof state:
case h
α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
b : M
h : a ≠ a'
s : α
⊢ (erase a (single a' b)) s = (single a' b) s

Tactic:
by_cases hs : s = a

Result:
case pos
α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
b : M
h : a ≠ a'
s : α
hs : s = a
⊢ (erase a (single a' b)) s = (single a' b) s

case neg
α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
b : M
h : a ≠ a'
s : α
hs : ¬s = a
⊢ (erase a (single a' b)) s = (single a' b) s

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
b : M
h : a ≠ a'
⊢ erase a (single a' b) = single a' b

Tactic:
ext s

Result:
case h
α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
b : M
h : a ≠ a'
s : α
⊢ (erase a (single a' b)) s = (single a' b) s

Proof state:
case neg
α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
b : M
h : a ≠ a'
s : α
hs : ¬s = a
⊢ (erase a (single a' b)) s = (single a' b) s

Tactic:
rw [erase_ne hs]

Result:
no goals
-- Mathlib/RingTheory/LocalProperties/Basic.lean
lemma RingHom.HoldsForLocalizationAway.containsIdentities (hPl : HoldsForLocalizationAway P) :
    ContainsIdentities P

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPl : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
R : Type u
inst✝ : CommRing R
⊢ P (id R)

Tactic:
exact hPl.of_bijective _ _ Function.bijective_id

Result:
no goals

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPl : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
⊢ ContainsIdentities fun {R S} [CommRing R] [CommRing S] => P

Tactic:
introv R

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPl : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
R : Type u
inst✝ : CommRing R
⊢ P (id R)
-- Mathlib/Topology/Basic.lean
theorem mem_closure_iff_nhds' : x ∈ closure s ↔ ∀ t ∈ 𝓝 x, ∃ y : s, ↑y ∈ t

Proof state:
X : Type u
x : X
s : Set X
inst✝ : TopologicalSpace X
⊢ x ∈ closure s ↔ ∀ t ∈ 𝓝 x, ∃ y, ↑y ∈ t

Tactic:
simp only [mem_closure_iff_nhds, Set.inter_nonempty_iff_exists_right, SetCoe.exists, exists_prop]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Icc_diff_Ioc_self (h : a ≤ b) : Icc a b \ Ioc a b = {a}

Proof state:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ Icc a b \ Ioc a b = {a}

Tactic:
simp [← coe_inj, h]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem lift_iSup_le_iff {ι : Type v} {f : ι → Cardinal.{w}} (hf : BddAbove (range f))
    {t : Cardinal} : lift.{u} (iSup f) ≤ t ↔ ∀ i, lift.{u} (f i) ≤ t

Proof state:
ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
t : Cardinal.{max u w}
⊢ lift.{u, w} (iSup f) ≤ t ↔ ∀ (i : ι), lift.{u, w} (f i) ≤ t

Tactic:
rw [lift_iSup hf]

Result:
ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
t : Cardinal.{max u w}
⊢ ⨆ i, lift.{u, w} (f i) ≤ t ↔ ∀ (i : ι), lift.{u, w} (f i) ≤ t

Proof state:
ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
t : Cardinal.{max u w}
⊢ ⨆ i, lift.{u, w} (f i) ≤ t ↔ ∀ (i : ι), lift.{u, w} (f i) ≤ t

Tactic:
exact ciSup_le_iff' (bddAbove_range_comp.{_,_,u} hf _)

Result:
no goals
-- Mathlib/LinearAlgebra/PiTensorProduct.lean
theorem reindex_symm (e : ι ≃ ι₂) :
    (reindex R (fun _ ↦ M) e).symm = reindex R (fun _ ↦ M) e.symm

Proof state:
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝² : CommSemiring R
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι ≃ ι₂
⊢ (reindex R (fun x => M) e).symm = reindex R (fun x => M) e.symm

Tactic:
ext x

Result:
case h
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝² : CommSemiring R
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι ≃ ι₂
x : ⨂[R] (i : ι₂), M
⊢ (reindex R (fun x => M) e).symm x = (reindex R (fun x => M) e.symm) x

Proof state:
case h
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝² : CommSemiring R
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι ≃ ι₂
x : ⨂[R] (i : ι₂), M
⊢ (reindex R (fun x => M) e).symm x = (reindex R (fun x => M) e.symm) x

Tactic:
simp only [reindex, domDomCongrLinearEquiv', LinearEquiv.coe_symm_mk, LinearEquiv.coe_mk,
  LinearEquiv.ofLinear_symm_apply, Equiv.symm_symm_apply, LinearEquiv.ofLinear_apply,
  Equiv.piCongrLeft'_symm]

Result:
no goals
-- Mathlib/Analysis/Convex/Side.lean
theorem wSameSide_of_left_mem {s : AffineSubspace R P} {x : P} (y : P) (hx : x ∈ s) :
    s.WSameSide x y

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
hx : x ∈ s
⊢ s.WSameSide x y

Tactic:
refine ⟨x, hx, x, hx, ?_⟩

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
hx : x ∈ s
⊢ SameRay R (x -ᵥ x) (y -ᵥ x)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
hx : x ∈ s
⊢ SameRay R (x -ᵥ x) (y -ᵥ x)

Tactic:
rw [vsub_self]

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
hx : x ∈ s
⊢ SameRay R 0 (y -ᵥ x)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
hx : x ∈ s
⊢ SameRay R 0 (y -ᵥ x)

Tactic:
apply SameRay.zero_left

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem comap_prodMap_prod (f : α → β) (g : γ → δ) (lb : Filter β) (ld : Filter δ) :
    comap (Prod.map f g) (lb ×ˢ ld) = comap f lb ×ˢ comap g ld

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ
lb : Filter β
ld : Filter δ
⊢ comap (Prod.map f g) (lb ×ˢ ld) = comap f lb ×ˢ comap g ld

Tactic:
simp [prod_eq_inf, comap_comap, Function.comp_def]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Operations.lean
/-- Except possibly for itself, the neighbours of `t` in `G.replaceVertex s t` are the neighbours of
`s` in `G`. -/
lemma adj_replaceVertex_iff_of_ne_right {w : V} (hw : w ≠ t) :
    (G.replaceVertex s t).Adj t w ↔ G.Adj s w

Proof state:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
w : V
hw : w ≠ t
⊢ (G.replaceVertex s t).Adj t w ↔ G.Adj s w

Tactic:
simp [replaceVertex, hw]

Result:
no goals
-- Mathlib/Data/Set/Subset.lean
@[simp]
lemma image_val_sUnion : ↑(⋃₀ T) = ⋃₀ { (B : Set α) | B ∈ T}

Proof state:
α : Type u_2
A : Set α
T : Set (Set ↑A)
⊢ Subtype.val '' ⋃₀ T = ⋃₀ {x | ∃ B ∈ T, Subtype.val '' B = x}

Tactic:
rw [image_sUnion, image]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Isometry.lean
theorem ediam_preimage (h : α ≃ᵢ β) (s : Set β) : EMetric.diam (h ⁻¹' s) = EMetric.diam s

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
s : Set β
⊢ EMetric.diam (⇑h ⁻¹' s) = EMetric.diam s

Tactic:
rw [← image_symm, ediam_image]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Module/Constructions.lean
private lemma lipschitzWith_one_equiv_pi_aux : LipschitzWith 1 (equiv (Π i, E i)) :=
  AddMonoidHomClass.lipschitz_of_bound_nnnorm (linearEquiv ℂ (Π i, E i)) 1 <| by
    simpa using norm_equiv_le_norm_pi

Proof state:
A : Type u_1
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → Module ℂ (E i)
inst✝² : (i : ι) → SMul Aᵐᵒᵖ (E i)
inst✝¹ : (i : ι) → CStarModule A (E i)
inst✝ : StarOrderedRing A
⊢ ∀ (x : C⋆ᵐᵒᵈ ((i : ι) → E i)), ‖(linearEquiv ℂ ((i : ι) → E i)) x‖₊ ≤ 1 * ‖x‖₊

Tactic:
simpa using norm_equiv_le_norm_pi

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem think_congr {s t : WSeq α} (h : s ~ʷ t) : think s ~ʷ think t

Proof state:
α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ s.think ~ʷ t.think

Tactic:
unfold Equiv

Result:
α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ LiftRel (fun x1 x2 => x1 = x2) s.think t.think

Proof state:
α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ LiftRel (fun x1 x2 => x1 = x2) s.think t.think

Tactic:
simpa using h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem Sublist.countP_le (s : l₁ <+ l₂) : countP p l₁ ≤ countP p l₂

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
s : l₁ <+ l₂
⊢ countP p l₁ ≤ countP p l₂

Tactic:
simp only [countP_eq_length_filter]

Result:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
s : l₁ <+ l₂
⊢ (filter p l₁).length ≤ (filter p l₂).length

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
s : l₁ <+ l₂
⊢ (filter p l₁).length ≤ (filter p l₂).length

Tactic:
apply s.filter _ |>.length_le

Result:
no goals
-- Mathlib/Algebra/Ring/Divisibility/Basic.lean
theorem dvd_add [LeftDistribClass α] {a b c : α} (h₁ : a ∣ b) (h₂ : a ∣ c) : a ∣ b + c :=
  Dvd.elim h₁ fun d hd => Dvd.elim h₂ fun e he => Dvd.intro (d + e) (by simp [left_distrib, hd, he])

Proof state:
α : Type u_1
inst✝² : Add α
inst✝¹ : Semigroup α
inst✝ : LeftDistribClass α
a b c : α
h₁ : a ∣ b
h₂ : a ∣ c
d : α
hd : b = a * d
e : α
he : c = a * e
⊢ a * (d + e) = b + c

Tactic:
simp [left_distrib, hd, he]

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem polar_smul [Monoid S] [DistribMulAction S N] (f : M → N) (s : S) (x y : M) :
    polar (s • f) x y = s • polar f x y

Proof state:
S : Type u_1
M : Type u_4
N : Type u_5
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Monoid S
inst✝ : DistribMulAction S N
f : M → N
s : S
x y : M
⊢ polar (s • f) x y = s • polar f x y

Tactic:
simp only [polar, Pi.smul_apply, smul_sub]

Result:
no goals
-- Mathlib/Algebra/CharP/Reduced.lean
theorem isSquare_of_charTwo' {R : Type*} [Finite R] [CommRing R] [IsReduced R] [CharP R 2]
    (a : R) : IsSquare a

Proof state:
case intro
R : Type u_1
inst✝³ : Finite R
inst✝² : CommRing R
inst✝¹ : IsReduced R
inst✝ : CharP R 2
a : R
val✝ : Fintype R
⊢ IsSquare a

Tactic:
exact
  Exists.imp (fun b h => pow_two b ▸ Eq.symm h)
    (((Fintype.bijective_iff_injective_and_card _).mpr ⟨frobenius_inj R 2, rfl⟩).surjective a)

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : Finite R
inst✝² : CommRing R
inst✝¹ : IsReduced R
inst✝ : CharP R 2
a : R
⊢ IsSquare a

Tactic:
cases nonempty_fintype R

Result:
case intro
R : Type u_1
inst✝³ : Finite R
inst✝² : CommRing R
inst✝¹ : IsReduced R
inst✝ : CharP R 2
a : R
val✝ : Fintype R
⊢ IsSquare a
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem X_sub_C_mul_divByMonic_eq_sub_modByMonic {K : Type*} [Field K] (f : K[X]) (a : K) :
    (X - C a) * (f /ₘ (X - C a)) = f - f %ₘ (X - C a)

Proof state:
case _hq
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
⊢ (X - C a).Monic

Tactic:
exact monic_X_sub_C a

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
⊢ (X - C a) * (f /ₘ (X - C a)) = f - f %ₘ (X - C a)

Tactic:
rw [eq_sub_iff_add_eq, ← eq_sub_iff_add_eq', modByMonic_eq_sub_mul_div]

Result:
case _hq
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
⊢ (X - C a).Monic
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem mul_nonneg_of_nonpos_of_nonpos {a b : Int}
  (ha : a ≤ 0) (hb : b ≤ 0) : 0 ≤ a * b

Proof state:
a b : Int
ha : a ≤ 0
hb : b ≤ 0
⊢ 0 ≤ a * b

Tactic:
have : 0 * b ≤ a * b := Int.mul_le_mul_of_nonpos_right ha hb

Result:
a b : Int
ha : a ≤ 0
hb : b ≤ 0
this : 0 * b ≤ a * b
⊢ 0 ≤ a * b

Proof state:
a b : Int
ha : a ≤ 0
hb : b ≤ 0
this : 0 * b ≤ a * b
⊢ 0 ≤ a * b

Tactic:
rwa [Int.zero_mul] at this

Result:
no goals
-- Mathlib/Analysis/Analytic/CPolynomial.lean
theorem CPolynomialAt.sub (hf : CPolynomialAt 𝕜 f x) (hg : CPolynomialAt 𝕜 g x) :
    CPolynomialAt 𝕜 (f - g) x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
x : E
hf : CPolynomialAt 𝕜 f x
hg : CPolynomialAt 𝕜 g x
⊢ CPolynomialAt 𝕜 (f - g) x

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Result:
no goals
-- Mathlib/Data/Complex/FiniteDimensional.lean
theorem finrank_real_complex : finrank ℝ ℂ = 2

Proof state:
⊢ finrank ℝ ℂ = 2

Tactic:
rw [finrank_eq_card_basis basisOneI, Fintype.card_fin]

Result:
no goals
-- Mathlib/Data/Finset/Grade.lean
lemma _root_.CovBy.card_multiset (h : s ⋖ t) : card s ⋖ card t

Proof state:
case intro
α : Type u_1
s : Multiset α
a : α
h : s ⋖ a ::ₘ s
⊢ s.card ⋖ s.card + 1

Tactic:
exact covBy_succ _

Result:
no goals

Proof state:
case intro
α : Type u_1
s : Multiset α
a : α
h : s ⋖ a ::ₘ s
⊢ s.card ⋖ (a ::ₘ s).card

Tactic:
rw [card_cons]

Result:
case intro
α : Type u_1
s : Multiset α
a : α
h : s ⋖ a ::ₘ s
⊢ s.card ⋖ s.card + 1

Proof state:
α : Type u_1
s t : Multiset α
h : s ⋖ t
⊢ s.card ⋖ t.card

Tactic:
obtain ⟨a, rfl⟩ := h.exists_multiset_cons

Result:
case intro
α : Type u_1
s : Multiset α
a : α
h : s ⋖ a ::ₘ s
⊢ s.card ⋖ (a ::ₘ s).card