harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Group/Subgroup/Defs.lean
theorem mul_mem_cancel_right {x y : G} (h : x ∈ H) : y * x ∈ H ↔ y ∈ H :=
  ⟨fun hba => by simpa using mul_mem hba (inv_mem h), fun hb => mul_mem hb h⟩

Proof state:
G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
x y : G
h : x ∈ H
hba : y * x ∈ H
⊢ y ∈ H

Tactic:
simpa using mul_mem hba (inv_mem h)

Result:
no goals
-- Mathlib/RepresentationTheory/Maschke.lean
theorem equivariantProjection_condition (hcard : IsUnit (Fintype.card G : k))
    (h : ∀ v : V, π (i v) = v) (v : V) : (π.equivariantProjection G) (i v) = v

Proof state:
k : Type u
inst✝¹⁰ : CommRing k
G : Type u
inst✝⁹ : Group G
V : Type v
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module (MonoidAlgebra k G) V
inst✝⁵ : IsScalarTower k (MonoidAlgebra k G) V
W : Type w
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module (MonoidAlgebra k G) W
inst✝¹ : IsScalarTower k (MonoidAlgebra k G) W
π : W →ₗ[k] V
i : V →ₗ[MonoidAlgebra k G] W
inst✝ : Fintype G
hcard : IsUnit ↑(Fintype.card G)
h : ∀ (v : V), π (i v) = v
v : V
⊢ (equivariantProjection G π) (i v) = v

Tactic:
rw [equivariantProjection_apply]

Result:
k : Type u
inst✝¹⁰ : CommRing k
G : Type u
inst✝⁹ : Group G
V : Type v
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module (MonoidAlgebra k G) V
inst✝⁵ : IsScalarTower k (MonoidAlgebra k G) V
W : Type w
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module (MonoidAlgebra k G) W
inst✝¹ : IsScalarTower k (MonoidAlgebra k G) W
π : W →ₗ[k] V
i : V →ₗ[MonoidAlgebra k G] W
inst✝ : Fintype G
hcard : IsUnit ↑(Fintype.card G)
h : ∀ (v : V), π (i v) = v
v : V
⊢ Ring.inverse ↑(Fintype.card G) • ∑ g : G, (π.conjugate g) (i v) = v

Proof state:
k : Type u
inst✝¹⁰ : CommRing k
G : Type u
inst✝⁹ : Group G
V : Type v
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module (MonoidAlgebra k G) V
inst✝⁵ : IsScalarTower k (MonoidAlgebra k G) V
W : Type w
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module (MonoidAlgebra k G) W
inst✝¹ : IsScalarTower k (MonoidAlgebra k G) W
π : W →ₗ[k] V
i : V →ₗ[MonoidAlgebra k G] W
inst✝ : Fintype G
hcard : IsUnit ↑(Fintype.card G)
h : ∀ (v : V), π (i v) = v
v : V
⊢ Ring.inverse ↑(Fintype.card G) • ∑ g : G, (π.conjugate g) (i v) = v

Tactic:
simp only [conjugate_i π i h]

Result:
k : Type u
inst✝¹⁰ : CommRing k
G : Type u
inst✝⁹ : Group G
V : Type v
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module (MonoidAlgebra k G) V
inst✝⁵ : IsScalarTower k (MonoidAlgebra k G) V
W : Type w
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module (MonoidAlgebra k G) W
inst✝¹ : IsScalarTower k (MonoidAlgebra k G) W
π : W →ₗ[k] V
i : V →ₗ[MonoidAlgebra k G] W
inst✝ : Fintype G
hcard : IsUnit ↑(Fintype.card G)
h : ∀ (v : V), π (i v) = v
v : V
⊢ Ring.inverse ↑(Fintype.card G) • ∑ x : G, v = v

Proof state:
k : Type u
inst✝¹⁰ : CommRing k
G : Type u
inst✝⁹ : Group G
V : Type v
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module (MonoidAlgebra k G) V
inst✝⁵ : IsScalarTower k (MonoidAlgebra k G) V
W : Type w
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module (MonoidAlgebra k G) W
inst✝¹ : IsScalarTower k (MonoidAlgebra k G) W
π : W →ₗ[k] V
i : V →ₗ[MonoidAlgebra k G] W
inst✝ : Fintype G
hcard : IsUnit ↑(Fintype.card G)
h : ∀ (v : V), π (i v) = v
v : V
⊢ Ring.inverse ↑(Fintype.card G) • ∑ x : G, v = v

Tactic:
rw [Finset.sum_const, Finset.card_univ, ← Nat.cast_smul_eq_nsmul k, smul_smul,
  Ring.inverse_mul_cancel _ hcard, one_smul]

Result:
no goals
-- Mathlib/Analysis/Convex/Function.lean
theorem ConvexOn.le_on_segment' (hf : ConvexOn 𝕜 s f) {x y : E} (hx : x ∈ s) (hy : y ∈ s) {a b : 𝕜}
    (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : f (a • x + b • y) ≤ max (f x) (f y) :=
  calc
    f (a • x + b • y) ≤ a • f x + b • f y := hf.2 hx hy ha hb hab
    _ ≤ a • max (f x) (f y) + b • max (f x) (f y)

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrderedAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y ≤ a • (f x ⊔ f y) + b • (f x ⊔ f y)

Tactic:
gcongr

Result:
case h₁.hb
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrderedAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f x ≤ f x ⊔ f y

case h₂.hb
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrderedAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f y ≤ f x ⊔ f y

Proof state:
case h₁.hb
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrderedAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f x ≤ f x ⊔ f y

Tactic:
apply le_max_left

Result:
no goals

Proof state:
case h₂.hb
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrderedAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f y ≤ f x ⊔ f y

Tactic:
apply le_max_right

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Multiset.lean
lemma map_add_right_Ioo (a b c : α) : ((Ioo a b).map fun x => x + c) = Ioo (a + c) (b + c)

Proof state:
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => x + c) (Ioo a b) = Ioo (a + c) (b + c)

Tactic:
simp_rw [add_comm _ c]

Result:
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => c + x) (Ioo a b) = Ioo (c + a) (c + b)

Proof state:
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => c + x) (Ioo a b) = Ioo (c + a) (c + b)

Tactic:
exact map_add_left_Ioo _ _ _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapFinIdx_eq_mapFinIdx_iff {l : Array α} {f g : (i : Nat) → α → (h : i < l.size) → β} :
    l.mapFinIdx f = l.mapFinIdx g ↔ ∀ (i : Nat) (h : i < l.size), f i l[i] h = g i l[i] h

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f g : (i : Nat) → α → i < l.size → β
⊢ l.mapFinIdx f = l.mapFinIdx g ↔ ∀ (i : Nat) (h : i < l.size), f i l[i] h = g i l[i] h

Tactic:
rw [eq_comm, mapFinIdx_eq_iff]

Result:
α : Type u_1
β : Type u_2
l : Array α
f g : (i : Nat) → α → i < l.size → β
⊢ (∃ h, ∀ (i : Nat) (h_1 : i < l.size), (l.mapFinIdx f)[i] = g i l[i] h_1) ↔
    ∀ (i : Nat) (h : i < l.size), f i l[i] h = g i l[i] h

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f g : (i : Nat) → α → i < l.size → β
⊢ (∃ h, ∀ (i : Nat) (h_1 : i < l.size), (l.mapFinIdx f)[i] = g i l[i] h_1) ↔
    ∀ (i : Nat) (h : i < l.size), f i l[i] h = g i l[i] h

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Ord.lean
theorem isGT_iff_eq_gt {o : Ordering} : o.isGT ↔ o = .gt

Proof state:
o : Ordering
⊢ o.isGT = true ↔ o = gt

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem Algebra.IsAlgebraic.tower_bot_of_injective [Algebra.IsAlgebraic R A]
    (hinj : Function.Injective (algebraMap S A)) :
    Algebra.IsAlgebraic R S where
  isAlgebraic x

Proof state:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R S
inst✝³ : Algebra S A
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R S A
inst✝ : Algebra.IsAlgebraic R A
hinj : Function.Injective ⇑(algebraMap S A)
x : S
⊢ IsAlgebraic R x

Tactic:
simpa [isAlgebraic_algebraMap_iff hinj] using isAlgebraic (R := R) (A := A) (algebraMap _ _ x)

Result:
no goals
-- Mathlib/Data/Matrix/DMatrix.lean
theorem map_zero [∀ i j, Zero (α i j)] {β : m → n → Type w} [∀ i j, Zero (β i j)]
    {f : ∀ ⦃i j⦄, α i j → β i j} (h : ∀ i j, f (0 : α i j) = 0) :
    (0 : DMatrix m n α).map f = 0

Proof state:
case a
m : Type u_1
n : Type u_2
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → Zero (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → Zero (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j
h : ∀ (i : m) (j : n), f 0 = 0
i✝ : m
j✝ : n
⊢ map 0 f i✝ j✝ = 0 i✝ j✝

Tactic:
simp [h]

Result:
no goals

Proof state:
m : Type u_1
n : Type u_2
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → Zero (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → Zero (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j
h : ∀ (i : m) (j : n), f 0 = 0
⊢ map 0 f = 0

Tactic:
ext

Result:
case a
m : Type u_1
n : Type u_2
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → Zero (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → Zero (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j
h : ∀ (i : m) (j : n), f 0 = 0
i✝ : m
j✝ : n
⊢ map 0 f i✝ j✝ = 0 i✝ j✝
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
lemma nilRankAux_basis_indep [Nontrivial R] (b : Basis ι R L) (b' : Basis ι' R L) :
    nilRankAux φ b = (polyCharpoly φ b').natTrailingDegree

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup L
inst✝⁹ : Module R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
φ : L →ₗ[R] End R M
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq ι'
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial R
b : Basis ι R L
b' : Basis ι' R L
⊢ φ.nilRankAux b = (φ.polyCharpoly b').natTrailingDegree

Tactic:
apply le_antisymm <;> apply nilRankAux_le

Result:
no goals
-- Mathlib/Order/Partition/Finpartition.lean
theorem ne_bot {b : α} (hb : b ∈ P.parts) : b ≠ ⊥

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
b : α
hb : b ∈ P.parts
h : b = ⊥
⊢ ⊥ ∈ P.parts

Tactic:
rw [h] at hb

Result:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
b : α
hb : ⊥ ∈ P.parts
h : b = ⊥
⊢ ⊥ ∈ P.parts

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
b : α
hb : b ∈ P.parts
h : b = ⊥
⊢ False

Tactic:
refine P.not_bot_mem (?_)

Result:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
b : α
hb : b ∈ P.parts
h : b = ⊥
⊢ ⊥ ∈ P.parts

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
b : α
hb : ⊥ ∈ P.parts
h : b = ⊥
⊢ ⊥ ∈ P.parts

Tactic:
exact hb

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
b : α
hb : b ∈ P.parts
⊢ b ≠ ⊥

Tactic:
intro h

Result:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
b : α
hb : b ∈ P.parts
h : b = ⊥
⊢ False
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem Products.max_eq_o_cons_tail [Inhabited I] (l : Products I) (hl : l.val ≠ [])
    (hlh : l.val.head! = term I ho) : l.val = term I ho :: l.Tail.val

Proof state:
I : Type u
inst✝² : LinearOrder I
inst✝¹ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
⊢ ↑l = term I ho :: ↑l.Tail

Tactic:
rw [← List.cons_head!_tail hl, hlh]

Result:
I : Type u
inst✝² : LinearOrder I
inst✝¹ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
⊢ term I ho :: (↑l).tail = term I ho :: ↑l.Tail

Proof state:
I : Type u
inst✝² : LinearOrder I
inst✝¹ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
⊢ term I ho :: (↑l).tail = term I ho :: ↑l.Tail

Tactic:
rfl

Result:
no goals
-- Mathlib/Probability/Distributions/Uniform.lean
theorem toMeasure_uniformOfFintype_apply [MeasurableSpace α] (hs : MeasurableSet s) :
    (uniformOfFintype α).toMeasure s = Fintype.card s / Fintype.card α

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : Nonempty α
s : Set α
inst✝ : MeasurableSpace α
hs : MeasurableSet s
⊢ (uniformOfFintype α).toMeasure s = ↑(Fintype.card ↑s) / ↑(Fintype.card α)

Tactic:
simp [uniformOfFintype, hs]

Result:
no goals
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem ofFinsupp_sum {k' G' : Type*} [AddCommMonoid k'] (f : G →₀ k)
    (g : G → k → G' →₀ k'):
    (⟨Finsupp.sum f g⟩ : SkewMonoidAlgebra k' G') = sum ⟨f⟩ (⟨g · ·⟩)

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
k' : Type u_3
G' : Type u_4
inst✝ : AddCommMonoid k'
f : G →₀ k
g : G → k → G' →₀ k'
⊢ { toFinsupp := f.sum g } = { toFinsupp := f }.sum fun x1 x2 => { toFinsupp := g x1 x2 }

Tactic:
apply toFinsupp_injective

Result:
case a
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
k' : Type u_3
G' : Type u_4
inst✝ : AddCommMonoid k'
f : G →₀ k
g : G → k → G' →₀ k'
⊢ { toFinsupp := f.sum g }.toFinsupp = ({ toFinsupp := f }.sum fun x1 x2 => { toFinsupp := g x1 x2 }).toFinsupp

Proof state:
case a
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
k' : Type u_3
G' : Type u_4
inst✝ : AddCommMonoid k'
f : G →₀ k
g : G → k → G' →₀ k'
⊢ { toFinsupp := f.sum g }.toFinsupp = ({ toFinsupp := f }.sum fun x1 x2 => { toFinsupp := g x1 x2 }).toFinsupp

Tactic:
simp only [toFinsupp_sum']

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean
theorem bot_eq_top_iff_rank_eq_one [Nontrivial E] [Module.Free F E] :
    (⊥ : Subalgebra F E) = ⊤ ↔ Module.rank F E = 1

Proof state:
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F E
⊢ ⊥ = ⊤ ↔ Module.rank F E = 1

Tactic:
haveI := Module.Free.of_equiv (Subalgebra.topEquiv (R := F) (A := E)).toLinearEquiv.symm

Result:
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F E
this : Free F ↥⊤
⊢ ⊥ = ⊤ ↔ Module.rank F E = 1

Proof state:
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F E
this : Free F ↥⊤
⊢ ⊥ = ⊤ ↔ Module.rank F E = 1

Tactic:
rw [← rank_top, Subalgebra.rank_eq_one_iff, eq_comm]

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Ray.lean
theorem norm_smul_eq (h : SameRay ℝ x y) : ‖x‖ • y = ‖y‖ • x

Proof state:
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
⊢ ‖a • u‖ • b • u = ‖b • u‖ • a • u

Tactic:
simp only [norm_smul_of_nonneg, *, mul_smul]

Result:
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
⊢ a • ‖u‖ • b • u = b • ‖u‖ • a • u

Proof state:
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
⊢ a • ‖u‖ • b • u = b • ‖u‖ • a • u

Tactic:
rw [smul_comm, smul_comm b, smul_comm a b u]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
h : SameRay ℝ x y
⊢ ‖x‖ • y = ‖y‖ • x

Tactic:
rcases h.exists_eq_smul with ⟨u, a, b, ha, hb, -, rfl, rfl⟩

Result:
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
⊢ ‖a • u‖ • b • u = ‖b • u‖ • a • u
-- Mathlib/Computability/Primrec.lean
theorem nat_iterate {f : α → ℕ} {g : α → β} {h : α → β → β} (hf : Primrec f) (hg : Primrec g)
    (hh : Primrec₂ h) : Primrec fun a => (h a)^[f a] (g a) :=
  (nat_rec' hf hg (hh.comp₂ Primrec₂.left <| snd.comp₂ Primrec₂.right)).of_eq fun a => by
    induction f a <;> simp [*, -Function.iterate_succ, Function.iterate_succ']

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → ℕ
g : α → β
h : α → β → β
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
a : α
⊢ Nat.rec (g a) (fun n IH => h a (n, IH).2) (f a) = (h a)^[f a] (g a)

Tactic:
induction f a <;> simp [*, -Function.iterate_succ, Function.iterate_succ']

Result:
no goals
-- Mathlib/Data/Finset/Sups.lean
theorem disjSups_inter_subset_left : (s₁ ∩ s₂) ○ t ⊆ s₁ ○ t ∩ s₂ ○ t

Proof state:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s₁ s₂ t : Finset α
⊢ (s₁ ∩ s₂) ○ t ⊆ s₁ ○ t ∩ s₂ ○ t

Tactic:
simpa only [disjSups, inter_product, filter_inter_distrib] using image_inter_subset _ _ _

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean
theorem FiniteField.isSquare_neg_one_iff : IsSquare (-1 : F) ↔ Fintype.card F % 4 ≠ 3

Proof state:
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h₁ : Fintype.card F % 2 = 1
⊢ (if 1 = 0 then 0 else if Fintype.card F % 4 = 1 then 1 else -1) = 1 ↔ Fintype.card F % 4 ≠ 3

Tactic:
omega

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
⊢ IsSquare (-1) ↔ Fintype.card F % 4 ≠ 3

Tactic:
by_cases hF : ringChar F = 2

Result:
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
⊢ IsSquare (-1) ↔ Fintype.card F % 4 ≠ 3

case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
⊢ IsSquare (-1) ↔ Fintype.card F % 4 ≠ 3

Proof state:
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
⊢ IsSquare (-1) ↔ Fintype.card F % 4 ≠ 3

Tactic:
simp only [FiniteField.isSquare_of_char_two hF, Ne, true_iff]

Result:
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
⊢ ¬Fintype.card F % 4 = 3

Proof state:
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F = 2
⊢ ¬Fintype.card F % 4 = 3

Tactic:
exact fun hf ↦
  one_ne_zero <|
    (Nat.odd_of_mod_four_eq_three hf).symm.trans <| FiniteField.even_card_of_char_two hF

Result:
no goals

Proof state:
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h₁ : Fintype.card F % 2 = 1
⊢ IsSquare (-1) ↔ Fintype.card F % 4 ≠ 3

Tactic:
rw [← quadraticChar_one_iff_isSquare (neg_ne_zero.mpr (one_ne_zero' F)),
  quadraticChar_neg_one hF, χ₄_nat_eq_if_mod_four, h₁]

Result:
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h₁ : Fintype.card F % 2 = 1
⊢ (if 1 = 0 then 0 else if Fintype.card F % 4 = 1 then 1 else -1) = 1 ↔ Fintype.card F % 4 ≠ 3

Proof state:
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
⊢ IsSquare (-1) ↔ Fintype.card F % 4 ≠ 3

Tactic:
have h₁ := FiniteField.odd_card_of_char_ne_two hF

Result:
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
h₁ : Fintype.card F % 2 = 1
⊢ IsSquare (-1) ↔ Fintype.card F % 4 ≠ 3
-- Mathlib/Order/SupIndep.lean
theorem iSupIndep.sSupIndep_range (ht : iSupIndep t) : sSupIndep <| range t

Proof state:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
⊢ sSupIndep (range t)

Tactic:
rw [sSupIndep_iff]

Result:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
⊢ iSupIndep Subtype.val

Proof state:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
⊢ iSupIndep Subtype.val

Tactic:
rw [← coe_comp_rangeFactorization t] at ht

Result:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep (Subtype.val ∘ rangeFactorization t)
⊢ iSupIndep Subtype.val

Proof state:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep (Subtype.val ∘ rangeFactorization t)
⊢ iSupIndep Subtype.val

Tactic:
exact ht.comp' surjective_onto_range

Result:
no goals
-- Mathlib/Topology/Category/CompHausLike/Limits.lean
theorem hasPullbacksOfInclusions
    (hP' : ∀ ⦃X Y B : CompHausLike.{u} P⦄ (f : X ⟶ B) (g : Y ⟶ B)
      (_ : IsOpenEmbedding f), HasExplicitPullback f g) :
    HasExplicitPullbacksOfInclusions P :=
  { hasProp

Proof state:
P : TopCat → Prop
inst✝ : HasExplicitFiniteCoproducts P
hP' :
  ∀ ⦃X Y B : CompHausLike P⦄ (f : X ⟶ B) (g : Y ⟶ B),
    IsOpenEmbedding ⇑(ConcreteCategory.hom f) → HasExplicitPullback f g
⊢ ∀ {X Y Z : CompHausLike P} (f : Z ⟶ X ⨿ Y), HasExplicitPullback coprod.inl f

Tactic:
intro _ _ _ f

Result:
P : TopCat → Prop
inst✝ : HasExplicitFiniteCoproducts P
hP' :
  ∀ ⦃X Y B : CompHausLike P⦄ (f : X ⟶ B) (g : Y ⟶ B),
    IsOpenEmbedding ⇑(ConcreteCategory.hom f) → HasExplicitPullback f g
X✝ Y✝ Z✝ : CompHausLike P
f : Z✝ ⟶ X✝ ⨿ Y✝
⊢ HasExplicitPullback coprod.inl f

Proof state:
case x
P : TopCat → Prop
inst✝ : HasExplicitFiniteCoproducts P
hP' :
  ∀ ⦃X Y B : CompHausLike P⦄ (f : X ⟶ B) (g : Y ⟶ B),
    IsOpenEmbedding ⇑(ConcreteCategory.hom f) → HasExplicitPullback f g
X✝ Y✝ Z✝ : CompHausLike P
f : Z✝ ⟶ X✝ ⨿ Y✝
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom coprod.inl)

Tactic:
exact Sigma.isOpenEmbedding_ι _ _

Result:
no goals

Proof state:
P : TopCat → Prop
inst✝ : HasExplicitFiniteCoproducts P
hP' :
  ∀ ⦃X Y B : CompHausLike P⦄ (f : X ⟶ B) (g : Y ⟶ B),
    IsOpenEmbedding ⇑(ConcreteCategory.hom f) → HasExplicitPullback f g
X✝ Y✝ Z✝ : CompHausLike P
f : Z✝ ⟶ X✝ ⨿ Y✝
⊢ HasExplicitPullback coprod.inl f

Tactic:
apply hP'

Result:
case x
P : TopCat → Prop
inst✝ : HasExplicitFiniteCoproducts P
hP' :
  ∀ ⦃X Y B : CompHausLike P⦄ (f : X ⟶ B) (g : Y ⟶ B),
    IsOpenEmbedding ⇑(ConcreteCategory.hom f) → HasExplicitPullback f g
X✝ Y✝ Z✝ : CompHausLike P
f : Z✝ ⟶ X✝ ⨿ Y✝
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom coprod.inl)
-- Mathlib/CategoryTheory/Endofunctor/Algebra.lean
theorem iso_of_iso (f : V₀ ⟶ V₁) [IsIso f.1] : IsIso f :=
  ⟨⟨{ f := inv f.1
      h

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
V₀ V₁ : Coalgebra F
f : V₀ ⟶ V₁
inst✝ : IsIso f.f
⊢ V₁.str ≫ F.map (inv f.f) = inv f.f ≫ V₀.str

Tactic:
rw [IsIso.eq_inv_comp f.1, ← Category.assoc, ← f.h, Category.assoc]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
V₀ V₁ : Coalgebra F
f : V₀ ⟶ V₁
inst✝ : IsIso f.f
⊢ V₀.str ≫ F.map f.f ≫ F.map (inv f.f) = V₀.str

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
V₀ V₁ : Coalgebra F
f : V₀ ⟶ V₁
inst✝ : IsIso f.f
⊢ V₀.str ≫ F.map f.f ≫ F.map (inv f.f) = V₀.str

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
V₀ V₁ : Coalgebra F
f : V₀ ⟶ V₁
inst✝ : IsIso f.f
⊢ { f := inv f.f, h := ⋯ } ≫ f = 𝟙 V₁

Tactic:
aesop_cat

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
V₀ V₁ : Coalgebra F
f : V₀ ⟶ V₁
inst✝ : IsIso f.f
⊢ f ≫ { f := inv f.f, h := ⋯ } = 𝟙 V₀

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Data/Finsupp/Weight.lean
theorem finite_of_degree_le [Finite σ] (n : ℕ) :
    {f : σ →₀ ℕ | degree f ≤ n}.Finite

Proof state:
σ : Type u_1
inst✝ : Finite σ
n : ℕ
⊢ {f | (weight fun x => 1) f ≤ n}.Finite

Tactic:
refine finite_of_nat_weight_le (Function.const σ 1) ?_ n

Result:
σ : Type u_1
inst✝ : Finite σ
n : ℕ
⊢ ∀ (x : σ), Function.const σ 1 x ≠ 0

Proof state:
σ : Type u_1
inst✝ : Finite σ
n : ℕ
⊢ ∀ (x : σ), Function.const σ 1 x ≠ 0

Tactic:
intro _

Result:
σ : Type u_1
inst✝ : Finite σ
n : ℕ
x✝ : σ
⊢ Function.const σ 1 x✝ ≠ 0

Proof state:
σ : Type u_1
inst✝ : Finite σ
n : ℕ
x✝ : σ
⊢ Function.const σ 1 x✝ ≠ 0

Tactic:
simp only [Function.const_apply, ne_eq, one_ne_zero, not_false_eq_true]

Result:
no goals

Proof state:
σ : Type u_1
inst✝ : Finite σ
n : ℕ
⊢ {f | f.degree ≤ n}.Finite

Tactic:
simp_rw [degree_eq_weight_one]

Result:
σ : Type u_1
inst✝ : Finite σ
n : ℕ
⊢ {f | (weight fun x => 1) f ≤ n}.Finite