harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem cycleFactorsFinset_eq_singleton_iff {f g : Perm α} :
    f.cycleFactorsFinset = {g} ↔ f.IsCycle ∧ f = g

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
⊢ f = g → (g.IsCycle ↔ f.IsCycle)

Tactic:
rintro rfl

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ f.IsCycle ↔ f.IsCycle

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
this : f = g → (g.IsCycle ↔ f.IsCycle)
⊢ ((∀ f ∈ {g}, f.IsCycle) ∧ ∃ (h : (↑{g}).Pairwise Disjoint), {g}.noncommProd id ⋯ = f) ↔ f.IsCycle ∧ f = g

Tactic:
simpa [eq_comm]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
⊢ f.cycleFactorsFinset = {g} ↔ f.IsCycle ∧ f = g

Tactic:
suffices f = g → (g.IsCycle ↔ f.IsCycle) by
  rw [cycleFactorsFinset_eq_finset]
  simpa [eq_comm]

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
⊢ f = g → (g.IsCycle ↔ f.IsCycle)

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ f.IsCycle ↔ f.IsCycle

Tactic:
exact Iff.rfl

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
this : f = g → (g.IsCycle ↔ f.IsCycle)
⊢ f.cycleFactorsFinset = {g} ↔ f.IsCycle ∧ f = g

Tactic:
rw [cycleFactorsFinset_eq_finset]

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
this : f = g → (g.IsCycle ↔ f.IsCycle)
⊢ ((∀ f ∈ {g}, f.IsCycle) ∧ ∃ (h : (↑{g}).Pairwise Disjoint), {g}.noncommProd id ⋯ = f) ↔ f.IsCycle ∧ f = g
-- Mathlib/Topology/Homeomorph.lean
theorem comp_isOpenMap_iff' (h : X ≃ₜ Y) {f : Y → Z} : IsOpenMap (f ∘ h) ↔ IsOpenMap f

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
h : X ≃ₜ Y
f : Y → Z
⊢ IsOpenMap (f ∘ ⇑h) → IsOpenMap f

Tactic:
intro hf

Result:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
h : X ≃ₜ Y
f : Y → Z
hf : IsOpenMap (f ∘ ⇑h)
⊢ IsOpenMap f

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
h : X ≃ₜ Y
f : Y → Z
hf : IsOpenMap (f ∘ ⇑h)
⊢ IsOpenMap f

Tactic:
rw [← Function.comp_id f, ← h.self_comp_symm, ← Function.comp_assoc]

Result:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
h : X ≃ₜ Y
f : Y → Z
hf : IsOpenMap (f ∘ ⇑h)
⊢ IsOpenMap ((f ∘ ⇑h) ∘ ⇑h.symm)

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
h : X ≃ₜ Y
f : Y → Z
⊢ IsOpenMap (f ∘ ⇑h) ↔ IsOpenMap f

Tactic:
refine ⟨?_, fun hf => hf.comp h.isOpenMap⟩

Result:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
h : X ≃ₜ Y
f : Y → Z
⊢ IsOpenMap (f ∘ ⇑h) → IsOpenMap f

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
h : X ≃ₜ Y
f : Y → Z
hf : IsOpenMap (f ∘ ⇑h)
⊢ IsOpenMap ((f ∘ ⇑h) ∘ ⇑h.symm)

Tactic:
exact hf.comp h.symm.isOpenMap

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_one : √1 = 1

Proof state:
⊢ √1 = 1

Tactic:
simp [Real.sqrt]

Result:
no goals
-- Mathlib/GroupTheory/FreeAbelianGroupFinsupp.lean
theorem support_add (a b : FreeAbelianGroup X) : support (a + b) ⊆ a.support ∪ b.support

Proof state:
X : Type u_1
a b : FreeAbelianGroup X
⊢ (a + b).support ⊆ a.support ∪ b.support

Tactic:
simp only [support, AddMonoidHom.map_add]

Result:
X : Type u_1
a b : FreeAbelianGroup X
⊢ (toFinsupp a + toFinsupp b).support ⊆ (toFinsupp a).support ∪ (toFinsupp b).support

Proof state:
X : Type u_1
a b : FreeAbelianGroup X
⊢ (toFinsupp a + toFinsupp b).support ⊆ (toFinsupp a).support ∪ (toFinsupp b).support

Tactic:
apply Finsupp.support_add

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getThenInsertIfNew?_fst (h : m.WF) {k : α} {v : β} :
    (getThenInsertIfNew? m k v).1 = get? m k

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
m : Raw α fun x => β
h : m.WF
k : α
v : β
⊢ (getThenInsertIfNew? m k v).fst = get? m k

Tactic:
simp_to_raw using Raw₀.Const.getThenInsertIfNew?_fst

Result:
no goals
-- Mathlib/Data/Multiset/ZeroCons.lean
theorem rel_refl_of_refl_on {m : Multiset α} {r : α → α → Prop} : (∀ x ∈ m, r x x) → Rel r m m

Proof state:
α : Type u_1
m : Multiset α
r : α → α → Prop
⊢ (∀ (x : α), x ∈ m → r x x) → Rel r m m

Tactic:
refine m.induction_on ?_ ?_

Result:
case refine_1
α : Type u_1
m : Multiset α
r : α → α → Prop
⊢ (∀ (x : α), x ∈ 0 → r x x) → Rel r 0 0

case refine_2
α : Type u_1
m : Multiset α
r : α → α → Prop
⊢ ∀ (a : α) (s : Multiset α),
    ((∀ (x : α), x ∈ s → r x x) → Rel r s s) → (∀ (x : α), x ∈ a ::ₘ s → r x x) → Rel r (a ::ₘ s) (a ::ₘ s)

Proof state:
case refine_2
α : Type u_1
m✝ : Multiset α
r : α → α → Prop
a : α
m : Multiset α
ih : (∀ (x : α), x ∈ m → r x x) → Rel r m m
h : ∀ (x : α), x ∈ a ::ₘ m → r x x
⊢ Rel r (a ::ₘ m) (a ::ₘ m)

Tactic:
exact Rel.cons (h _ (mem_cons_self _ _)) (ih fun _ ha => h _ (mem_cons_of_mem ha))

Result:
no goals

Proof state:
case refine_2
α : Type u_1
m : Multiset α
r : α → α → Prop
⊢ ∀ (a : α) (s : Multiset α),
    ((∀ (x : α), x ∈ s → r x x) → Rel r s s) → (∀ (x : α), x ∈ a ::ₘ s → r x x) → Rel r (a ::ₘ s) (a ::ₘ s)

Tactic:
intro a m ih h

Result:
case refine_2
α : Type u_1
m✝ : Multiset α
r : α → α → Prop
a : α
m : Multiset α
ih : (∀ (x : α), x ∈ m → r x x) → Rel r m m
h : ∀ (x : α), x ∈ a ::ₘ m → r x x
⊢ Rel r (a ::ₘ m) (a ::ₘ m)

Proof state:
case refine_1
α : Type u_1
m : Multiset α
r : α → α → Prop
a✝ : ∀ (x : α), x ∈ 0 → r x x
⊢ Rel r 0 0

Tactic:
apply Rel.zero

Result:
no goals

Proof state:
case refine_1
α : Type u_1
m : Multiset α
r : α → α → Prop
⊢ (∀ (x : α), x ∈ 0 → r x x) → Rel r 0 0

Tactic:
intros

Result:
case refine_1
α : Type u_1
m : Multiset α
r : α → α → Prop
a✝ : ∀ (x : α), x ∈ 0 → r x x
⊢ Rel r 0 0
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem length_le_length_insertList [BEq α]
    {l toInsert : List ((a : α) × β a)} :
    l.length ≤ (insertList l toInsert).length

Proof state:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
⊢ l.length ≤ (insertList l []).length

Tactic:
apply Nat.le_refl

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l toInsert : List ((a : α) × β a)
⊢ l.length ≤ (insertList l toInsert).length

Tactic:
induction toInsert generalizing l with
| nil => apply Nat.le_refl
| cons hd tl ih => exact Nat.le_trans length_le_length_insertEntry ih

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : BEq α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih : ∀ {l : List ((a : α) × β a)}, l.length ≤ (insertList l tl).length
l : List ((a : α) × β a)
⊢ l.length ≤ (insertList l (hd :: tl)).length

Tactic:
exact Nat.le_trans length_le_length_insertEntry ih

Result:
no goals
-- Mathlib/Probability/Variance.lean
theorem IndepFun.variance_sum [IsProbabilityMeasure μ] {ι : Type*} {X : ι → Ω → ℝ}
    {s : Finset ι} (hs : ∀ i ∈ s, MemLp (X i) 2 μ)
    (h : Set.Pairwise ↑s fun i j => IndepFun (X i) (X j) μ) :
    variance (∑ i ∈ s, X i) μ = ∑ i ∈ s, variance (X i) μ

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
X : ι → Ω → ℝ
k : ι
s : Finset ι
ks : k ∉ s
IH :
  (∀ i ∈ s, MemLp (X i) 2 μ) →
    ((↑s).Pairwise fun i j => IndepFun (X i) (X j) μ) → Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
hs : ∀ i ∈ insert k s, MemLp (X i) 2 μ
h : (↑(insert k s)).Pairwise fun i j => IndepFun (X i) (X j) μ
⊢ Var[X k; μ] + Var[∑ i ∈ s, X i; μ] = Var[X k; μ] + ∑ i ∈ s, Var[X i; μ]

Tactic:
rw [IH (fun i hi => hs i (mem_insert_of_mem hi))
    (h.mono (by simp only [coe_insert, Set.subset_insert]))]

Result:
no goals

Proof state:
case hXY
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
X : ι → Ω → ℝ
k : ι
s : Finset ι
ks : k ∉ s
IH :
  (∀ i ∈ s, MemLp (X i) 2 μ) →
    ((↑s).Pairwise fun i j => IndepFun (X i) (X j) μ) → Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
hs : ∀ i ∈ insert k s, MemLp (X i) 2 μ
h : (↑(insert k s)).Pairwise fun i j => IndepFun (X i) (X j) μ
i : ι
hi : i ∈ s
⊢ IndepFun (X k) (X i) μ

Tactic:
apply h (mem_insert_self _ _) (mem_insert_of_mem hi)

Result:
case hXY
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
X : ι → Ω → ℝ
k : ι
s : Finset ι
ks : k ∉ s
IH :
  (∀ i ∈ s, MemLp (X i) 2 μ) →
    ((↑s).Pairwise fun i j => IndepFun (X i) (X j) μ) → Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
hs : ∀ i ∈ insert k s, MemLp (X i) 2 μ
h : (↑(insert k s)).Pairwise fun i j => IndepFun (X i) (X j) μ
i : ι
hi : i ∈ s
⊢ k ≠ i
-- Mathlib/.lake/packages/batteries/Batteries/Data/AssocList.lean
theorem contains_eq [BEq α] (a : α) (l : AssocList α β) :
    contains a l = l.toList.any (·.1 == a)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : BEq α
a : α
l : AssocList α β
⊢ contains a l = l.toList.any fun x => x.fst == a

Tactic:
induction l <;> simp [*, contains]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Basic.lean
theorem coeff_eq_zero_of_lt_orderTop {x : HahnSeries Γ R} {i : Γ} (hi : i < x.orderTop) :
    x.coeff i = 0

Proof state:
case inr
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
i : Γ
hx : x ≠ 0
hi : i ∈ x.support
⊢ ¬i < ⋯.min ⋯

Tactic:
exact Set.IsWF.not_lt_min _ _ hi

Result:
no goals

Proof state:
case inl
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
i : Γ
hi : ↑i < orderTop 0
⊢ coeff 0 i = 0

Tactic:
exact coeff_zero

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
i : Γ
hi : ↑i < x.orderTop
⊢ x.coeff i = 0

Tactic:
rcases eq_or_ne x 0 with (rfl | hx)

Result:
case inl
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
i : Γ
hi : ↑i < orderTop 0
⊢ coeff 0 i = 0

case inr
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
i : Γ
hi : ↑i < x.orderTop
hx : x ≠ 0
⊢ x.coeff i = 0

Proof state:
case inr
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
i : Γ
hx : x ≠ 0
hi : x.coeff i ≠ 0
⊢ ¬↑i < x.orderTop

Tactic:
rw [← mem_support] at hi

Result:
case inr
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
i : Γ
hx : x ≠ 0
hi : i ∈ x.support
⊢ ¬↑i < x.orderTop

Proof state:
case inr
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
i : Γ
hx : x ≠ 0
hi : i ∈ x.support
⊢ ¬↑i < x.orderTop

Tactic:
rw [orderTop_of_ne hx, WithTop.coe_lt_coe]

Result:
case inr
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
i : Γ
hx : x ≠ 0
hi : i ∈ x.support
⊢ ¬i < ⋯.min ⋯

Proof state:
case inr
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
i : Γ
hi : ↑i < x.orderTop
hx : x ≠ 0
⊢ x.coeff i = 0

Tactic:
contrapose! hi

Result:
case inr
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
i : Γ
hx : x ≠ 0
hi : x.coeff i ≠ 0
⊢ ¬↑i < x.orderTop
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
lemma one_sub_sq_div_two_lt_cos (hx : x ≠ 0) : 1 - x ^ 2 / 2 < cos x

Proof state:
x : ℝ
hx : x ≠ 0
this : 1 / 2 + cos x * (-1 / 2) < x ^ 2 * (1 / 4)
⊢ 1 - x ^ 2 / 2 < cos x

Tactic:
linarith

Result:
no goals

Proof state:
x : ℝ
hx : x ≠ 0
⊢ x / 2 ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
x : ℝ
hx : x ≠ 0
this : 1 / 2 - cos (2 * (x / 2)) / 2 < (x / 2) ^ 2
⊢ 1 - x ^ 2 / 2 < cos x

Tactic:
ring_nf at this

Result:
x : ℝ
hx : x ≠ 0
this : 1 / 2 + cos x * (-1 / 2) < x ^ 2 * (1 / 4)
⊢ 1 - x ^ 2 / 2 < cos x

Proof state:
x : ℝ
hx : x ≠ 0
⊢ 1 - x ^ 2 / 2 < cos x

Tactic:
have := (sin_sq_lt_sq (by positivity)).trans_eq' (sin_sq_eq_half_sub (x / 2)).symm

Result:
x : ℝ
hx : x ≠ 0
this : 1 / 2 - cos (2 * (x / 2)) / 2 < (x / 2) ^ 2
⊢ 1 - x ^ 2 / 2 < cos x
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem hausdorffMeasure_zero_singleton (x : X) : μH[0] ({x} : Set X) = 1

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
this :
  1 ≤ ⨅ t, ⨅ (_ : {x} ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ 1), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ 0
⊢ 1 ≤
    ⨆ r,
      ⨆ (_ : 0 < r),
        ⨅ t,
          ⨅ (_ : {x} ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ 0

Tactic:
apply le_trans this _

Result:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
this :
  1 ≤ ⨅ t, ⨅ (_ : {x} ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ 1), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ 0
⊢ ⨅ t, ⨅ (_ : {x} ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ 1), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ 0 ≤
    ⨆ r,
      ⨆ (_ : 0 < r),
        ⨅ t,
          ⨅ (_ : {x} ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ 0

Proof state:
case h.e'_3
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
this :
  1 ≤ ⨅ t, ⨅ (_ : {x} ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ 1), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ 0
⊢ ⨅ t, ⨅ (_ : {x} ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ 1), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ 0 =
    ⨅ t, ⨅ (_ : {x} ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ 1), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ 0

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/DFinsupp.lean
theorem iSupIndep.dfinsupp_lsum_injective {p : ι → Submodule R N} (h : iSupIndep p) :
    Function.Injective (lsum ℕ (M := fun i ↦ ↥(p i)) fun i => (p i).subtype)

Proof state:
case h
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0
m : Π₀ (i : ι), ↥(p i)
hm : ((lsum ℕ) fun i => (p i).subtype) m = 0
i : ι
⊢ ((lsum ℕ) fun i => (p i).subtype) (erase i m) = ↑(-m i)

Tactic:
rwa [← erase_add_single i m, LinearMap.map_add, lsum_single, Submodule.subtype_apply,
  add_eq_zero_iff_eq_neg, ← Submodule.coe_neg] at hm

Result:
no goals
-- Mathlib/LinearAlgebra/UnitaryGroup.lean
theorem mem_orthogonalGroup_iff {A : Matrix n n β} :
    A ∈ Matrix.orthogonalGroup n β ↔ A * star A = 1

Proof state:
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
β : Type v
inst✝ : CommRing β
A : Matrix n n β
hA : A * star A = 1
⊢ star A * A = 1

Tactic:
simpa only [mul_eq_one_comm] using hA

Result:
no goals

Proof state:
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
β : Type v
inst✝ : CommRing β
A : Matrix n n β
⊢ A ∈ orthogonalGroup n β ↔ A * star A = 1

Tactic:
refine ⟨And.right, fun hA => ⟨?_, hA⟩⟩

Result:
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
β : Type v
inst✝ : CommRing β
A : Matrix n n β
hA : A * star A = 1
⊢ star A * A = 1
-- Mathlib/Data/Finite/Card.lean
theorem card_subtype_le [Finite α] (p : α → Prop) : Nat.card { x // p x } ≤ Nat.card α

Proof state:
α : Type u_1
inst✝ : Finite α
p : α → Prop
this : Fintype α
⊢ Nat.card { x // p x } ≤ Nat.card α

Tactic:
simpa only [Nat.card_eq_fintype_card] using Fintype.card_subtype_le p

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Finite α
p : α → Prop
⊢ Nat.card { x // p x } ≤ Nat.card α

Tactic:
haveI := Fintype.ofFinite α

Result:
α : Type u_1
inst✝ : Finite α
p : α → Prop
this : Fintype α
⊢ Nat.card { x // p x } ≤ Nat.card α

Proof state:
α : Type u_1
inst✝ : Finite α
p : α → Prop
⊢ Nat.card { x // p x } ≤ Nat.card α

Tactic:
classical
haveI := Fintype.ofFinite α
simpa only [Nat.card_eq_fintype_card] using Fintype.card_subtype_le p

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean
@[simp]
lemma coe_map_inv_mul_map (g : GL n R) : g.val⁻¹.map f * g.val.map f = 1

Proof state:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g : GL n R
⊢ ((↑g)⁻¹ * ↑g).map ⇑f = 1

Tactic:
simp only [isUnits_det_units, nonsing_inv_mul, map_zero, _root_.map_one, Matrix.map_one]

Result:
no goals

Proof state:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g : GL n R
⊢ (↑g)⁻¹.map ⇑f * (↑g).map ⇑f = 1

Tactic:
rw [← Matrix.map_mul]

Result:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g : GL n R
⊢ ((↑g)⁻¹ * ↑g).map ⇑f = 1
-- Mathlib/Data/Multiset/Lattice.lean
theorem sup_union (s₁ s₂ : Multiset α) : (s₁ ∪ s₂).sup = s₁.sup ⊔ s₂.sup

Proof state:
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁ ∪ s₂).sup = s₁.sup ⊔ s₂.sup

Tactic:
rw [← sup_dedup, dedup_ext.2, sup_dedup, sup_add]

Result:
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ + s₂

Proof state:
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ + s₂

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Submodule.lean
theorem mulRightMap_eq_mulMap_comp {ι : Type*} [DecidableEq ι] (n : ι → N) :
    mulRightMap M n = mulMap M N ∘ₗ LinearMap.lTensor M (Finsupp.linearCombination R n) ∘ₗ
      (TensorProduct.finsuppScalarRight R M ι).symm.toLinearMap

Proof state:
case h.h
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
M N : Submodule R S
ι : Type u_1
inst✝ : DecidableEq ι
n : ι → ↥N
a✝ : ι
x✝ : ↥M
⊢ (M.mulRightMap n ∘ₗ Finsupp.lsingle a✝) x✝ =
    ((M.mulMap N ∘ₗ
          LinearMap.lTensor (↥M) (Finsupp.linearCombination R n) ∘ₗ
            ↑(TensorProduct.finsuppScalarRight R (↥M) ι).symm) ∘ₗ
        Finsupp.lsingle a✝)
      x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
M N : Submodule R S
ι : Type u_1
inst✝ : DecidableEq ι
n : ι → ↥N
⊢ M.mulRightMap n =
    M.mulMap N ∘ₗ
      LinearMap.lTensor (↥M) (Finsupp.linearCombination R n) ∘ₗ ↑(TensorProduct.finsuppScalarRight R (↥M) ι).symm

Tactic:
ext

Result:
case h.h
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
M N : Submodule R S
ι : Type u_1
inst✝ : DecidableEq ι
n : ι → ↥N
a✝ : ι
x✝ : ↥M
⊢ (M.mulRightMap n ∘ₗ Finsupp.lsingle a✝) x✝ =
    ((M.mulMap N ∘ₗ
          LinearMap.lTensor (↥M) (Finsupp.linearCombination R n) ∘ₗ
            ↑(TensorProduct.finsuppScalarRight R (↥M) ι).symm) ∘ₗ
        Finsupp.lsingle a✝)
      x✝
-- Mathlib/Algebra/Category/Grp/EpiMono.lean
theorem h_apply_infinity (x : B) (hx : x ∈ f.hom.range) : (h x) ∞ = ∞

Proof state:
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∈ (Hom.hom f).range
⊢ (h x) ∞ = ∞

Tactic:
change ((τ).symm.trans (g x)).trans τ _ = _

Result:
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∈ (Hom.hom f).range
⊢ (((Equiv.symm τ).trans (g x)).trans τ) ∞ = ∞

Proof state:
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∈ (Hom.hom f).range
⊢ τ (fromCoset ⟨x • ↑⟨↑(Hom.hom f).range, ⋯⟩, ⋯⟩) = ∞

Tactic:
simpa only using τ_apply_fromCoset' f x hx

Result:
no goals

Proof state:
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∈ (Hom.hom f).range
⊢ τ ((g x) ((Equiv.symm τ) ∞)) = ∞

Tactic:
rw [τ_symm_apply_infinity, g_apply_fromCoset]

Result:
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∈ (Hom.hom f).range
⊢ τ (fromCoset ⟨x • ↑⟨↑(Hom.hom f).range, ⋯⟩, ⋯⟩) = ∞

Proof state:
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∈ (Hom.hom f).range
⊢ (((Equiv.symm τ).trans (g x)).trans τ) ∞ = ∞

Tactic:
simp only [MonoidHom.coe_mk, Equiv.toFun_as_coe, Equiv.coe_trans, Function.comp_apply]

Result:
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∈ (Hom.hom f).range
⊢ τ ((g x) ((Equiv.symm τ) ∞)) = ∞
-- Mathlib/Algebra/Group/Submonoid/Operations.lean
theorem bot_or_nontrivial (S : Submonoid M) : S = ⊥ ∨ Nontrivial S

Proof state:
M : Type u_1
inst✝ : MulOneClass M
S : Submonoid M
⊢ S = ⊥ ∨ Nontrivial ↥S

Tactic:
simp only [eq_bot_iff_forall, nontrivial_iff_exists_ne_one, ← not_forall, ← Classical.not_imp,
  Classical.em]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_one : (1#w).msb = decide (w = 1)

Proof state:
w : Nat
⊢ (1#w).msb = decide (w = 1)

Tactic:
simp [BitVec.msb, getMsbD_one, ← Bool.decide_and]

Result:
w : Nat
⊢ 0 = w - 1 ∧ 0 < w ↔ w = 1

Proof state:
w : Nat
⊢ 0 = w - 1 ∧ 0 < w ↔ w = 1

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Matroid/Constructions.lean
theorem uniqueBaseOn_indep_iff (hIE : I ⊆ E) : (uniqueBaseOn I E).Indep J ↔ J ⊆ I

Proof state:
α : Type u_1
E I J : Set α
hIE : I ⊆ E
⊢ (uniqueBaseOn I E).Indep J ↔ J ⊆ I

Tactic:
rw [uniqueBaseOn, restrict_indep_iff, freeOn_indep_iff, and_iff_left_iff_imp]

Result:
α : Type u_1
E I J : Set α
hIE : I ⊆ E
⊢ J ⊆ I → J ⊆ E

Proof state:
α : Type u_1
E I J : Set α
hIE : I ⊆ E
⊢ J ⊆ I → J ⊆ E

Tactic:
exact fun h ↦ h.trans hIE

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem volume_eq_zero (w : {w // IsReal w}) :
    volume ({x : mixedSpace K | x.1 w = 0}) = 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : { w // w.IsReal }
A : AffineSubspace ℝ (mixedSpace K) :=
  { carrier := {x | x.1 w = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }.toAffineSubspace
⊢ volume {x | x.1 w = 0} = 0

Tactic:
convert Measure.addHaar_affineSubspace volume A fun h ↦ ?_

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : { w // w.IsReal }
A : AffineSubspace ℝ (mixedSpace K) :=
  { carrier := {x | x.1 w = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }.toAffineSubspace
h : A = ⊤
⊢ False

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : { w // w.IsReal }
⊢ ∀ {a b : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)},
    a ∈ {x | x.1 w = 0} → b ∈ {x | x.1 w = 0} → a + b ∈ {x | x.1 w = 0}

Tactic:
aesop

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : { w // w.IsReal }
⊢ ∀ (c : ℝ) {x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)},
    x ∈ { carrier := {x | x.1 w = 0}, add_mem' := ⋯, zero_mem' := ⋯ }.carrier →
      c • x ∈ { carrier := {x | x.1 w = 0}, add_mem' := ⋯, zero_mem' := ⋯ }.carrier

Tactic:
aesop

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : { w // w.IsReal }
⊢ volume {x | x.1 w = 0} = 0

Tactic:
let A : AffineSubspace ℝ (mixedSpace K) :=
  Submodule.toAffineSubspace (Submodule.mk ⟨⟨{x | x.1 w = 0}, by aesop⟩, rfl⟩ (by aesop))

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : { w // w.IsReal }
A : AffineSubspace ℝ (mixedSpace K) :=
  { carrier := {x | x.1 w = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }.toAffineSubspace
⊢ volume {x | x.1 w = 0} = 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : { w // w.IsReal }
A : AffineSubspace ℝ (mixedSpace K) :=
  { carrier := {x | x.1 w = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }.toAffineSubspace
h : A = ⊤
⊢ False

Tactic:
simpa [A] using (h ▸ Set.mem_univ _ : 1 ∈ A)

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
lemma take_drop : (a.drop m).take n = (a.take (m + n)).drop m

Proof state:
α : Type u
m n : ℕ
a : Stream' α
⊢ take n (drop m a) = List.drop m (take (m + n) a)

Tactic:
apply List.ext_getElem <;> simp

Result:
no goals