Theorem: LO.Modal.Standard.DeductionParameter.IsGeach.eq_axiomset (Logic/Modal/Standard/Geach.lean)

State before:
α : Type u_1
Ax : AxiomSet α
L : DeductionParameter α
geach : L.IsGeach
⊢ Ax(L) = 𝗚𝗲(taples L)
Tactic:
have := geach.char
State after:
α : Type u_1
Ax : AxiomSet α
L : DeductionParameter α
geach : L.IsGeach
this : L = 𝐆𝐞(taples L)
⊢ Ax(L) = 𝗚𝗲(taples L)

State before:
α : Type u_1
Ax : AxiomSet α
L : DeductionParameter α
geach : L.IsGeach
this : L = 𝐆𝐞(taples L)
⊢ Ax(L) = 𝗚𝗲(taples L)
Tactic:
simp_all
State after:
no goals