harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem disjoint_sum_left {a : Multiset α} {i : Multiset (Multiset α)} :
    Disjoint i.sum a ↔ ∀ b ∈ i, Disjoint b a :=
  Quotient.inductionOn i fun l => by
    rw [quot_mk_to_coe, Multiset.sum_coe]
    exact disjoint_list_sum_left

Proof state:
α : Type u_3
a : Multiset α
i : Multiset (Multiset α)
l : List (Multiset α)
⊢ Disjoint (sum ⟦l⟧) a ↔ ∀ b ∈ ⟦l⟧, Disjoint b a

Tactic:
rw [quot_mk_to_coe, Multiset.sum_coe]

Result:
α : Type u_3
a : Multiset α
i : Multiset (Multiset α)
l : List (Multiset α)
⊢ Disjoint l.sum a ↔ ∀ b ∈ ↑l, Disjoint b a

Proof state:
α : Type u_3
a : Multiset α
i : Multiset (Multiset α)
l : List (Multiset α)
⊢ Disjoint l.sum a ↔ ∀ b ∈ ↑l, Disjoint b a

Tactic:
exact disjoint_list_sum_left

Result:
no goals
-- Mathlib/InformationTheory/KullbackLeibler/KLFun.lean
lemma isMinOn_klFun : IsMinOn klFun (Ici 0) 1 :=
  convexOn_klFun.isMinOn_of_rightDeriv_eq_zero (by simp) (by simp)

Proof state:
⊢ derivWithin klFun (Ioi 1) 1 = 0

Tactic:
simp

Result:
no goals

Proof state:
⊢ 1 ∈ interior (Ici 0)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Rank.lean
theorem rank_sup_eq_rank_right_mul_rank_of_free :
    Module.rank R ↥(A ⊔ B) = Module.rank R B * Module.rank B (Algebra.adjoin B (A : Set S))

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥B
inst✝ : Free ↥B ↥(Algebra.adjoin ↥B ↑A)
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥B * Module.rank ↥B ↥(Algebra.adjoin ↥B ↑A)

Tactic:
rw [sup_comm, rank_sup_eq_rank_left_mul_rank_of_free]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem singletonSubgraph_fst_le_subgraphOfAdj {u v : V} {h : G.Adj u v} :
    G.singletonSubgraph u ≤ G.subgraphOfAdj h

Proof state:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ G.singletonSubgraph u ≤ G.subgraphOfAdj h

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/Basic.lean
theorem coe_decompose_mul_of_right_mem_of_not_le (b_mem : b ∈ 𝒜 i) (h : ¬i ≤ n) :
    (decompose 𝒜 (a * b) n : A) = 0

Proof state:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
a b : A
n i : ι
b_mem : b ∈ 𝒜 i
h : ¬i ≤ n
⊢ ↑(((decompose 𝒜) (a * b)) n) = 0

Tactic:
lift b to 𝒜 i using b_mem

Result:
case intro
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
a : A
n i : ι
h : ¬i ≤ n
b : ↥(𝒜 i)
⊢ ↑(((decompose 𝒜) (a * ↑b)) n) = 0

Proof state:
case intro
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
a : A
n i : ι
h : ¬i ≤ n
b : ↥(𝒜 i)
⊢ ↑(((decompose 𝒜) (a * ↑b)) n) = 0

Tactic:
rwa [decompose_mul, decompose_coe, coe_mul_of_apply_of_not_le]

Result:
no goals
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem isCoprime_one_left : IsCoprime 1 x :=
  ⟨1, 0, by rw [one_mul, zero_mul, add_zero]⟩

Proof state:
R : Type u
inst✝ : CommSemiring R
x : R
⊢ 1 * 1 + 0 * x = 1

Tactic:
rw [one_mul, zero_mul, add_zero]

Result:
no goals
-- Mathlib/Data/Matrix/Notation.lean
theorem cons_dotProduct (x : α) (v : Fin n → α) (w : Fin n.succ → α) :
    dotProduct (vecCons x v) w = x * vecHead w + dotProduct v (vecTail w)

Proof state:
α : Type u
n : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
x : α
v : Fin n → α
w : Fin n.succ → α
⊢ vecCons x v ⬝ᵥ w = x * vecHead w + v ⬝ᵥ vecTail w

Tactic:
simp [dotProduct, Fin.sum_univ_succ, vecHead, vecTail]

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Basic.lean
lemma mem_posFittingCompOf (x : L) (m : M) :
    m ∈ posFittingCompOf R M x ↔ ∀ (k : ℕ), ∃ n, (toEnd R L M x ^ k) n = m

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
x : L
m : M
⊢ m ∈ posFittingCompOf R M x ↔ ∀ (k : ℕ), ∃ n, ((toEnd R L M) x ^ k) n = m

Tactic:
simp [posFittingCompOf]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem bihimp_right_comm : a ⇔ b ⇔ c = a ⇔ c ⇔ b

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⇔ b ⇔ c = a ⇔ c ⇔ b

Tactic:
simp_rw [bihimp_assoc, bihimp_comm]

Result:
no goals
-- Mathlib/Tactic/NoncommRing.lean
lemma mul_nat_lit_eq_nsmul [n.AtLeastTwo] : r * ofNat(n) = OfNat.ofNat n • r

Proof state:
R : Type u_1
inst✝¹ : NonAssocSemiring R
r : R
n : ℕ
inst✝ : n.AtLeastTwo
⊢ r * OfNat.ofNat n = OfNat.ofNat n • r

Tactic:
simp only [nsmul_eq_mul', Nat.cast_ofNat]

Result:
no goals
-- Mathlib/Data/List/Nodup.lean
theorem idxOf_getElem [DecidableEq α] {l : List α} (H : Nodup l) (i : Nat) (h : i < l.length) :
    idxOf l[i] l = i :=
  suffices (⟨idxOf l[i] l, idxOf_lt_length_iff.2 (getElem_mem _)⟩ : Fin l.length) = ⟨i, h⟩
    from Fin.val_eq_of_eq this
  nodup_iff_injective_get.1 H (by simp)

Proof state:
α : Type u
inst✝ : DecidableEq α
l : List α
H : l.Nodup
i : ℕ
h : i < l.length
⊢ l.get ⟨idxOf l[i] l, ⋯⟩ = l.get ⟨i, h⟩

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKeyD_insertListConst_of_contains_eq_false [BEq α] [EquivBEq α]
    {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k fallback : α}
    (not_contains : (toInsert.map Prod.fst).contains k = false) :
    getKeyD k (insertListConst l toInsert) fallback = getKeyD k l fallback

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k fallback : α
not_contains : (List.map Prod.fst toInsert).contains k = false
⊢ getKeyD k (insertListConst l toInsert) fallback = getKeyD k l fallback

Tactic:
rw [getKeyD_eq_getKey?, getKey?_insertListConst_of_contains_eq_false not_contains,
  getKeyD_eq_getKey?]

Result:
no goals
-- Mathlib/Order/Minimal.lean
theorem map_minimal_mem (f : s ≃o t) (hx : Minimal (· ∈ s) x) :
    Minimal (· ∈ t) (f ⟨x, hx.prop⟩)

Proof state:
α : Type u_1
x : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
s : Set α
t : Set β
f : ↑s ≃o ↑t
hx : Minimal (fun x => x ∈ s) x
⊢ t = range (Subtype.val ∘ ⇑f)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
x : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
s : Set α
t : Set β
f : ↑s ≃o ↑t
hx : Minimal (fun x => x ∈ s) x
⊢ Minimal (fun x => x ∈ t) ↑(f ⟨x, ⋯⟩)

Tactic:
simpa only [show t = range (Subtype.val ∘ f) by simp, mem_univ, minimal_true_subtype, hx,
  true_imp_iff, image_univ] using OrderEmbedding.minimal_mem_image
  (f.toOrderEmbedding.trans (OrderEmbedding.subtype t)) (s := univ) (x := ⟨x, hx.prop⟩)

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Cast.lean
@[simp] lemma cast_pos : (0 : R) < n ↔ 0 < n

Proof state:
R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
n : ℤ
⊢ 0 < ↑n ↔ 0 < n

Tactic:
rw [← cast_zero, cast_lt]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem isEmpty_iff {l : Array α} : l.isEmpty ↔ l = #[]

Proof state:
α : Type u_1
l : Array α
⊢ l.isEmpty = true ↔ l = #[]

Tactic:
cases l <;> simp

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem cycleFactorsFinset_eq_empty_iff {f : Perm α} : cycleFactorsFinset f = ∅ ↔ f = 1

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ f.cycleFactorsFinset = ∅ ↔ f = 1

Tactic:
simpa [cycleFactorsFinset_eq_finset] using eq_comm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem coe_iff_coe : ∀{a b : Bool}, (a ↔ b) ↔ a = b

Proof state:
⊢ ∀ {a b : Bool}, (a = true ↔ b = true) ↔ a = b

Tactic:
decide

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean
lemma IsLimit.isIso_π_app_of_isInitial {F : J ⥤ C} {c : Cone F} (hc : IsLimit c)
    (X : J) (hX : IsInitial X) :
    IsIso (c.π.app X)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ C
c : Cone F
hc : IsLimit c
X : J
hX : IsInitial X
⊢ IsIso (c.π.app X)

Tactic:
change IsIso (conePointUniqueUpToIso hc (limitOfDiagramInitial hX F)).hom

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ C
c : Cone F
hc : IsLimit c
X : J
hX : IsInitial X
⊢ IsIso (hc.conePointUniqueUpToIso (limitOfDiagramInitial hX F)).hom

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ C
c : Cone F
hc : IsLimit c
X : J
hX : IsInitial X
⊢ IsIso (hc.conePointUniqueUpToIso (limitOfDiagramInitial hX F)).hom

Tactic:
infer_instance

Result:
no goals
-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem mkSpanSingleton'_apply (x : E) (y : F) (H : ∀ c : R, c • x = 0 → c • y = 0) (c : R) (h) :
    mkSpanSingleton' x y H ⟨c • x, h⟩ = c • y

Proof state:
case a
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
x : E
y : F
H : ∀ (c : R), c • x = 0 → c • y = 0
c : R
h : c • x ∈ (mkSpanSingleton' x y H).domain
⊢ Classical.choose ⋯ • x = c • x

Tactic:
apply Classical.choose_spec (mem_span_singleton.1 h)

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
x : E
y : F
H : ∀ (c : R), c • x = 0 → c • y = 0
c : R
h : c • x ∈ (mkSpanSingleton' x y H).domain
⊢ ↑(mkSpanSingleton' x y H) ⟨c • x, h⟩ = c • y

Tactic:
dsimp [mkSpanSingleton']

Result:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
x : E
y : F
H : ∀ (c : R), c • x = 0 → c • y = 0
c : R
h : c • x ∈ (mkSpanSingleton' x y H).domain
⊢ Classical.choose ⋯ • y = c • y

Proof state:
case a
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
x : E
y : F
H : ∀ (c : R), c • x = 0 → c • y = 0
c : R
h : c • x ∈ (mkSpanSingleton' x y H).domain
⊢ (Classical.choose ⋯ - c) • x = 0

Tactic:
simp only [sub_smul, one_smul, sub_eq_zero]

Result:
case a
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
x : E
y : F
H : ∀ (c : R), c • x = 0 → c • y = 0
c : R
h : c • x ∈ (mkSpanSingleton' x y H).domain
⊢ Classical.choose ⋯ • x = c • x

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
x : E
y : F
H : ∀ (c : R), c • x = 0 → c • y = 0
c : R
h : c • x ∈ (mkSpanSingleton' x y H).domain
⊢ (Classical.choose ⋯ - c) • y = 0

Tactic:
apply H

Result:
case a
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
x : E
y : F
H : ∀ (c : R), c • x = 0 → c • y = 0
c : R
h : c • x ∈ (mkSpanSingleton' x y H).domain
⊢ (Classical.choose ⋯ - c) • x = 0

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
x : E
y : F
H : ∀ (c : R), c • x = 0 → c • y = 0
c : R
h : c • x ∈ (mkSpanSingleton' x y H).domain
⊢ Classical.choose ⋯ • y = c • y

Tactic:
rw [← sub_eq_zero, ← sub_smul]

Result:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
x : E
y : F
H : ∀ (c : R), c • x = 0 → c • y = 0
c : R
h : c • x ∈ (mkSpanSingleton' x y H).domain
⊢ (Classical.choose ⋯ - c) • y = 0
-- Mathlib/Analysis/Convex/Function.lean
theorem ConvexOn.add (hf : ConvexOn 𝕜 s f) (hg : ConvexOn 𝕜 s g) : ConvexOn 𝕜 s (f + g) :=
  ⟨hf.1, fun x hx y hy a b ha hb hab =>
    calc
      f (a • x + b • y) + g (a • x + b • y) ≤ a • f x + b • f y + (a • g x + b • g y) :=
        add_le_add (hf.2 hx hy ha hb hab) (hg.2 hx hy ha hb hab)
      _ = a • (f x + g x) + b • (f y + g y)

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

Tactic:
rw [smul_add, smul_add, add_add_add_comm]

Result:
no goals
-- Mathlib/Order/Filter/Curry.lean
theorem eventually_curry_prod_iff [NeBot l] [NeBot m] :
    (∀ᶠ x in l.curry m, x ∈ s ×ˢ t) ↔ s ∈ l ∧ t ∈ m

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
m : Filter β
s : Set α
t : Set β
inst✝¹ : l.NeBot
inst✝ : m.NeBot
⊢ (∀ᶠ (x : α × β) in l.curry m, x ∈ s ×ˢ t) ↔ s ∈ l ∧ t ∈ m

Tactic:
simp [eventually_curry_iff]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem coe_intCast (a : ℤ) : cast (a : ZMod n) = a % n

Proof state:
case zero
a : ℤ
⊢ (↑a).cast = a % ↑0

Tactic:
rw [Int.ofNat_zero, Int.emod_zero, Int.cast_id]

Result:
case zero
a : ℤ
⊢ cast a = a

Proof state:
n : ℕ
a : ℤ
⊢ (↑a).cast = a % ↑n

Tactic:
cases n

Result:
case zero
a : ℤ
⊢ (↑a).cast = a % ↑0

case succ
a : ℤ
n✝ : ℕ
⊢ (↑a).cast = a % ↑(n✝ + 1)

Proof state:
case succ
a : ℤ
n✝ : ℕ
⊢ (↑a).cast = a % ↑(n✝ + 1)

Tactic:
rw [← val_intCast, val]

Result:
case succ
a : ℤ
n✝ : ℕ
⊢ (↑a).cast = ↑↑↑a

Proof state:
case succ
a : ℤ
n✝ : ℕ
⊢ (↑a).cast = ↑↑↑a

Tactic:
rfl

Result:
no goals

Proof state:
case zero
a : ℤ
⊢ cast a = a

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Module/ZMod.lean
/-- In an elementary abelian `p`-group, every finite subgroup `H` contains a further subgroup of
cardinality between `k` and `p * k`, if `k ≤ |H|`. -/
lemma exists_submodule_subset_card_le (hp : p.Prime) [Module (ZMod p) G]
    (H : Submodule (ZMod p) G) {k : ℕ} (hk : k ≤ Nat.card H) (h'k : k ≠ 0) :
    ∃ H' : Submodule (ZMod p) G, Nat.card H' ≤ k ∧ k < p * Nat.card H' ∧ H' ≤ H

Proof state:
p : ℕ
G : Type u_5
inst✝¹ : AddCommGroup G
hp : Nat.Prime p
inst✝ : Module (ZMod p) G
H : Submodule (ZMod p) G
k : ℕ
hk : k ≤ Nat.card ↥H
h'k : k ≠ 0
⊢ ∃ H', Nat.card ↥H' ≤ k ∧ k < p * Nat.card ↥H' ∧ H' ≤ H

Tactic:
obtain ⟨H'm, H'mHm, H'mk, kH'm⟩ := Sylow.exists_subgroup_le_card_le
  (H := AddSubgroup.toSubgroup ((AddSubgroup.toZModSubmodule _).symm H)) hp
    isPGroup_multiplicative hk h'k

Result:
case intro.intro.intro
p : ℕ
G : Type u_5
inst✝¹ : AddCommGroup G
hp : Nat.Prime p
inst✝ : Module (ZMod p) G
H : Submodule (ZMod p) G
k : ℕ
hk : k ≤ Nat.card ↥H
h'k : k ≠ 0
H'm : Subgroup (Multiplicative G)
H'mHm : H'm ≤ AddSubgroup.toSubgroup ((AddSubgroup.toZModSubmodule p).symm H)
H'mk : Nat.card ↥H'm ≤ k
kH'm : k < p * Nat.card ↥H'm
⊢ ∃ H', Nat.card ↥H' ≤ k ∧ k < p * Nat.card ↥H' ∧ H' ≤ H

Proof state:
case intro.intro.intro
p : ℕ
G : Type u_5
inst✝¹ : AddCommGroup G
hp : Nat.Prime p
inst✝ : Module (ZMod p) G
H : Submodule (ZMod p) G
k : ℕ
hk : k ≤ Nat.card ↥H
h'k : k ≠ 0
H'm : Subgroup (Multiplicative G)
H'mHm : H'm ≤ AddSubgroup.toSubgroup ((AddSubgroup.toZModSubmodule p).symm H)
H'mk : Nat.card ↥H'm ≤ k
kH'm : k < p * Nat.card ↥H'm
⊢ ∃ H', Nat.card ↥H' ≤ k ∧ k < p * Nat.card ↥H' ∧ H' ≤ H

Tactic:
exact ⟨AddSubgroup.toZModSubmodule _ (AddSubgroup.toSubgroup.symm H'm), H'mk, kH'm, H'mHm⟩

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Membership.lean
theorem card_le_one_iff_eq_bot : card S ≤ 1 ↔ S = ⊥ :=
  ⟨fun h =>
    (eq_bot_iff_forall _).2 fun x hx => by
      simpa [Subtype.ext_iff] using card_le_one_iff.1 h ⟨x, hx⟩ 1,
    fun h => by simp [h]⟩

Proof state:
M : Type u_1
inst✝¹ : Monoid M
S : Submonoid M
inst✝ : Fintype ↥S
h : S = ⊥
⊢ card ↥S ≤ 1

Tactic:
simp [h]

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : Monoid M
S : Submonoid M
inst✝ : Fintype ↥S
h : card ↥S ≤ 1
x : M
hx : x ∈ S
⊢ x = 1

Tactic:
simpa [Subtype.ext_iff] using card_le_one_iff.1 h ⟨x, hx⟩ 1

Result:
no goals
-- Mathlib/RingTheory/Norm/Transitivity.lean
lemma eval_zero_comp_det :
    eval 0 (comp m m n n R[X] <| (cornerAddX M k).map f.polyToMatrix).det =
      (comp m m n n R <| M.map f).det

Proof state:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ ((compRingEquiv m n R).toRingHom (f.mapMatrix ((evalRingHom 0).mapMatrix (cornerAddX M k)))).det =
    (↑(compRingEquiv m n R) (f.mapMatrix M)).det

Tactic:
congr with i j

Result:
case e_M.h.e_6.h.h.e_6.h.a
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
i j : m
⊢ (evalRingHom 0).mapMatrix (cornerAddX M k) i j = M i j

Proof state:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ eval 0 ((Matrix.comp m m n n R[X]) ((cornerAddX M k).map ⇑f.polyToMatrix)).det =
    ((Matrix.comp m m n n R) (M.map ⇑f)).det

Tactic:
simp_rw [← coe_evalRingHom, RingHom.map_det, ← compRingEquiv_apply, ← RingEquiv.coe_toRingHom,
  ← RingHom.mapMatrix_apply, ← RingHom.comp_apply, ← RingHom.comp_assoc,
  evalRingHom_mapMatrix_comp_compRingEquiv, RingHom.comp_assoc, RingHom.mapMatrix_comp,
  evalRingHom_mapMatrix_comp_polyToMatrix, ← RingHom.mapMatrix_comp, RingHom.comp_apply]

Result:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ ((compRingEquiv m n R).toRingHom (f.mapMatrix ((evalRingHom 0).mapMatrix (cornerAddX M k)))).det =
    (↑(compRingEquiv m n R) (f.mapMatrix M)).det

Proof state:
case e_M.h.e_6.h.h.e_6.h.a
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
i j : m
⊢ (evalRingHom 0).mapMatrix (cornerAddX M k) i j = M i j

Tactic:
simp [cornerAddX, diagonal, apply_ite]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
theorem appLE (H : P f) (U : Y.affineOpens) (V : X.affineOpens) (e) : Q (f.appLE U V e).hom

Proof state:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
H : P f
U : ↑Y.affineOpens
V : ↑X.affineOpens
e : ↑V ≤ f ⁻¹ᵁ ↑U
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))

Tactic:
rw [eq_affineLocally P, affineLocally_iff_affineOpens_le] at H

Result:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
H :
  ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
U : ↑Y.affineOpens
V : ↑X.affineOpens
e : ↑V ≤ f ⁻¹ᵁ ↑U
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))

Proof state:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
H :
  ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
U : ↑Y.affineOpens
V : ↑X.affineOpens
e : ↑V ≤ f ⁻¹ᵁ ↑U
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))

Tactic:
exact H _ _ _

Result:
no goals
-- Mathlib/Algebra/Homology/Homotopy.lean
theorem nullHomotopicMap'_f_eq_zero {k₀ : ι} (hk₀ : ∀ l : ι, ¬c.Rel k₀ l)
    (hk₀' : ∀ l : ι, ¬c.Rel l k₀) (h : ∀ i j, c.Rel j i → (C.X i ⟶ D.X j)) :
    (nullHomotopicMap' h).f k₀ = 0

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₀ : ι
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hk₀' : ∀ (l : ι), ¬c.Rel l k₀
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (nullHomotopicMap fun i j => dite (c.Rel j i) (h i j) fun x => 0).f k₀ = 0

Tactic:
apply nullHomotopicMap_f_eq_zero hk₀ hk₀'

Result:
no goals

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₀ : ι
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hk₀' : ∀ (l : ι), ¬c.Rel l k₀
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (nullHomotopicMap' h).f k₀ = 0

Tactic:
simp only [nullHomotopicMap']

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₀ : ι
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hk₀' : ∀ (l : ι), ¬c.Rel l k₀
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (nullHomotopicMap fun i j => dite (c.Rel j i) (h i j) fun x => 0).f k₀ = 0
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem IsGLB.mul_right {s : Set α} (ha : 0 ≤ a) (hs : IsGLB s b) :
    IsGLB ((fun b => b * a) '' s) (b * a)

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a b : α
s : Set α
ha : 0 ≤ a
hs : IsGLB s b
⊢ IsGLB ((fun b => b * a) '' s) (b * a)

Tactic:
simpa [mul_comm] using hs.mul_left ha

Result:
no goals
-- Mathlib/Data/Multiset/Antidiagonal.lean
theorem antidiagonal_map_fst (s : Multiset α) : (antidiagonal s).map Prod.fst = powerset s :=
  Quotient.inductionOn s fun l ↦ by simp [powersetAux']

Proof state:
α : Type u_1
s : Multiset α
l : List α
⊢ map Prod.fst (antidiagonal ⟦l⟧) = powerset ⟦l⟧

Tactic:
simp [powersetAux']

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem coeff_neg (p : R[X]) (n : ℕ) : coeff (-p) n = -coeff p n

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
n : ℕ
⊢ (-p).coeff n = -p.coeff n

Tactic:
rcases p with ⟨⟩

Result:
case ofFinsupp
R : Type u
inst✝ : Ring R
n : ℕ
toFinsupp✝ : R[ℕ]
⊢ (-{ toFinsupp := toFinsupp✝ }).coeff n = -{ toFinsupp := toFinsupp✝ }.coeff n

Proof state:
case ofFinsupp
R : Type u
inst✝ : Ring R
n : ℕ
toFinsupp✝ : R[ℕ]
⊢ (-{ toFinsupp := toFinsupp✝ }).coeff n = -{ toFinsupp := toFinsupp✝ }.coeff n

Tactic:
rw [← ofFinsupp_neg, coeff, coeff, Finsupp.neg_apply]

Result:
no goals