mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
ι : Type u_2
s✝ : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
⊢ (map f (a :: s)).prod < (map g (a :: s)).prod

Tactic:
simp only [map_cons, prod_cons]
    have := posMulStrictMono_iff_mulPosStrictMono.1 ‹PosMulStrictMono R›
    apply mul_lt_mul
    · apply h
      simp
    · apply prod_map_le_prod_map₀
      · intro i hi
        apply le_of_lt
        apply h0
        simp [hi]
      · intro i hi
        apply le_of_lt
        apply h
        simp [hi]
    · apply prod_pos
      grind
    · apply le_of_lt ((h0 _ _).trans (h _ _)) <;> simp

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset

Goal state before:
pp: case mk
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
m : Multiset R
l : List R
⊢ 0 < prod (Quot.mk (⇑(List.isSetoid R)) l) ↔ ∀ (x : R), x ∈ Quot.mk (⇑(List.isSetoid R)) l → 0 < x

Tactic:
Multiset.quot_mk_to_coe'',

Goal state after:
case mk
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
m : Multiset R
l : List R
⊢ 0 < (↑l).prod ↔ ∀ (x : R), x ∈ ↑l → 0 < x
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝² : Zero M
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
f✝ : α →₀ M
p : α → Prop
inst✝ : DecidablePred p
f : α →₀ M
a : α
⊢ a ∈ Finset.filter p f.support ↔ (if p a then f a else 0) ≠ 0

Tactic:
by
    split_ifs with h <;>
      · simp only [h, mem_filter, mem_support_iff]
        tauto

Goal state after:
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α →₀ M
g : β →₀ M
⊢ f.sumElim g = mapDomain Sum.inl f + mapDomain Sum.inr g

Tactic:
ext (_ | _) <;> simp [mapDomain_of_notMem_range, Sum.inl_injective, Sum.inr_injective]

Goal state after:
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: ι₁ : Type u_12
ι₂ : Type u_13
α : Type u_14
M : Type u_15
inst✝¹ : Zero α
inst✝ : CommMonoid M
f₁ : ι₁ →₀ α
f₂ : ι₂ →₀ α
g : ι₁ ⊕ ι₂ → α → M
⊢ (f₁.sumElim f₂).prod g = f₁.prod (g ∘ Sum.inl) * f₂.prod (g ∘ Sum.inr)

Tactic:
by
  simp [Finsupp.prod, Finset.prod_disjSum]

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f (b i) = ⇑(single i 1)
x : M
i : ι
x✝¹ x✝ : M
⊢ f (x✝¹ + x✝) i = f x✝¹ i + f x✝ i

Tactic:
rw [hadd, Pi.add_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: M' : Type u_7
inst✝⁷ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
i : ι
⊢ ((b.constr S) f) (b i) = f i

Tactic:
simp [Basis.constr_apply, b.repr_self]

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_10
R : Type u_14
M : Type u_15
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
ι' : Type u_17
inst✝ : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
⊢ ∑ j, (b.repr (b' j)) i * (b'.repr x) j = (∑ x_1, (b'.repr x) x_1 • b.repr (b' x_1)) i

Tactic:
Finset.sum_apply'

Goal state after:
ι : Type u_10
R : Type u_14
M : Type u_15
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
ι' : Type u_17
inst✝ : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
⊢ ∑ j, (b.repr (b' j)) i * (b'.repr x) j = ∑ k, ((b'.repr x) k • b.repr (b' k)) i
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport fun a ↦ f a b
⊢ ∏ᶠ (a : α), ∏ b ∈ s, f a b = ∏ b ∈ s, ∏ᶠ (a : α), f a b

Tactic:
have hU :
    (mulSupport fun a => ∏ b ∈ s, f a b) ⊆
      (s.finite_toSet.biUnion fun b hb => h b (Finset.mem_coe.1 hb)).toFinset := by
    rw [Finite.coe_toFinset]
    intro x hx
    simp only [exists_prop, mem_iUnion, Ne, mem_mulSupport, Finset.mem_coe]
    contrapose! hx
    rw [mem_mulSupport, not_not, Finset.prod_congr rfl hx, Finset.prod_const_one]

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport fun a ↦ f a b
hU : (mulSupport fun a ↦ ∏ b ∈ s, f a b) ⊆ ↑⋯.toFinset
⊢ ∏ᶠ (a : α), ∏ b ∈ s, f a b = ∏ b ∈ s, ∏ᶠ (a : α), f a b
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
i : ι
hv : LinearIndependent R v
h : v i = 0
⊢ (Finsupp.linearCombination R v) (Finsupp.single i 1) = (Finsupp.linearCombination R v) 0

Tactic:
by simpa using h

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: y : ℕ∞
⊢ Monotone fun x ↦ x ^ y

Tactic:
intro x z x_z

Goal state after:
y x z : ℕ∞
x_z : x ≤ z
⊢ (fun x ↦ x ^ y) x ≤ (fun x ↦ x ^ y) z
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top.inl
y x z : ℕ∞
x_z : x ≤ z
x_0 : x < 1
⊢ 0 ^ ⊤ ≤ z ^ ⊤

Tactic:
zero_epow_top

Goal state after:
case top.inl
y x z : ℕ∞
x_z : x ≤ z
x_0 : x < 1
⊢ 0 ≤ z ^ ⊤
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top.inr.inr.inr.inr
x y z : ℕ∞
x_2 : 1 < x
y_2 : 1 < y
⊢ (x * y) ^ ⊤ = ⊤

Tactic:
exact epow_top (one_lt_mul x_2.le y_2)

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr.inr.inr.coe.coe
x y z : ℕ∞
x_2 : 1 < x
a✝¹ : ℕ
y_0 : ↑a✝¹ ≠ 0
a✝ : ℕ
z_0 : ↑a✝ ≠ 0
⊢ x ^ (↑a✝¹ * ↑a✝) = (x ^ ↑a✝¹) ^ ↑a✝

Tactic:
· simp only [← Nat.cast_mul, epow_natCast, pow_mul x]

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: case inr
a b c : ℕ
hb : c % b < b
⊢ (a ^ b - 1).gcd (a ^ c - 1) = a ^ b.gcd c - 1

Tactic:
rw [gcd_rec, pow_sub_one_mod_pow_sub_one, pow_sub_one_gcd_pow_sub_one, ← gcd_rec]

Goal state after:
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b : ℕ
⊢ a + b ≡ b [MOD n] ↔ n ∣ a

Tactic:
rw [add_comm, add_modEq_left_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case mpr
ι : Type w
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
p : ∀ (κ : Type v) (w : κ → M), LinearIndependent R w → ∀ (j : ι → κ), w ∘ j = v → Surjective j
w : Set M
⊢ LinearIndependent R Subtype.val → range v ⊆ w → range v = w

Tactic:
i'

Goal state after:
case mpr
ι : Type w
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
p : ∀ (κ : Type v) (w : κ → M), LinearIndependent R w → ∀ (j : ι → κ), w ∘ j = v → Surjective j
w : Set M
i' : LinearIndependent R Subtype.val
⊢ range v ⊆ w → range v = w
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_2.specialize_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
h :
  ∀ (s t : Finset ι) (f : ι → R),
    Disjoint s t → ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
⊢ ∑ i ∈ s with g i ≤ f i, (if g i ≤ f i then f i - g i else g i - f i) • v i +
      (∑ i ∈ s with g i ≤ f i, g i • v i + ∑ i ∈ s with f i < g i, f i • v i) =
    ∑ i ∈ s with f i < g i, (if g i ≤ f i then f i - g i else g i - f i) • v i +
      (∑ i ∈ s with g i ≤ f i, g i • v i + ∑ i ∈ s with f i < g i, f i • v i)

Tactic:
conv_lhs => rw [← add_assoc, ← Finset.sum_add_distrib]

Goal state after:
case refine_2.specialize_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
h :
  ∀ (s t : Finset ι) (f : ι → R),
    Disjoint s t → ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
⊢ ∑ x ∈ s with g x ≤ f x, ((if g x ≤ f x then f x - g x else g x - f x) • v x + g x • v x) +
      ∑ i ∈ s with f i < g i, f i • v i =
    ∑ i ∈ s with f i < g i, (if g i ≤ f i then f i - g i else g i - f i) • v i +
      (∑ i ∈ s with g i ≤ f i, g i • v i + ∑ i ∈ s with f i < g i, f i • v i)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m n : ℕ
hm1 : m % 2 = 1
hn1 : n % 2 = 1
h : n = 0
⊢ False

Tactic:
by simp_all

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_3
⊢ 0 < card α ↔ Nonempty α

Tactic:
rw [pos_iff_ne_zero, card_ne_zero_iff_nonempty]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
i : R → R'
j : M ≃+ M'
hi : Bijective i
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
x✝¹ : R
x✝ : M'
⊢ i x✝¹ • x✝ = j (x✝¹ • ↑j.symm x✝)

Tactic:
by simp_all

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ (↑s).encard = ↑s.card

Tactic:
rw [Finite.encard_eq_coe_toFinset_card (Finset.finite_toSet s)]; simp

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (s ×ˢ t).encard = s.encard * t.encard

Tactic:
unfold encard
  simp [ENat.card_congr (Equiv.Set.prod ..)]

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: case empty
η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
x : (i : η) → f i
h1 : ∀ i ∉ ∅, x i = 1
h2 : ∀ i ∈ ∅, Pi.mulSingle i (x i) ∈ H
⊢ x ∈ H

Tactic:
have : x = 1 := funext fun i => h1 i (Finset.notMem_empty i)

Goal state after:
case empty
η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
x : (i : η) → f i
h1 : ∀ i ∉ ∅, x i = 1
h2 : ∀ i ∈ ∅, Pi.mulSingle i (x i) ∈ H
this : x = 1
⊢ x ∈ H
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: case empty
η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
x : (i : η) → f i
h1 : ∀ i ∉ ∅, x i = 1
h2 : ∀ i ∈ ∅, Pi.mulSingle i (x i) ∈ H
this : x = 1
⊢ x ∈ H

Tactic:
exact this ▸ one_mem H

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: case mp.left
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : z ∈ center A
⊢ ∀ (i : ι), Commute (b i) z

Tactic:
intro i
      apply (h.1 (b i)).symm

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
⊢ (insert a s \ {b}).ncard = (insert a (s \ {b})).ncard

Tactic:
← singleton_union,

Goal state after:
α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
⊢ (({a} ∪ s) \ {b}).ncard = (insert a (s \ {b})).ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
⊢ (({a} ∪ s) \ {b}).ncard = (insert a (s \ {b})).ncard

Tactic:
← singleton_union,

Goal state after:
α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
⊢ (({a} ∪ s) \ {b}).ncard = ({a} ∪ s \ {b}).ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
⊢ (insert a s \ {b}).ncard = s.ncard

Tactic:
rw [← ncard_exchange ha hb, ← singleton_union, ← singleton_union, union_sdiff_distrib,
    sdiff_singleton_eq_self fun h ↦ ha (by rwa [← mem_singleton_iff.mp h])]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊂ t
ht : t.Finite
⊢ ↑s.ncard < t.encard

Tactic:
(ht.subset h.subset).cast_ncard_eq

Goal state after:
α : Type u_1
s t : Set α
h : s ⊂ t
ht : t.Finite
⊢ s.encard < t.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
a : α
ha : a ∈ s
hy : f a ha ∈ t
⊢ ∃ a_1, f' a_1 = ⟨f a ha, hy⟩

Tactic:
simp only [Subtype.exists]

Goal state after:
case right
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
a : α
ha : a ∈ s
hy : f a ha ∈ t
⊢ ∃ a_1, ∃ (b : a_1 ∈ s), f' ⟨a_1, b⟩ = ⟨f a ha, hy⟩
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
a : α
h : a ∈ s.toFinset
⊢ a ∈ s

Tactic:
by simpa using h

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
a : α
ha : a ∈ s
hy : f a ha ∈ t
⊢ ∃ a_1, f' a_1 = ⟨f a ha, hy⟩

Tactic:
simp only [Subtype.exists]

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
a : α
ha : a ∈ s
hy : f a ha ∈ t
⊢ ∃ a_1, ∃ (b : a_1 ∈ s), f' ⟨a_1, b⟩ = ⟨f a ha, hy⟩
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
a : α
h : a ∈ s.toFinset
⊢ a ∈ s

Tactic:
by simpa using h

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
⊢ RightInverse (fun a ↦ Quotient.map' (fun b ↦ f a.1 * ↑b) ⋯ a.2) fun a ↦
    (Quotient.map' id ⋯ a, Quotient.map' (fun g ↦ ⟨(f (Quotient.mk'' g))⁻¹ * g, ⋯⟩) ⋯ a)

Tactic:
refine Prod.rec ?_

Goal state after:
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
⊢ ∀ (fst : α ⧸ t) (snd : ↥t ⧸ s.subgroupOf t),
    (fun a ↦ (Quotient.map' id ⋯ a, Quotient.map' (fun g ↦ ⟨(f (Quotient.mk'' g))⁻¹ * g, ⋯⟩) ⋯ a))
        ((fun a ↦ Quotient.map' (fun b ↦ f a.1 * ↑b) ⋯ a.2) (fst, snd)) =
      (fst, snd)
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
x : α ⧸ ⊥
⊢ ↑(Quotient.lift id ⋯ x) = x

Tactic:
induction x using Quotient.inductionOn

Goal state after:
case h
α : Type u_1
inst✝ : Group α
a✝ : α
⊢ ↑(Quotient.lift id ⋯ ⟦a✝⟧) = ⟦a✝⟧
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
φ : G →* H
g : G
⊢ ∃ a, (rangeKerLift φ) a = ⟨φ g, ⋯⟩

Tactic:
use mk g

Goal state after:
case h
G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
φ : G →* H
g : G
⊢ (rangeKerLift φ) ↑g = ⟨φ g, ⋯⟩
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
inst✝ : Subsingleton α
s : Set α
⊢ ⋯.toFinset.card ≤ 1

Tactic:
exact Finset.card_le_one_of_subsingleton _

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
hsf : s.Finite
h : hsf.toFinset.card = n + 1
⊢ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.ncard = n

Tactic:
Finset.card_eq_succ

Goal state after:
α : Type u_1
s : Set α
n : ℕ
hsf : s.Finite
h : ∃ a t, a ∉ t ∧ insert a t = hsf.toFinset ∧ t.card = n
⊢ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.ncard = n
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.ncard = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y}

Tactic:
rw [← encard_eq_two, ncard_def]
  simp

Goal state after:
Module: Mathlib.Algebra.Field.IsField

Goal state before:
pp: R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
⊢ y = y * (x * z)

Tactic:
by rw [hxz, mul_one]

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M₂ : Type u_3
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
M₃ : Type u_4
inst✝¹ : AddCommGroup M₃
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
y : M
z : M₂
h : f y + g z = 0
⊢ f y ∈ f.range ⊓ g.range

Tactic:
simp only [true_and, mem_range, mem_inf, exists_apply_eq_apply]

Goal state after:
R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M₂ : Type u_3
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
M₃ : Type u_4
inst✝¹ : AddCommGroup M₃
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
y : M
z : M₂
h : f y + g z = 0
⊢ ∃ y_1, g y_1 = f y
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_1.smul
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
k : ι'
t : R
u : ι ⊕ ι' → R
hx✝ : u ∈ span R (Set.range fun i ↦ single (Sum.inl i) 1)
hu : u (Sum.inr k) = 0
⊢ (t • u) (Sum.inr k) = 0

Tactic:
simp [hu]

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_2
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this : Fintype ι
⊢ x = ∑ i, x (Sum.inl i) • single (Sum.inl i) 1

Tactic:
ext (i | i)

Goal state after:
case refine_2.inl
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this : Fintype ι
i : ι
⊢ x (Sum.inl i) = (∑ i, x (Sum.inl i) • single (Sum.inl i) 1) (Sum.inl i)

case refine_2.inr
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this : Fintype ι
i : ι'
⊢ x (Sum.inr i) = (∑ i, x (Sum.inl i) • single (Sum.inl i) 1) (Sum.inr i)
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_2.inr
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this : Fintype ι
i : ι'
⊢ x (Sum.inr i) = (∑ i, x (Sum.inl i) • single (Sum.inl i) 1) (Sum.inr i)

Tactic:
simp [hx i]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Monoid

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a b : M
⊢ (fun x ↦ a + x) '' Ioi b = Ioi (a + b)

Tactic:
simp only [add_comm a, image_add_const_Ioi]

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case inl
ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : (∀ x ∈ Set.Ioi i, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioi i, x ≤ x_1) → x ≤ k
x : ι
hx : ∀ x_1 ∈ Set.Ioc i j, x ≤ x_1
y : ι
hy : y ∈ Set.Ioi i
h_le : y ≤ j
⊢ x ≤ y

pp: case inr
ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : (∀ x ∈ Set.Ioi i, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioi i, x ≤ x_1) → x ≤ k
x : ι
hx : ∀ x_1 ∈ Set.Ioc i j, x ≤ x_1
y : ι
hy : y ∈ Set.Ioi i
h_lt : j < y
⊢ x ≤ y

Tactic:
· exact hx y ⟨hy, h_le⟩

Goal state after:
case inr
ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : (∀ x ∈ Set.Ioi i, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioi i, x ≤ x_1) → x ≤ k
x : ι
hx : ∀ x_1 ∈ Set.Ioc i j, x ≤ x_1
y : ι
hy : y ∈ Set.Ioi i
h_lt : j < y
⊢ x ≤ y
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : ℕ → Finset α
hs : Monotone s
g : α → β
n : ℕ
| ∏ i ∈ s n, g i

Tactic:
← hs.partialSups_eq,

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : ℕ → Finset α
hs : Monotone s
g : α → β
n : ℕ
| ∏ i ∈ (partialSups s) n, g i
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
m : ℕ := (toZ i0 (succ^[n] i0)).toNat
h_eq : succ^[m] i0 = succ^[n] i0
hmn : m = n
⊢ toZ i0 (succ^[n] i0) = ↑m

Tactic:
rw [Int.toNat_eq_max, toZ_of_ge (le_succ_iterate _ _), max_eq_left]

Goal state after:
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
m : ℕ := (toZ i0 (succ^[n] i0)).toNat
h_eq : succ^[m] i0 = succ^[n] i0
hmn : m = n
⊢ 0 ≤ ↑(Nat.find ⋯)
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case neg
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
m n : ℕ
h : n ≤ m
⊢ ∏ k ∈ Ico m n, f k = ∏ k ∈ range (n - m), f (m + k)

Tactic:
rw [Ico_eq_empty_of_le h, tsub_eq_zero_iff_le.mpr h, range_zero, prod_empty, prod_empty]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case succ
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
n✝ : ℕ
⊢ ∏ x ∈ Ico 0 (n✝ + 1), f (n✝ - x) = ∏ x ∈ Ico 0 (n✝ + 1), f x

Tactic:
prod_Ico_reflect _ _ le_rfl

Goal state after:
case succ
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
n✝ : ℕ
⊢ ∏ j ∈ Ico (n✝ + 1 - (n✝ + 1)) (n✝ + 1 - 0), f j = ∏ x ∈ Ico 0 (n✝ + 1), f x
Module: Mathlib.Data.List.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ map (Prod.swap ∘ fun i ↦ (i, n - i)) (range (n + 1)) = (map (fun i ↦ (i, n - i)) (range (n + 1))).reverse

Tactic:
← List.map_reverse,

Goal state after:
n : ℕ
⊢ map (Prod.swap ∘ fun i ↦ (i, n - i)) (range (n + 1)) = map (fun i ↦ (i, n - i)) (range (n + 1)).reverse
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Ring α
x x✝ : α
⊢ x✝ ∈ span {-x} ↔ x✝ ∈ span {x}

Tactic:
simp only [mem_span_singleton']

Goal state after:
α : Type u
inst✝ : Ring α
x x✝ : α
⊢ (∃ a, a * -x = x✝) ↔ ∃ a, a * x = x✝