harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SetFamily/LYM.lean
theorem card_mul_le_card_shadow_mul (h𝒜 : (𝒜 : Set (Finset α)).Sized r) :
    #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)

Proof state:
case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 => x1 ⊆ x2 := fun x x_1 => Classical.dec ((fun x1 x2 => x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
⊢ t ∈ image (fun a => insert a s) sᶜ

Tactic:
have : ∅ ∉ 𝒜 := by
  rw [← mem_coe, h𝒜.empty_mem_iff, coe_eq_singleton]
  rintro rfl
  rw [shadow_singleton_empty] at hs
  exact not_mem_empty s hs

Result:
case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 => x1 ⊆ x2 := fun x x_1 => Classical.dec ((fun x1 x2 => x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
this : ∅ ∉ 𝒜
⊢ t ∈ image (fun a => insert a s) sᶜ

Proof state:
case refine_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 => x1 ⊆ x2 := fun x x_1 => Classical.dec ((fun x1 x2 => x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ #(image s.erase s) ≤ #(bipartiteBelow (fun x1 x2 => x1 ⊆ x2) (∂ 𝒜) s)

Tactic:
refine card_le_card ?_

Result:
case refine_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 => x1 ⊆ x2 := fun x x_1 => Classical.dec ((fun x1 x2 => x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ image s.erase s ⊆ bipartiteBelow (fun x1 x2 => x1 ⊆ x2) (∂ 𝒜) s

Proof state:
case refine_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 => x1 ⊆ x2 := fun x x_1 => Classical.dec ((fun x1 x2 => x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ r ≤ #(bipartiteBelow (fun x1 x2 => x1 ⊆ x2) (∂ 𝒜) s)

Tactic:
rw [← h𝒜 hs, ← card_image_of_injOn s.erase_injOn]

Result:
case refine_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 => x1 ⊆ x2 := fun x x_1 => Classical.dec ((fun x1 x2 => x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ #(image s.erase s) ≤ #(bipartiteBelow (fun x1 x2 => x1 ⊆ x2) (∂ 𝒜) s)

Proof state:
case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 => x1 ⊆ x2 := fun x x_1 => Classical.dec ((fun x1 x2 => x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
⊢ #(bipartiteAbove (fun x1 x2 => x1 ⊆ x2) 𝒜 s) ≤ Fintype.card α - r + 1

Tactic:
refine le_trans ?_ tsub_tsub_le_tsub_add

Result:
case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 => x1 ⊆ x2 := fun x x_1 => Classical.dec ((fun x1 x2 => x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
⊢ #(bipartiteAbove (fun x1 x2 => x1 ⊆ x2) 𝒜 s) ≤ Fintype.card α - (r - 1)
-- Mathlib/Data/Fin/Basic.lean
protected lemma lt_or_eq_of_le : a ≤ b → a < b ∨ a = b

Proof state:
n : ℕ
a b : Fin n
⊢ a ≤ b → a < b ∨ ↑a = ↑b

Tactic:
exact Nat.lt_or_eq_of_le

Result:
no goals

Proof state:
n : ℕ
a b : Fin n
⊢ a ≤ b → a < b ∨ a = b

Tactic:
rw [Fin.ext_iff]

Result:
n : ℕ
a b : Fin n
⊢ a ≤ b → a < b ∨ ↑a = ↑b
-- Mathlib/Order/MinMax.lean
theorem Max.left_comm (a b c : α) : max a (max b c) = max b (max a c)

Proof state:
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ a ⊔ (b ⊔ c) = b ⊔ (a ⊔ c)

Tactic:
rw [← max_assoc, max_comm a, max_assoc]

Result:
no goals
-- Mathlib/RingTheory/Ideal/GoingUp.lean
theorem injective_quotient_le_comap_map (P : Ideal R[X]) :
    Function.Injective <|
      Ideal.quotientMap
        (Ideal.map (Polynomial.mapRingHom (Quotient.mk (P.comap (C : R →+* R[X])))) P)
        (Polynomial.mapRingHom (Ideal.Quotient.mk (P.comap (C : R →+* R[X]))))
        le_comap_map

Proof state:
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
⊢ comap (mapRingHom (Quotient.mk (comap C P))) (map (mapRingHom (Quotient.mk (comap C P))) P) = P

Tactic:
rw [comap_map_of_surjective (mapRingHom (Ideal.Quotient.mk (P.comap (C : R →+* R[X]))))
    (map_surjective (Ideal.Quotient.mk (P.comap (C : R →+* R[X]))) Ideal.Quotient.mk_surjective)]

Result:
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
⊢ P ⊔ comap (mapRingHom (Quotient.mk (comap C P))) ⊥ = P

Proof state:
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
⊢ Function.Injective
    ⇑(quotientMap (map (mapRingHom (Quotient.mk (comap C P))) P) (mapRingHom (Quotient.mk (comap C P))) ⋯)

Tactic:
refine quotientMap_injective' (le_of_eq ?_)

Result:
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
⊢ comap (mapRingHom (Quotient.mk (comap C P))) (map (mapRingHom (Quotient.mk (comap C P))) P) = P

Proof state:
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
⊢ comap (mapRingHom (Quotient.mk (comap C P))) ⊥ ≤ P

Tactic:
refine fun p hp =>
  polynomial_mem_ideal_of_coeff_mem_ideal P p fun n => Ideal.Quotient.eq_zero_iff_mem.mp ?_

Result:
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
p : R[X]
hp : p ∈ comap (mapRingHom (Quotient.mk (comap C P))) ⊥
n : ℕ
⊢ (Quotient.mk (comap C P)) (p.coeff n) = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
p : R[X]
hp : p ∈ comap (mapRingHom (Quotient.mk (comap C P))) ⊥
n : ℕ
⊢ (Quotient.mk (comap C P)) (p.coeff n) = 0

Tactic:
simpa only [coeff_map, coe_mapRingHom] using ext_iff.mp (Ideal.mem_bot.mp (mem_comap.mp hp)) n

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
⊢ P ⊔ comap (mapRingHom (Quotient.mk (comap C P))) ⊥ = P

Tactic:
refine le_antisymm (sup_le le_rfl ?_) (le_sup_of_le_left le_rfl)

Result:
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
⊢ comap (mapRingHom (Quotient.mk (comap C P))) ⊥ ≤ P
-- Mathlib/Order/Monotone/Basic.lean
lemma StrictMono.add_le_nat {f : ℕ → ℕ} (hf : StrictMono f) (m n : ℕ) : m + f n ≤ f (m + n)

Proof state:
f : ℕ → ℕ
hf : StrictMono f
m n : ℕ
⊢ f n + m ≤ f (n + m)

Tactic:
induction m with
| zero => rw [Nat.add_zero, Nat.add_zero]
| succ m ih =>
  rw [← Nat.add_assoc, ← Nat.add_assoc, Nat.succ_le]
  exact ih.trans_lt (hf (n + m).lt_succ_self)

Result:
no goals

Proof state:
case zero
f : ℕ → ℕ
hf : StrictMono f
n : ℕ
⊢ f n + 0 ≤ f (n + 0)

Tactic:
rw [Nat.add_zero, Nat.add_zero]

Result:
no goals

Proof state:
case succ
f : ℕ → ℕ
hf : StrictMono f
n m : ℕ
ih : f n + m ≤ f (n + m)
⊢ f n + (m + 1) ≤ f (n + (m + 1))

Tactic:
rw [← Nat.add_assoc, ← Nat.add_assoc, Nat.succ_le]

Result:
case succ
f : ℕ → ℕ
hf : StrictMono f
n m : ℕ
ih : f n + m ≤ f (n + m)
⊢ f n + m < f (n + m + 1)

Proof state:
case succ
f : ℕ → ℕ
hf : StrictMono f
n m : ℕ
ih : f n + m ≤ f (n + m)
⊢ f n + m < f (n + m + 1)

Tactic:
exact ih.trans_lt (hf (n + m).lt_succ_self)

Result:
no goals

Proof state:
f : ℕ → ℕ
hf : StrictMono f
m n : ℕ
⊢ m + f n ≤ f (m + n)

Tactic:
rw [Nat.add_comm m, Nat.add_comm m]

Result:
f : ℕ → ℕ
hf : StrictMono f
m n : ℕ
⊢ f n + m ≤ f (n + m)
-- Mathlib/Data/Num/Lemmas.lean
theorem mod_to_int : ∀ n d, ((n % d : ZNum) : ℤ) = n % d
  | 0, _ => (Int.zero_emod _).symm
  | pos n, d =>
    (Num.cast_toZNum _).trans <| by
      rw [← Num.to_nat_to_int, cast_pos, Num.mod_to_nat, ← PosNum.to_nat_to_int, abs_to_nat]
      rfl
  | neg n, d =>
    (Num.cast_sub' _ _).trans <| by
      rw [← Num.to_nat_to_int, cast_neg, ← Num.to_nat_to_int, Num.succ_to_nat, Num.mod_to_nat,
          abs_to_nat, ← Int.subNatNat_eq_coe, n.to_int_eq_succ_pred]
      rfl

Proof state:
n : PosNum
d : ZNum
⊢ ↑(↑(Num.pos n) % (↑d).natAbs) = ↑↑n % ↑d

Tactic:
rfl

Result:
no goals

Proof state:
n : PosNum
d : ZNum
⊢ ↑(Num.pos n % d.abs) = ↑(pos n) % ↑d

Tactic:
rw [← Num.to_nat_to_int, cast_pos, Num.mod_to_nat, ← PosNum.to_nat_to_int, abs_to_nat]

Result:
n : PosNum
d : ZNum
⊢ ↑(↑(Num.pos n) % (↑d).natAbs) = ↑↑n % ↑d

Proof state:
n : PosNum
d : ZNum
⊢ subNatNat (↑d).natAbs (↑n.pred' % (↑d).natAbs + 1) = -(↑↑n.pred' + 1) % ↑d

Tactic:
rfl

Result:
no goals

Proof state:
n : PosNum
d : ZNum
⊢ ↑d.abs - ↑(n.pred' % d.abs).succ = ↑(neg n) % ↑d

Tactic:
rw [← Num.to_nat_to_int, cast_neg, ← Num.to_nat_to_int, Num.succ_to_nat, Num.mod_to_nat,
    abs_to_nat, ← Int.subNatNat_eq_coe, n.to_int_eq_succ_pred]

Result:
n : PosNum
d : ZNum
⊢ subNatNat (↑d).natAbs (↑n.pred' % (↑d).natAbs + 1) = -(↑↑n.pred' + 1) % ↑d
-- Mathlib/Algebra/Order/Module/Defs.lean
/-- A constructor for `SMulPosReflectLT` requiring you to prove `a₁ • b < a₂ • b → a₁ < a₂` only
when `0 < b` -/
lemma SMulPosReflectLT.of_pos (h₀ : ∀ b : β, 0 < b → ∀ a₁ a₂ : α, a₁ • b < a₂ • b → a₁ < a₂) :
    SMulPosReflectLT α β where
  elim b hb a₁ a₂ h

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ • b < a₂ • b → a₁ < a₂
b : β
hb : 0 ≤ b
a₁ a₂ : α
h : a₁ • b < a₂ • b
⊢ a₁ < a₂

Tactic:
obtain hb | hb := hb.eq_or_lt

Result:
case inl
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ • b < a₂ • b → a₁ < a₂
b : β
hb✝ : 0 ≤ b
a₁ a₂ : α
h : a₁ • b < a₂ • b
hb : 0 = b
⊢ a₁ < a₂

case inr
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ • b < a₂ • b → a₁ < a₂
b : β
hb✝ : 0 ≤ b
a₁ a₂ : α
h : a₁ • b < a₂ • b
hb : 0 < b
⊢ a₁ < a₂

Proof state:
case inl
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ • b < a₂ • b → a₁ < a₂
b : β
hb✝ : 0 ≤ b
a₁ a₂ : α
h : a₁ • b < a₂ • b
hb : 0 = b
⊢ a₁ < a₂

Tactic:
simp [← hb] at h

Result:
no goals

Proof state:
case inr
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ • b < a₂ • b → a₁ < a₂
b : β
hb✝ : 0 ≤ b
a₁ a₂ : α
h : a₁ • b < a₂ • b
hb : 0 < b
⊢ a₁ < a₂

Tactic:
exact h₀ _ hb _ _ h

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem IsAlgebraic.exists_nonzero_coeff_and_aeval_eq_zero
    {s : S} (hRs : IsAlgebraic R s) (hs : s ∈ nonZeroDivisors S) :
    ∃ q : R[X], q.coeff 0 ≠ 0 ∧ aeval s q = 0

Proof state:
case intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hs : s ∈ nonZeroDivisors S
p : R[X]
hp0 : p ≠ 0
q : R[X]
hp : (aeval s) q * s ^ rootMultiplicity 0 p = 0
hpq : p = q * X ^ rootMultiplicity 0 p
hq : ¬q.coeff 0 = 0
⊢ ∃ q, q.coeff 0 ≠ 0 ∧ (aeval s) q = 0

Tactic:
exact ⟨q, hq, (nonZeroDivisors S).pow_mem hs (rootMultiplicity 0 p) (aeval s q) hp⟩

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ nonZeroDivisors S
⊢ ∃ q, q.coeff 0 ≠ 0 ∧ (aeval s) q = 0

Tactic:
obtain ⟨p, hp0, hp⟩ := hRs

Result:
case intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hs : s ∈ nonZeroDivisors S
p : R[X]
hp0 : p ≠ 0
hp : (aeval s) p = 0
⊢ ∃ q, q.coeff 0 ≠ 0 ∧ (aeval s) q = 0

Proof state:
case intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hs : s ∈ nonZeroDivisors S
p : R[X]
hp0 : p ≠ 0
hp : (aeval s) p = 0
q : R[X]
hpq : p = q * X ^ rootMultiplicity 0 p
hq : ¬q.coeff 0 = 0
⊢ ∃ q, q.coeff 0 ≠ 0 ∧ (aeval s) q = 0

Tactic:
rw [hpq, map_mul, aeval_X_pow] at hp

Result:
case intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hs : s ∈ nonZeroDivisors S
p : R[X]
hp0 : p ≠ 0
q : R[X]
hp : (aeval s) q * s ^ rootMultiplicity 0 p = 0
hpq : p = q * X ^ rootMultiplicity 0 p
hq : ¬q.coeff 0 = 0
⊢ ∃ q, q.coeff 0 ≠ 0 ∧ (aeval s) q = 0

Proof state:
case intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hs : s ∈ nonZeroDivisors S
p : R[X]
hp0 : p ≠ 0
hp : (aeval s) p = 0
q : R[X]
hpq : p = (X - C 0) ^ rootMultiplicity 0 p * q
hq : ¬X - C 0 ∣ q
⊢ ∃ q, q.coeff 0 ≠ 0 ∧ (aeval s) q = 0

Tactic:
simp only [C_0, sub_zero, X_pow_mul, X_dvd_iff] at hpq hq

Result:
case intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hs : s ∈ nonZeroDivisors S
p : R[X]
hp0 : p ≠ 0
hp : (aeval s) p = 0
q : R[X]
hpq : p = q * X ^ rootMultiplicity 0 p
hq : ¬q.coeff 0 = 0
⊢ ∃ q, q.coeff 0 ≠ 0 ∧ (aeval s) q = 0

Proof state:
case intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hs : s ∈ nonZeroDivisors S
p : R[X]
hp0 : p ≠ 0
hp : (aeval s) p = 0
⊢ ∃ q, q.coeff 0 ≠ 0 ∧ (aeval s) q = 0

Tactic:
obtain ⟨q, hpq, hq⟩ := exists_eq_pow_rootMultiplicity_mul_and_not_dvd p hp0 0

Result:
case intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hs : s ∈ nonZeroDivisors S
p : R[X]
hp0 : p ≠ 0
hp : (aeval s) p = 0
q : R[X]
hpq : p = (X - C 0) ^ rootMultiplicity 0 p * q
hq : ¬X - C 0 ∣ q
⊢ ∃ q, q.coeff 0 ≠ 0 ∧ (aeval s) q = 0
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem exists_fixed_point_of_prime {p n : ℕ} [hp : Fact p.Prime] (hα : ¬p ∣ Fintype.card α)
    {σ : Perm α} (hσ : σ ^ p ^ n = 1) : ∃ a : α, σ a = a

Proof state:
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : ¬p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
⊢ ∃ a, σ a = a

Tactic:
contrapose! hα

Result:
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
hα : ∀ (a : α), σ a ≠ a
⊢ p ∣ Fintype.card α

Proof state:
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : ¬p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
⊢ ∃ a, σ a = a

Tactic:
classical
  contrapose! hα
  simp_rw [← mem_support, ← Finset.eq_univ_iff_forall] at hα
  exact Nat.modEq_zero_iff_dvd.1 ((congr_arg _ (Finset.card_eq_zero.2 (compl_eq_bot.2 hα))).mp
    (card_compl_support_modEq hσ).symm)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
hα : ∀ (a : α), σ a ≠ a
⊢ p ∣ Fintype.card α

Tactic:
simp_rw [← mem_support, ← Finset.eq_univ_iff_forall] at hα

Result:
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
hα : σ.support = Finset.univ
⊢ p ∣ Fintype.card α

Proof state:
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
hα : σ.support = Finset.univ
⊢ p ∣ Fintype.card α

Tactic:
exact Nat.modEq_zero_iff_dvd.1 ((congr_arg _ (Finset.card_eq_zero.2 (compl_eq_bot.2 hα))).mp
  (card_compl_support_modEq hσ).symm)

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_inter_add_diff₀ (s : Set α) (ht : NullMeasurableSet t μ) :
    μ.restrict (s ∩ t) + μ.restrict (s \ t) = μ.restrict s

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
⊢ μ.restrict (s ∩ t) + μ.restrict (s \ t) = μ.restrict s

Tactic:
ext1 u hu

Result:
case h
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
u : Set α
hu : MeasurableSet u
⊢ (μ.restrict (s ∩ t) + μ.restrict (s \ t)) u = (μ.restrict s) u

Proof state:
case h
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
u : Set α
hu : MeasurableSet u
⊢ μ (u ∩ s ∩ t) + μ (u ∩ s ∩ tᶜ) = μ (u ∩ s)

Tactic:
exact measure_inter_add_diff₀ (u ∩ s) ht

Result:
no goals

Proof state:
case h
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
u : Set α
hu : MeasurableSet u
⊢ (μ.restrict (s ∩ t) + μ.restrict (s \ t)) u = (μ.restrict s) u

Tactic:
simp only [add_apply, restrict_apply hu, ← inter_assoc, diff_eq]

Result:
case h
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
u : Set α
hu : MeasurableSet u
⊢ μ (u ∩ s ∩ t) + μ (u ∩ s ∩ tᶜ) = μ (u ∩ s)
-- Mathlib/Data/Finsupp/Basic.lean
theorem mapDomain_support [DecidableEq β] {f : α → β} {s : α →₀ M} :
    (s.mapDomain f).support ⊆ s.support.image f :=
  Finset.Subset.trans support_sum <|
    Finset.Subset.trans (Finset.biUnion_mono fun _ _ => support_single_subset) <| by
      rw [Finset.biUnion_singleton]

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq β
f : α → β
s : α →₀ M
⊢ (s.support.biUnion fun x => {f x}) ⊆ image f s.support

Tactic:
rw [Finset.biUnion_singleton]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
theorem Orthonormal.inner_left_right_finset {s : Finset ι} {v : ι → E} (hv : Orthonormal 𝕜 v)
    {a : ι → ι → 𝕜} : (∑ i ∈ s, ∑ j ∈ s, a i j • ⟪v j, v i⟫) = ∑ k ∈ s, a k k

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
s : Finset ι
v : ι → E
hv : Orthonormal 𝕜 v
a : ι → ι → 𝕜
⊢ ∑ i ∈ s, ∑ j ∈ s, a i j • inner (v j) (v i) = ∑ k ∈ s, a k k

Tactic:
classical
simp [orthonormal_iff_ite.mp hv, Finset.sum_ite_of_true]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
s : Finset ι
v : ι → E
hv : Orthonormal 𝕜 v
a : ι → ι → 𝕜
⊢ ∑ i ∈ s, ∑ j ∈ s, a i j • inner (v j) (v i) = ∑ k ∈ s, a k k

Tactic:
simp [orthonormal_iff_ite.mp hv, Finset.sum_ite_of_true]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast!_cons_eq_getLastD [Inhabited α] : @getLast! α _ (a::l) = getLastD l a

Proof state:
α : Type u_1
a : α
l : List α
inst✝ : Inhabited α
⊢ (a :: l).getLast! = l.getLastD a

Tactic:
simp [getLast!, getLast_eq_getLastD]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_map {mβ : MeasurableSpace β} {f : β → ℝ≥0∞} {g : α → β} (hf : Measurable f)
    (hg : Measurable g) : ∫⁻ a, f a ∂map g μ = ∫⁻ a, f (g a) ∂μ

Proof state:
case e_s.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
n : ℕ
⊢ (eapprox f n).lintegral (Measure.map g μ) = (eapprox (f ∘ g) n).lintegral μ

Tactic:
convert SimpleFunc.lintegral_map _ hg

Result:
case h.e'_3.h.e'_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
n : ℕ
⊢ eapprox (f ∘ g) n = (eapprox f n).comp g hg

Proof state:
case h.e'_3.h.e'_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
n : ℕ
⊢ eapprox (f ∘ g) n = (eapprox f n).comp g hg

Tactic:
ext1 x

Result:
case h.e'_3.h.e'_3.H
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
n : ℕ
x : α
⊢ (eapprox (f ∘ g) n) x = ((eapprox f n).comp g hg) x

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
⊢ ∫⁻ (a : β), f a ∂Measure.map g μ = ∫⁻ (a : α), f (g a) ∂μ

Tactic:
erw [lintegral_eq_iSup_eapprox_lintegral hf, lintegral_eq_iSup_eapprox_lintegral (hf.comp hg)]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
⊢ ⨆ n, (eapprox f n).lintegral (Measure.map g μ) = ⨆ n, (eapprox (f ∘ g) n).lintegral μ

Proof state:
case h.e'_3.h.e'_3.H
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
n : ℕ
x : α
⊢ (eapprox (f ∘ g) n) x = ((eapprox f n).comp g hg) x

Tactic:
simp only [eapprox_comp hf hg, coe_comp]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
⊢ ⨆ n, (eapprox f n).lintegral (Measure.map g μ) = ⨆ n, (eapprox (f ∘ g) n).lintegral μ

Tactic:
congr with n : 1

Result:
case e_s.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
n : ℕ
⊢ (eapprox f n).lintegral (Measure.map g μ) = (eapprox (f ∘ g) n).lintegral μ
-- Mathlib/Data/Finsupp/Basic.lean
theorem some_zero [Zero M] : (0 : Option α →₀ M).some = 0

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
⊢ some 0 = 0

Tactic:
ext

Result:
case h
α : Type u_1
M : Type u_5
inst✝ : Zero M
a✝ : α
⊢ (some 0) a✝ = 0 a✝

Proof state:
case h
α : Type u_1
M : Type u_5
inst✝ : Zero M
a✝ : α
⊢ (some 0) a✝ = 0 a✝

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem lt_iff_lex_lt (l m : Products I) : l < m ↔ List.Lex (· < ·) l.val m.val

Proof state:
case mk.mk
I : Type u
inst✝ : LinearOrder I
val✝¹ : List I
property✝¹ : List.Chain' (fun x1 x2 => x1 > x2) val✝¹
val✝ : List I
property✝ : List.Chain' (fun x1 x2 => x1 > x2) val✝
⊢ val✝¹ < val✝ ↔ List.Lex (fun x1 x2 => x1 < x2) ↑⟨val✝¹, property✝¹⟩ ↑⟨val✝, property✝⟩

Tactic:
exact Iff.rfl

Result:
no goals

Proof state:
case mk.mk
I : Type u
inst✝ : LinearOrder I
val✝¹ : List I
property✝¹ : List.Chain' (fun x1 x2 => x1 > x2) val✝¹
val✝ : List I
property✝ : List.Chain' (fun x1 x2 => x1 > x2) val✝
⊢ ⟨val✝¹, property✝¹⟩ < ⟨val✝, property✝⟩ ↔ List.Lex (fun x1 x2 => x1 < x2) ↑⟨val✝¹, property✝¹⟩ ↑⟨val✝, property✝⟩

Tactic:
rw [Subtype.mk_lt_mk]

Result:
case mk.mk
I : Type u
inst✝ : LinearOrder I
val✝¹ : List I
property✝¹ : List.Chain' (fun x1 x2 => x1 > x2) val✝¹
val✝ : List I
property✝ : List.Chain' (fun x1 x2 => x1 > x2) val✝
⊢ val✝¹ < val✝ ↔ List.Lex (fun x1 x2 => x1 < x2) ↑⟨val✝¹, property✝¹⟩ ↑⟨val✝, property✝⟩

Proof state:
I : Type u
inst✝ : LinearOrder I
l m : Products I
⊢ l < m ↔ List.Lex (fun x1 x2 => x1 < x2) ↑l ↑m

Tactic:
cases l

Result:
case mk
I : Type u
inst✝ : LinearOrder I
m : Products I
val✝ : List I
property✝ : List.Chain' (fun x1 x2 => x1 > x2) val✝
⊢ ⟨val✝, property✝⟩ < m ↔ List.Lex (fun x1 x2 => x1 < x2) ↑⟨val✝, property✝⟩ ↑m

Proof state:
case mk
I : Type u
inst✝ : LinearOrder I
m : Products I
val✝ : List I
property✝ : List.Chain' (fun x1 x2 => x1 > x2) val✝
⊢ ⟨val✝, property✝⟩ < m ↔ List.Lex (fun x1 x2 => x1 < x2) ↑⟨val✝, property✝⟩ ↑m

Tactic:
cases m

Result:
case mk.mk
I : Type u
inst✝ : LinearOrder I
val✝¹ : List I
property✝¹ : List.Chain' (fun x1 x2 => x1 > x2) val✝¹
val✝ : List I
property✝ : List.Chain' (fun x1 x2 => x1 > x2) val✝
⊢ ⟨val✝¹, property✝¹⟩ < ⟨val✝, property✝⟩ ↔ List.Lex (fun x1 x2 => x1 < x2) ↑⟨val✝¹, property✝¹⟩ ↑⟨val✝, property✝⟩
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Icc_bot : Icc ⊥ a = Iic a

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderBot α
a : α
⊢ Icc ⊥ a = Iic a

Tactic:
simp [← Ici_inter_Iic]

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem lift_relrank_comap_comap_eq_lift_relrank_of_le (f : L →+* E) (h : B ≤ f.fieldRange) :
    lift.{v} (relrank (A.comap f) (B.comap f)) =
    lift.{w} (relrank A B)

Proof state:
E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A B : Subfield E
f : L →+* E
h : B ≤ f.fieldRange
⊢ lift.{v, w} ((comap f A).relrank (comap f B)) = lift.{w, v} (A.relrank B)

Tactic:
simpa only [inf_of_le_left h] using lift_relrank_comap_comap_eq_lift_relrank_inf A B f

Result:
no goals